let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let seq be sequence of X; :: thesis: for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let z be Complex; :: thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq)
set PSseq = Partial_Sums seq;

A1: now :: thesis: for n being Nat holds (z * (Partial_Sums seq)) . (n + 1) = ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1))

let n be Nat; :: thesis: (z * (Partial_Sums seq)) . (n + 1) = ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1))
thus (z * (Partial_Sums seq)) . (n + 1) = z * ((Partial_Sums seq) . (n + 1)) by CLVECT_1:def 14
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by BHSP_4:def 1
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by CLVECT_1:def 2
.= ((z * (Partial_Sums seq)) . n) + (z * (seq . (n + 1))) by CLVECT_1:def 14
.= ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1)) by CLVECT_1:def 14 ; :: thesis: verum

end;

(z * (Partial_Sums seq)) . 0 = z * ((Partial_Sums seq) . 0) by CLVECT_1:def 14
.= z * (seq . 0) by BHSP_4:def 1
.= (z * seq) . 0 by CLVECT_1:def 14 ;
hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by A1, BHSP_4:def 1; :: thesis: verum