let r be Complex; :: thesis: for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *')
let s be convergent Complex_Sequence; :: thesis: lim ((r (#) s) *') = (r *') * ((lim s) *')
thus lim ((r (#) s) *') = (lim (r (#) s)) *' by Th11
.= (r * (lim s)) *' by Th14
.= (r *') * ((lim s) *') by COMPLEX1:35 ; :: thesis: verum