let a be Real; :: thesis: for X being non empty RealLinearSpace-like RLSStruct
for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
let X be non empty RealLinearSpace-like 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

let n be Element of 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 8
.= a * (((Partial_Sums seq) . n) + (seq . (n + 1))) by Def1
.= (a * ((Partial_Sums seq) . n)) + (a * (seq . (n + 1))) by RLVECT_1:def 9
.= ((a * (Partial_Sums seq)) . n) + (a * (seq . (n + 1))) by NORMSP_1:def 8
.= ((a * (Partial_Sums seq)) . n) + ((a * seq) . (n + 1)) by NORMSP_1:def 8 ; :: thesis: verum

end;

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