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

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