let r be Element of COMPLEX ; :: thesis: for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
let seq be Complex_Sequence; :: thesis: (r (#) seq) " = (r ") (#) (seq ")

now

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:205
.= (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:113; :: thesis: verum