let M be Cardinal; :: thesis:
defpred S₁[ 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₁[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 object st x in union Z holds
ex y1, y2 being object st [y1,y2] = x :: according to RELAT_1:def 1 :: thesis:

proof

let x be object ; :: 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 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:

end;

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: 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 ) ;
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:

end;

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

proof

let x1, x2 be object ; :: 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 ) ;
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:

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 object ; :: 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 object ; :: according to RELAT_1:def 3 :: thesis:
assume A29: [x1,x2] in [:(rng f),(rng f):] ; :: thesis:
[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:

end;

A42: rng f c= M

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
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:

end;

dom f c= [:M,M:]

proof

let x be object ; :: 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
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:

end;

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

end;

consider f being Function such that
A52: f is one-to-one and
A53: ( dom f = [:omega,omega:] & rng f = omega ) by Th5;
assume A54: not M is finite ; :: thesis:
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:

proof

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:
assume that
A86: x in dom (g +* f) and
A87: y in dom (g +* f) ; :: thesis:
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:

end;

set x = the Element of omega \ (rng f);
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:

end;

A91: now :: thesis:

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A109: x in dom (g +* f) and
A110: y in dom (g +* f) ; :: thesis:
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:
hence x = y by A113, A112, XBOOLE_0:def 4; :: thesis:

end;

set x = the Element of rng h;
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:

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 A91, A61, CARD_1:5; :: thesis: