I'm struggling to understand the proof of Corollary III.2.13(2) in Shelah's Classification Theory. The corollary reads:
Suppose $T$ is stable. Let $A\subseteq |M|$, $M$ $\lambda$-saturated with $|A|,\aleph_0<\lambda$. Then:
(1) Every $m$-type which is almost over $A$ is realized in $M$
(2) If $J$ is an infinite indiscernible set based on $A$, then there is an equivalent indiscernible set $I\subseteq|M|$. (I is also indiscernible over $A$.)
I don't have any problem with the proof of (1). For (2), Shelah says:
Choose distinct $\bar a_l\in J$, $\bar b_0\in |M|$ realizing $\text{stp}(\bar a_0,A)$ and $\bar b_n\in |M|$ such that $\text{tp}(\bar a_0^\frown\cdots^\frown\bar a_n,A)=\text{tp}(\bar b_0^\frown\cdots^\frown\bar b_n,A)$ and let $I=\{\bar b_n\mid n<\omega\}$.
From prior results, I can finish the proof with this step, (except showing $I$ indiscernible over $A$. Does "based on" imply "indiscernible over"? The word "also" seems to imply this is the case for $J$...) However, I do not see the justification for the above. We use part (1) (or just saturation) to find $\bar b_0$, but then I'm stuck defining the rest of the $\bar b_n$. This is probably where we use "based on", since I don't think I need it to show the rest, (except perhaps the parenthetical above.)
Any help would be greatly appreciated. Thanks!
EDIT: Here are Shelah's definitions for "based on" and "equivalent". Fairly certain that we work in a stable theory throughout.
$\text{Av}(I,A)$, the average type of an indiscernible set $I$ over $A$, is the set of all formulas $\varphi(\bar v;\bar a)$, $\bar a\in A$, such that all but finitely many members of $I$ realize $\varphi$. We say that $I$ is based on $A$ provided $\text{Av}(I,B)$ does not fork over $A$ for all $B$. Finally, we say $I$ is equivalent to $J$ provided there exists an infinite indiscernible set $K$ such that $I\cup K$ and $J\cup K$ are both still indiscernible, (which we proved equivalent to showing $\text{Av}(I,A)=\text{Av}(J,A)$ for all $A$.)
Shelah's entire book is available at a pdf here if you want his definition of forking or anything else, (beginning of Ch III.) Indeed, one of the frustrating things I've come across is that his definitions and notation are frequently different from other sources!
I also don't understand what Shelah writes in the proof of (2). Here's how I would do it:
Let $M'$ be a model contaning $M$ and $J$. Let $p(x) = \text{Av}(J,M')$, and let $q(x) = \text{stp}(a/A)$ for any realization $a$ of $p(x)$. Note that $p(x)\vdash q(x)$ (since every finite equivalence relation over $A$ has a representative in $M'$). Also, $q(x)$ is stationary (Corollary 2.9(1)), and we know that $p(x)$ doesn't fork over $A$, so $p(x)$ is the unique nonforking extension of $q(x)$ to a type over $M'$.
Pick a sequence $I = (a_n)_{n\in \omega}$ in $M$, such that $a_0\models q(x)$ and $a_n\models p(x)|_{Aa_0\dots a_{n-1}}\cup q(x)$ for all $n\geq 1$.
This is possible by (1), $q(x)$ is almost over $A$, and $p(x)|_{Aa_0\dots a_{n-1}}\cup q(x)$ is almost over $Aa_0\dots a_{n-1}$ for all $n\geq 1$. Note also that $\text{tp}(a_n/Aa_0\dots a_{n-1})$ doesn't fork over $A$.
Now by Lemma 1.10, $I = (a_n)_{n\in \omega}$ is an indiscernible set over $A$, and $\text{Av}(I/M')$ is the unique nonforking extension of $q(x)$ in $S(M')$. That is, $\text{Av}(I/M') = p(x) = \text{Av}(J/M')$. Hence $I$ and $J$ are equivalent by Lemma 1.8.
By the way, it's not true that "based on" implies "indiscernible over". In the remark after Definition 1.8, Shelah points out that $I$ is based on $\bigcup I$, but $I$ is certainly not indiscernible over $\bigcup I$! I think the parenthetical in the statement is just saying "in addition to all the other claims, we also naturally get that $I$ is indiscernible over $A$."