let s9, s be Complex_Sequence; :: thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-empty implies lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).| )
assume A1: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-empty ) ; :: thesis: lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).|
then s9 /" s is convergent by Th38;
hence lim |.(s9 /" s).| = |.(lim (s9 /" s)).| by Th11
.= |.((lim s9) / (lim s)).| by A1, Th39
.= |.(lim s9).| / |.(lim s).| by COMPLEX1:153 ;
:: thesis: verum