theorem :: MEASUR11:19

for X1, X2, A, B being set
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:]