let i be Nat; :: thesis: ( i in dom ((Sum M1) + (Sum M2)) implies ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i )
assume A4: i in dom ((Sum M1) + (Sum M2)) ; :: thesis: ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i
then A5: i in dom (addreal .: ((Sum M1),(Sum M2))) ;
i in Seg (len (M1 ^^ M2)) by A2, A3, A4, Def1;
then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
then A7: i in (dom M1) /\ (dom M2) by PRE_POLY:def 4;
then i in dom M1 by XBOOLE_0:def 4;
then i in Seg (len M1) by FINSEQ_1:def 3;
then i in Seg (len (Sum M1)) by Def1;
then A8: i in dom (Sum M1) by FINSEQ_1:def 3;
i in dom M2 by A7, XBOOLE_0:def 4;
then i in Seg (len M2) by FINSEQ_1:def 3;
then i in Seg (len (Sum M2)) by Def1;
then A9: i in dom (Sum M2) by FINSEQ_1:def 3;
A10: i in dom (Sum (M1 ^^ M2)) by A2, A3, A4, FINSEQ_1:def 3;
A11: (M1 . i) ^ (M2 . i) = (M1 ^^ M2) . i by A6, PRE_POLY:def 4;
thus ((Sum M1) + (Sum M2)) . i = (addreal .: ((Sum M1),(Sum M2))) . i
.= addreal . (((Sum M1) . i),((Sum M2) . i)) by A5, FUNCOP_1:22
.= ((Sum M1) . i) + ((Sum M2) . i) by BINOP_2:def 9
.= (Sum (M1 . i)) + ((Sum M2) . i) by A8, Def1
.= (Sum (M1 . i)) + (Sum (M2 . i)) by A9, Def1
.= Sum ((M1 ^^ M2) . i) by A11, RVSUM_1:75
.= (Sum (M1 ^^ M2)) . i by A10, Def1 ; :: thesis: verum