let r be Real; :: thesis: for seq being Real_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
let seq be Real_Sequence; :: thesis: (r (#) seq) " = (r ") (#) (seq ")

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

let n be Element of NAT ; :: thesis: ((r (#) seq) ") . n = ((r ") (#) (seq ")) . n
thus ((r (#) seq) ") . n = ((r (#) seq) . n) " by VALUED_1:10
.= (r * (seq . n)) " by Th9
.= (r ") * ((seq . n) ") by XCMPLX_1:204
.= (r ") * ((seq ") . n) by VALUED_1:10
.= ((r ") (#) (seq ")) . n by Th9 ; :: thesis: verum

end;

hence (r (#) seq) " = (r ") (#) (seq ") by FUNCT_2:63; :: thesis: verum