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 increasing sequence of NAT such that
A2: a = h * I by VALUED_0:def 17;
for n being Nat holds not a . n = 0 by A2, SEQ_1:5;
then A3: a is non-zero by SEQ_1:5;
A4: 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 A4, A3, FDIFF_1:def 1; :: thesis: verum