let a, b be Real; :: thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
let seq1, seq2 be sequence of X; :: thesis: (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
thus (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = (Partial_Sums (a * seq1)) + (b * (Partial_Sums seq2)) by Th3
.= (Partial_Sums (a * seq1)) + (Partial_Sums (b * seq2)) by Th3
.= Partial_Sums ((a * seq1) + (b * seq2)) by Th1 ; :: thesis: verum