let x, z be Surreal; :: thesis: for r being 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< yb
let r be 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< 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< 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< 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< 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< 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< 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< 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)) * yb);
( x is sB,yb,r . B _Term & z is sB,yb,r . B _Term ) by A1, A2, A3;
then A4: |.((x - (sB + ((uReal . (r . B)) * yb))) - (z - (sB + ((uReal . (r . B)) * yb)))).| infinitely< yb by Th43;
A5: (- (sB + ((uReal . (r . B)) * yb))) - (- (sB + ((uReal . (r . B)) * yb))) == 0_No by SURREALR:39;
(x + (- (sB + ((uReal . (r . B)) * yb)))) + (- (z + (- (sB + ((uReal . (r . B)) * yb))))) = (x + (- (sB + ((uReal . (r . B)) * yb)))) + ((- (- (sB + ((uReal . (r . B)) * yb)))) + (- z)) by SURREALR:40
.= ((x + (- (sB + ((uReal . (r . B)) * yb)))) + (- (- (sB + ((uReal . (r . B)) * yb))))) + (- z) by SURREALR:37
.= (x + ((- (sB + ((uReal . (r . B)) * yb))) + (- (- (sB + ((uReal . (r . B)) * yb)))))) + (- z) by SURREALR:37
.= ((- (sB + ((uReal . (r . B)) * yb))) + (- (- (sB + ((uReal . (r . B)) * yb))))) + ((- z) + x) by SURREALR:37 ;
then ( (x - (sB + ((uReal . (r . B)) * yb))) - (z - (sB + ((uReal . (r . B)) * yb))) == (x - z) + 0_No & (x - z) + 0_No = x - z ) by A5, SURREALR:43;
then |.((x - (sB + ((uReal . (r . B)) * yb))) + (- (z - (sB + ((uReal . (r . B)) * yb))))).| == |.(x - z).| by Th48;
hence |.(x - z).| infinitely< yb by Th11, A4; :: thesis: verum