let seq9, seq be Real_Sequence; :: thesis: ( seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-empty 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-empty ; :: thesis: lim (seq9 /" seq) = (lim seq9) / (lim seq)
seq " is convergent by A2, A3, A4, Th35;
then lim (seq9 (#) (seq ")) = (lim seq9) * (lim (seq ")) by A1, Th29
.= (lim seq9) * ((lim seq) ") by A2, A3, A4, Th36
.= (lim seq9) / (lim seq) by XCMPLX_0:def 9 ;
hence lim (seq9 /" seq) = (lim seq9) / (lim seq) ; :: thesis: verum