let seq1, seq2 be Real_Sequence; :: thesis: for r being real number holds seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2)
let r be real number ; :: thesis: seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2)
set RS = r (#) seq2;
set S = seq1 (##) seq2;

now

let x be set ; :: thesis: ( x in NAT implies (seq1 (##) (r (#) seq2)) . x = (r (#) (seq1 (##) seq2)) . x )
assume x in NAT ; :: thesis: (seq1 (##) (r (#) seq2)) . x = (r (#) (seq1 (##) seq2)) . x
then reconsider k = x as Element of NAT ;
consider Fr1 being XFinSequence of such that
A1: dom Fr1 = k + 1 and
A2: for n being Nat st n in k + 1 holds
Fr1 . n = (seq1 . n) * ((r (#) seq2) . (k -' n)) and
A3: Sum Fr1 = (seq1 (##) (r (#) seq2)) . k by Def5;
consider Fr2 being XFinSequence of such that
A4: dom Fr2 = k + 1 and
A5: for n being Nat st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) and
A6: Sum Fr2 = (seq1 (##) seq2) . k by Def5;

now

let n be Nat; :: thesis: ( n in len Fr1 implies Fr1 . n = r * (Fr2 . n) )
assume n in len Fr1 ; :: thesis: Fr1 . n = r * (Fr2 . n)
then A7: ( Fr1 . n = (seq1 . n) * ((r (#) seq2) . (k -' n)) & Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) ) by A1, A2, A5;
(r (#) seq2) . (k -' n) = r * (seq2 . (k -' n)) by SEQ_1:13;
hence Fr1 . n = r * (Fr2 . n) by A7; :: thesis: verum

end;

then Sum Fr1 = r * (Sum Fr2) by A1, A4, Th49;
hence (seq1 (##) (r (#) seq2)) . x = (r (#) (seq1 (##) seq2)) . x by A3, A6, SEQ_1:13; :: thesis: verum

end;

hence seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2) by FUNCT_2:18; :: thesis: verum