let A, B be SetSequence of the carrier of (TOP-REAL 2); 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):]; ( ( 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
; 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
; 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
; ( 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):]
hence
( A1 is subsequence of A & B1 is subsequence of B & ( for i being Nat holds C1 . i = [:(A1 . i),(B1 . i):] ) )
; verum