let r be real number ; :: thesis: for seq being Real_Sequence holds (r (#) seq) " = (r " ) (#) (seq " )
let seq be Real_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 Th13
.= (r " ) * ((seq . n) " ) by XCMPLX_1:205
.= (r " ) * ((seq " ) . n) by VALUED_1:10
.= ((r " ) (#) (seq " )) . n by Th13 ; :: thesis: verum

end;

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