let A, B, C be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Element of NAT holds A . i c= B . i ) & C is subsequence of A implies ex D being subsequence of B st
for i being Element of NAT holds C . i c= D . i )
assume that
A1: for i being Element of 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 Element of 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 Element of NAT holds C . i c= D . i
for i being Element of NAT holds C . i c= D . i

proof

let i be Element of 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in C . i or x in D . i )
assume x in C . i ; :: thesis: x in D . i
then A5: x in A . (NS . i) by A3, A4, FUNCT_1:13;
A . (NS . i) c= B . (NS . i) by A1;
then x in B . (NS . i) by A5;
hence x in D . i by A4, FUNCT_1:13; :: thesis: verum

end;

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

end;

hence for i being Element of NAT holds C . i c= D . i ; :: thesis: verum