set Z = x (#) y;
defpred S₁[ set ] means ex p, r being set st $1 = [p,r];

A1: now

consider B being set such that
A2: for o being set holds
( o in B iff ( o in y & S₁[o] ) ) from XBOOLE_0:sch 1();
for o being set st o in B holds
o in y by A2;
then B c= y by TARSKI:def 3;
then A3: B in V by CLASSES1:def 1;
consider A being set such that
A4: for o being set holds
( o in A iff ( o in x & S₁[o] ) ) from XBOOLE_0:sch 1();
ex g being Function st
( dom g = [:A,B:] & x (#) y c= rng g )

proof

deffunc H₁( set ) -> set = [(($1 `1) `1),(($1 `2) `2)];
consider g being Function such that
A5: ( dom g = [:A,B:] & ( for o being set st o in [:A,B:] holds
g . o = H₁(o) ) ) from FUNCT_1:sch 3();
take g ; :: thesis: ( dom g = [:A,B:] & x (#) y c= rng g )
thus dom g = [:A,B:] by A5; :: thesis: x (#) y c= rng g
thus x (#) y c= rng g :: thesis: verum

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in x (#) y or o in rng g )
assume o in x (#) y ; :: thesis: o in rng g
then consider p, q, r being set such that
A6: o = [p,r] and
A7: ( [p,q] in x & [q,r] in y ) by Def1;
set s = [[p,q],[q,r]];
( [p,q] in A & [q,r] in B ) by A4, A2, A7;
then A8: [[p,q],[q,r]] in [:A,B:] by ZFMISC_1:def 2;
then g . [[p,q],[q,r]] = [(([[p,q],[q,r]] `1) `1),(([[p,q],[q,r]] `2) `2)] by A5
.= [([p,q] `1),(([[p,q],[q,r]] `2) `2)] by MCART_1:7
.= [([p,q] `1),([q,r] `2)] by MCART_1:7
.= [p,([q,r] `2)] by MCART_1:7
.= o by A6, MCART_1:7 ;
hence o in rng g by A5, A8, FUNCT_1:def 3; :: thesis: verum

end;

end;

then A9: card (x (#) y) c= card [:A,B:] by CARD_1:12;
for o being set st o in A holds
o in x by A4;
then A c= x by TARSKI:def 3;
then A in V by CLASSES1:def 1;
then [:A,B:] in V by A3, CLASSES2:61;
then card [:A,B:] in card V by CLASSES2:1;
hence card (x (#) y) in card V by A9, ORDINAL1:12; :: thesis: verum

end;

x (#) y c= V

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in x (#) y or o in V )
assume o in x (#) y ; :: thesis: o in V
then consider q, r, s being set such that
A10: o = [q,s] and
A11: [q,r] in x and
A12: [r,s] in y by Def1;
y c= V by ORDINAL1:def 2;
then {{r,s},{r}} c= V by A12, ORDINAL1:def 2;
then {r,s} in V by ZFMISC_1:32;
then {r,s} c= V by ORDINAL1:def 2;
then A13: s in V by ZFMISC_1:32;
x c= V by ORDINAL1:def 2;
then {{q,r},{q}} c= V by A11, ORDINAL1:def 2;
then {q} in V by ZFMISC_1:32;
then {q} c= V by ORDINAL1:def 2;
then q in V by ZFMISC_1:31;
hence o in V by A10, A13, CLASSES2:58; :: thesis: verum

end;

hence x (#) y is Element of V by A1, CLASSES1:1; :: thesis: verum