let M be Cardinal; :: thesis: ( not M is finite implies M *` M = M )

defpred S_{1}[ object ] means ex f being Function st

( f = $1 & f is one-to-one & dom f = [:(rng f),(rng f):] );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in PFuncs ([:M,M:],M) & S_{1}[x] ) )
from XBOOLE_0:sch 1();

A2: for x being set st x in X holds

x is Function

union Z in X

A52: f is one-to-one and

A53: ( dom f = [:omega,omega:] & rng f = omega ) by Th5;

assume A54: not M is finite ; :: thesis: M *` M = M

then not M in omega ;

then A55: omega c= M by CARD_1:4;

then [:omega,omega:] c= [:M,M:] by ZFMISC_1:96;

then f in PFuncs ([:M,M:],M) by A53, A55, PARTFUN1:def 3;

then X <> {} by A1, A52, A53;

then consider Y being set such that

A56: Y in X and

A57: for Z being set st Z in X & Z <> Y holds

not Y c= Z by A3, ORDERS_1:67;

consider f being Function such that

A58: f = Y and

A59: f is one-to-one and

A60: dom f = [:(rng f),(rng f):] by A1, A56;

set A = rng f;

A61: [:(rng f),(rng f):], rng f are_equipotent by A59, A60;

Y in PFuncs ([:M,M:],M) by A1, A56;

then A62: ex f being Function st

( Y = f & dom f c= [:M,M:] & rng f c= M ) by PARTFUN1:def 3;

set N = card (rng f);

A63: card M = M ;

then A64: card (rng f) c= M by A58, A62, CARD_1:11;

.= card [:(rng f),(rng f):] by CARD_2:7 ;

hence M *` M = M by A91, A61, CARD_1:5; :: thesis: verum

defpred S

( f = $1 & f is one-to-one & dom f = [:(rng f),(rng f):] );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in PFuncs ([:M,M:],M) & S

A2: for x being set st x in X holds

x is Function

proof

A3:
for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
let x be set ; :: thesis: ( x in X implies x is Function )

assume x in X ; :: thesis: x is Function

then ex f being Function st

( f = x & f is one-to-one & dom f = [:(rng f),(rng f):] ) by A1;

hence x is Function ; :: thesis: verum

end;assume x in X ; :: thesis: x is Function

then ex f being Function st

( f = x & f is one-to-one & dom f = [:(rng f),(rng f):] ) by A1;

hence x is Function ; :: thesis: verum

union Z in X

proof

consider f being Function such that
let Z be set ; :: thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )

assume that

Z <> {} and

A4: Z c= X and

A5: Z is c=-linear ; :: thesis: union Z in X

( union Z is Relation-like & union Z is Function-like )

A12: f is one-to-one

hence union Z in X by A1, A12, A23; :: thesis: verum

end;assume that

Z <> {} and

A4: Z c= X and

A5: Z is c=-linear ; :: thesis: union Z in X

( union Z is Relation-like & union Z is Function-like )

proof

then reconsider f = union Z as Function ;
set F = union Z;

thus for x being object st x in union Z holds

ex y1, y2 being object st [y1,y2] = x :: according to RELAT_1:def 1 :: thesis: union Z is Function-like

assume [x,y1] in union Z ; :: thesis: ( not [x,y2] in union Z or y1 = y2 )

then consider X1 being set such that

A8: [x,y1] in X1 and

A9: X1 in Z by TARSKI:def 4;

assume [x,y2] in union Z ; :: thesis: y1 = y2

then consider X2 being set such that

A10: [x,y2] in X2 and

A11: X2 in Z by TARSKI:def 4;

reconsider f1 = X1, f2 = X2 as Function by A2, A4, A9, A11;

X1,X2 are_c=-comparable by A5, A9, A11, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( [x,y2] in X1 & ( for x, y1, y2 being object st [x,y1] in f1 & [x,y2] in f1 holds

y1 = y2 ) ) or ( [x,y1] in X2 & ( for x, y1, y2 being object st [x,y1] in f2 & [x,y2] in f2 holds

y1 = y2 ) ) ) by A8, A10, FUNCT_1:def 1;

hence y1 = y2 by A8, A10; :: thesis: verum

end;thus for x being object st x in union Z holds

ex y1, y2 being object st [y1,y2] = x :: according to RELAT_1:def 1 :: thesis: union Z is Function-like

proof

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in union Z or not [x,y2] in union Z or y1 = y2 )
let x be object ; :: thesis: ( x in union Z implies ex y1, y2 being object st [y1,y2] = x )

assume x in union Z ; :: thesis: ex y1, y2 being object st [y1,y2] = x

then consider Y being set such that

A6: x in Y and

A7: Y in Z by TARSKI:def 4;

reconsider f = Y as Function by A2, A4, A7;

for x being object st x in f holds

ex y1, y2 being object st [y1,y2] = x by RELAT_1:def 1;

hence ex y1, y2 being object st [y1,y2] = x by A6; :: thesis: verum

end;assume x in union Z ; :: thesis: ex y1, y2 being object st [y1,y2] = x

then consider Y being set such that

A6: x in Y and

A7: Y in Z by TARSKI:def 4;

reconsider f = Y as Function by A2, A4, A7;

for x being object st x in f holds

ex y1, y2 being object st [y1,y2] = x by RELAT_1:def 1;

hence ex y1, y2 being object st [y1,y2] = x by A6; :: thesis: verum

assume [x,y1] in union Z ; :: thesis: ( not [x,y2] in union Z or y1 = y2 )

then consider X1 being set such that

A8: [x,y1] in X1 and

A9: X1 in Z by TARSKI:def 4;

assume [x,y2] in union Z ; :: thesis: y1 = y2

then consider X2 being set such that

A10: [x,y2] in X2 and

A11: X2 in Z by TARSKI:def 4;

reconsider f1 = X1, f2 = X2 as Function by A2, A4, A9, A11;

X1,X2 are_c=-comparable by A5, A9, A11, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( [x,y2] in X1 & ( for x, y1, y2 being object st [x,y1] in f1 & [x,y2] in f1 holds

y1 = y2 ) ) or ( [x,y1] in X2 & ( for x, y1, y2 being object st [x,y1] in f2 & [x,y2] in f2 holds

y1 = y2 ) ) ) by A8, A10, FUNCT_1:def 1;

hence y1 = y2 by A8, A10; :: thesis: verum

A12: f is one-to-one

proof

A23:
dom f = [:(rng f),(rng f):]
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A13: x1 in dom f and

A14: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )

[x1,(f . x1)] in f by A13, FUNCT_1:1;

then consider X1 being set such that

A15: [x1,(f . x1)] in X1 and

A16: X1 in Z by TARSKI:def 4;

[x2,(f . x2)] in f by A14, FUNCT_1:1;

then consider X2 being set such that

A17: [x2,(f . x2)] in X2 and

A18: X2 in Z by TARSKI:def 4;

consider f2 being Function such that

A19: f2 = X2 and

A20: f2 is one-to-one and

dom f2 = [:(rng f2),(rng f2):] by A1, A4, A18;

consider f1 being Function such that

A21: f1 = X1 and

A22: f1 is one-to-one and

dom f1 = [:(rng f1),(rng f1):] by A1, A4, A16;

X1,X2 are_c=-comparable by A5, A16, A18, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( x1 in dom f1 & x2 in dom f1 & f . x1 = f1 . x1 & f . x2 = f1 . x2 ) or ( x1 in dom f2 & x2 in dom f2 & f . x1 = f2 . x1 & f . x2 = f2 . x2 ) ) by A15, A17, A21, A19, FUNCT_1:1;

hence ( not f . x1 = f . x2 or x1 = x2 ) by A22, A20; :: thesis: verum

end;assume that

A13: x1 in dom f and

A14: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )

[x1,(f . x1)] in f by A13, FUNCT_1:1;

then consider X1 being set such that

A15: [x1,(f . x1)] in X1 and

A16: X1 in Z by TARSKI:def 4;

[x2,(f . x2)] in f by A14, FUNCT_1:1;

then consider X2 being set such that

A17: [x2,(f . x2)] in X2 and

A18: X2 in Z by TARSKI:def 4;

consider f2 being Function such that

A19: f2 = X2 and

A20: f2 is one-to-one and

dom f2 = [:(rng f2),(rng f2):] by A1, A4, A18;

consider f1 being Function such that

A21: f1 = X1 and

A22: f1 is one-to-one and

dom f1 = [:(rng f1),(rng f1):] by A1, A4, A16;

X1,X2 are_c=-comparable by A5, A16, A18, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( x1 in dom f1 & x2 in dom f1 & f . x1 = f1 . x1 & f . x2 = f1 . x2 ) or ( x1 in dom f2 & x2 in dom f2 & f . x1 = f2 . x1 & f . x2 = f2 . x2 ) ) by A15, A17, A21, A19, FUNCT_1:1;

hence ( not f . x1 = f . x2 or x1 = x2 ) by A22, A20; :: thesis: verum

proof

A42:
rng f c= M
thus
dom f c= [:(rng f),(rng f):]
:: according to XBOOLE_0:def 10 :: thesis: [:(rng f),(rng f):] c= dom f

assume A29: [x1,x2] in [:(rng f),(rng f):] ; :: thesis: [x1,x2] in dom f

[x1,x2] `1 in rng f by A29, MCART_1:10;

then consider y1 being object such that

A30: ( y1 in dom f & [x1,x2] `1 = f . y1 ) by FUNCT_1:def 3;

[x1,x2] `2 in rng f by A29, MCART_1:10;

then consider y2 being object such that

A31: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by FUNCT_1:def 3;

[y2,([x1,x2] `2)] in f by A31, FUNCT_1:1;

then consider X2 being set such that

A32: [y2,([x1,x2] `2)] in X2 and

A33: X2 in Z by TARSKI:def 4;

consider f2 being Function such that

A34: f2 = X2 and

f2 is one-to-one and

A35: dom f2 = [:(rng f2),(rng f2):] by A1, A4, A33;

f2 c= f by A33, A34, ZFMISC_1:74;

then A36: dom f2 c= dom f by RELAT_1:11;

[y1,([x1,x2] `1)] in f by A30, FUNCT_1:1;

then consider X1 being set such that

A37: [y1,([x1,x2] `1)] in X1 and

A38: X1 in Z by TARSKI:def 4;

consider f1 being Function such that

A39: f1 = X1 and

f1 is one-to-one and

A40: dom f1 = [:(rng f1),(rng f1):] by A1, A4, A38;

X1,X2 are_c=-comparable by A5, A38, A33, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( y1 in dom f1 & y2 in dom f1 & f1 . y1 = [x1,x2] `1 & f1 . y2 = [x1,x2] `2 ) or ( y1 in dom f2 & y2 in dom f2 & f2 . y1 = [x1,x2] `1 & f2 . y2 = [x1,x2] `2 ) ) by A37, A32, A39, A34, FUNCT_1:1;

then ( ( [x1,x2] `1 in rng f1 & [x1,x2] `2 in rng f1 ) or ( [x1,x2] `1 in rng f2 & [x1,x2] `2 in rng f2 ) ) by FUNCT_1:def 3;

then A41: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A40, A35, ZFMISC_1:87;

f1 c= f by A38, A39, ZFMISC_1:74;

then dom f1 c= dom f by RELAT_1:11;

hence [x1,x2] in dom f by A41, A36; :: thesis: verum

end;proof

let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in [:(rng f),(rng f):] or [x1,x2] in dom f )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in [:(rng f),(rng f):] )

assume x in dom f ; :: thesis: x in [:(rng f),(rng f):]

then [x,(f . x)] in f by FUNCT_1:def 2;

then consider Y being set such that

A24: [x,(f . x)] in Y and

A25: Y in Z by TARSKI:def 4;

consider g being Function such that

A26: g = Y and

g is one-to-one and

A27: dom g = [:(rng g),(rng g):] by A1, A4, A25;

g c= f by A25, A26, ZFMISC_1:74;

then rng g c= rng f by RELAT_1:11;

then A28: dom g c= [:(rng f),(rng f):] by A27, ZFMISC_1:96;

x in dom g by A24, A26, FUNCT_1:1;

hence x in [:(rng f),(rng f):] by A28; :: thesis: verum

end;assume x in dom f ; :: thesis: x in [:(rng f),(rng f):]

then [x,(f . x)] in f by FUNCT_1:def 2;

then consider Y being set such that

A24: [x,(f . x)] in Y and

A25: Y in Z by TARSKI:def 4;

consider g being Function such that

A26: g = Y and

g is one-to-one and

A27: dom g = [:(rng g),(rng g):] by A1, A4, A25;

g c= f by A25, A26, ZFMISC_1:74;

then rng g c= rng f by RELAT_1:11;

then A28: dom g c= [:(rng f),(rng f):] by A27, ZFMISC_1:96;

x in dom g by A24, A26, FUNCT_1:1;

hence x in [:(rng f),(rng f):] by A28; :: thesis: verum

assume A29: [x1,x2] in [:(rng f),(rng f):] ; :: thesis: [x1,x2] in dom f

[x1,x2] `1 in rng f by A29, MCART_1:10;

then consider y1 being object such that

A30: ( y1 in dom f & [x1,x2] `1 = f . y1 ) by FUNCT_1:def 3;

[x1,x2] `2 in rng f by A29, MCART_1:10;

then consider y2 being object such that

A31: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by FUNCT_1:def 3;

[y2,([x1,x2] `2)] in f by A31, FUNCT_1:1;

then consider X2 being set such that

A32: [y2,([x1,x2] `2)] in X2 and

A33: X2 in Z by TARSKI:def 4;

consider f2 being Function such that

A34: f2 = X2 and

f2 is one-to-one and

A35: dom f2 = [:(rng f2),(rng f2):] by A1, A4, A33;

f2 c= f by A33, A34, ZFMISC_1:74;

then A36: dom f2 c= dom f by RELAT_1:11;

[y1,([x1,x2] `1)] in f by A30, FUNCT_1:1;

then consider X1 being set such that

A37: [y1,([x1,x2] `1)] in X1 and

A38: X1 in Z by TARSKI:def 4;

consider f1 being Function such that

A39: f1 = X1 and

f1 is one-to-one and

A40: dom f1 = [:(rng f1),(rng f1):] by A1, A4, A38;

X1,X2 are_c=-comparable by A5, A38, A33, ORDINAL1:def 8;

then ( X1 c= X2 or X2 c= X1 ) ;

then ( ( y1 in dom f1 & y2 in dom f1 & f1 . y1 = [x1,x2] `1 & f1 . y2 = [x1,x2] `2 ) or ( y1 in dom f2 & y2 in dom f2 & f2 . y1 = [x1,x2] `1 & f2 . y2 = [x1,x2] `2 ) ) by A37, A32, A39, A34, FUNCT_1:1;

then ( ( [x1,x2] `1 in rng f1 & [x1,x2] `2 in rng f1 ) or ( [x1,x2] `1 in rng f2 & [x1,x2] `2 in rng f2 ) ) by FUNCT_1:def 3;

then A41: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A40, A35, ZFMISC_1:87;

f1 c= f by A38, A39, ZFMISC_1:74;

then dom f1 c= dom f by RELAT_1:11;

hence [x1,x2] in dom f by A41, A36; :: thesis: verum

proof

dom f c= [:M,M:]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in M )

assume y in rng f ; :: thesis: y in M

then consider x being object such that

A43: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in union Z by A43, FUNCT_1:def 2;

then consider Y being set such that

A44: [x,y] in Y and

A45: Y in Z by TARSKI:def 4;

Y in PFuncs ([:M,M:],M) by A1, A4, A45;

then consider g being Function such that

A46: Y = g and

dom g c= [:M,M:] and

A47: rng g c= M by PARTFUN1:def 3;

( x in dom g & g . x = y ) by A44, A46, FUNCT_1:1;

then y in rng g by FUNCT_1:def 3;

hence y in M by A47; :: thesis: verum

end;assume y in rng f ; :: thesis: y in M

then consider x being object such that

A43: ( x in dom f & y = f . x ) by FUNCT_1:def 3;

[x,y] in union Z by A43, FUNCT_1:def 2;

then consider Y being set such that

A44: [x,y] in Y and

A45: Y in Z by TARSKI:def 4;

Y in PFuncs ([:M,M:],M) by A1, A4, A45;

then consider g being Function such that

A46: Y = g and

dom g c= [:M,M:] and

A47: rng g c= M by PARTFUN1:def 3;

( x in dom g & g . x = y ) by A44, A46, FUNCT_1:1;

then y in rng g by FUNCT_1:def 3;

hence y in M by A47; :: thesis: verum

proof

then
f in PFuncs ([:M,M:],M)
by A42, PARTFUN1:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in [:M,M:] )

assume x in dom f ; :: thesis: x in [:M,M:]

then [x,(f . x)] in union Z by FUNCT_1:def 2;

then consider Y being set such that

A48: [x,(f . x)] in Y and

A49: Y in Z by TARSKI:def 4;

Y in PFuncs ([:M,M:],M) by A1, A4, A49;

then consider g being Function such that

A50: Y = g and

A51: dom g c= [:M,M:] and

rng g c= M by PARTFUN1:def 3;

x in dom g by A48, A50, FUNCT_1:1;

hence x in [:M,M:] by A51; :: thesis: verum

end;assume x in dom f ; :: thesis: x in [:M,M:]

then [x,(f . x)] in union Z by FUNCT_1:def 2;

then consider Y being set such that

A48: [x,(f . x)] in Y and

A49: Y in Z by TARSKI:def 4;

Y in PFuncs ([:M,M:],M) by A1, A4, A49;

then consider g being Function such that

A50: Y = g and

A51: dom g c= [:M,M:] and

rng g c= M by PARTFUN1:def 3;

x in dom g by A48, A50, FUNCT_1:1;

hence x in [:M,M:] by A51; :: thesis: verum

hence union Z in X by A1, A12, A23; :: thesis: verum

A52: f is one-to-one and

A53: ( dom f = [:omega,omega:] & rng f = omega ) by Th5;

assume A54: not M is finite ; :: thesis: M *` M = M

then not M in omega ;

then A55: omega c= M by CARD_1:4;

then [:omega,omega:] c= [:M,M:] by ZFMISC_1:96;

then f in PFuncs ([:M,M:],M) by A53, A55, PARTFUN1:def 3;

then X <> {} by A1, A52, A53;

then consider Y being set such that

A56: Y in X and

A57: for Z being set st Z in X & Z <> Y holds

not Y c= Z by A3, ORDERS_1:67;

consider f being Function such that

A58: f = Y and

A59: f is one-to-one and

A60: dom f = [:(rng f),(rng f):] by A1, A56;

set A = rng f;

A61: [:(rng f),(rng f):], rng f are_equipotent by A59, A60;

Y in PFuncs ([:M,M:],M) by A1, A56;

then A62: ex f being Function st

( Y = f & dom f c= [:M,M:] & rng f c= M ) by PARTFUN1:def 3;

set N = card (rng f);

A63: card M = M ;

then A64: card (rng f) c= M by A58, A62, CARD_1:11;

A65: now :: thesis: not rng f is finite

omega \ (rng f) misses rng f
by XBOOLE_1:79;

then A66: (omega \ (rng f)) /\ (rng f) = {} ;

then [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (omega \ (rng f))):] = {} by ZFMISC_1:90;

then A67: [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (omega \ (rng f))),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(omega \ (rng f)),(rng f):] = {} by ZFMISC_1:100;

then A68: [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(omega \ (rng f)),(rng f):] ;

[:((rng f) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then A69: [:(rng f),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then A70: ( {} \/ {} = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(rng f):] = {} ) by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;

then A71: ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(rng f):] = {} by A70, XBOOLE_1:23;

A72: ( omega c= omega +` (card (rng f)) & omega +` omega = omega ) by CARD_2:75, CARD_2:94;

assume A73: rng f is finite ; :: thesis: contradiction

then card (rng f) in omega by CARD_3:42;

then omega +` (card (rng f)) c= omega +` omega by CARD_2:83;

then A74: omega = omega +` (card (rng f)) by A72;

card (rng f) = card (card (rng f)) ;

then omega *` (card (rng f)) c= omega by A73, CARD_2:89;

then A75: omega +` (omega *` (card (rng f))) = omega by CARD_2:76;

A76: omega = card (omega \ (rng f)) by A73, A74, CARD_2:98, CARD_3:42;

[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (omega \ (rng f))):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;

then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(omega \ (rng f)):] = {} \/ {} by A67, XBOOLE_1:23

.= {} ;

then [:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] ;

then card (([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):]) = (card ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by CARD_2:35

.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by A68, CARD_2:35

.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A76, CARD_2:7

.= ((card [:omega,omega:]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A76, CARD_2:7

.= (omega +` (card [:omega,(card (rng f)):])) +` (card [:(card (rng f)),omega:]) by A76, Th5, CARD_2:7

.= (omega +` (omega *` (card (rng f)))) +` (card [:(card (rng f)),omega:]) by CARD_2:def 2

.= (omega +` (omega *` (card (rng f)))) +` ((card (rng f)) *` omega) by CARD_2:def 2 ;

then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):],omega \ (rng f) are_equipotent by A76, A75, CARD_1:5;

then consider g being Function such that

A77: g is one-to-one and

A78: dom g = ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):] and

A79: rng g = omega \ (rng f) ;

A80: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1;

then A81: dom (g +* f) = ([:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),(omega \ (rng f)):]) \/ [:(rng f),(rng f):] by A60, A78, ZFMISC_1:97

.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ ([:(rng f),(omega \ (rng f)):] \/ [:(rng f),(rng f):]) by XBOOLE_1:4

.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97

.= [:((omega \ (rng f)) \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97

.= [:(omega \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by XBOOLE_1:39

.= [:(omega \/ (rng f)),(omega \/ (rng f)):] by XBOOLE_1:39 ;

{} \/ {} = {} ;

then (dom g) /\ (dom f) = {} by A60, A78, A71, A69, XBOOLE_1:23;

then A82: dom g misses dom f ;

then g c= g +* f by FUNCT_4:32;

then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;

then ( rng (g +* f) c= (rng g) \/ (rng f) & (rng g) \/ (rng f) c= rng (g +* f) ) by FUNCT_4:17, XBOOLE_1:8;

then A83: rng (g +* f) = (rng g) \/ (rng f)

.= omega \/ (rng f) by A79, XBOOLE_1:39 ;

A84: g +* f is one-to-one

omega \ (rng f) <> {} by A73, A74, CARD_1:68, CARD_3:42;

then A89: ( the Element of omega \ (rng f) in omega & not the Element of omega \ (rng f) in rng f ) by XBOOLE_0:def 5;

A90: omega \/ (rng f) c= M by A55, A58, A62, XBOOLE_1:8;

then [:(omega \/ (rng f)),(omega \/ (rng f)):] c= [:M,M:] by ZFMISC_1:96;

then g +* f in PFuncs ([:M,M:],M) by A83, A81, A90, PARTFUN1:def 3;

then g +* f in X by A1, A83, A81, A84;

then g +* f = f by A57, A58, FUNCT_4:25;

hence contradiction by A83, A89, XBOOLE_0:def 3; :: thesis: verum

end;then A66: (omega \ (rng f)) /\ (rng f) = {} ;

then [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (omega \ (rng f))):] = {} by ZFMISC_1:90;

then A67: [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (omega \ (rng f))),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(omega \ (rng f)),(rng f):] = {} by ZFMISC_1:100;

then A68: [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(omega \ (rng f)),(rng f):] ;

[:((rng f) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then A69: [:(rng f),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then A70: ( {} \/ {} = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(rng f):] = {} ) by ZFMISC_1:100;

[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} by ZFMISC_1:100;

then A71: ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(rng f):] = {} by A70, XBOOLE_1:23;

A72: ( omega c= omega +` (card (rng f)) & omega +` omega = omega ) by CARD_2:75, CARD_2:94;

assume A73: rng f is finite ; :: thesis: contradiction

then card (rng f) in omega by CARD_3:42;

then omega +` (card (rng f)) c= omega +` omega by CARD_2:83;

then A74: omega = omega +` (card (rng f)) by A72;

card (rng f) = card (card (rng f)) ;

then omega *` (card (rng f)) c= omega by A73, CARD_2:89;

then A75: omega +` (omega *` (card (rng f))) = omega by CARD_2:76;

A76: omega = card (omega \ (rng f)) by A73, A74, CARD_2:98, CARD_3:42;

[:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (omega \ (rng f))):] = {} by A66, ZFMISC_1:90;

then [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(omega \ (rng f)):] = {} by ZFMISC_1:100;

then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(omega \ (rng f)):] = {} \/ {} by A67, XBOOLE_1:23

.= {} ;

then [:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] ;

then card (([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):]) = (card ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by CARD_2:35

.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by A68, CARD_2:35

.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A76, CARD_2:7

.= ((card [:omega,omega:]) +` (card [:omega,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A76, CARD_2:7

.= (omega +` (card [:omega,(card (rng f)):])) +` (card [:(card (rng f)),omega:]) by A76, Th5, CARD_2:7

.= (omega +` (omega *` (card (rng f)))) +` (card [:(card (rng f)),omega:]) by CARD_2:def 2

.= (omega +` (omega *` (card (rng f)))) +` ((card (rng f)) *` omega) by CARD_2:def 2 ;

then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):],omega \ (rng f) are_equipotent by A76, A75, CARD_1:5;

then consider g being Function such that

A77: g is one-to-one and

A78: dom g = ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):] and

A79: rng g = omega \ (rng f) ;

A80: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1;

then A81: dom (g +* f) = ([:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),(omega \ (rng f)):]) \/ [:(rng f),(rng f):] by A60, A78, ZFMISC_1:97

.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ ([:(rng f),(omega \ (rng f)):] \/ [:(rng f),(rng f):]) by XBOOLE_1:4

.= [:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97

.= [:((omega \ (rng f)) \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:97

.= [:(omega \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by XBOOLE_1:39

.= [:(omega \/ (rng f)),(omega \/ (rng f)):] by XBOOLE_1:39 ;

{} \/ {} = {} ;

then (dom g) /\ (dom f) = {} by A60, A78, A71, A69, XBOOLE_1:23;

then A82: dom g misses dom f ;

then g c= g +* f by FUNCT_4:32;

then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;

then ( rng (g +* f) c= (rng g) \/ (rng f) & (rng g) \/ (rng f) c= rng (g +* f) ) by FUNCT_4:17, XBOOLE_1:8;

then A83: rng (g +* f) = (rng g) \/ (rng f)

.= omega \/ (rng f) by A79, XBOOLE_1:39 ;

A84: g +* f is one-to-one

proof

set x = the Element of omega \ (rng f);
rng f misses rng g
by A79, XBOOLE_1:79;

then A85: (rng f) /\ (rng g) = {} ;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y )

assume that

A86: x in dom (g +* f) and

A87: y in dom (g +* f) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )

A88: ( y in dom g or y in dom f ) by A80, A87, XBOOLE_0:def 3;

( x in dom f or x in dom g ) by A80, A86, XBOOLE_0:def 3;

then ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A59, A77, A82, A88, FUNCT_1:def 3, FUNCT_4:13, FUNCT_4:16;

hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A85, XBOOLE_0:def 4; :: thesis: verum

end;then A85: (rng f) /\ (rng g) = {} ;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y )

assume that

A86: x in dom (g +* f) and

A87: y in dom (g +* f) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )

A88: ( y in dom g or y in dom f ) by A80, A87, XBOOLE_0:def 3;

( x in dom f or x in dom g ) by A80, A86, XBOOLE_0:def 3;

then ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A59, A77, A82, A88, FUNCT_1:def 3, FUNCT_4:13, FUNCT_4:16;

hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A85, XBOOLE_0:def 4; :: thesis: verum

omega \ (rng f) <> {} by A73, A74, CARD_1:68, CARD_3:42;

then A89: ( the Element of omega \ (rng f) in omega & not the Element of omega \ (rng f) in rng f ) by XBOOLE_0:def 5;

A90: omega \/ (rng f) c= M by A55, A58, A62, XBOOLE_1:8;

then [:(omega \/ (rng f)),(omega \/ (rng f)):] c= [:M,M:] by ZFMISC_1:96;

then g +* f in PFuncs ([:M,M:],M) by A83, A81, A90, PARTFUN1:def 3;

then g +* f in X by A1, A83, A81, A84;

then g +* f = f by A57, A58, FUNCT_4:25;

hence contradiction by A83, A89, XBOOLE_0:def 3; :: thesis: verum

A91: now :: thesis: not card (rng f) <> M

then M *` M =
card [:(card (rng f)),(card (rng f)):]
by CARD_2:def 2
(card (rng f)) *` (card (rng f)) = card [:(card (rng f)),(card (rng f)):]
by CARD_2:def 2;

then A92: (card (rng f)) *` (card (rng f)) = card [:(rng f),(rng f):] by CARD_2:7;

[:(rng f),(rng f):], rng f are_equipotent by A59, A60;

then A93: (card (rng f)) *` (card (rng f)) = card (rng f) by A92, CARD_1:5;

assume card (rng f) <> M ; :: thesis: contradiction

then A94: card (rng f) in M by A64, CARD_1:3;

M +` (card (rng f)) = M by A54, A64, CARD_2:76;

then card (M \ (rng f)) = M by A63, A94, CARD_2:98;

then consider h being Function such that

A95: ( h is one-to-one & dom h = rng f ) and

A96: rng h c= M \ (rng f) by A64, CARD_1:10;

set B = rng h;

rng f, rng h are_equipotent by A95;

then A97: card (rng f) = card (rng h) by CARD_1:5;

( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A96, XBOOLE_1:26, XBOOLE_1:79;

then (rng f) /\ (rng h) c= {} ;

then (rng f) /\ (rng h) = {} ;

then A98: rng f misses rng h ;

((rng f) \/ (rng h)) \ (rng f) = (rng h) \ (rng f) by XBOOLE_1:40

.= rng h by A98, XBOOLE_1:83 ;

then A99: [:(rng h),(rng h):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] by ZFMISC_1:96;

( [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] & [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] = [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] ) by XBOOLE_1:7, ZFMISC_1:103;

then A100: [:(rng h),(rng h):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] by A99;

(card (rng f)) +` (card (rng f)) = card (rng f) by A65, CARD_2:75;

then card ((rng f) \/ (rng h)) = card (rng f) by A97, A98, CARD_2:35;

then card [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] = card [:(card (rng f)),(card (rng f)):] by CARD_2:7

.= card (rng f) by A93, CARD_2:def 2 ;

then A101: card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) c= card (rng f) by CARD_1:11;

card (rng f) = card [:(card (rng f)),(card (rng f)):] by A93, CARD_2:def 2;

then card (rng f) = card [:(rng h),(rng h):] by A97, CARD_2:7;

then card (rng f) c= card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) by A100, CARD_1:11;

then card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) = card (rng f) by A101;

then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):], rng h are_equipotent by A97, CARD_1:5;

then consider g being Function such that

A102: g is one-to-one and

A103: dom g = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] and

A104: rng g = rng h ;

A105: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1;

then ( rng f c= (rng f) \/ (rng h) & dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \/ [:(rng f),(rng f):] ) by A60, A103, XBOOLE_1:7, XBOOLE_1:39;

then A106: dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] by XBOOLE_1:12, ZFMISC_1:96;

A107: [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] misses [:(rng f),(rng f):] by XBOOLE_1:79;

A108: g +* f is one-to-one

A114: rng h <> {} by A65, A97;

then the Element of rng h in M \ (rng f) by A96;

then A115: not the Element of rng h in rng f by XBOOLE_0:def 5;

g c= g +* f by A60, A103, FUNCT_4:32, XBOOLE_1:79;

then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;

then A116: (rng g) \/ (rng f) c= rng (g +* f) by XBOOLE_1:8;

rng (g +* f) c= (rng g) \/ (rng f) by FUNCT_4:17;

then A117: rng (g +* f) = (rng g) \/ (rng f) by A116;

rng h c= M by A96, XBOOLE_1:1;

then A118: (rng f) \/ (rng h) c= M by A58, A62, XBOOLE_1:8;

then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] c= [:M,M:] by ZFMISC_1:96;

then g +* f in PFuncs ([:M,M:],M) by A104, A117, A106, A118, PARTFUN1:def 3;

then A119: g +* f in X by A1, A104, A117, A106, A108;

the Element of rng h in rng (g +* f) by A104, A117, A114, XBOOLE_0:def 3;

hence contradiction by A57, A58, A119, A115, FUNCT_4:25; :: thesis: verum

end;then A92: (card (rng f)) *` (card (rng f)) = card [:(rng f),(rng f):] by CARD_2:7;

[:(rng f),(rng f):], rng f are_equipotent by A59, A60;

then A93: (card (rng f)) *` (card (rng f)) = card (rng f) by A92, CARD_1:5;

assume card (rng f) <> M ; :: thesis: contradiction

then A94: card (rng f) in M by A64, CARD_1:3;

M +` (card (rng f)) = M by A54, A64, CARD_2:76;

then card (M \ (rng f)) = M by A63, A94, CARD_2:98;

then consider h being Function such that

A95: ( h is one-to-one & dom h = rng f ) and

A96: rng h c= M \ (rng f) by A64, CARD_1:10;

set B = rng h;

rng f, rng h are_equipotent by A95;

then A97: card (rng f) = card (rng h) by CARD_1:5;

( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A96, XBOOLE_1:26, XBOOLE_1:79;

then (rng f) /\ (rng h) c= {} ;

then (rng f) /\ (rng h) = {} ;

then A98: rng f misses rng h ;

((rng f) \/ (rng h)) \ (rng f) = (rng h) \ (rng f) by XBOOLE_1:40

.= rng h by A98, XBOOLE_1:83 ;

then A99: [:(rng h),(rng h):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] by ZFMISC_1:96;

( [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] c= [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] & [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] = [:(((rng f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] ) by XBOOLE_1:7, ZFMISC_1:103;

then A100: [:(rng h),(rng h):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] by A99;

(card (rng f)) +` (card (rng f)) = card (rng f) by A65, CARD_2:75;

then card ((rng f) \/ (rng h)) = card (rng f) by A97, A98, CARD_2:35;

then card [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] = card [:(card (rng f)),(card (rng f)):] by CARD_2:7

.= card (rng f) by A93, CARD_2:def 2 ;

then A101: card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) c= card (rng f) by CARD_1:11;

card (rng f) = card [:(card (rng f)),(card (rng f)):] by A93, CARD_2:def 2;

then card (rng f) = card [:(rng h),(rng h):] by A97, CARD_2:7;

then card (rng f) c= card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) by A100, CARD_1:11;

then card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) = card (rng f) by A101;

then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):], rng h are_equipotent by A97, CARD_1:5;

then consider g being Function such that

A102: g is one-to-one and

A103: dom g = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] and

A104: rng g = rng h ;

A105: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1;

then ( rng f c= (rng f) \/ (rng h) & dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \/ [:(rng f),(rng f):] ) by A60, A103, XBOOLE_1:7, XBOOLE_1:39;

then A106: dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] by XBOOLE_1:12, ZFMISC_1:96;

A107: [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] misses [:(rng f),(rng f):] by XBOOLE_1:79;

A108: g +* f is one-to-one

proof

set x = the Element of rng h;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (g +* f) or not y in dom (g +* f) or not (g +* f) . x = (g +* f) . y or x = y )

assume that

A109: x in dom (g +* f) and

A110: y in dom (g +* f) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )

A111: ( y in dom g or y in dom f ) by A105, A110, XBOOLE_0:def 3;

( x in dom f or x in dom g ) by A105, A109, XBOOLE_0:def 3;

then A112: ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A59, A60, A102, A103, A107, A111, FUNCT_1:def 3, FUNCT_4:13, FUNCT_4:16;

( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A96, XBOOLE_1:26, XBOOLE_1:79;

then A113: (rng f) /\ (rng g) c= {} by A104;

assume (g +* f) . x = (g +* f) . y ; :: thesis: x = y

hence x = y by A113, A112, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A109: x in dom (g +* f) and

A110: y in dom (g +* f) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )

A111: ( y in dom g or y in dom f ) by A105, A110, XBOOLE_0:def 3;

( x in dom f or x in dom g ) by A105, A109, XBOOLE_0:def 3;

then A112: ( ( (g +* f) . x = f . x & (g +* f) . y = f . y & ( f . x = f . y implies x = y ) ) or ( (g +* f) . x = g . x & (g +* f) . y = g . y & ( g . x = g . y implies x = y ) ) or ( (g +* f) . x = f . x & (g +* f) . y = g . y & f . x in rng f & g . y in rng g ) or ( (g +* f) . x = g . x & (g +* f) . y = f . y & g . x in rng g & f . y in rng f ) ) by A59, A60, A102, A103, A107, A111, FUNCT_1:def 3, FUNCT_4:13, FUNCT_4:16;

( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A96, XBOOLE_1:26, XBOOLE_1:79;

then A113: (rng f) /\ (rng g) c= {} by A104;

assume (g +* f) . x = (g +* f) . y ; :: thesis: x = y

hence x = y by A113, A112, XBOOLE_0:def 4; :: thesis: verum

A114: rng h <> {} by A65, A97;

then the Element of rng h in M \ (rng f) by A96;

then A115: not the Element of rng h in rng f by XBOOLE_0:def 5;

g c= g +* f by A60, A103, FUNCT_4:32, XBOOLE_1:79;

then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:18, RELAT_1:11;

then A116: (rng g) \/ (rng f) c= rng (g +* f) by XBOOLE_1:8;

rng (g +* f) c= (rng g) \/ (rng f) by FUNCT_4:17;

then A117: rng (g +* f) = (rng g) \/ (rng f) by A116;

rng h c= M by A96, XBOOLE_1:1;

then A118: (rng f) \/ (rng h) c= M by A58, A62, XBOOLE_1:8;

then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] c= [:M,M:] by ZFMISC_1:96;

then g +* f in PFuncs ([:M,M:],M) by A104, A117, A106, A118, PARTFUN1:def 3;

then A119: g +* f in X by A1, A104, A117, A106, A108;

the Element of rng h in rng (g +* f) by A104, A117, A114, XBOOLE_0:def 3;

hence contradiction by A57, A58, A119, A115, FUNCT_4:25; :: thesis: verum

.= card [:(rng f),(rng f):] by CARD_2:7 ;

hence M *` M = M by A91, A61, CARD_1:5; :: thesis: verum