let r be Sequence of REAL ; :: thesis: for y being Sequence
for s1, s2 being uSurreal-Sequence
for alpha being Ordinal st alpha c= dom s1 & alpha c= dom s2 & s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha holds
s1 | alpha = s2 | alpha
let y be Sequence; :: thesis: for s1, s2 being uSurreal-Sequence
for alpha being Ordinal st alpha c= dom s1 & alpha c= dom s2 & s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha holds
s1 | alpha = s2 | alpha
let s1, s2 be uSurreal-Sequence; :: thesis: for alpha being Ordinal st alpha c= dom s1 & alpha c= dom s2 & s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha holds
s1 | alpha = s2 | alpha
let alpha be Ordinal; :: thesis: ( alpha c= dom s1 & alpha c= dom s2 & s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha implies s1 | alpha = s2 | alpha )
assume that
A1: ( alpha c= dom s1 & alpha c= dom s2 ) and
A2: ( s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha ) ; :: thesis: s1 | alpha = s2 | alpha
defpred S₁[ Ordinal] means ( $1 in alpha implies s1 . $1 = s2 . $1 );
A3: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A4: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A5: D in alpha ; :: thesis: s1 . D = s2 . D
then A6: ( s1,y,r simplest_on_position D & s2,y,r simplest_on_position D ) by A2;
A7: D c= alpha by A5, ORDINAL1:def 2;
A8: ( dom (s1 | D) = D & D = dom (s2 | D) ) by RELAT_1:62, A5, ORDINAL1:def 2, A1;
A9: for x being object st x in D holds
(s1 | D) . x = (s2 | D) . x

proof

let x be object ; :: thesis: ( x in D implies (s1 | D) . x = (s2 | D) . x )
assume A10: x in D ; :: thesis: (s1 | D) . x = (s2 | D) . x
reconsider o = x as Ordinal by A10;
thus (s1 | D) . x = s1 . o by A10, FUNCT_1:49
.= s2 . o by A7, A4, A10
.= (s2 | D) . x by A10, FUNCT_1:49 ; :: thesis: verum

end;

( s1 . D in rng s1 & s2 . D in rng s2 ) by A1, A5, FUNCT_1:def 3;
then ( s1 . D is uSurreal & s2 . D is uSurreal ) by SURREALO:def 12;
hence s1 . D = s2 . D by A9, A6, A8, FUNCT_1:2, Th76; :: thesis: verum

end;

A11: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A3);
A12: ( dom (s1 | alpha) = alpha & alpha = dom (s2 | alpha) ) by A1, RELAT_1:62;
for x being object st x in alpha holds
(s1 | alpha) . x = (s2 | alpha) . x

proof

let x be object ; :: thesis: ( x in alpha implies (s1 | alpha) . x = (s2 | alpha) . x )
assume A13: x in alpha ; :: thesis: (s1 | alpha) . x = (s2 | alpha) . x
reconsider o = x as Ordinal by A13;
thus (s1 | alpha) . x = s1 . o by A13, FUNCT_1:49
.= s2 . o by A11, A13
.= (s2 | alpha) . x by A13, FUNCT_1:49 ; :: thesis: verum

end;

hence s1 | alpha = s2 | alpha by A12, FUNCT_1:2; :: thesis: verum