let r be Element of COMPLEX ; :: thesis: for s being Complex_Sequence st s is convergent holds
lim ((r (#) s) *' ) = (r *' ) * ((lim s) *' )
let s be Complex_Sequence; :: thesis: ( s is convergent implies lim ((r (#) s) *' ) = (r *' ) * ((lim s) *' ) )
assume A1: s is convergent ; :: thesis: lim ((r (#) s) *' ) = (r *' ) * ((lim s) *' )
hence lim ((r (#) s) *' ) = (lim (r (#) s)) *' by Th12
.= (r * (lim s)) *' by A1, Th18
.= (r *' ) * ((lim s) *' ) by COMPLEX1:121 ;
:: thesis: verum