let r be Sequence of REAL ; :: thesis: for y being Surreal-Sequence
for s being uSurreal-Sequence
for A being Ordinal st s,y,r simplest_up_to A & A c= succ (dom y) holds
s | A is one-to-one
let y be Surreal-Sequence; :: thesis: for s being uSurreal-Sequence
for A being Ordinal st s,y,r simplest_up_to A & A c= succ (dom y) holds
s | A is one-to-one
let s be uSurreal-Sequence; :: thesis: for A being Ordinal st s,y,r simplest_up_to A & A c= succ (dom y) holds
s | A is one-to-one
let A be Ordinal; :: thesis: ( s,y,r simplest_up_to A & A c= succ (dom y) implies s | A is one-to-one )
assume A1: ( s,y,r simplest_up_to A & A c= succ (dom y) ) ; :: thesis: s | A is one-to-one
A2: for a, b being Ordinal st a in b & b in dom (s | A) holds
(s | A) . a <> (s | A) . b

proof

let a, b be Ordinal; :: thesis: ( a in b & b in dom (s | A) implies (s | A) . a <> (s | A) . b )
assume A3: ( a in b & b in dom (s | A) ) ; :: thesis: (s | A) . a <> (s | A) . b
A4: ( b in A & b in dom s ) by A3, RELAT_1:57;
then a in dom s by A3, ORDINAL1:10;
then ( s . b in rng s & s . a in rng s ) by A4, FUNCT_1:def 3;
then reconsider sb = s . b, sa = s . a as uSurreal by SURREALO:def 12;
A5: ( sa = (s | A) . a & sb = (s | A) . b ) by A3, FUNCT_1:47, ORDINAL1:10;
A6: succ a c= b by A3, ORDINAL1:21;
s,y,r simplest_on_position b by A1, A3;
then sb in_meets_terms s,y,r,b ;
then A7: sb in_meets_terms s,y,r, succ a by A6;
b c= dom y by A1, A4, ORDINAL1:22;
then y . a in rng y by A3, FUNCT_1:def 3;
then reconsider ya = y . a as Surreal by SURREAL0:def 16;
sb is sa,ya,r . a _term by A7, ORDINAL1:6;
then A8: not sb + (- sa) == 0_No ;
not sb == sa

proof

assume sb == sa ; :: thesis: contradiction
then ( sb + (- sa) == sa - sa & sa - sa == 0_No ) by SURREALR:43, SURREALR:39;
hence contradiction by A8, SURREALO:4; :: thesis: verum

end;

hence (s | A) . a <> (s | A) . b by A5; :: thesis: verum

end;

for x1, x2 being object st x1 in dom (s | A) & x2 in dom (s | A) & (s | A) . x1 = (s | A) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (s | A) & x2 in dom (s | A) & (s | A) . x1 = (s | A) . x2 implies x1 = x2 )
assume A9: ( x1 in dom (s | A) & x2 in dom (s | A) & (s | A) . x1 = (s | A) . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Ordinal by A9;
( not x1 in x2 & not x2 in x1 ) by A9, A2;
hence x1 = x2 by ORDINAL1:14; :: thesis: verum

end;

hence s | A is one-to-one by FUNCT_1:def 4; :: thesis: verum