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 B implies ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i )
assume that
A1: for i being Element of NAT holds A . i c= B . i and
A2: C is subsequence of B ; :: thesis: ex D being subsequence of A st
for i being Element of NAT holds D . i c= C . i
consider NS being increasing sequence of NAT such that
A3: C = B * NS by A2, VALUED_0:def 17;
set D = A * NS;
reconsider D = A * NS as SetSequence of (TOP-REAL 2) ;
reconsider D = D as subsequence of A ;
take D ; :: thesis: for i being Element of NAT holds D . i c= C . i
for i being Element of NAT holds D . i c= C . i

proof

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

proof

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

end;

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

end;

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