let s, s9 be Complex_Sequence; ( 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 )
; 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
;
verum