let s, s9 be Complex_Sequence; :: thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *') )

assume A1: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero ) ; :: thesis: lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *')

then s9 /" s is convergent by Th26;

hence lim ((s9 /" s) *') = (lim (s9 /" s)) *' by Th11

.= ((lim s9) / (lim s)) *' by A1, Th27

.= ((lim s9) *') / ((lim s) *') by COMPLEX1:37 ;

:: thesis: verum

assume A1: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero ) ; :: thesis: lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *')

then s9 /" s is convergent by Th26;

hence lim ((s9 /" s) *') = (lim (s9 /" s)) *' by Th11

.= ((lim s9) / (lim s)) *' by A1, Th27

.= ((lim s9) *') / ((lim s) *') by COMPLEX1:37 ;

:: thesis: verum