let r be Sequence of REAL ; :: thesis:
let y, s be Sequence; :: thesis:
let alpha be Ordinal; :: thesis:

suppose dom s c= succ alpha ; :: thesis:

hence ( s | (succ alpha),y,r simplest_on_position alpha iff s,y,r simplest_on_position alpha ) by RELAT_1:68; :: thesis:

end;

suppose not dom s c= succ alpha ; :: thesis:

thus ( s | (succ alpha),y,r simplest_on_position alpha implies s,y,r simplest_on_position alpha ) :: thesis:

assume A1: s | (succ alpha),y,r simplest_on_position alpha ; :: thesis:
let sa be Surreal; :: according to SURREALC:def 15 :: thesis:
assume A2: sa = s . alpha ; :: thesis:
A3: (s | (succ alpha)) . alpha = sa by ORDINAL1:6, A2, FUNCT_1:49;
hence ( 0 = alpha implies sa = 0_No ) by A1; :: thesis:
assume A4: 0 <> alpha ; :: thesis:
sa in_meets_terms s | (succ alpha),y,r,alpha by A1, A3;
hence sa in_meets_terms s,y,r,alpha by Th79; :: thesis:
let x be uSurreal; :: thesis:
assume A5: ( x in_meets_terms s,y,r,alpha & x <> sa ) ; :: thesis:
x in_meets_terms s | (succ alpha),y,r,alpha by A5, Th79;
hence born sa in born x by A4, A1, A3, A5; :: thesis:

end;

assume A6: s,y,r simplest_on_position alpha ; :: thesis:
let sa be Surreal; :: according to SURREALC:def 15 :: thesis:
assume A7: sa = (s | (succ alpha)) . alpha ; :: thesis:
A8: s . alpha = sa by ORDINAL1:6, A7, FUNCT_1:49;
hence ( 0 = alpha implies sa = 0_No ) by A6; :: thesis:
assume A9: 0 <> alpha ; :: thesis:
sa in_meets_terms s,y,r,alpha by A6, A8;
hence sa in_meets_terms s | (succ alpha),y,r,alpha by Th79; :: thesis:
let x be uSurreal; :: thesis:
assume A10: ( x in_meets_terms s | (succ alpha),y,r,alpha & x <> sa ) ; :: thesis:
x in_meets_terms s,y,r,alpha by A10, Th79;
hence born sa in born x by A9, A6, A8, A10; :: thesis:

end;

end;