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

proof

let i be Nat; :: thesis: C1 . i = [:(A1 . i),(B1 . i):]
A4: i in NAT by ORDINAL1:def 12;
A5: dom NS = NAT by FUNCT_2:def 1;
then A6: ( A1 . i = A . (NS . i) & B1 . i = B . (NS . i) ) by FUNCT_1:13, A4;
C1 . i = C . (NS . i) by A3, A5, FUNCT_1:13, A4
.= [:(A1 . i),(B1 . i):] by A1, A6 ;
hence C1 . i = [:(A1 . i),(B1 . i):] ; :: thesis: verum

end;

hence ( A1 is subsequence of A & B1 is subsequence of B & ( for i being Nat holds C1 . i = [:(A1 . i),(B1 . i):] ) ) ; :: thesis: verum