theorem :: SEQ_1:39

for seq, seq1 being Real_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero