let b1, b2 be Ordinal-Sequence; :: thesis: ( dom b1 = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b1 . alpha = born sa ) & dom b2 = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b2 . alpha = born sa ) implies b1 = b2 )
assume that
A8: ( dom b1 = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b1 . alpha = born sa ) ) and
A9: ( dom b2 = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b2 . alpha = born sa ) ) ; :: thesis: b1 = b2
for o being object st o in dom s holds
b1 . o = b2 . o

proof

let o be object ; :: thesis: ( o in dom s implies b1 . o = b2 . o )
assume A10: o in dom s ; :: thesis: b1 . o = b2 . o
then s . o in rng s by FUNCT_1:def 3;
then reconsider so = s . o as Surreal by SURREAL0:def 16;
b1 . o = born so by A10, A8;
hence b1 . o = b2 . o by A10, A9; :: thesis: verum

end;

hence b1 = b2 by A8, A9, FUNCT_1:2; :: thesis: verum