let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st A c= (dom r) /\ (dom y) holds
(Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))
let y be strictly_decreasing Surreal-Sequence; :: thesis: for A being Ordinal st A c= (dom r) /\ (dom y) holds
(Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))
let A be Ordinal; :: thesis: ( A c= (dom r) /\ (dom y) implies (Partial_Sums (r,y)) . A = Sum ((r | A),(y | A)) )
assume A1: A c= (dom r) /\ (dom y) ; :: thesis: (Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))
( dom (r | A) = (dom r) /\ A & dom (y | A) = (dom y) /\ A ) by RELAT_1:61;
then A2: (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
.= A by A1, XBOOLE_1:28 ;
thus (Partial_Sums (r,y)) . A = ((Partial_Sums (r,y)) | (succ A)) . A by ORDINAL1:6, FUNCT_1:49
.= Sum ((r | A),(y | A)) by A2, Th85 ; :: thesis: verum