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 A1: x in NAT ; :: thesis: (seq1 (##) (r (#) seq2)) . x = (r (#) (seq1 (##) seq2)) . x
reconsider k = x as Element of NAT by A1;
consider Fr1 being XFinSequence of REAL such that
A2: dom Fr1 = k + 1 and
A3: for n being Element of NAT st n in k + 1 holds
Fr1 . n = (seq1 . n) * ((r (#) seq2) . (k -' n)) and
A4: Sum Fr1 = (seq1 (##) (r (#) seq2)) . k by Def5;
consider Fr2 being XFinSequence of REAL such that
A5: dom Fr2 = k + 1 and
A6: for n being Element of NAT st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) and
A7: Sum Fr2 = (seq1 (##) seq2) . k by Def5;

now

let n be Element of NAT ; :: thesis: ( n in len Fr1 implies Fr1 . n = r * (Fr2 . n) )
assume A8: n in len Fr1 ; :: thesis: Fr1 . n = r * (Fr2 . n)
( Fr1 . n = (seq1 . n) * ((r (#) seq2) . (k -' n)) & Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) & (r (#) seq2) . (k -' n) = r * (seq2 . (k -' n)) ) by A2, A3, A6, A8, SEQ_1:13;
hence Fr1 . n = r * (Fr2 . n) ; :: thesis: verum

end;

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

end;

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