let M be Cardinal; ( not M is finite implies M *` M = M )
defpred S1[ 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) & S1[x] ) )
from XBOOLE_0:sch 1();
A2:
for x being set st x in X holds
x is Function
A3:
for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X
proof
let Z be
set ;
( 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
;
union Z in X
(
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
RELAT_1:def 1 union Z is Function-like proof
let x be
object ;
( x in union Z implies ex y1, y2 being object st [y1,y2] = x )
assume
x in union Z
;
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;
verum
end;
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( not [x,y1] in union Z or not [x,y2] in union Z or y1 = y2 )
assume
[x,y1] in union Z
;
( 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
;
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;
verum
end;
then reconsider f =
union Z as
Function ;
A12:
f is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( 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
;
( 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;
verum
end;
A23:
dom f = [:(rng f),(rng f):]
proof
thus
dom f c= [:(rng f),(rng f):]
XBOOLE_0:def 10 [:(rng f),(rng f):] c= dom fproof
let x be
object ;
TARSKI:def 3 ( not x in dom f or x in [:(rng f),(rng f):] )
assume
x in dom f
;
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;
verum
end;
let x1,
x2 be
object ;
RELAT_1:def 3 ( not [x1,x2] in [:(rng f),(rng f):] or [x1,x2] in dom f )
assume A29:
[x1,x2] in [:(rng f),(rng f):]
;
[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;
verum
end;
A42:
rng f c= M
proof
let y be
object ;
TARSKI:def 3 ( not y in rng f or y in M )
assume
y in rng f
;
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;
verum
end;
dom f c= [:M,M:]
proof
let x be
object ;
TARSKI:def 3 ( not x in dom f or x in [:M,M:] )
assume
x in dom f
;
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;
verum
end;
then
f in PFuncs (
[:M,M:],
M)
by A42, PARTFUN1:def 3;
hence
union Z in X
by A1, A12, A23;
verum
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
; 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 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
;
contradictionthen
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
rng f misses rng g
by A79, XBOOLE_1:79;
then A85:
(rng f) /\ (rng g) = {}
;
let x,
y be
object ;
FUNCT_1:def 4 ( 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)
;
( 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;
verum
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;
verum end;
A91:
now not card (rng f) <> M
(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
;
contradictionthen 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
let x,
y be
object ;
FUNCT_1:def 4 ( 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)
;
( 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
;
x = y
hence
x = y
by A113, A112, XBOOLE_0:def 4;
verum
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;
verum 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; verum