let seq, seq1 be Real_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, Th32;

hence seq /" seq1 is non-zero by A1, Th33; :: thesis: verum

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, Th32;

hence seq /" seq1 is non-zero by A1, Th33; :: thesis: verum