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 & lim s <> 0c & s is non-zero ) ; :: thesis: s' /" s is convergent
s " is convergent by A2, Th34;
hence s' /" s is convergent by A1, Th29; :: thesis: verum