let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
let seq1, seq2 be sequence of X; :: thesis: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
set PSseq1 = Partial_Sums seq1;
set PSseq2 = Partial_Sums seq2;

A1: now :: thesis: for n being Nat holds ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1))

let n be Nat; :: thesis: ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1))
thus ((Partial_Sums seq1) + (Partial_Sums seq2)) . (n + 1) = ((Partial_Sums seq1) . (n + 1)) + ((Partial_Sums seq2) . (n + 1)) by NORMSP_1:def 2
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((Partial_Sums seq2) . (n + 1)) by BHSP_4:def 1
.= (((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + ((seq2 . (n + 1)) + ((Partial_Sums seq2) . n)) by BHSP_4:def 1
.= ((((Partial_Sums seq1) . n) + (seq1 . (n + 1))) + (seq2 . (n + 1))) + ((Partial_Sums seq2) . n) by RLVECT_1:def 3
.= (((Partial_Sums seq1) . n) + ((seq1 . (n + 1)) + (seq2 . (n + 1)))) + ((Partial_Sums seq2) . n) by RLVECT_1:def 3
.= (((Partial_Sums seq1) . n) + ((seq1 + seq2) . (n + 1))) + ((Partial_Sums seq2) . n) by NORMSP_1:def 2
.= (((Partial_Sums seq1) . n) + ((Partial_Sums seq2) . n)) + ((seq1 + seq2) . (n + 1)) by RLVECT_1:def 3
.= (((Partial_Sums seq1) + (Partial_Sums seq2)) . n) + ((seq1 + seq2) . (n + 1)) by NORMSP_1:def 2 ; :: thesis: verum

end;

((Partial_Sums seq1) + (Partial_Sums seq2)) . 0 = ((Partial_Sums seq1) . 0) + ((Partial_Sums seq2) . 0) by NORMSP_1:def 2
.= (seq1 . 0) + ((Partial_Sums seq2) . 0) by BHSP_4:def 1
.= (seq1 . 0) + (seq2 . 0) by BHSP_4:def 1
.= (seq1 + seq2) . 0 by NORMSP_1:def 2 ;
hence (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by A1, BHSP_4:def 1; :: thesis: verum