for X, Y being set
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):] )