let A, B, C be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds A . i c= B . i ) & C is subsequence of A implies ex D being subsequence of B st
for i being Nat holds C . i c= D . i )
assume that
A1: for i being Nat holds A . i c= B . i and
A2: C is subsequence of A ; :: thesis: ex D being subsequence of B st
for i being Nat holds C . i c= D . i
consider NS being increasing sequence of NAT such that
A3: C = A * NS by A2, VALUED_0:def 17;
set D = B * NS;
reconsider D = B * NS as SetSequence of (TOP-REAL 2) ;
reconsider D = D as subsequence of B ;
take D ; :: thesis: for i being Nat holds C . i c= D . i
for i being Nat holds C . i c= D . i

proof

let i be Nat; :: thesis: C . i c= D . i
A4: dom NS = NAT by FUNCT_2:def 1;
C . i c= D . i

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C . i or x in D . i )
A5: i in NAT by ORDINAL1:def 12;
assume x in C . i ; :: thesis: x in D . i
then A6: x in A . (NS . i) by A3, A4, FUNCT_1:13, A5;
A . (NS . i) c= B . (NS . i) by A1;
then x in B . (NS . i) by A6;
hence x in D . i by A4, FUNCT_1:13, A5; :: thesis: verum

end;

hence C . i c= D . i ; :: thesis: verum

end;

hence for i being Nat holds C . i c= D . i ; :: thesis: verum