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
then consider I being V36() sequence of NAT such that
A2: a = h * I by VALUED_0:def 17;
A3: h is non-empty by FDIFF_1:def 1;

now

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

end;

then A5: a is non-empty by SEQ_1:7;
A6: h is convergent by FDIFF_1:def 1;
then A7: a is convergent by A1, SEQ_4:29;
lim h = 0 by FDIFF_1:def 1;
then lim a = 0 by A1, A6, SEQ_4:30;
hence a is convergent_to_0 Real_Sequence by A7, A5, FDIFF_1:def 1; :: thesis: verum