theorem Th32: :: SEQ_1:33

for seq being Real_Sequence st seq is non-zero holds
seq " is non-zero