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