let X1, X2 be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: 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; :: thesis: ( 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 } ; :: thesis: 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:]
proof
let k be Nat; :: thesis: ( k in dom H implies ex A being Element of S1 ex B being Element of S2 st H . k = [:A,B:] )
assume A2: k in dom H ; :: thesis: ex A being Element of S1 ex B being Element of S2 st H . k = [:A,B:]
H /. k in S ;
then H . k in S by A2, PARTFUN1:def 6;
hence ex A being Element of S1 ex B being Element of S2 st H . k = [:A,B:] by AS; :: thesis: verum
end;
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]
proof
let k be Nat; :: thesis: ( k in Seg (len H) implies ex B being Element of S2 st S2[k,B] )
assume k in Seg (len H) ; :: thesis: ex B being Element of S2 st S2[k,B]
then k in dom H by FINSEQ_1:def 3;
then ex A being Element of S1 ex B being Element of S2 st H . k = [:A,B:] by A1;
hence ex B being Element of S2 st S2[k,B] ; :: thesis: verum
end;
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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: for k being Nat st k in dom H & H . k <> {} holds
H . k = [:(F . k),(G . k):]
hereby :: thesis: verum
let k be Nat; :: thesis: ( k in dom H & H . k <> {} implies H . k = [:(F . k),(G . k):] )
assume A8: ( k in dom H & H . k <> {} ) ; :: thesis: H . k = [:(F . k),(G . k):]
then A9: k in Seg (len H) by FINSEQ_1:def 3;
then consider B being Element of S2 such that
A10: H . k = [:(F . k),B:] by A4;
consider A being Element of S1 such that
A11: H . k = [:A,(G . k):] by A9, A6;
( F . k <> {} & B <> {} ) by A8, A10;
hence H . k = [:(F . k),(G . k):] by A10, A11, ZFMISC_1:110; :: thesis: verum
end;