let a be Real_Sequence; :: thesis: for h being non-zero 0 -convergent Real_Sequence st a is subsequence of h holds
a is non-zero 0 -convergent Real_Sequence
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( a is subsequence of h implies a is non-zero 0 -convergent Real_Sequence )
assume A1: a is subsequence of h ; :: thesis: a is non-zero 0 -convergent Real_Sequence
then consider I being V37() sequence of NAT such that
A2: a = h * I by VALUED_0:def 17;

now :: thesis: for n being Element of NAT holds not a . n = 0

given n being Element of NAT such that A4: a . n = 0 ; :: thesis: contradiction
h . (I . n) <> 0 by SEQ_1:5;
hence contradiction by A2, A4, FUNCT_2:15; :: thesis: verum

end;

then A5: a is non-zero by SEQ_1:5;
A7: a is convergent by A1, SEQ_4:16;
lim h = 0 ;
then lim a = 0 by A1, SEQ_4:17;
hence a is non-zero 0 -convergent Real_Sequence by A7, A5, FDIFF_1:def 1; :: thesis: verum