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

now :: thesis: for n being Element of NAT holds (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . n

let n be Element of NAT ; :: thesis: (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . n
thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by Th9
.= r * ((seq1 . n) * (seq2 . n)) by Th8
.= (r * (seq1 . n)) * (seq2 . n)
.= ((r (#) seq1) . n) * (seq2 . n) by Th9
.= ((r (#) seq1) (#) seq2) . n by Th8 ; :: thesis: verum

end;

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