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