let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
let seq1, seq2 be sequence of X; :: thesis: for z1, z2 being Complex holds (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
let z1, z2 be Complex; :: thesis: (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = Partial_Sums ((z1 * seq1) + (z2 * seq2))
thus (z1 * (Partial_Sums seq1)) + (z2 * (Partial_Sums seq2)) = (Partial_Sums (z1 * seq1)) + (z2 * (Partial_Sums seq2)) by Th3
.= (Partial_Sums (z1 * seq1)) + (Partial_Sums (z2 * seq2)) by Th3
.= Partial_Sums ((z1 * seq1) + (z2 * seq2)) by Th1 ; :: thesis: verum