let M be Cardinal; :: thesis: ( not M is finite implies M *` M = M )
assume A1: not M is finite ; :: thesis: M *` M = M
defpred S1[ 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
A2: for x being set holds
( x in X iff ( x in PFuncs [:M,M:],M & S1[x] ) ) from XBOOLE_0:sch 1();
 A3: for x being set st x in X holds
x is Function
proof
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 A2;
hence x is Function ; :: thesis: verum
end;
consider f being Function such that
A4: ( f is one-to-one & dom f = [:omega ,omega :] & rng f = omega ) by Th53, WELLORD2:def 4;
not M in omega by A1;
then A5: omega c= M by CARD_1:14;
then [:omega ,omega :] c= [:M,M:] by ZFMISC_1:119;
then f in PFuncs [:M,M:],M by A4, A5, PARTFUN1:def 5;
then A6: X <> {} by A2, A4;
for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X
proof
let Z be set ; :: thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )
assume that
A7: ( Z <> {} & Z c= X ) and
A8: Z is c=-linear ; :: thesis: union Z in X
( 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: union Z is Function-like
proof
let x be set ; :: thesis: ( x in union Z implies ex y1, y2 being set st [y1,y2] = x )
assume x in union Z ; :: thesis: ex y1, y2 being set st [y1,y2] = x
then consider Y being set such that
A9: ( x in Y & Y in Z ) by TARSKI:def 4;
reconsider f = Y as Function by A3, A7, A9;
( f = f & ( 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 A9; :: thesis: verum
end;
let x be set ; :: according to FUNCT_1:def 1 :: thesis: for b1, b2 being set holds
( not [x,b1] in union Z or not [x,b2] in union Z or b1 = b2 )
let y1, y2 be set ; :: thesis: ( not [x,y1] in union Z or not [x,y2] in union Z or y1 = y2 )
assume [x,y1] in union Z ; :: thesis: ( not [x,y2] in union Z or y1 = y2 )
then consider X1 being set such that
A10: ( [x,y1] in X1 & X1 in Z ) by TARSKI:def 4;
assume [x,y2] in union Z ; :: thesis: y1 = y2
then consider X2 being set such that
A11: ( [x,y2] in X2 & X2 in Z ) by TARSKI:def 4;
reconsider f1 = X1, f2 = X2 as Function by A3, A7, A10, A11;
X1,X2 are_c=-comparable by A8, A10, A11, ORDINAL1:def 9;
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 A10, A11, FUNCT_1:def 1;
hence y1 = y2 by A10, A11; :: thesis: verum
end;
then reconsider f = union Z as Function ;
A12: dom f c= [:M,M:]
proof
let x be set ; :: 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 4;
then consider Y being set such that
A13: ( [x,(f . x)] in Y & Y in Z ) by TARSKI:def 4;
Y in PFuncs [:M,M:],M by A2, A7, A13;
then consider g being Function such that
A14: ( Y = g & dom g c= [:M,M:] & rng g c= M ) by PARTFUN1:def 5;
x in dom g by A13, A14, FUNCT_1:8;
hence x in [:M,M:] by A14; :: thesis: verum
end;
rng f c= M
proof
let y be set ; :: 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 set such that
A15: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
[x,y] in union Z by A15, FUNCT_1:def 4;
then consider Y being set such that
A16: ( [x,y] in Y & Y in Z ) by TARSKI:def 4;
Y in PFuncs [:M,M:],M by A2, A7, A16;
then consider g being Function such that
A17: ( Y = g & dom g c= [:M,M:] & rng g c= M ) by PARTFUN1:def 5;
( x in dom g & g . x = y ) by A16, A17, FUNCT_1:8;
then y in rng g by FUNCT_1:def 5;
hence y in M by A17; :: thesis: verum
end;
then A18: f in PFuncs [:M,M:],M by A12, PARTFUN1:def 5;
A19: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then A20: ( [x1,(f . x1)] in f & [x2,(f . x2)] in f ) by FUNCT_1:8;
then consider X1 being set such that
A21: ( [x1,(f . x1)] in X1 & X1 in Z ) by TARSKI:def 4;
consider X2 being set such that
A22: ( [x2,(f . x2)] in X2 & X2 in Z ) by A20, TARSKI:def 4;
consider f1 being Function such that
A23: ( f1 = X1 & f1 is one-to-one & dom f1 = [:(rng f1),(rng f1):] ) by A2, A7, A21;
consider f2 being Function such that
A24: ( f2 = X2 & f2 is one-to-one & dom f2 = [:(rng f2),(rng f2):] ) by A2, A7, A22;
X1,X2 are_c=-comparable by A8, A21, A22, ORDINAL1:def 9;
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 A21, A22, A23, A24, FUNCT_1:8;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A23, A24, FUNCT_1:def 8; :: thesis: verum
end;
dom f = [:(rng f),(rng f):]
proof
thus dom f c= [:(rng f),(rng f):] :: according to XBOOLE_0:def 10 :: thesis: [:(rng f),(rng f):] c= dom f
proof
let x be set ; :: 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 4;
then consider Y being set such that
A25: ( [x,(f . x)] in Y & Y in Z ) by TARSKI:def 4;
consider g being Function such that
A26: ( g = Y & g is one-to-one & dom g = [:(rng g),(rng g):] ) by A2, A7, A25;
g c= f by A25, A26, ZFMISC_1:92;
then rng g c= rng f by RELAT_1:25;
then ( dom g c= [:(rng f),(rng f):] & x in dom g ) by A25, A26, FUNCT_1:8, ZFMISC_1:119;
hence x in [:(rng f),(rng f):] ; :: thesis: verum
end;
let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in [:(rng f),(rng f):] or [x1,x2] in dom f )
assume [x1,x2] in [:(rng f),(rng f):] ; :: thesis: [x1,x2] in dom f
then A27: ( [x1,x2] = [([x1,x2] `1 ),([x1,x2] `2 )] & [x1,x2] `1 in rng f & [x1,x2] `2 in rng f ) by MCART_1:10, MCART_1:23;
then consider y1 being set such that
A28: ( y1 in dom f & [x1,x2] `1 = f . y1 ) by FUNCT_1:def 5;
consider y2 being set such that
A29: ( y2 in dom f & [x1,x2] `2 = f . y2 ) by A27, FUNCT_1:def 5;
A30: ( [y1,([x1,x2] `1 )] in f & [y2,([x1,x2] `2 )] in f ) by A28, A29, FUNCT_1:8;
then consider X1 being set such that
A31: ( [y1,([x1,x2] `1 )] in X1 & X1 in Z ) by TARSKI:def 4;
consider X2 being set such that
A32: ( [y2,([x1,x2] `2 )] in X2 & X2 in Z ) by A30, TARSKI:def 4;
consider f1 being Function such that
A33: ( f1 = X1 & f1 is one-to-one & dom f1 = [:(rng f1),(rng f1):] ) by A2, A7, A31;
consider f2 being Function such that
A34: ( f2 = X2 & f2 is one-to-one & dom f2 = [:(rng f2),(rng f2):] ) by A2, A7, A32;
X1,X2 are_c=-comparable by A8, A31, A32, ORDINAL1:def 9;
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 A31, A32, A33, A34, FUNCT_1:8;
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 5;
then A35: ( [x1,x2] in dom f1 or [x1,x2] in dom f2 ) by A27, A33, A34, ZFMISC_1:106;
( f1 c= f & f2 c= f ) by A31, A32, A33, A34, ZFMISC_1:92;
then ( dom f1 c= dom f & dom f2 c= dom f ) by RELAT_1:25;
hence [x1,x2] in dom f by A35; :: thesis: verum
end;
hence union Z in X by A2, A18, A19; :: thesis: verum
end;
then consider Y being set such that
A36: ( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) by A6, ORDERS_1:177;
consider f being Function such that
A37: ( f = Y & f is one-to-one & dom f = [:(rng f),(rng f):] ) by A2, A36;
Y in PFuncs [:M,M:],M by A2, A36;
then A38: ex f being Function st
( Y = f & dom f c= [:M,M:] & rng f c= M ) by PARTFUN1:def 5;
then A39: ( dom f c= [:M,M:] & rng f c= M & card M = M ) by A37, CARD_1:def 5;
set A = rng f;
set N = card (rng f);
B60: now
assume A40: rng f is finite ; :: thesis: contradiction
then A41: ( card (rng f) in omega & omega c= omega & card (rng f) = card (card (rng f)) ) by CARD_1:84, CARD_3:58;
then A42: ( omega c= omega +` (card (rng f)) & not omega is finite & omega +` (card (rng f)) c= omega +` omega ) by CARD_3:125, CARD_3:140;
omega +` omega = omega by CARD_3:117;
then A43: ( omega = omega +` (card (rng f)) & card omega = omega & omega c= omega \/ (rng f) ) by A42, CARD_1:def 5, XBOOLE_0:def 10, XBOOLE_1:7;
then A44: ( omega = card (omega \ (rng f)) & card (omega \/ (rng f)) c= omega & omega c= card (omega \/ (rng f)) ) by A40, CARD_1:27, CARD_2:47, CARD_3:58, CARD_3:144;
( omega \ (rng f) misses rng f & rng f misses omega \ (rng f) ) by XBOOLE_1:79;
then A45: ( (omega \ (rng f)) /\ (rng f) = {} & (rng f) /\ (omega \ (rng f)) = {} ) by XBOOLE_0:def 7;
then ( [:((omega \ (rng f)) /\ (omega \ (rng f))),((omega \ (rng f)) /\ (rng f)):] = {} & [:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (omega \ (rng f))):] = {} & [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (omega \ (rng f))):] = {} ) by ZFMISC_1:113;
then A46: ( [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(omega \ (rng f)),(rng f):] = {} & [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(omega \ (rng f)):] = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(omega \ (rng f)):] = {} ) by ZFMISC_1:123;
then A47: ( [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(omega \ (rng f)),(rng f):] & [:(omega \ (rng f)),(omega \ (rng f)):] misses [:(rng f),(omega \ (rng f)):] & [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] ) by XBOOLE_0:def 7;
([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(omega \ (rng f)):] = {} \/ {} by A46, XBOOLE_1:23
.= {} ;
then [:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):] misses [:(rng f),(omega \ (rng f)):] by XBOOLE_0:def 7;
then A48: 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:48
.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:(omega \ (rng f)),(rng f):])) +` (card [:(rng f),(omega \ (rng f)):]) by A47, CARD_2:48
.= ((card [:(omega \ (rng f)),(omega \ (rng f)):]) +` (card [:omega ,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A44, CARD_2:14
.= ((card [:omega ,omega :]) +` (card [:omega ,(card (rng f)):])) +` (card [:(rng f),(omega \ (rng f)):]) by A44, CARD_2:14
.= (omega +` (card [:omega ,(card (rng f)):])) +` (card [:(card (rng f)),omega :]) by A44, Th53, CARD_2:14
.= (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 ;
omega *` (card (rng f)) c= omega by A41, CARD_3:135;
then ( omega +` (omega *` (card (rng f))) = omega & (card (rng f)) *` omega c= omega ) by CARD_3:118;
then ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):],omega \ (rng f) are_equipotent by A44, A48, CARD_1:21;
then consider g being Function such that
A49: ( g is one-to-one & dom g = ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) \/ [:(rng f),(omega \ (rng f)):] & rng g = omega \ (rng f) ) by WELLORD2:def 4;
A50: ( [:((omega \ (rng f)) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} & [:((omega \ (rng f)) /\ (rng f)),((rng f) /\ (rng f)):] = {} & [:((rng f) /\ (rng f)),((omega \ (rng f)) /\ (rng f)):] = {} ) by A45, ZFMISC_1:113;
then ( [:(omega \ (rng f)),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} & {} \/ {} = {} & [:(omega \ (rng f)),(rng f):] /\ [:(rng f),(rng f):] = {} ) by ZFMISC_1:123;
then ( ([:(omega \ (rng f)),(omega \ (rng f)):] \/ [:(omega \ (rng f)),(rng f):]) /\ [:(rng f),(rng f):] = {} & [:(rng f),(omega \ (rng f)):] /\ [:(rng f),(rng f):] = {} & {} \/ {} = {} ) by A50, XBOOLE_1:23, ZFMISC_1:123;
then (dom g) /\ (dom f) = {} by A37, A49, XBOOLE_1:23;
then A51: dom g misses dom f by XBOOLE_0:def 7;
then A52: ( dom (g +* f) = (dom g) \/ (dom f) & g c= g +* f & rng f c= rng (g +* f) & rng (g +* f) c= (rng g) \/ (rng f) ) by FUNCT_4:18, FUNCT_4:19, FUNCT_4:33, FUNCT_4:def 1;
then rng g c= rng (g +* f) by RELAT_1:25;
then (rng g) \/ (rng f) c= rng (g +* f) by A52, XBOOLE_1:8;
then A53: rng (g +* f) = (rng g) \/ (rng f) by A52, XBOOLE_0:def 10
.= omega \/ (rng f) by A49, XBOOLE_1:39 ;
A54: dom (g +* f) = ([:(omega \ (rng f)),((omega \ (rng f)) \/ (rng f)):] \/ [:(rng f),(omega \ (rng f)):]) \/ [:(rng f),(rng f):] by A37, A49, A52, ZFMISC_1:120
.= [:(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:120
.= [:((omega \ (rng f)) \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by ZFMISC_1:120
.= [:(omega \/ (rng f)),((omega \ (rng f)) \/ (rng f)):] by XBOOLE_1:39
.= [:(omega \/ (rng f)),(omega \/ (rng f)):] by XBOOLE_1:39 ;
A55: omega \/ (rng f) c= M by A5, A37, A38, XBOOLE_1:8;
then [:(omega \/ (rng f)),(omega \/ (rng f)):] c= [:M,M:] by ZFMISC_1:119;
then A56: g +* f in PFuncs [:M,M:],M by A53, A54, A55, PARTFUN1:def 5;
g +* f is one-to-one
proof
rng f misses rng g by A49, XBOOLE_1:79;
then A57: (rng f) /\ (rng g) = {} by XBOOLE_0:def 7;
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in dom (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 )
let y be set ; :: 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 ( x in dom (g +* f) & y in dom (g +* f) ) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )
then ( ( x in dom f or x in dom g ) & ( y in dom g or y in dom f ) ) by A52, 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 A37, A49, A51, FUNCT_1:def 5, FUNCT_1:def 8, FUNCT_4:14, FUNCT_4:17;
hence ( not (g +* f) . x = (g +* f) . y or x = y ) by A57, XBOOLE_0:def 4; :: thesis: verum
end;
then ( g +* f in X & f c= g +* f & f = Y & g +* f = g +* f ) by A2, A37, A53, A54, A56, FUNCT_4:26;
then A58: g +* f = f by A36;
A59: omega \ (rng f) <> {} by A40, A43, CARD_2:4, CARD_3:58;
consider x being Element of omega \ (rng f);
( x in omega & not x in rng f ) by A59, XBOOLE_0:def 5;
hence contradiction by A53, A58, XBOOLE_0:def 3; :: thesis: verum
end;
then A60: ( not card (rng f) is finite & card (rng f) c= M ) by A39, CARD_1:27;
A61: now
assume card (rng f) <> M ; :: thesis: contradiction
then ( card (rng f) in M & M +` (card (rng f)) = M ) by A1, A60, CARD_1:13, CARD_3:118;
then card (M \ (rng f)) = M by A39, CARD_3:144;
then consider h being Function such that
A62: ( h is one-to-one & dom h = rng f & rng h c= M \ (rng f) ) by A60, CARD_1:26;
set B = rng h;
rng f, rng h are_equipotent by A62, WELLORD2:def 4;
then A63: card (rng f) = card (rng h) by CARD_1:21;
(card (rng f)) *` (card (rng f)) = card [:(card (rng f)),(card (rng f)):] by CARD_2:def 2;
then ( [:(rng f),(rng f):], rng f are_equipotent & (card (rng f)) *` (card (rng f)) = card [:(rng f),(rng f):] ) by A37, CARD_2:14, WELLORD2:def 4;
then A64: ( (card (rng f)) *` (card (rng f)) = card (rng f) & (card (rng f)) +` (card (rng f)) = card (rng f) ) by B60, CARD_1:21, CARD_3:117;
A65: rng f misses M \ (rng f) by XBOOLE_1:79;
(rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) by A62, XBOOLE_1:26;
then (rng f) /\ (rng h) c= {} by A65, XBOOLE_0:def 7;
then ( (rng f) /\ (rng h) = {} & (rng f) /\ (rng h) = (rng h) /\ (rng f) ) ;
then A66: ( rng f misses rng h & (rng f) /\ (rng h) = (rng h) /\ (rng f) ) by XBOOLE_0:def 7;
then card ((rng f) \/ (rng h)) = card (rng f) by A63, A64, CARD_2:48;
then A67: card [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] = card [:(card (rng f)),(card (rng f)):] by CARD_2:14
.= card (rng f) by A64, CARD_2:def 2 ;
A68: ((rng f) \/ (rng h)) \ (rng f) = (rng h) \ (rng f) by XBOOLE_1:40
.= rng h by A66, XBOOLE_1:83 ;
then A69: ( rng h c= (rng f) \/ (rng h) & rng f c= (rng f) \/ (rng h) & rng h c= ((rng f) \/ (rng h)) \ (rng f) ) by XBOOLE_1:7;
( [:(((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 h),(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 f) \/ (rng h)) \ (rng f)),((rng f) \/ (rng h)):] \/ [:((rng f) \/ (rng h)),(((rng f) \/ (rng h)) \ (rng f)):] & card (rng f) = card [:(card (rng f)),(card (rng f)):] ) by A64, A68, CARD_2:def 2, XBOOLE_1:7, ZFMISC_1:119, ZFMISC_1:126;
then ( [:(rng h),(rng h):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] & card (rng f) = card [:(rng h),(rng h):] & [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] ) by A63, CARD_2:14, XBOOLE_1:1;
then ( card (rng f) c= card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) & card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) c= card (rng f) ) by A67, CARD_1:27;
then card ([:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):]) = card (rng f) by XBOOLE_0:def 10;
then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):], rng h are_equipotent by A63, CARD_1:21;
then consider g being Function such that
A70: ( g is one-to-one & dom g = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] & rng g = rng h ) by WELLORD2:def 4;
A71: [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \ [:(rng f),(rng f):] misses [:(rng f),(rng f):] by XBOOLE_1:79;
g c= g +* f by A37, A70, FUNCT_4:33, XBOOLE_1:79;
then ( rng f c= rng (g +* f) & rng g c= rng (g +* f) ) by FUNCT_4:19, RELAT_1:25;
then ( (rng g) \/ (rng f) c= rng (g +* f) & rng (g +* f) c= (rng g) \/ (rng f) ) by FUNCT_4:18, XBOOLE_1:8;
then A72: rng (g +* f) = (rng g) \/ (rng f) by XBOOLE_0:def 10;
A73: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def 1;
then ( dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] \/ [:(rng f),(rng f):] & [:(rng f),(rng f):] c= [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] ) by A37, A69, A70, XBOOLE_1:39, ZFMISC_1:119;
then A74: dom (g +* f) = [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] by XBOOLE_1:12;
rng h c= M by A62, XBOOLE_1:1;
then A75: (rng f) \/ (rng h) c= M by A37, A38, XBOOLE_1:8;
then [:((rng f) \/ (rng h)),((rng f) \/ (rng h)):] c= [:M,M:] by ZFMISC_1:119;
then A76: g +* f in PFuncs [:M,M:],M by A70, A72, A74, A75, PARTFUN1:def 5;
g +* f is one-to-one
proof
A77: rng f misses M \ (rng f) by XBOOLE_1:79;
(rng f) /\ (rng h) c= (rng f) /\ (M \ (rng f)) by A62, XBOOLE_1:26;
then B78: (rng f) /\ (rng g) c= {} by A70, A77, XBOOLE_0:def 7;
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x in dom (g +* f) or not b1 in dom (g +* f) or not (g +* f) . x = (g +* f) . b1 or x = b1 )
let y be set ; :: 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 ( x in dom (g +* f) & y in dom (g +* f) ) ; :: thesis: ( not (g +* f) . x = (g +* f) . y or x = y )
then ( ( x in dom f or x in dom g ) & ( y in dom g or y in dom f ) ) by A73, XBOOLE_0:def 3;
then A79: ( ( (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 A37, A70, A71, FUNCT_1:def 5, FUNCT_1:def 8, FUNCT_4:14, FUNCT_4:17;
assume (g +* f) . x = (g +* f) . y ; :: thesis: x = y
hence x = y by B78, A79, XBOOLE_0:def 4; :: thesis: verum
end;
then A80: ( g +* f in X & f c= g +* f & f = Y & g +* f = g +* f ) by A2, A37, A70, A72, A74, A76, FUNCT_4:26;
A81: rng h <> {} by B60, A63;
consider x being Element of rng h;
x in M \ (rng f) by A62, A81, TARSKI:def 3;
then ( not x in rng f & x in rng (g +* f) ) by A70, A72, A81, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence contradiction by A36, A80; :: thesis: verum
end;
then A82: M *` M = card [:(card (rng f)),(card (rng f)):] by CARD_2:def 2
.= card [:(rng f),(rng f):] by CARD_2:14 ;
[:(rng f),(rng f):], rng f are_equipotent by A37, WELLORD2:def 4;
hence M *` M = M by A61, A82, CARD_1:21; :: thesis: verum