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