theorem Th4: :: SEQ_1:4

for seq being Real_Sequence holds
( seq is non-zero iff for x being object st x in NAT holds
seq . x <> 0 )