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 that
A1: s9 is convergent and
A2: ( s is convergent & lim s <> 0c & s is non-zero ) ; :: thesis: lim (s9 /" s) = (lim s9) / (lim s)
s " is convergent by A2, Th23;
then lim (s9 (#) (s ")) = (lim s9) * (lim (s ")) by A1, Th20
.= (lim s9) * ((lim s) ") by A2, Th24
.= (lim s9) / (lim s) by XCMPLX_0:def 9 ;
hence lim (s9 /" s) = (lim s9) / (lim s) ; :: thesis: verum