let s', s be Complex_Sequence; :: thesis: ( s' is convergent & s is convergent & lim s <> 0c & s is non-zero implies s' /" s is convergent )
assume that
A1: s' is convergent and
A2: s is convergent and
A3: lim s <> 0c and
A4: s is non-zero ; :: thesis: s' /" s is convergent
s " is convergent by A2, A3, A4, Th34;
hence s' /" s is convergent by A1, Th29; :: thesis: verum