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

let n be Element of 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 15
.= 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 15
.= ((z * (Partial_Sums seq)) . n) + ((z * seq) . (n + 1)) by CLVECT_1:def 15 ; :: thesis: verum

end;

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