theorem :: MEASUR10:23

for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2
for S being non empty Subset-Family of [:X1,X2:]
for H being FinSequence of S st S = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } holds
ex F being FinSequence of S1 ex G being FinSequence of S2 st
( len H = len F & len H = len G & ( for k being Nat st k in dom H & H . k <> {} holds
H . k = [:(F . k),(G . k):] ) )