defpred S₁[ object , object ] means ( $2 is Ordinal & ( for sa being Surreal st sa = s . $1 holds
$2 = born sa ) );
A1: for o being object st o in dom s holds
ex u being object st S₁[o,u]

proof

let o be object ; :: thesis: ( o in dom s implies ex u being object st S₁[o,u] )
assume o in dom s ; :: thesis: ex u being object st S₁[o,u]
then s . o in rng s by FUNCT_1:def 3;
then reconsider so = s . o as Surreal by SURREAL0:def 16;
take born so ; :: thesis: S₁[o, born so]
thus S₁[o, born so] ; :: thesis: verum

end;

consider b being Function such that
A2: ( dom b = dom s & ( for o being object st o in dom s holds
S₁[o,b . o] ) ) from CLASSES1:sch 1(A1);
reconsider b = b as Sequence by A2, ORDINAL1:def 7;
consider M being Ordinal such that
A3: for o being object st o in rng s holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
rng b c= M

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng b or a in M )
assume A4: a in rng b ; :: thesis: a in M
consider o being object such that
A5: ( o in dom b & b . o = a ) by A4, FUNCT_1:def 3;
A6: s . o in rng s by A2, A5, FUNCT_1:def 3;
then reconsider so = s . o as Surreal by SURREAL0:def 16;
consider A being Ordinal such that
A7: ( A in M & so in Day A ) by A6, A3;
born so c= A by A7, SURREAL0:def 18;
then born so in M by A7, ORDINAL1:12;
hence a in M by A5, A2; :: thesis: verum

end;

then reconsider b = b as Ordinal-Sequence by ORDINAL2:def 4;
take b ; :: thesis: ( dom b = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b . alpha = born sa ) )
thus ( dom b = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b . alpha = born sa ) ) by A2; :: thesis: verum