let s', s be Complex_Sequence; :: thesis: ( s' is convergent & s is convergent & lim s <> 0c & s is non-zero implies lim (s' /" s) = (lim s') / (lim s) )
assume that
A1: s' is convergent and
A2: s is convergent and
A3: lim s <> 0c and
A4: s is non-zero ; :: thesis: lim (s' /" s) = (lim s') / (lim s)
s " is convergent by A2, A3, A4, Th34;
then lim (s' (#) (s " )) = (lim s') * (lim (s " )) by A1, Th30
.= (lim s') * ((lim s) " ) by A2, A3, A4, Th35
.= (lim s') / (lim s) by XCMPLX_0:def 9 ;
hence lim (s' /" s) = (lim s') / (lim s) ; :: thesis: verum