let r be Sequence of REAL ; :: thesis: for y, s1, s2 being Sequence
for alpha being Ordinal st s1 . alpha is uSurreal & s2 . alpha is uSurreal & s1 | alpha = s2 | alpha & s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha holds
s1 . alpha = s2 . alpha
let y, s1, s2 be Sequence; :: thesis: for alpha being Ordinal st s1 . alpha is uSurreal & s2 . alpha is uSurreal & s1 | alpha = s2 | alpha & s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha holds
s1 . alpha = s2 . alpha
let alpha be Ordinal; :: thesis: ( s1 . alpha is uSurreal & s2 . alpha is uSurreal & s1 | alpha = s2 | alpha & s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha implies s1 . alpha = s2 . alpha )
assume that
A1: ( s1 . alpha is uSurreal & s2 . alpha is uSurreal ) and
A2: s1 | alpha = s2 | alpha and
A3: ( s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha ) and
A4: s1 . alpha <> s2 . alpha ; :: thesis: contradiction
reconsider s1a = s1 . alpha, s2a = s2 . alpha as uSurreal by A1;

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

suppose alpha = 0 ; :: thesis: contradiction

then ( s1 . alpha = 0_No & 0_No = s2 . alpha ) by A1, A3;
hence contradiction by A4; :: thesis: verum

end;

suppose A5: alpha <> 0 ; :: thesis: contradiction

s1a in_meets_terms s1,y,r,alpha by A3;
then s1a in_meets_terms s2,y,r,alpha by A2, Th75;
then A6: born s2a in born s1a by A4, A3, A5;
s2a in_meets_terms s2,y,r,alpha by A3;
then s2a in_meets_terms s1,y,r,alpha by A2, Th75;
hence contradiction by A6, A4, A3, A5; :: thesis: verum

end;

end;