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 Th12
.= ((lim s') / (lim s)) *' by A1, Th39
.= ((lim s') *' ) / ((lim s) *' ) by COMPLEX1:123 ;
:: thesis: verum