let X be set ; :: thesis:
let R be Relation; :: thesis:
let C be Cardinal; :: thesis:
assume A1: for x being object st x in X holds
card (Im (R,x)) = C ; :: thesis:
set DA = (dom R) \ X;

suppose A2: X c= dom R ; :: thesis:

deffunc H₁( object ) -> set = Im (R,$1);
consider f being Function such that
A3: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
defpred S₁[ object , object ] means ex g being Function st
( g = $2 & dom g = f . $1 & rng g = C & g is one-to-one );
A4: for x being object st x in X holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in X ; :: thesis:
then ( f . x = Im (R,x) & card (Im (R,x)) = C ) by A1, A3;
then f . x,C are_equipotent by CARD_1:def 2;
then consider g being Function such that
A5: ( g is one-to-one & dom g = f . x & rng g = C ) by WELLORD2:def 4;
take g ; :: thesis:
thus S₁[x,g] by A5; :: thesis:

end;

consider ff being Function such that
A6: ( dom ff = X & ( for x being object st x in X holds
S₁[x,ff . x] ) ) from CLASSES1:sch 1(A4);

let x be object ; :: thesis:
assume x in dom ff ; :: thesis:
then ex g being Function st
( g = ff . x & dom g = f . x & rng g = C & g is one-to-one ) by A6;
hence ff . x is Function ; :: thesis:

end;

then reconsider ff = ff as Function-yielding Function by FUNCOP_1:def 6;
deffunc H₂( object ) -> object = [($1 `1),((ff . ($1 `1)) . ($1 `2))];
consider p being Function such that
A7: ( dom p = R | X & ( for x being object st x in R | X holds
p . x = H₂(x) ) ) from FUNCT_1:sch 3();
A8: rng p = [:X,C:]

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let y be object ; :: thesis:
assume y in rng p ; :: thesis:
then consider x being object such that
A9: x in dom p and
A10: p . x = y by FUNCT_1:def 3;
A11: p . x = [(x `1),((ff . (x `1)) . (x `2))] by A7, A9;
A12: x = [(x `1),(x `2)] by A7, A9, MCART_1:21;
then ( x `1 in {(x `1)} & x in R ) by A7, A9, RELAT_1:def 11, TARSKI:def 1;
then A13: x `2 in R .: {(x `1)} by A12, RELAT_1:def 13;
A14: x `1 in X by A7, A9, A12, RELAT_1:def 11;
then consider g being Function such that
A15: g = ff . (x `1) and
A16: dom g = f . (x `1) and
A17: rng g = C and
g is one-to-one by A6;
f . (x `1) = Im (R,(x `1)) by A3, A14;
then x `2 in dom g by A13, A16, RELAT_1:def 16;
then g . (x `2) in C by A17, FUNCT_1:def 3;
hence y in [:X,C:] by A10, A11, A14, A15, ZFMISC_1:87; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in [:X,C:] ; :: thesis:
then consider y1, y2 being object such that
A18: y1 in X and
A19: y2 in C and
A20: y = [y1,y2] by ZFMISC_1:def 2;
consider g being Function such that
A21: g = ff . y1 and
A22: dom g = f . y1 and
A23: rng g = C and
g is one-to-one by A6, A18;
consider x2 being object such that
A24: x2 in dom g and
A25: g . x2 = y2 by A19, A23, FUNCT_1:def 3;
A26: H₂([y1,x2]) = y by A20, A21, A25;
f . y1 = Im (R,y1) by A3, A18;
then [y1,x2] in R by A22, A24, RELSET_2:9;
then A27: [y1,x2] in R | X by A18, RELAT_1:def 11;
then p . [y1,x2] = H₂([y1,x2]) by A7;
hence y in rng p by A7, A26, A27, FUNCT_1:def 3; :: thesis:

end;

let x1, x2 be object ; :: thesis:
assume that
A28: x1 in dom p and
A29: x2 in dom p and
A30: p . x1 = p . x2 ; :: thesis:
A31: ( p . x1 = H₂(x1) & p . x2 = H₂(x2) ) by A7, A28, A29;
then A32: x1 `1 = x2 `1 by A30, XTUPLE_0:1;
A33: x1 = [(x1 `1),(x1 `2)] by A7, A28, MCART_1:21;
then x1 in R by A7, A28, RELAT_1:def 11;
then A34: x1 `2 in Im (R,(x1 `1)) by A33, RELSET_2:9;
A35: x2 = [(x2 `1),(x2 `2)] by A7, A29, MCART_1:21;
then x2 in R by A7, A29, RELAT_1:def 11;
then A36: x2 `2 in Im (R,(x2 `1)) by A35, RELSET_2:9;
x2 `1 in X by A7, A29, A35, RELAT_1:def 11;
then consider g2 being Function such that
A37: g2 = ff . (x2 `1) and
dom g2 = f . (x2 `1) and
rng g2 = C and
g2 is one-to-one by A6;
A38: x1 `1 in X by A7, A28, A33, RELAT_1:def 11;
then consider g1 being Function such that
A39: g1 = ff . (x1 `1) and
A40: dom g1 = f . (x1 `1) and
rng g1 = C and
A41: g1 is one-to-one by A6;
A42: f . (x1 `1) = Im (R,(x1 `1)) by A3, A38;
g1 . (x1 `2) = g2 . (x2 `2) by A30, A31, A37, A39, XTUPLE_0:1;
hence x1 = x2 by A32, A35, A36, A33, A34, A37, A39, A40, A41, A42, FUNCT_1:def 4; :: thesis:

end;

then p is one-to-one by FUNCT_1:def 4;
then R | X,[:X,C:] are_equipotent by A7, A8, WELLORD2:def 4;
then A43: card (R | X) = card [:X,C:] by CARD_1:5
.= card [:(card X),C:] by CARD_2:7
.= C *` (card X) by CARD_2:def 2 ;
A44: R | X misses R | ((dom R) \ X)

assume R | X meets R | ((dom R) \ X) ; :: thesis:
then consider x being object such that
A45: x in R | X and
A46: x in R | ((dom R) \ X) by XBOOLE_0:3;
consider x1, x2 being object such that
A47: x = [x1,x2] by A45, RELAT_1:def 1;
( x1 in X & x1 in (dom R) \ X ) by A45, A46, A47, RELAT_1:def 11;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

((dom R) \ X) \/ X = (dom R) \/ X by XBOOLE_1:39
.= dom R by A2, XBOOLE_1:12 ;
then (R | X) \/ (R | ((dom R) \ X)) = R | (dom R) by RELAT_1:78
.= R ;
hence card R = (card (R | ((dom R) \ X))) +` (C *` (card X)) by A43, A44, CARD_2:35; :: thesis:

end;

suppose not X c= dom R ; :: thesis:

then consider x being object such that
A48: x in X and
A49: not x in dom R ;
Im (R,x) = {}

assume Im (R,x) <> {} ; :: thesis:
then consider y being object such that
A50: y in Im (R,x) by XBOOLE_0:def 1;
[x,y] in R by A50, RELSET_2:9;
hence contradiction by A49, XTUPLE_0:def 12; :: thesis:

end;

then A51: C = card {} by A1, A48;
dom R misses X

assume dom R meets X ; :: thesis:
then consider x being object such that
A52: x in dom R and
A53: x in X by XBOOLE_0:3;
card (Im (R,x)) = C by A1, A53;
then A54: Im (R,x) is empty by A51;
ex y being object st [x,y] in R by A52, XTUPLE_0:def 12;
hence contradiction by A54, RELSET_2:9; :: thesis:

end;

then A55: (dom R) \ X = dom R by XBOOLE_1:83;
C *` (card X) = 0 by A51, CARD_2:20;
then (card (R | ((dom R) \ X))) +` (C *` (card X)) = card (R | ((dom R) \ X)) by CARD_2:18;
hence card R = (card (R | ((dom R) \ X))) +` (C *` (card X)) by A55; :: thesis:

end;

end;