let s, s9 be Complex_Sequence; :: thesis: ( s is convergent & s9 is convergent implies lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).| )
assume A1: ( s is convergent & s9 is convergent ) ; :: thesis: lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|
then s (#) s9 is convergent by Th29;
hence lim |.(s (#) s9).| = |.(lim (s (#) s9)).| by Th11
.= |.((lim s) * (lim s9)).| by A1, Th30
.= |.(lim s).| * |.(lim s9).| by COMPLEX1:151 ;
:: thesis: verum