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 B implies ex D being subsequence of A st
for i being Nat holds D . i c= C . i )
assume that
A1: for i being 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 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 Nat holds D . i c= C . i
for i being Nat holds D . i c= C . i
proof
let i be 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in D . i or x in C . i )
A5: i in NAT by ORDINAL1:def 12;
assume x in D . i ; :: thesis: x in C . i
then A6: x in A . (NS . i) by 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 C . i by A3, A4, FUNCT_1:13, A5; :: thesis: verum
end;
hence D . i c= C . i ; :: thesis: verum
end;
hence for i being Nat holds D . i c= C . i ; :: thesis: verum