theorem :: SEQ_1:53

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