let seq, seq1 be Complex_Sequence; :: thesis: ( seq is non-zero & seq1 is non-zero implies seq /" seq1 is non-zero )
assume that
A1: seq is non-zero and
A2: seq1 is non-zero ; :: thesis: seq /" seq1 is non-zero
seq1 " is non-zero by A2, Th27;
hence seq /" seq1 is non-zero by A1, Th28; :: thesis: verum