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).|
then r (#) s is convergent ;
hence lim |.(r (#) s).| = |.(lim (r (#) s)).| by Th11
.= |.(r * (lim s)).| by A1, Th18
.= |.r.| * |.(lim s).| by COMPLEX1:151 ;
:: thesis: verum