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

now :: thesis: for x being object st x in NAT holds
(seq1 (##) (r (#) seq2)) . x = (r (#) (seq1 (##) seq2)) . x

let x be object ; :: 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 Nat ;
consider Fr1 being XFinSequence of REAL 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 Def4;
consider Fr2 being XFinSequence of REAL 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 Def4;

now :: thesis: for n being Nat st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n)

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:9;
hence Fr1 . n = r * (Fr2 . n) by A7; :: thesis: verum

end;

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

end;

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