let x, z be Surreal; :: thesis: for r being non-zero Sequence of REAL
for y being strictly_decreasing 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
omega-y (x - z) < yA
let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing 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
omega-y (x - z) < yA
let y be strictly_decreasing 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
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
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
omega-y (x - z) < yA
let yA be Surreal; :: thesis: ( A in (dom r) /\ (dom y) & yA = y . A implies omega-y (x - z) < yA )
assume A3: ( A in (dom r) /\ (dom y) & yA = y . A ) ; :: thesis: 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 Def17;
then A5: |.(x - z).| infinitely< No_omega^ yA by XBOOLE_1:7, A3, A1, Th90;
|.(x - z).|, No_omega^ (omega-y (x + (- z))) are_commensurate by A4, Def7;
then No_omega^ (omega-y (x + (- z))) < No_omega^ yA by Th9, A5, Th15;
hence omega-y (x - z) < yA by Lm5; :: thesis: verum