let M be Cardinal; :: thesis:
defpred S₁[ set ] 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 set holds
( x in X iff ( x in PFuncs ([:M,M:],M) & S₁[x] ) ) from XBOOLE_0:sch 1();
A2: for x being set st x in X holds
x is Function

proof

let x be set ; :: thesis:
assume x in X ; :: thesis:
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:

end;

A3: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X

proof

let Z be set ; :: thesis:
assume that
Z <> {} and
A4: Z c= X and
A5: Z is c=-linear ; :: thesis:
( union Z is Relation-like & union Z is Function-like )

proof

set F = union Z;
thus for x being set st x in union Z holds
ex y1, y2 being set st [y1,y2] = x :: according to RELAT_1:def 1 :: thesis:

proof

let x be set ; :: thesis:
assume x in union Z ; :: thesis:
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 set st x in f holds
ex y1, y2 being set st [y1,y2] = x by RELAT_1:def 1;
hence ex y1, y2 being set st [y1,y2] = x by A6; :: thesis:

end;

let x be set ; :: according to FUNCT_1:def 1 :: thesis:
let y1, y2 be set ; :: thesis:
assume [x,y1] in union Z ; :: thesis:
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:
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 ) by XBOOLE_0:def 9;
then ( ( [x,y2] in X1 & ( for x, y1, y2 being set st [x,y1] in f1 & [x,y2] in f1 holds
y1 = y2 ) ) or ( [x,y1] in X2 & ( for x, y1, y2 being set 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:

end;

then reconsider f = union Z as Function ;
A12: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A13: x1 in dom f and
A14: x2 in dom f ; :: thesis:
[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 ) by XBOOLE_0:def 9;
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, FUNCT_1:def 4; :: thesis:

end;

A23: dom f = [:(rng f),(rng f):]

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in dom f ; :: thesis:
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:

end;

let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis:
assume A29: [x1,x2] in [:(rng f),(rng f):] ; :: thesis:
then A30: [x1,x2] = [([x1,x2] `1),([x1,x2] `2)] by MCART_1:21;
[x1,x2] `1 in rng f by A29, MCART_1:10;
then consider y1 being set such that
A31: ( 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 set such that
A32: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by FUNCT_1:def 3;
[y2,([x1,x2] `2)] in f by A32, FUNCT_1:1;
then consider X2 being set such that
A33: [y2,([x1,x2] `2)] in X2 and
A34: X2 in Z by TARSKI:def 4;
consider f2 being Function such that
A35: f2 = X2 and
f2 is one-to-one and
A36: dom f2 = [:(rng f2),(rng f2):] by A1, A4, A34;
f2 c= f by A34, A35, ZFMISC_1:74;
then A37: dom f2 c= dom f by RELAT_1:11;
[y1,([x1,x2] `1)] in f by A31, FUNCT_1:1;
then consider X1 being set such that
A38: [y1,([x1,x2] `1)] in X1 and
A39: X1 in Z by TARSKI:def 4;
consider f1 being Function such that
A40: f1 = X1 and
f1 is one-to-one and
A41: dom f1 = [:(rng f1),(rng f1):] by A1, A4, A39;
X1,X2 are_c=-comparable by A5, A39, A34, ORDINAL1:def 8;
then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9;
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 A38, A33, A40, A35, 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 A42: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A30, A41, A36, ZFMISC_1:87;
f1 c= f by A39, A40, ZFMISC_1:74;
then dom f1 c= dom f by RELAT_1:11;
hence [x1,x2] in dom f by A42, A37; :: thesis:

end;

A43: rng f c= M

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A44: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
[x,y] in union Z by A44, FUNCT_1:def 2;
then consider Y being set such that
A45: [x,y] in Y and
A46: Y in Z by TARSKI:def 4;
Y in PFuncs ([:M,M:],M) by A1, A4, A46;
then consider g being Function such that
A47: Y = g and
dom g c= [:M,M:] and
A48: rng g c= M by PARTFUN1:def 3;
( x in dom g & g . x = y ) by A45, A47, FUNCT_1:1;
then y in rng g by FUNCT_1:def 3;
hence y in M by A48; :: thesis:

end;

dom f c= [:M,M:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in dom f ; :: thesis:
then [x,(f . x)] in union Z by FUNCT_1:def 2;
then consider Y being set such that
A49: [x,(f . x)] in Y and
A50: Y in Z by TARSKI:def 4;
Y in PFuncs ([:M,M:],M) by A1, A4, A50;
then consider g being Function such that
A51: Y = g and
A52: dom g c= [:M,M:] and
rng g c= M by PARTFUN1:def 3;
x in dom g by A49, A51, FUNCT_1:1;
hence x in [:M,M:] by A52; :: thesis:

end;

then f in PFuncs ([:M,M:],M) by A43, PARTFUN1:def 3;
hence union Z in X by A1, A12, A23; :: thesis:

end;

consider f being Function such that
A53: f is one-to-one and
A54: ( dom f = [:omega,omega:] & rng f = omega ) by Th53, WELLORD2:def 4;
assume A55: not M is finite ; :: thesis:
then not M in omega ;
then A56: 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 A54, A56, PARTFUN1:def 3;
then X <> {} by A1, A53, A54;
then consider Y being set such that
A57: Y in X and
A58: 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
A59: f = Y and
A60: f is one-to-one and
A61: dom f = [:(rng f),(rng f):] by A1, A57;
set A = rng f;
A62: [:(rng f),(rng f):], rng f are_equipotent by A60, A61, WELLORD2:def 4;
Y in PFuncs ([:M,M:],M) by A1, A57;
then A63: 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);
A64: card M = M by CARD_1:def 2;
then A65: card (rng f) c= M by A59, A63, CARD_1:11;

A66: now

proof

rng f misses rng g by A80, XBOOLE_1:79;
then A86: (rng f) /\ (rng g) = {} by XBOOLE_0:def 7;
let x be set ; :: according to FUNCT_1:def 4 :: thesis:
let y be set ; :: thesis:
assume that
A87: x in dom (g +* f) and
A88: y in dom (g +* f) ; :: thesis:
A89: ( y in dom g or y in dom f ) by A81, A88, XBOOLE_0:def 3;
( x in dom f or x in dom g ) by A81, A87, 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 A60, A78, A83, A89, FUNCT_1:def 3, FUNCT_1:def 4, FUNCT_4:13, FUNCT_4:16;
hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A86, XBOOLE_0:def 4; :: thesis:

end;

set x = the Element of omega \ (rng f);
omega \ (rng f) <> {} by A74, A75, CARD_1:68, CARD_3:42;
then A90: ( the Element of omega \ (rng f) in omega & not the Element of omega \ (rng f) in rng f ) by XBOOLE_0:def 5;
A91: omega \/ (rng f) c= M by A56, A59, A63, 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 A84, A82, A91, PARTFUN1:def 3;
then g +* f in X by A1, A84, A82, A85;
then g +* f = f by A58, A59, FUNCT_4:25;
hence contradiction by A84, A90, XBOOLE_0:def 3; :: thesis:

end;

A92: now

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis:
let y be set ; :: thesis:
assume that
A110: x in dom (g +* f) and
A111: y in dom (g +* f) ; :: thesis:
A112: ( y in dom g or y in dom f ) by A106, A111, XBOOLE_0:def 3;
( x in dom f or x in dom g ) by A106, A110, XBOOLE_0:def 3;
then A113: ( ( (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 A60, A61, A103, A104, A108, A112, FUNCT_1:def 3, FUNCT_1:def 4, FUNCT_4:13, FUNCT_4:16;
( rng f misses M \ (rng f) & (rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) ) by A97, XBOOLE_1:26, XBOOLE_1:79;
then A114: (rng f) /\ (rng g) c= {} by A105, XBOOLE_0:def 7;
assume (g +* f) . x = (g +* f) . y ; :: thesis:
hence x = y by A114, A113, XBOOLE_0:def 4; :: thesis:

end;

set x = the Element of rng h;
A115: rng h <> {} by A66, A98;
then the Element of rng h in M \ (rng f) by A97, TARSKI:def 3;
then A116: not the Element of rng h in rng f by XBOOLE_0:def 5;
g c= g +* f by A61, A104, 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 A117: (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 A118: rng (g +* f) = (rng g) \/ (rng f) by A117, XBOOLE_0:def 10;
rng h c= M by A97, XBOOLE_1:1;
then A119: (rng f) \/ (rng h) c= M by A59, A63, 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 A105, A118, A107, A119, PARTFUN1:def 3;
then A120: g +* f in X by A1, A105, A118, A107, A109;
the Element of rng h in rng (g +* f) by A105, A118, A115, XBOOLE_0:def 3;
hence contradiction by A58, A59, A120, A116, FUNCT_4:25; :: thesis:

end;

then M *` M = card [:(card (rng f)),(card (rng f)):] by CARD_2:def 2
.= card [:(rng f),(rng f):] by CARD_2:7 ;
hence M *` M = M by A92, A62, CARD_1:5; :: thesis: