let x, z be Surreal; :: thesis: for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not x == z holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA
let r be Sequence of REAL ; :: thesis: for y being positive decreasing_infinitely Surreal-Sequence st x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not x == z holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA
let y be positive decreasing_infinitely Surreal-Sequence; :: thesis: ( x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not x == z implies for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA )
set s = Partial_Sums (r,y);
set D = (dom r) /\ (dom y);
assume that
A1: ( x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) ) and
A2: not x == z ; :: thesis: for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA
let A be Ordinal; :: thesis: for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA
let yA be Surreal; :: thesis: ( A in (dom r) /\ (dom y) & yA = y . A implies No_omega^ (omega-y (x - z)) < yA )
assume A3: ( A in (dom r) /\ (dom y) & yA = y . A ) ; :: thesis: No_omega^ (omega-y (x - z)) < yA
A4: not x - z == 0_No by SURREALR:47, A2;
dom (Partial_Sums (r,y)) = succ ((dom r) /\ (dom y)) by Def20;
then A5: |.(x - z).| infinitely< yA by XBOOLE_1:7, A3, A1, Th93;
|.(x - z).|, No_omega^ (omega-y (x + (- z))) are_commensurate by A4, Def7;
hence No_omega^ (omega-y (x - z)) < yA by Th9, A5, Th15; :: thesis: verum