let X be set ; :: thesis: for R being Relation
for C being Cardinal st ( for x being object st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))

let R be Relation; :: thesis: for C being Cardinal st ( for x being object st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))

let C be Cardinal; :: thesis: ( ( for x being object st x in X holds
card (Im (R,x)) = C ) implies card R = (card (R | ((dom R) \ X))) +` (C *` (card X)) )

assume A1: for x being object st x in X holds
card (Im (R,x)) = C ; :: thesis: card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
set DA = (dom R) \ X;
per cases ( X c= dom R or not X c= dom R ) ;
suppose A2: X c= dom R ; :: thesis: card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
deffunc H1( 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 = H1(x) ) ) from defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in X implies ex y being object st S1[x,y] )
assume x in X ; :: thesis: ex y being object st S1[x,y]
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: S1[x,g]
thus S1[x,g] by A5; :: thesis: verum
end;
consider ff being Function such that
A6: ( dom ff = X & ( for x being object st x in X holds
S1[x,ff . x] ) ) from
now :: thesis: for x being object st x in dom ff holds
ff . x is Function
let x be object ; :: thesis: ( x in dom ff implies ff . x is Function )
assume x in dom ff ; :: thesis: ff . x is Function
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: verum
end;
then reconsider ff = ff as Function-yielding Function by FUNCOP_1:def 6;
deffunc H2( 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 = H2(x) ) ) from A8: rng p = [:X,C:]
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:X,C:] c= rng p
let y be object ; :: thesis: ( y in rng p implies y in [:X,C:] )
assume y in rng p ; :: thesis: y in [:X,C:]
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 ;
then ( x `1 in {(x `1)} & x in R ) by ;
then A13: x `2 in R .: {(x `1)} by ;
A14: x `1 in X by ;
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 ;
then x `2 in dom g by ;
then g . (x `2) in C by ;
hence y in [:X,C:] by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:X,C:] or y in rng p )
assume y in [:X,C:] ; :: thesis: y in rng p
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 ;
consider x2 being object such that
A24: x2 in dom g and
A25: g . x2 = y2 by ;
A26: H2([y1,x2]) = y by ;
f . y1 = Im (R,y1) by ;
then [y1,x2] in R by ;
then A27: [y1,x2] in R | X by ;
then p . [y1,x2] = H2([y1,x2]) by A7;
hence y in rng p by ; :: thesis: verum
end;
now :: thesis: for x1, x2 being object st x1 in dom p & x2 in dom p & p . x1 = p . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 )
assume that
A28: x1 in dom p and
A29: x2 in dom p and
A30: p . x1 = p . x2 ; :: thesis: x1 = x2
A31: ( p . x1 = H2(x1) & p . x2 = H2(x2) ) by A7, A28, A29;
then A32: x1 `1 = x2 `1 by ;
A33: x1 = [(x1 `1),(x1 `2)] by ;
then x1 in R by ;
then A34: x1 `2 in Im (R,(x1 `1)) by ;
A35: x2 = [(x2 `1),(x2 `2)] by ;
then x2 in R by ;
then A36: x2 `2 in Im (R,(x2 `1)) by ;
x2 `1 in X by ;
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 ;
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 ;
g1 . (x1 `2) = g2 . (x2 `2) by ;
hence x1 = x2 by ; :: thesis: verum
end;
then p is one-to-one by FUNCT_1:def 4;
then R | X,[:X,C:] are_equipotent by ;
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)
proof
assume R | X meets R | ((dom R) \ X) ; :: thesis: contradiction
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 ;
( x1 in X & x1 in (dom R) \ X ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
((dom R) \ X) \/ X = (dom R) \/ X by XBOOLE_1:39
.= dom R by ;
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 ; :: thesis: verum
end;
suppose not X c= dom R ; :: thesis: card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
then consider x being object such that
A48: x in X and
A49: not x in dom R ;
Im (R,x) = {}
proof
assume Im (R,x) <> {} ; :: thesis: contradiction
then consider y being object such that
A50: y in Im (R,x) by XBOOLE_0:def 1;
[x,y] in R by ;
hence contradiction by A49, XTUPLE_0:def 12; :: thesis: verum
end;
then A51: C = card {} by ;
dom R misses X
proof
assume dom R meets X ; :: thesis: contradiction
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 ;
then A54: Im (R,x) is empty by A51;
ex y being object st [x,y] in R by ;
hence contradiction by A54, RELSET_2:9; :: thesis: verum
end;
then A55: (dom R) \ X = dom R by XBOOLE_1:83;
C *` (card X) = 0 by ;
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: verum
end;
end;