let x be Surreal; :: thesis: for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st r,y,A name_like x holds
x in_meets_terms Partial_Sums (r,y),y,r,A
let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st r,y,A name_like x holds
x in_meets_terms Partial_Sums (r,y),y,r,A
let y be strictly_decreasing Surreal-Sequence; :: thesis: for A being Ordinal st r,y,A name_like x holds
x in_meets_terms Partial_Sums (r,y),y,r,A
let A be Ordinal; :: thesis: ( r,y,A name_like x implies x in_meets_terms Partial_Sums (r,y),y,r,A )
assume A1: r,y,A name_like x ; :: thesis: x in_meets_terms Partial_Sums (r,y),y,r,A
set s = Partial_Sums (r,y);
let beta be Ordinal; :: according to SURREALC:def 14 :: thesis: for sb, yb being Surreal st beta in A & sb = (Partial_Sums (r,y)) . beta & yb = y . beta holds
x is sb,yb,r . beta _term
let sb, yb be Surreal; :: thesis: ( beta in A & sb = (Partial_Sums (r,y)) . beta & yb = y . beta implies x is sb,yb,r . beta _term )
assume A2: ( beta in A & sb = (Partial_Sums (r,y)) . beta & yb = y . beta ) ; :: thesis: x is sb,yb,r . beta _term
A3: ( not x == sb & r . beta = omega-r (x - sb) & y . beta = omega-y (x - sb) ) by A2, A1;
A4: not x - sb == 0_No by A2, A1, SURREALR:47;
then A5: |.((x - sb) - ((No_omega^ yb) * (uReal . (r . beta)))).| infinitely< |.(x - sb).| by A2, A3, Def8;
|.(x + (- sb)).|, No_omega^ yb are_commensurate by A2, A3, A4, Def7;
then A6: |.((x - sb) - ((No_omega^ yb) * (uReal . (r . beta)))).| infinitely< No_omega^ yb by A5, Th16;
A7: (x - sb) - ((No_omega^ yb) * (uReal . (r . beta))) = x + ((- sb) - ((No_omega^ yb) * (uReal . (r . beta)))) by SURREALR:37
.= x - (sb + ((No_omega^ yb) * (uReal . (r . beta)))) by SURREALR:40 ;
r . beta in rng r by A2, A1, FUNCT_1:def 3;
hence x is sb,yb,r . beta _term by A6, A7, Th73; :: thesis: verum