theorem Th5: :: SEQ_1:5

for seq being Real_Sequence holds
( seq is non-zero iff for n being Nat holds seq . n <> 0 )