let r be Complex; :: thesis: for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
let seq be Complex_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 VALUED_1:6
.= (r ") * ((seq . n) ") by XCMPLX_1:204
.= (r ") * ((seq ") . n) by VALUED_1:10
.= ((r ") (#) (seq ")) . n by VALUED_1:6 ; :: thesis: verum

end;

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