let x, z be Surreal; :: thesis: for r being non-zero Sequence of REAL
for y being Sequence
for s being Surreal-Sequence
for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb
let r be non-zero Sequence of REAL ; :: thesis: for y being Sequence
for s being Surreal-Sequence
for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb
let y be Sequence; :: thesis: for s being Surreal-Sequence
for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb
let s be Surreal-Sequence; :: thesis: for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb
let A, B be Ordinal; :: thesis: ( B in A & A c= (dom r) /\ (dom y) & A c= dom s implies for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb )
assume A1: ( B in A & A c= (dom r) /\ (dom y) & A c= dom s ) ; :: thesis: for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb
let yb be Surreal; :: thesis: ( yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A implies |.(x - z).| infinitely< No_omega^ yb )
assume that
A2: yb = y . B and
A3: ( x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A ) ; :: thesis: |.(x - z).| infinitely< No_omega^ yb
s . B in rng s by A1, FUNCT_1:def 3;
then reconsider sB = s . B as Surreal by SURREAL0:def 16;
set S = sB + ((uReal . (r . B)) * (No_omega^ yb));
( x is sB,yb,r . B _term & z is sB,yb,r . B _term ) by A1, A2, A3;
then ( |.(x - (sB + ((uReal . (r . B)) * (No_omega^ yb)))).| infinitely< No_omega^ yb & |.(z - (sB + ((uReal . (r . B)) * (No_omega^ yb)))).| infinitely< No_omega^ yb ) by Th73;
then A4: |.((x - (sB + ((uReal . (r . B)) * (No_omega^ yb)))) - (z - (sB + ((uReal . (r . B)) * (No_omega^ yb))))).| infinitely< No_omega^ yb by Th43;
A5: (- (sB + ((uReal . (r . B)) * (No_omega^ yb)))) - (- (sB + ((uReal . (r . B)) * (No_omega^ yb)))) == 0_No by SURREALR:39;
(x + (- (sB + ((uReal . (r . B)) * (No_omega^ yb))))) + (- (z + (- (sB + ((uReal . (r . B)) * (No_omega^ yb)))))) = (x + (- (sB + ((uReal . (r . B)) * (No_omega^ yb))))) + ((- (- (sB + ((uReal . (r . B)) * (No_omega^ yb))))) + (- z)) by SURREALR:40
.= ((x + (- (sB + ((uReal . (r . B)) * (No_omega^ yb))))) + (- (- (sB + ((uReal . (r . B)) * (No_omega^ yb)))))) + (- z) by SURREALR:37
.= (x + ((- (sB + ((uReal . (r . B)) * (No_omega^ yb)))) + (- (- (sB + ((uReal . (r . B)) * (No_omega^ yb))))))) + (- z) by SURREALR:37
.= ((- (sB + ((uReal . (r . B)) * (No_omega^ yb)))) + (- (- (sB + ((uReal . (r . B)) * (No_omega^ yb)))))) + ((- z) + x) by SURREALR:37 ;
then ( (x - (sB + ((uReal . (r . B)) * (No_omega^ yb)))) - (z - (sB + ((uReal . (r . B)) * (No_omega^ yb)))) == (x - z) + 0_No & (x - z) + 0_No = x - z ) by A5, SURREALR:43;
then |.((x - (sB + ((uReal . (r . B)) * (No_omega^ yb)))) + (- (z - (sB + ((uReal . (r . B)) * (No_omega^ yb)))))).| == |.(x - z).| by Th48;
hence |.(x - z).| infinitely< No_omega^ yb by Th11, A4; :: thesis: verum