let seq, seq9 be Real_Sequence; :: thesis: ( seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies seq9 /" seq is convergent )
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: lim seq <> 0 and
A4: seq is non-zero ; :: thesis: seq9 /" seq is convergent
seq " is convergent by A2, A3, A4, Th21;
hence seq9 /" seq is convergent by A1; :: thesis: verum