let X, Y be set ; :: thesis: for A being SetSequence of X
for B being SetSequence of Y
for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let A be SetSequence of X; :: thesis: for B being SetSequence of Y
for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let B be SetSequence of Y; :: thesis: for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let C be SetSequence of [:X,Y:]; :: thesis: ( A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) implies ( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] ) )
assume that
A1: A is non-descending and
A2: B is non-descending and
A3: for n being Nat holds C . n = [:(A . n),(B . n):] ; :: thesis: ( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
for n, m being Nat st n <= m holds
C . n c= C . m

proof

let n, m be Nat; :: thesis: ( n <= m implies C . n c= C . m )
assume n <= m ; :: thesis: C . n c= C . m
then ( A . n c= A . m & B . n c= B . m ) by A1, A2, PROB_1:def 5;
then [:(A . n),(B . n):] c= [:(A . m),(B . m):] by ZFMISC_1:96;
then C . n c= [:(A . m),(B . m):] by A3;
hence C . n c= C . m by A3; :: thesis: verum

end;

hence C is non-descending by PROB_1:def 5; :: thesis: ( C is convergent & Union C = [:(Union A),(Union B):] )
hence C is convergent by SETLIM_1:63; :: thesis: Union C = [:(Union A),(Union B):]

now :: thesis: for z being set st z in [:(Union A),(Union B):] holds
z in Union C

let z be set ; :: thesis: ( z in [:(Union A),(Union B):] implies z in Union C )
assume z in [:(Union A),(Union B):] ; :: thesis: z in Union C
then consider x, y being object such that
A6: ( x in Union A & y in Union B & z = [x,y] ) by ZFMISC_1:def 2;
A7: ( x in union (rng A) & y in union (rng B) ) by A6, CARD_3:def 4;
then consider A1 being set such that
A8: ( x in A1 & A1 in rng A ) by TARSKI:def 4;
consider n being object such that
A9: ( n in dom A & A1 = A . n ) by A8, FUNCT_1:def 3;
reconsider n = n as Nat by A9;
consider B1 being set such that
A10: ( y in B1 & B1 in rng B ) by A7, TARSKI:def 4;
consider m being object such that
A11: ( m in dom B & B1 = B . m ) by A10, FUNCT_1:def 3;
reconsider m = m as Nat by A11;
reconsider N = max (n,m) as Element of NAT by ORDINAL1:def 12;
( A . n c= A . N & B . m c= B . N ) by A1, A2, XXREAL_0:25, PROB_1:def 5;
then z in [:(A . N),(B . N):] by A6, A8, A9, A10, A11, ZFMISC_1:def 2;
then ( z in C . N & C . N in rng C ) by A3, FUNCT_2:112;
then z in union (rng C) by TARSKI:def 4;
hence z in Union C by CARD_3:def 4; :: thesis: verum

end;

then A12: [:(Union A),(Union B):] c= Union C ;

now :: thesis: for z being set st z in Union C holds
z in [:(Union A),(Union B):]

let z be set ; :: thesis: ( z in Union C implies z in [:(Union A),(Union B):] )
assume z in Union C ; :: thesis: z in [:(Union A),(Union B):]
then z in union (rng C) by CARD_3:def 4;
then consider C1 being set such that
A13: ( z in C1 & C1 in rng C ) by TARSKI:def 4;
consider n being object such that
A14: ( n in dom C & C1 = C . n ) by A13, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A14;
z in [:(A . n),(B . n):] by A3, A13, A14;
then consider x, y being object such that
A15: ( x in A . n & y in B . n & z = [x,y] ) by ZFMISC_1:def 2;
( A . n in rng A & B . n in rng B ) by FUNCT_2:112;
then ( x in union (rng A) & y in union (rng B) ) by A15, TARSKI:def 4;
then ( x in Union A & y in Union B ) by CARD_3:def 4;
hence z in [:(Union A),(Union B):] by A15, ZFMISC_1:def 2; :: thesis: verum

end;

then Union C c= [:(Union A),(Union B):] ;
hence Union C = [:(Union A),(Union B):] by A12; :: thesis: verum