let r be Sequence of REAL ; :: thesis: for y being Surreal-Sequence
for s being uSurreal-Sequence
for alpha being Ordinal st s,y,r simplest_up_to alpha & s | alpha is one-to-one holds
(born s) | alpha is increasing
let y be Surreal-Sequence; :: thesis: for s being uSurreal-Sequence
for alpha being Ordinal st s,y,r simplest_up_to alpha & s | alpha is one-to-one holds
(born s) | alpha is increasing
let s be uSurreal-Sequence; :: thesis: for alpha being Ordinal st s,y,r simplest_up_to alpha & s | alpha is one-to-one holds
(born s) | alpha is increasing
let alpha be Ordinal; :: thesis: ( s,y,r simplest_up_to alpha & s | alpha is one-to-one implies (born s) | alpha is increasing )
assume A1: ( s,y,r simplest_up_to alpha & s | alpha is one-to-one ) ; :: thesis: (born s) | alpha is increasing
for A, B being Ordinal st A in B & B in dom ((born s) | alpha) holds
((born s) | alpha) . A in ((born s) | alpha) . B

proof

set bs = born s;
let A, B be Ordinal; :: thesis: ( A in B & B in dom ((born s) | alpha) implies ((born s) | alpha) . A in ((born s) | alpha) . B )
assume A2: ( A in B & B in dom ((born s) | alpha) ) ; :: thesis: ((born s) | alpha) . A in ((born s) | alpha) . B
A3: ( B in alpha & B in dom (born s) & dom (born s) = dom s ) by Def20, A2, RELAT_1:57;
A4: s,y,r simplest_on_position B by A1, A2;
A5: ( B in dom s & A in dom s ) by A2, A3, ORDINAL1:10;
then ( s . B in rng s & s . A in rng s ) by FUNCT_1:def 3;
then reconsider sB = s . B, sA = s . A as uSurreal by SURREALO:def 12;
A6: A in alpha by A2, ORDINAL1:10;
A7: s,y,r simplest_on_position A by A1, A2, ORDINAL1:10;
A8: A c= B by A2, ORDINAL1:def 2;
sB in_meets_terms s,y,r,B by A4;
then A9: sB in_meets_terms s,y,r,A by A8;
A10: A <> B by A2;
( B in dom (s | alpha) & A in dom (s | alpha) & sA = (s | alpha) . A & sB = (s | alpha) . B ) by RELAT_1:57, A2, A5, A6, FUNCT_1:49;
then A11: sA <> sB by A10, A1, FUNCT_1:def 4;
( ((born s) | alpha) . A = (born s) . A & ((born s) | alpha) . B = (born s) . B ) by A2, ORDINAL1:10, FUNCT_1:49;
then A12: ( ((born s) | alpha) . A = born sA & ((born s) | alpha) . B = born sB ) by Def20, A2, A3, ORDINAL1:10;

per cases ( A = 0 or A <> 0 ) ;

suppose A = 0 ; :: thesis: ((born s) | alpha) . A in ((born s) | alpha) . B

then A13: sA = 0_No by A7;
then A14: born sA = 0 by SURREAL0:37;
A15: {} c= born sB ;
born sB <> 0 by A13, A11, SURREAL0:37;
hence ((born s) | alpha) . A in ((born s) | alpha) . B by A12, A14, ORDINAL1:11, A15, XBOOLE_0:def 8; :: thesis: verum

end;

suppose A <> 0 ; :: thesis: ((born s) | alpha) . A in ((born s) | alpha) . B

hence ((born s) | alpha) . A in ((born s) | alpha) . B by A12, A7, A9, A11; :: thesis: verum

end;

end;

end;

hence (born s) | alpha is increasing by ORDINAL2:def 12; :: thesis: verum