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