let x be Surreal; :: thesis: for r1, r2 being non-zero Sequence of REAL
for y1, y2 being strictly_decreasing Surreal-Sequence
for A being Ordinal st r1,y1,A name_like x & r2,y2,A name_like x holds
( r1 | A = r2 | A & y1 | A = y2 | A )
let r1, r2 be non-zero Sequence of REAL ; :: thesis: for y1, y2 being strictly_decreasing Surreal-Sequence
for A being Ordinal st r1,y1,A name_like x & r2,y2,A name_like x holds
( r1 | A = r2 | A & y1 | A = y2 | A )
let y1, y2 be strictly_decreasing Surreal-Sequence; :: thesis: for A being Ordinal st r1,y1,A name_like x & r2,y2,A name_like x holds
( r1 | A = r2 | A & y1 | A = y2 | A )
let A be Ordinal; :: thesis: ( r1,y1,A name_like x & r2,y2,A name_like x implies ( r1 | A = r2 | A & y1 | A = y2 | A ) )
assume that
A1: r1,y1,A name_like x and
A2: r2,y2,A name_like x ; :: thesis: ( r1 | A = r2 | A & y1 | A = y2 | A )
defpred S₁[ Ordinal] means ( r1,y1,$1 name_like x & r2,y2,$1 name_like x implies ( r1 | $1 = r2 | $1 & y1 | $1 = y2 | $1 ) );
A3: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A4: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A5: ( r1,y1,D name_like x & r2,y2,D name_like x ) ; :: thesis: ( r1 | D = r2 | D & y1 | D = y2 | D )
A6: ( dom (r1 | D) = D & D = dom (r2 | D) & dom (y1 | D) = D & D = dom (y2 | D) ) by A5, RELAT_1:62;
A7: for o being object st o in D holds
( (r1 | D) . o = (r2 | D) . o & (y1 | D) . o = (y2 | D) . o )

proof

let o be object ; :: thesis: ( o in D implies ( (r1 | D) . o = (r2 | D) . o & (y1 | D) . o = (y2 | D) . o ) )
assume A8: o in D ; :: thesis: ( (r1 | D) . o = (r2 | D) . o & (y1 | D) . o = (y2 | D) . o )
then reconsider o = o as Ordinal ;
A9: ( r1 . o = (r1 | D) . o & r2 . o = (r2 | D) . o & y1 . o = (y1 | D) . o & y2 . o = (y2 | D) . o ) by A8, FUNCT_1:49;
A10: S₁[o] by A8, A4;
o c= (dom r1) /\ (dom y1) by A5, A8, ORDINAL1:def 2;
then o in succ ((dom r1) /\ (dom y1)) by ORDINAL1:22;
then o in dom (Partial_Sums (r1,y1)) by Def17;
then (Partial_Sums (r1,y1)) . o in rng (Partial_Sums (r1,y1)) by FUNCT_1:def 3;
then reconsider Po1 = (Partial_Sums (r1,y1)) . o as uSurreal by SURREALO:def 12;
o c= (dom r2) /\ (dom y2) by A5, A8, ORDINAL1:def 2;
then o in succ ((dom r2) /\ (dom y2)) by ORDINAL1:22;
then o in dom (Partial_Sums (r2,y2)) by Def17;
then (Partial_Sums (r2,y2)) . o in rng (Partial_Sums (r2,y2)) by FUNCT_1:def 3;
then reconsider Po2 = (Partial_Sums (r2,y2)) . o as uSurreal by SURREALO:def 12;
A11: Po1 = ((Partial_Sums (r1,y1)) | (succ o)) . o by FUNCT_1:49, ORDINAL1:6
.= (Partial_Sums ((r2 | o),(y2 | o))) . o by Th85, A8, ORDINAL1:def 2, A10, A5, Th86
.= ((Partial_Sums (r2,y2)) | (succ o)) . o by Th85
.= Po2 by ORDINAL1:6, FUNCT_1:49 ;
( r1 . o = omega-r (x - Po1) & y1 . o = omega-y (x - Po1) & r2 . o = omega-r (x - Po2) & y2 . o = omega-y (x - Po2) ) by A8, A5;
hence ( (r1 | D) . o = (r2 | D) . o & (y1 | D) . o = (y2 | D) . o ) by A11, A9; :: thesis: verum

end;

then for o being object st o in D holds
(r1 | D) . o = (r2 | D) . o ;
hence r1 | D = r2 | D by A6, FUNCT_1:2; :: thesis: y1 | D = y2 | D
for o being object st o in D holds
(y1 | D) . o = (y2 | D) . o by A7;
hence y1 | D = y2 | D by A6, FUNCT_1:2; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A3);
hence ( r1 | A = r2 | A & y1 | A = y2 | A ) by A1, A2; :: thesis: verum