let r be Real; :: thesis: for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)
let s be Real_Sequence; :: thesis: Partial_Sums (r (#) s) = r (#) (Partial_Sums s)

A1: now :: thesis: for n being Nat holds (r (#) (Partial_Sums s)) . (n + 1) = ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1))

let n be Nat; :: thesis: (r (#) (Partial_Sums s)) . (n + 1) = ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1))
thus (r (#) (Partial_Sums s)) . (n + 1) = r * ((Partial_Sums s) . (n + 1)) by SEQ_1:9
.= r * (((Partial_Sums s) . n) + (s . (n + 1))) by Def1
.= (r * ((Partial_Sums s) . n)) + (r * (s . (n + 1)))
.= ((r (#) (Partial_Sums s)) . n) + (r * (s . (n + 1))) by SEQ_1:9
.= ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1)) by SEQ_1:9 ; :: thesis: verum

end;

(r (#) (Partial_Sums s)) . 0 = r * ((Partial_Sums s) . 0) by SEQ_1:9
.= r * (s . 0) by Def1
.= (r (#) s) . 0 by SEQ_1:9 ;
hence Partial_Sums (r (#) s) = r (#) (Partial_Sums s) by A1, Def1; :: thesis: verum