let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence
for A being Ordinal holds (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A))
let y be strictly_decreasing Surreal-Sequence; :: thesis: for A being Ordinal holds (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A))
let A be Ordinal; :: thesis: (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A))
A1: dom (Partial_Sums (r,y)) = succ ((dom r) /\ (dom y)) by Def17;
then A2: dom ((Partial_Sums (r,y)) | (succ A)) = (succ ((dom r) /\ (dom y))) /\ (succ A) by RELAT_1:61;
( dom (r | A) = (dom r) /\ A & dom (y | A) = (dom y) /\ A ) by RELAT_1:61;
then A3: (dom (r | A)) /\ (dom (y | A)) = ((A /\ (dom r)) /\ (dom y)) /\ A by XBOOLE_1:16
.= (A /\ ((dom r) /\ (dom y))) /\ A by XBOOLE_1:16
.= ((dom r) /\ (dom y)) /\ (A /\ A) by XBOOLE_1:16
.= ((dom r) /\ (dom y)) /\ A ;
A4: (succ ((dom r) /\ (dom y))) /\ (succ A) = succ ((dom (r | A)) /\ (dom (y | A)))

proof

per cases ( (dom r) /\ (dom y) c= A or A in (dom r) /\ (dom y) ) by ORDINAL1:16;

suppose A5: (dom r) /\ (dom y) c= A ; :: thesis: (succ ((dom r) /\ (dom y))) /\ (succ A) = succ ((dom (r | A)) /\ (dom (y | A)))

then A6: ((dom r) /\ (dom y)) /\ A = (dom r) /\ (dom y) by XBOOLE_1:28;
(dom r) /\ (dom y) in succ A by A5, ORDINAL1:22;
hence (succ ((dom r) /\ (dom y))) /\ (succ A) = succ ((dom (r | A)) /\ (dom (y | A))) by A6, A3, XBOOLE_1:28, ORDINAL1:21; :: thesis: verum

end;

suppose A7: A in (dom r) /\ (dom y) ; :: thesis: (succ ((dom r) /\ (dom y))) /\ (succ A) = succ ((dom (r | A)) /\ (dom (y | A)))

then A8: A c= (dom r) /\ (dom y) by ORDINAL1:def 2;
A9: ((dom r) /\ (dom y)) /\ A = A by A7, ORDINAL1:def 2, XBOOLE_1:28;
A in succ ((dom r) /\ (dom y)) by A8, ORDINAL1:22;
hence (succ ((dom r) /\ (dom y))) /\ (succ A) = succ ((dom (r | A)) /\ (dom (y | A))) by A9, A3, XBOOLE_1:28, ORDINAL1:21; :: thesis: verum

end;

end;

end;

(Partial_Sums (r,y)) | (succ A),y | A,r | A simplest_up_to dom ((Partial_Sums (r,y)) | (succ A))

proof

let B be Ordinal; :: according to SURREALC:def 16 :: thesis: ( B in dom ((Partial_Sums (r,y)) | (succ A)) implies (Partial_Sums (r,y)) | (succ A),y | A,r | A simplest_on_position B )
assume A10: B in dom ((Partial_Sums (r,y)) | (succ A)) ; :: thesis: (Partial_Sums (r,y)) | (succ A),y | A,r | A simplest_on_position B
A11: ( succ B c= succ A & B c= A ) by A10, ORDINAL1:21, ORDINAL1:22;
A12: ((Partial_Sums (r,y)) | (succ A)) | (succ B) = (Partial_Sums (r,y)) | (succ B) by RELAT_1:74, A10, ORDINAL1:21;
A13: B in dom (Partial_Sums (r,y)) by A1, A10, A2, XBOOLE_0:def 4;
Partial_Sums (r,y),y,r simplest_on_position B by A13, Def17;
then Partial_Sums (r,y),y | A,r | A simplest_on_position B by A11, Th84;
then (Partial_Sums (r,y)) | (succ B),y | A,r | A simplest_on_position B by Th80;
hence (Partial_Sums (r,y)) | (succ A),y | A,r | A simplest_on_position B by A12, Th80; :: thesis: verum

end;

hence (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A)) by A4, A1, RELAT_1:61, Def17; :: thesis: verum