theorem :: TOPRNS_1:22

for N being Nat
for seq being Real_Sequence of N st seq is non-zero holds
- seq is non-zero