let seq be Complex_Sequence; :: thesis: for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
let z be complex number ; :: thesis: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq)
defpred S₁[ Element of NAT ] means (Partial_Sums (z (#) seq)) . $1 = (z (#) (Partial_Sums seq)) . $1;
A1: S₁[ 0 ]

proof

thus (Partial_Sums (z (#) seq)) . 0 = (z (#) seq) . 0 by Def7
.= z * (seq . 0 ) by VALUED_1:6
.= z * ((Partial_Sums seq) . 0 ) by Def7
.= (z (#) (Partial_Sums seq)) . 0 by VALUED_1:6 ; :: thesis: verum

end;

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

thus (Partial_Sums (z (#) seq)) . (n + 1) = ((Partial_Sums (z (#) seq)) . n) + ((z (#) seq) . (n + 1)) by Def7
.= (z * ((Partial_Sums seq) . n)) + ((z (#) seq) . (n + 1)) by A3, VALUED_1:6
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by VALUED_1:6
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1)))
.= z * ((Partial_Sums seq) . (n + 1)) by Def7
.= (z (#) (Partial_Sums seq)) . (n + 1) by VALUED_1:6 ; :: thesis: verum

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by FUNCT_2:113; :: thesis: verum