set Z = x (#) y;
defpred S1[ object ] means ex p, r being object st $1 = [p,r];
A1: now :: thesis: card (x (#) y) in card V
consider B being set such that
A2: for o being object holds
( o in B iff ( o in y & S1[o] ) ) from XBOOLE_0:sch 1();
 for o being object st o in B holds
o in y by A2;
then B c= y ;
then A3: B in V by CLASSES1:def 1;
consider A being set such that
A4: for o being object holds
( o in A iff ( o in x & S1[o] ) ) from XBOOLE_0:sch 1();
 ex g being Function st
( dom g = [:A,B:] & x (#) y c= rng g )
proof
deffunc H1( object ) -> object = [(($1 `1) `1),(($1 `2) `2)];
consider g being Function such that
A5: ( dom g = [:A,B:] & ( for o being object st o in [:A,B:] holds
g . o = H1(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 p, r be object ; :: according to RELAT_1:def 3 :: thesis: ( not [p,r] in x (#) y or [p,r] in rng g )
assume [p,r] in x (#) y ; :: thesis: [p,r] in rng g
then consider q being object such that
A6: ( [p,q] in x & [q,r] in y ) by RELAT_1:def 8;
set s = [[p,q],[q,r]];
( [p,q] in A & [q,r] in B ) by A4, A2, A6;
then A7: [[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)]
.= [([p,q] `1),([q,r] `2)]
.= [p,([q,r] `2)]
.= [p,r] ;
hence [p,r] in rng g by A5, A7, FUNCT_1:def 3; :: thesis: verum
end;
end;
then A8: card (x (#) y) c= card [:A,B:] by CARD_1:12;
for o being object st o in A holds
o in x by A4;
then A c= x ;
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 A8, ORDINAL1:12; :: thesis: verum
end;
x (#) y c= V
proof
let q, s be object ; :: according to RELAT_1:def 3 :: thesis: ( not [q,s] in x (#) y or [q,s] in V )
assume [q,s] in x (#) y ; :: thesis: [q,s] in V
then consider r being object such that
A9: [q,r] in x and
A10: [r,s] in y by RELAT_1:def 8;
y c= V by ORDINAL1:def 2;
then {{r,s},{r}} c= V by A10, ORDINAL1:def 2;
then {r,s} in V by ZFMISC_1:32;
then {r,s} c= V by ORDINAL1:def 2;
then A11: s in V by ZFMISC_1:32;
x c= V by ORDINAL1:def 2;
then {{q,r},{q}} c= V by A9, 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 [q,s] in V by A11, CLASSES2:58; :: thesis: verum
end;
hence x (#) y is Relation-like Element of V by A1, CLASSES1:1; :: thesis: verum