let X1, X2 be 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):] ) )
let S1 be 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):] ) )
let S2 be 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):] ) )
let S be 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):] ) )
let H be FinSequence of S; ( S = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } implies 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):] ) ) )
assume AS:
S = { [:A,B:] where A is Element of S1, B is Element of S2 : verum }
; 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):] ) )
A1:
for k being Nat st k in dom H holds
ex A being Element of S1 ex B being Element of S2 st H . k = [:A,B:]
defpred S1[ Nat, set ] means ex B being Element of S2 st H . $1 = [:$2,B:];
Seg (len H) = dom H
by FINSEQ_1:def 3;
then A3:
for k being Nat st k in Seg (len H) holds
ex A being Element of S1 st S1[k,A]
by A1;
consider F being FinSequence of S1 such that
A4:
( dom F = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S1[k,F . k] ) )
from FINSEQ_1:sch 5(A3);
defpred S2[ Nat, set ] means ex A being Element of S1 st H . $1 = [:A,$2:];
A5:
for k being Nat st k in Seg (len H) holds
ex B being Element of S2 st S2[k,B]
consider G being FinSequence of S2 such that
A6:
( dom G = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S2[k,G . k] ) )
from FINSEQ_1:sch 5(A5);
take
F
; 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):] ) )
take
G
; ( 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):] ) )
thus
( len H = len F & len H = len G )
by A4, A6, FINSEQ_1:def 3; for k being Nat st k in dom H & H . k <> {} holds
H . k = [:(F . k),(G . k):]