let a, b, c, d, e, f, g, h be set ; [:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
set X1 = {a,b,c,d};
set Y1 = {e,f,g,h};
set X11 = {a,b};
set X12 = {c,d};
set Y11 = {e,f};
set Y12 = {g,h};
A1:
( [:{c,d},{e,f}:] = {[c,e],[c,f],[d,e],[d,f]} & [:{c,d},{g,h}:] = {[c,g],[c,h],[d,g],[d,h]} )
by MCART_1:23;
( {a,b,c,d} = {a,b} \/ {c,d} & {e,f,g,h} = {e,f} \/ {g,h} )
by ENUMSET1:5;
then A2:
[:{a,b,c,d},{e,f,g,h}:] = (([:{a,b},{e,f}:] \/ [:{a,b},{g,h}:]) \/ [:{c,d},{e,f}:]) \/ [:{c,d},{g,h}:]
by ZFMISC_1:98;
( [:{a,b},{e,f}:] = {[a,e],[a,f],[b,e],[b,f]} & [:{a,b},{g,h}:] = {[a,g],[a,h],[b,g],[b,h]} )
by MCART_1:23;
then [:{a,b,c,d},{e,f,g,h}:] =
({[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f]}) \/ {[c,g],[c,h],[d,g],[d,h]}
by A1, A2, ENUMSET1:25
.=
{[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ ({[c,e],[c,f],[d,e],[d,f]} \/ {[c,g],[c,h],[d,g],[d,h]})
by XBOOLE_1:4
.=
{[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
by ENUMSET1:25
;
hence
[:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
; verum