for a being Real_Sequence
for h being non-zero 0 -convergent Real_Sequence st a is subsequence of h holds
a is non-zero 0 -convergent Real_Sequence