let seq, seq9 be Real_Sequence; :: thesis: ( seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies lim (seq9 /" seq) = (lim seq9) / (lim seq) )
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: lim seq <> 0 and
A4: seq is non-zero ; :: thesis: lim (seq9 /" seq) = (lim seq9) / (lim seq)
seq " is convergent by A2, A3, A4, Th21;
then lim (seq9 (#) (seq ")) = (lim seq9) * (lim (seq ")) by A1, Th15
.= (lim seq9) * ((lim seq) ") by A2, A3, A4, Th22
.= (lim seq9) / (lim seq) by XCMPLX_0:def 9 ;
hence lim (seq9 /" seq) = (lim seq9) / (lim seq) ; :: thesis: verum