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 ")

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

hence
(r (#) seq) " = (r ") (#) (seq ")
by FUNCT_2:63; :: thesis: verumlet 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;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