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;

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 )
;

end;

suppose A2:
X c= dom R
; :: thesis: card R = (card (R | ((dom R) \ X))) +` (C *` (card X))

deffunc H_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 3();

defpred S_{1}[ 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_{1}[x,y]

A6: ( dom ff = X & ( for x being object st x in X holds

S_{1}[x,ff . x] ) )
from CLASSES1:sch 1(A4);

deffunc H_{2}( 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_{2}(x) ) )
from FUNCT_1:sch 3();

A8: rng p = [:X,C:]

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)

.= 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: verum

end;consider f being Function such that

A3: ( dom f = X & ( for x being object st x in X holds

f . x = H

defpred S

( 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

proof

consider ff being Function such that
let x be object ; :: thesis: ( x in X implies ex y being object st S_{1}[x,y] )

assume x in X ; :: thesis: ex y being object st S_{1}[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: S_{1}[x,g]

thus S_{1}[x,g]
by A5; :: thesis: verum

end;assume x in X ; :: thesis: ex y being object st S

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: S

thus S

A6: ( dom ff = X & ( for x being object st x in X holds

S

now :: thesis: for x being object st x in dom ff holds

ff . x is Function

then reconsider ff = ff as Function-yielding Function by FUNCOP_1:def 6;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;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

deffunc H

consider p being Function such that

A7: ( dom p = R | X & ( for x being object st x in R | X holds

p . x = H

A8: rng p = [:X,C:]

proof

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 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_{2}([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_{2}([y1,x2])
by A7;

hence y in rng p by A7, A26, A27, FUNCT_1:def 3; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:X,C:] c= rng p

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:X,C:] or y in 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 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: verum

end;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 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: verum

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 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

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

hence y in rng p by A7, A26, A27, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for x1, x2 being object st x1 in dom p & x2 in dom p & p . x1 = p . x2 holds

x1 = x2

then
p is one-to-one
by FUNCT_1:def 4;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 = H_{2}(x1) & p . x2 = H_{2}(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: verum

end;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 = H

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: verum

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)

proof

((dom R) \ X) \/ X =
(dom R) \/ X
by XBOOLE_1:39
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 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: verum

end;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: verum

.= 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: verum

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) = {}

dom R misses X

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: verum

end;A48: x in X and

A49: not x in dom R ;

Im (R,x) = {}

proof

then A51:
C = card {}
by A1, A48;
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 A50, RELSET_2:9;

hence contradiction by A49, XTUPLE_0:def 12; :: thesis: verum

end;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: verum

dom R misses X

proof

then A55:
(dom R) \ X = dom R
by XBOOLE_1:83;
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 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: verum

end;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: verum

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: verum