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 COMSEQ_2:38;
hence lim |.(s9 /" s).| =
|.(lim (s9 /" s)).|
by Th27
.=
|.((lim s9) / (lim s)).|
by A1, COMSEQ_2:39
.=
|.(lim s9).| / |.(lim s).|
by COMPLEX1:67
;
verum