let X be RealNormSpace; :: thesis: for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let seq be sequence of X; :: thesis: for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let z be Real; :: thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq)
defpred S₁[ Nat] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $1;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Sums (z * seq)) . (n + 1) = ((Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1)) by BHSP_4:def 1
.= (z * ((Partial_Sums seq) . n)) + ((z * seq) . (n + 1)) by A2, NORMSP_1:def 5
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by NORMSP_1:def 5
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by RLVECT_1:def 5
.= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . (n + 1) by NORMSP_1:def 5 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def 1
.= z * (seq . 0) by NORMSP_1:def 5
.= z * ((Partial_Sums seq) . 0) by BHSP_4:def 1
.= (z * (Partial_Sums seq)) . 0 by NORMSP_1:def 5 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
then for n being Element of NAT holds S₁[n] ;
hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; :: thesis: verum