let a be Real_Sequence; :: thesis: for h being convergent_to_0 Real_Sequence st a is subsequence of h holds
a is convergent_to_0 Real_Sequence
let h be convergent_to_0 Real_Sequence; :: thesis: ( a is subsequence of h implies a is convergent_to_0 Real_Sequence )
assume A1: a is subsequence of h ; :: thesis: a is convergent_to_0 Real_Sequence
A2: ( h is convergent & lim h = 0 & h is non-zero ) by FDIFF_1:def 1;
then A3: a is convergent by A1, SEQ_4:29;
A4: lim a = 0 by A1, A2, SEQ_4:30;
consider I being V35() sequence of NAT such that
A5: a = h * I by A1, VALUED_0:def 17;

now

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

end;

then a is non-zero by SEQ_1:7;
hence a is convergent_to_0 Real_Sequence by A3, A4, FDIFF_1:def 1; :: thesis: verum