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