let X1, X2, A, B be set ; :: thesis: for F1 being SetSequence of X1
for F2 being SetSequence of X2
for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds
lim F = [:A,B:]
let F1 be SetSequence of X1; :: thesis: for F2 being SetSequence of X2
for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds
lim F = [:A,B:]
let F2 be SetSequence of X2; :: thesis: for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds
lim F = [:A,B:]
let F be SetSequence of [:X1,X2:]; :: thesis: ( F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) implies lim F = [:A,B:] )
assume that
A1: F1 is non-descending and
A2: lim F1 = A and
A3: F2 is non-descending and
A4: lim F2 = B and
A5: for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ; :: thesis: lim F = [:A,B:]

now :: thesis: for n being Nat holds F . n c= F . (n + 1)

let n be Nat; :: thesis: F . n c= F . (n + 1)
( F . n = [:(F1 . n),(F2 . n):] & F . (n + 1) = [:(F1 . (n + 1)),(F2 . (n + 1)):] ) by A5;
hence F . n c= F . (n + 1) by A1, A3, Th4; :: thesis: verum

end;

then F is non-descending by PROB_2:7;
then A6: lim F = Union F by SETLIM_1:63;
( Union F1 = A & Union F2 = B ) by A1, A2, A3, A4, SETLIM_1:63;
then A8: ( union (rng F1) = A & union (rng F2) = B ) by CARD_3:def 4;
then A7: [:A,B:] = union { [:P,Q:] where P is Element of rng F1, Q is Element of rng F2 : ( P in rng F1 & Q in rng F2 ) } by LATTICE5:2;

now :: thesis: for z being object st z in [:A,B:] holds
z in union (rng F)

let z be object ; :: thesis: ( z in [:A,B:] implies z in union (rng F) )
assume z in [:A,B:] ; :: thesis: z in union (rng F)
then consider Z being set such that
X1: ( z in Z & Z in { [:A,B:] where A is Element of rng F1, B is Element of rng F2 : ( A in rng F1 & B in rng F2 ) } ) by A7, TARSKI:def 4;
consider A being Element of rng F1, B being Element of rng F2 such that
X2: ( Z = [:A,B:] & A in rng F1 & B in rng F2 ) by X1;
consider n1 being Element of NAT such that
X3: ( n1 in dom F1 & A = F1 . n1 ) by PARTFUN1:3;
consider n2 being Element of NAT such that
X4: ( n2 in dom F2 & B = F2 . n2 ) by PARTFUN1:3;
set n = max (n1,n2);
( A c= F1 . (max (n1,n2)) & B c= F2 . (max (n1,n2)) ) by A1, A3, X3, X4, PROB_1:def 5, XXREAL_0:25;
then X5: Z c= [:(F1 . (max (n1,n2))),(F2 . (max (n1,n2))):] by X2, ZFMISC_1:96;
max (n1,n2) in NAT ;
then max (n1,n2) in dom F by FUNCT_2:def 1;
then F . (max (n1,n2)) in rng F by FUNCT_1:3;
then [:(F1 . (max (n1,n2))),(F2 . (max (n1,n2))):] in rng F by A5;
hence z in union (rng F) by X1, X5, TARSKI:def 4; :: thesis: verum

end;

then X6: [:A,B:] c= union (rng F) ;

now :: thesis: for z being object st z in union (rng F) holds
z in [:A,B:]

let z be object ; :: thesis: ( z in union (rng F) implies z in [:A,B:] )
assume z in union (rng F) ; :: thesis: z in [:A,B:]
then consider Z being set such that
Y1: ( z in Z & Z in rng F ) by TARSKI:def 4;
consider n being Element of NAT such that
Y2: ( n in dom F & Z = F . n ) by Y1, PARTFUN1:3;
Y3: Z = [:(F1 . n),(F2 . n):] by A5, Y2;
( dom F1 = NAT & dom F2 = NAT ) by FUNCT_2:def 1;
then ( F1 . n c= union (rng F1) & F2 . n c= union (rng F2) ) by FUNCT_1:3, ZFMISC_1:74;
then Z c= [:A,B:] by A8, Y3, ZFMISC_1:96;
hence z in [:A,B:] by Y1; :: thesis: verum

end;

then union (rng F) c= [:A,B:] ;
hence lim F = [:A,B:] by A6, X6, CARD_3:def 4; :: thesis: verum