let a be Real; :: thesis: for X being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
let X be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
let seq be sequence of X; :: thesis: Partial_Sums (a * seq) = a * (Partial_Sums seq)
set PSseq = Partial_Sums seq;

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

let n be Nat; :: thesis: (a * (Partial_Sums seq)) . (n + 1) = ((a * (Partial_Sums seq)) . n) + ((a * seq) . (n + 1))
thus (a * (Partial_Sums seq)) . (n + 1) = a * ((Partial_Sums seq) . (n + 1)) by NORMSP_1:def 5
.= a * (((Partial_Sums seq) . n) + (seq . (n + 1))) by Def1
.= (a * ((Partial_Sums seq) . n)) + (a * (seq . (n + 1))) by RLVECT_1:def 5
.= ((a * (Partial_Sums seq)) . n) + (a * (seq . (n + 1))) by NORMSP_1:def 5
.= ((a * (Partial_Sums seq)) . n) + ((a * seq) . (n + 1)) by NORMSP_1:def 5 ; :: thesis: verum

end;

(a * (Partial_Sums seq)) . 0 = a * ((Partial_Sums seq) . 0) by NORMSP_1:def 5
.= a * (seq . 0) by Def1
.= (a * seq) . 0 by NORMSP_1:def 5 ;
hence Partial_Sums (a * seq) = a * (Partial_Sums seq) by A1, Def1; :: thesis: verum