:: FUNCT_2 semantic presentation begin definition let X, Y be set ; let R be Relation of X,Y; attrR is quasi_total means :Def1: :: FUNCT_2:def 1 X = dom R if Y <> {} otherwise R = {} ; consistency verum ; end; :: deftheorem Def1 defines quasi_total FUNCT_2:def_1_:_ for X, Y being set for R being Relation of X,Y holds ( ( Y <> {} implies ( R is quasi_total iff X = dom R ) ) & ( not Y <> {} implies ( R is quasi_total iff R = {} ) ) ); registration let X, Y be set ; cluster Relation-like X -defined Y -valued Function-like quasi_total for Element of bool [:X,Y:]; existence ex b1 being PartFunc of X,Y st b1 is quasi_total proof percases ( Y = {} or Y <> {} ) ; supposeA1: Y = {} ; ::_thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total reconsider R = {} as PartFunc of X,Y by RELSET_1:12; take R ; ::_thesis: R is quasi_total thus R is quasi_total by A1, Def1; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total then consider f being Function such that A3: X = dom f and A4: rng f c= Y by FUNCT_1:8; reconsider R = f as PartFunc of X,Y by A3, A4, RELSET_1:4; take R ; ::_thesis: R is quasi_total thus R is quasi_total by A2, A3, Def1; ::_thesis: verum end; end; end; end; registration let X, Y be set ; cluster total -> quasi_total for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y st b1 is total holds b1 is quasi_total proof let f be Relation of X,Y; ::_thesis: ( f is total implies f is quasi_total ) assume A1: dom f = X ; :: according to PARTFUN1:def_2 ::_thesis: f is quasi_total percases ( Y <> {} or Y = {} ) ; :: according to FUNCT_2:def_1 case Y <> {} ; ::_thesis: X = dom f thus X = dom f by A1; ::_thesis: verum end; case Y = {} ; ::_thesis: f = {} hence f = {} ; ::_thesis: verum end; end; end; end; definition let X, Y be set ; mode Function of X,Y is quasi_total PartFunc of X,Y; end; registration let X be empty set ; let Y be set ; cluster quasi_total -> total for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y st b1 is quasi_total holds b1 is total ; end; registration let X be set ; let Y be non empty set ; cluster quasi_total -> total for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y st b1 is quasi_total holds b1 is total proof let F be Relation of X,Y; ::_thesis: ( F is quasi_total implies F is total ) assume F is quasi_total ; ::_thesis: F is total hence X = dom F by Def1; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; registration let X be set ; cluster quasi_total -> total for Element of bool [:X,X:]; coherence for b1 being Relation of X,X st b1 is quasi_total holds b1 is total proof percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: for b1 being Relation of X,X st b1 is quasi_total holds b1 is total hence for b1 being Relation of X,X st b1 is quasi_total holds b1 is total ; ::_thesis: verum end; suppose X <> {} ; ::_thesis: for b1 being Relation of X,X st b1 is quasi_total holds b1 is total hence for b1 being Relation of X,X st b1 is quasi_total holds b1 is total ; ::_thesis: verum end; end; end; end; theorem :: FUNCT_2:1 for f being Function holds f is Function of (dom f),(rng f) proof let f be Function; ::_thesis: f is Function of (dom f),(rng f) reconsider R = f as Relation of (dom f),(rng f) by RELSET_1:4; ( rng R <> {} or rng R = {} ) ; hence f is Function of (dom f),(rng f) by Def1; ::_thesis: verum end; theorem Th2: :: FUNCT_2:2 for Y being set for f being Function st rng f c= Y holds f is Function of (dom f),Y proof let Y be set ; ::_thesis: for f being Function st rng f c= Y holds f is Function of (dom f),Y let f be Function; ::_thesis: ( rng f c= Y implies f is Function of (dom f),Y ) assume rng f c= Y ; ::_thesis: f is Function of (dom f),Y then reconsider R = f as Relation of (dom f),Y by RELSET_1:4; ( Y = {} or Y <> {} ) ; then R is quasi_total by Def1; hence f is Function of (dom f),Y ; ::_thesis: verum end; theorem :: FUNCT_2:3 for X, Y being set for f being Function st dom f = X & ( for x being set st x in X holds f . x in Y ) holds f is Function of X,Y proof let X, Y be set ; ::_thesis: for f being Function st dom f = X & ( for x being set st x in X holds f . x in Y ) holds f is Function of X,Y let f be Function; ::_thesis: ( dom f = X & ( for x being set st x in X holds f . x in Y ) implies f is Function of X,Y ) assume that A1: dom f = X and A2: for x being set st x in X holds f . x in Y ; ::_thesis: f is Function of X,Y rng f c= Y proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Y ) assume y in rng f ; ::_thesis: y in Y then ex x being set st ( x in X & y = f . x ) by A1, FUNCT_1:def_3; hence y in Y by A2; ::_thesis: verum end; then reconsider R = f as Relation of (dom f),Y by RELSET_1:4; ( Y = {} or Y <> {} ) ; then R is quasi_total by Def1; hence f is Function of X,Y by A1; ::_thesis: verum end; theorem Th4: :: FUNCT_2:4 for X, Y, x being set for f being Function of X,Y st Y <> {} & x in X holds f . x in rng f proof let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X holds f . x in rng f let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X implies f . x in rng f ) assume Y <> {} ; ::_thesis: ( not x in X or f . x in rng f ) then dom f = X by Def1; hence ( not x in X or f . x in rng f ) by FUNCT_1:def_3; ::_thesis: verum end; theorem Th5: :: FUNCT_2:5 for X, Y, x being set for f being Function of X,Y st Y <> {} & x in X holds f . x in Y proof let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X holds f . x in Y let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X implies f . x in Y ) assume ( Y <> {} & x in X ) ; ::_thesis: f . x in Y then f . x in rng f by Th4; hence f . x in Y ; ::_thesis: verum end; theorem :: FUNCT_2:6 for X, Y, Z being set for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds f is Function of X,Z proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & rng f c= Z holds f is Function of X,Z let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & rng f c= Z implies f is Function of X,Z ) assume ( Y <> {} or X = {} ) ; ::_thesis: ( not rng f c= Z or f is Function of X,Z ) then A1: dom f = X by Def1; assume A2: rng f c= Z ; ::_thesis: f is Function of X,Z now__::_thesis:_(_Z_=_{}_implies_X_=_{}_) assume Z = {} ; ::_thesis: X = {} then rng f = {} by A2; hence X = {} by A1, RELAT_1:42; ::_thesis: verum end; hence f is Function of X,Z by A1, A2, Def1, RELSET_1:4; ::_thesis: verum end; theorem :: FUNCT_2:7 for X, Y, Z being set for f being Function of X,Y st ( Y = {} implies X = {} ) & Y c= Z holds f is Function of X,Z by RELSET_1:7; scheme :: FUNCT_2:sch 1 FuncEx1{ F1() -> set , F2() -> set , P1[ set , set ] } : ex f being Function of F1(),F2() st for x being set st x in F1() holds P1[x,f . x] provided A1: for x being set st x in F1() holds ex y being set st ( y in F2() & P1[x,y] ) proof consider f being Function such that A2: ( dom f = F1() & rng f c= F2() ) and A3: for x being set st x in F1() holds P1[x,f . x] from FUNCT_1:sch_5(A1); reconsider f = f as Function of F1(),F2() by A2, Th2; take f ; ::_thesis: for x being set st x in F1() holds P1[x,f . x] thus for x being set st x in F1() holds P1[x,f . x] by A3; ::_thesis: verum end; scheme :: FUNCT_2:sch 2 Lambda1{ F1() -> set , F2() -> set , F3( set ) -> set } : ex f being Function of F1(),F2() st for x being set st x in F1() holds f . x = F3(x) provided A1: for x being set st x in F1() holds F3(x) in F2() proof defpred S1[ set , set ] means \$2 = F3(\$1); A2: for x being set st x in F1() holds ex y being set st ( y in F2() & S1[x,y] ) by A1; thus ex f being Function of F1(),F2() st for x being set st x in F1() holds S1[x,f . x] from FUNCT_2:sch_1(A2); ::_thesis: verum end; definition let X, Y be set ; func Funcs (X,Y) -> set means :Def2: :: FUNCT_2:def 2 for x being set holds ( x in it iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) proof defpred S1[ set ] means ex f being Function st ( \$1 = f & dom f = X & rng f c= Y ); consider F being set such that A1: for z being set holds ( z in F iff ( z in bool [:X,Y:] & S1[z] ) ) from XBOOLE_0:sch_1(); take F ; ::_thesis: for x being set holds ( x in F iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) let z be set ; ::_thesis: ( z in F iff ex f being Function st ( z = f & dom f = X & rng f c= Y ) ) thus ( z in F implies ex f being Function st ( z = f & dom f = X & rng f c= Y ) ) by A1; ::_thesis: ( ex f being Function st ( z = f & dom f = X & rng f c= Y ) implies z in F ) given f being Function such that A2: z = f and A3: ( dom f = X & rng f c= Y ) ; ::_thesis: z in F f c= [:X,Y:] proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f or p in [:X,Y:] ) assume A4: p in f ; ::_thesis: p in [:X,Y:] then consider x, y being set such that A5: p = [x,y] by RELAT_1:def_1; A6: x in dom f by A4, A5, XTUPLE_0:def_12; then y = f . x by A4, A5, FUNCT_1:def_2; then y in rng f by A6, FUNCT_1:def_3; hence p in [:X,Y:] by A3, A5, A6, ZFMISC_1:def_2; ::_thesis: verum end; hence z in F by A1, A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds ( x in b2 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ) holds b1 = b2 proof let F1, F2 be set ; ::_thesis: ( ( for x being set holds ( x in F1 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ) & ( for x being set holds ( x in F2 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ) implies F1 = F2 ) assume that A7: for x being set holds ( x in F1 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) and A8: for x being set holds ( x in F2 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ; ::_thesis: F1 = F2 for x being set holds ( x in F1 iff x in F2 ) proof let x be set ; ::_thesis: ( x in F1 iff x in F2 ) ( x in F1 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) by A7; hence ( x in F1 iff x in F2 ) by A8; ::_thesis: verum end; hence F1 = F2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def2 defines Funcs FUNCT_2:def_2_:_ for X, Y, b3 being set holds ( b3 = Funcs (X,Y) iff for x being set holds ( x in b3 iff ex f being Function st ( x = f & dom f = X & rng f c= Y ) ) ); theorem Th8: :: FUNCT_2:8 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds f in Funcs (X,Y) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds f in Funcs (X,Y) let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f in Funcs (X,Y) ) assume ( Y = {} implies X = {} ) ; ::_thesis: f in Funcs (X,Y) then A1: dom f = X by Def1; rng f c= Y ; hence f in Funcs (X,Y) by A1, Def2; ::_thesis: verum end; theorem :: FUNCT_2:9 for X being set for f being Function of X,X holds f in Funcs (X,X) by Th8; registration let X be set ; let Y be non empty set ; cluster Funcs (X,Y) -> non empty ; coherence not Funcs (X,Y) is empty by Th8; end; registration let X be set ; cluster Funcs (X,X) -> non empty ; coherence not Funcs (X,X) is empty by Th8; end; registration let X be non empty set ; let Y be empty set ; cluster Funcs (X,Y) -> empty ; coherence Funcs (X,Y) is empty proof assume not Funcs (X,Y) is empty ; ::_thesis: contradiction then consider f being Function such that the Element of Funcs (X,Y) = f and A1: dom f = X and A2: rng f c= {} by Def2; rng f = {} by A2; hence contradiction by A1, RELAT_1:42; ::_thesis: verum end; end; theorem :: FUNCT_2:10 for X, Y being set for f being Function of X,Y st ( for y being set st y in Y holds ex x being set st ( x in X & y = f . x ) ) holds rng f = Y proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( for y being set st y in Y holds ex x being set st ( x in X & y = f . x ) ) holds rng f = Y let f be Function of X,Y; ::_thesis: ( ( for y being set st y in Y holds ex x being set st ( x in X & y = f . x ) ) implies rng f = Y ) assume A1: for y being set st y in Y holds ex x being set st ( x in X & y = f . x ) ; ::_thesis: rng f = Y percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: rng f = Y hence rng f = Y ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: rng f = Y for y being set holds ( y in rng f iff y in Y ) proof let y be set ; ::_thesis: ( y in rng f iff y in Y ) dom f = X by A2, Def1; then ( y in rng f iff ex x being set st ( x in X & y = f . x ) ) by FUNCT_1:def_3; hence ( y in rng f iff y in Y ) by A1; ::_thesis: verum end; hence rng f = Y by TARSKI:1; ::_thesis: verum end; end; end; theorem Th11: :: FUNCT_2:11 for X, Y, y being set for f being Function of X,Y st y in rng f holds ex x being set st ( x in X & f . x = y ) proof let X, Y, y be set ; ::_thesis: for f being Function of X,Y st y in rng f holds ex x being set st ( x in X & f . x = y ) let f be Function of X,Y; ::_thesis: ( y in rng f implies ex x being set st ( x in X & f . x = y ) ) assume A1: y in rng f ; ::_thesis: ex x being set st ( x in X & f . x = y ) then dom f = X by Def1; hence ex x being set st ( x in X & f . x = y ) by A1, FUNCT_1:def_3; ::_thesis: verum end; theorem Th12: :: FUNCT_2:12 for X, Y being set for f1, f2 being Function of X,Y st ( for x being set st x in X holds f1 . x = f2 . x ) holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function of X,Y st ( for x being set st x in X holds f1 . x = f2 . x ) holds f1 = f2 let f1, f2 be Function of X,Y; ::_thesis: ( ( for x being set st x in X holds f1 . x = f2 . x ) implies f1 = f2 ) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: ( ( for x being set st x in X holds f1 . x = f2 . x ) implies f1 = f2 ) hence ( ( for x being set st x in X holds f1 . x = f2 . x ) implies f1 = f2 ) ; ::_thesis: verum end; suppose Y <> {} ; ::_thesis: ( ( for x being set st x in X holds f1 . x = f2 . x ) implies f1 = f2 ) then ( dom f1 = X & dom f2 = X ) by Def1; hence ( ( for x being set st x in X holds f1 . x = f2 . x ) implies f1 = f2 ) by FUNCT_1:2; ::_thesis: verum end; end; end; theorem Th13: :: FUNCT_2:13 for X, Y, Z being set for f being quasi_total Relation of X,Y for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds f * g is quasi_total proof let X, Y, Z be set ; ::_thesis: for f being quasi_total Relation of X,Y for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds f * g is quasi_total let f be quasi_total Relation of X,Y; ::_thesis: for g being quasi_total Relation of Y,Z st ( not Y = {} or Z = {} or X = {} ) holds f * g is quasi_total let g be quasi_total Relation of Y,Z; ::_thesis: ( ( not Y = {} or Z = {} or X = {} ) implies f * g is quasi_total ) assume A1: ( not Y = {} or Z = {} or X = {} ) ; ::_thesis: f * g is quasi_total percases ( Z <> {} or Z = {} ) ; :: according to FUNCT_2:def_1 caseA2: Z <> {} ; ::_thesis: X = dom (f * g) then A3: dom g = Y by Def1; ( dom f = X & rng f c= Y ) by A1, A2, Def1; hence X = dom (f * g) by A3, RELAT_1:27; ::_thesis: verum end; case Z = {} ; ::_thesis: f * g = {} hence f * g = {} ; ::_thesis: verum end; end; end; theorem :: FUNCT_2:14 for X, Y, Z being set for f being Function of X,Y for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds rng (g * f) = Z proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds rng (g * f) = Z let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st Z <> {} & rng f = Y & rng g = Z holds rng (g * f) = Z let g be Function of Y,Z; ::_thesis: ( Z <> {} & rng f = Y & rng g = Z implies rng (g * f) = Z ) assume Z <> {} ; ::_thesis: ( not rng f = Y or not rng g = Z or rng (g * f) = Z ) then dom g = Y by Def1; hence ( not rng f = Y or not rng g = Z or rng (g * f) = Z ) by RELAT_1:28; ::_thesis: verum end; theorem Th15: :: FUNCT_2:15 for X, Y, x being set for f being Function of X,Y for g being Function st Y <> {} & x in X holds (g * f) . x = g . (f . x) proof let X, Y, x be set ; ::_thesis: for f being Function of X,Y for g being Function st Y <> {} & x in X holds (g * f) . x = g . (f . x) let f be Function of X,Y; ::_thesis: for g being Function st Y <> {} & x in X holds (g * f) . x = g . (f . x) let g be Function; ::_thesis: ( Y <> {} & x in X implies (g * f) . x = g . (f . x) ) assume Y <> {} ; ::_thesis: ( not x in X or (g * f) . x = g . (f . x) ) then X = dom f by Def1; hence ( not x in X or (g * f) . x = g . (f . x) ) by FUNCT_1:13; ::_thesis: verum end; theorem :: FUNCT_2:16 for X, Y being set for f being Function of X,Y st Y <> {} holds ( rng f = Y iff for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds ( rng f = Y iff for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) let f be Function of X,Y; ::_thesis: ( Y <> {} implies ( rng f = Y iff for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) ) assume A1: Y <> {} ; ::_thesis: ( rng f = Y iff for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) thus ( rng f = Y implies for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) ::_thesis: ( ( for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ) implies rng f = Y ) proof assume A2: rng f = Y ; ::_thesis: for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h let Z be set ; ::_thesis: ( Z <> {} implies for g, h being Function of Y,Z st g * f = h * f holds g = h ) assume A3: Z <> {} ; ::_thesis: for g, h being Function of Y,Z st g * f = h * f holds g = h let g, h be Function of Y,Z; ::_thesis: ( g * f = h * f implies g = h ) ( dom g = Y & dom h = Y ) by A3, Def1; hence ( g * f = h * f implies g = h ) by A2, FUNCT_1:86; ::_thesis: verum end; assume A4: for Z being set st Z <> {} holds for g, h being Function of Y,Z st g * f = h * f holds g = h ; ::_thesis: rng f = Y for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds g = h proof let g, h be Function; ::_thesis: ( dom g = Y & dom h = Y & g * f = h * f implies g = h ) assume that A5: dom g = Y and A6: dom h = Y ; ::_thesis: ( not g * f = h * f or g = h ) A7: rng g <> {} by A1, A5, RELAT_1:42; A8: g is Function of Y,((rng g) \/ (rng h)) by A5, Th2, XBOOLE_1:7; h is Function of Y,((rng g) \/ (rng h)) by A6, Th2, XBOOLE_1:7; hence ( not g * f = h * f or g = h ) by A4, A7, A8; ::_thesis: verum end; hence rng f = Y by FUNCT_1:16; ::_thesis: verum end; theorem :: FUNCT_2:17 for X, Y being set for f being Relation of X,Y holds ( (id X) * f = f & f * (id Y) = f ) proof let X, Y be set ; ::_thesis: for f being Relation of X,Y holds ( (id X) * f = f & f * (id Y) = f ) let f be Relation of X,Y; ::_thesis: ( (id X) * f = f & f * (id Y) = f ) dom f c= X ; hence (id X) * f = f by RELAT_1:51; ::_thesis: f * (id Y) = f rng f c= Y ; hence f * (id Y) = f by RELAT_1:53; ::_thesis: verum end; theorem :: FUNCT_2:18 for X, Y being set for f being Function of X,Y for g being Function of Y,X st f * g = id Y holds rng f = Y proof let X, Y be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,X st f * g = id Y holds rng f = Y let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f * g = id Y holds rng f = Y let g be Function of Y,X; ::_thesis: ( f * g = id Y implies rng f = Y ) assume f * g = id Y ; ::_thesis: rng f = Y then rng (f * g) = Y by RELAT_1:45; then Y c= rng f by RELAT_1:26; hence rng f = Y by XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FUNCT_2:19 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) ) assume ( Y = {} implies X = {} ) ; ::_thesis: ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) then dom f = X by Def1; hence ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) by FUNCT_1:def_4; ::_thesis: verum end; theorem :: FUNCT_2:20 for X, Y, Z being set for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds f is one-to-one proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds f is one-to-one let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one holds f is one-to-one let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) & g * f is one-to-one implies f is one-to-one ) assume ( Z <> {} or Y = {} ) ; ::_thesis: ( not g * f is one-to-one or f is one-to-one ) then A1: Y = dom g by Def1; rng f c= Y ; hence ( not g * f is one-to-one or f is one-to-one ) by A1, FUNCT_1:25; ::_thesis: verum end; theorem :: FUNCT_2:21 for X, Y being set for f being Function of X,Y st X <> {} & Y <> {} holds ( f is one-to-one iff for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st X <> {} & Y <> {} holds ( f is one-to-one iff for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) let f be Function of X,Y; ::_thesis: ( X <> {} & Y <> {} implies ( f is one-to-one iff for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) ) assume that A1: X <> {} and A2: Y <> {} ; ::_thesis: ( f is one-to-one iff for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) A3: dom f = X by A2, Def1; thus ( f is one-to-one implies for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) ::_thesis: ( ( for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ) implies f is one-to-one ) proof assume A4: f is one-to-one ; ::_thesis: for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h let Z be set ; ::_thesis: for g, h being Function of Z,X st f * g = f * h holds g = h let g, h be Function of Z,X; ::_thesis: ( f * g = f * h implies g = h ) A5: ( rng g c= X & rng h c= X ) ; ( dom g = Z & dom h = Z ) by A1, Def1; hence ( f * g = f * h implies g = h ) by A3, A4, A5, FUNCT_1:27; ::_thesis: verum end; assume A6: for Z being set for g, h being Function of Z,X st f * g = f * h holds g = h ; ::_thesis: f is one-to-one now__::_thesis:_for_g,_h_being_Function_st_rng_g_c=_dom_f_&_rng_h_c=_dom_f_&_dom_g_=_dom_h_&_f_*_g_=_f_*_h_holds_ g_=_h let g, h be Function; ::_thesis: ( rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h implies g = h ) assume ( rng g c= dom f & rng h c= dom f & dom g = dom h ) ; ::_thesis: ( f * g = f * h implies g = h ) then ( g is Function of (dom g),X & h is Function of (dom g),X ) by A3, Th2; hence ( f * g = f * h implies g = h ) by A6; ::_thesis: verum end; hence f is one-to-one by FUNCT_1:27; ::_thesis: verum end; theorem :: FUNCT_2:22 for X, Y, Z being set for f being Function of X,Y for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds rng f = Y proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds rng f = Y let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds rng f = Y let g be Function of Y,Z; ::_thesis: ( Z <> {} & rng (g * f) = Z & g is one-to-one implies rng f = Y ) assume that A1: Z <> {} and A2: rng (g * f) = Z and A3: g is one-to-one ; ::_thesis: rng f = Y A4: dom g = Y by A1, Def1; rng (g * f) c= rng g by RELAT_1:26; then rng g = rng (g * f) by A2, XBOOLE_0:def_10; then Y c= rng f by A3, A4, FUNCT_1:29; hence rng f = Y by XBOOLE_0:def_10; ::_thesis: verum end; definition let Y be set ; let f be Y -valued Relation; attrf is onto means :Def3: :: FUNCT_2:def 3 rng f = Y; end; :: deftheorem Def3 defines onto FUNCT_2:def_3_:_ for Y being set for f being b1 -valued Relation holds ( f is onto iff rng f = Y ); theorem :: FUNCT_2:23 for X, Y being set for f being Function of X,Y for g being Function of Y,X st g * f = id X holds ( f is one-to-one & g is onto ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,X st g * f = id X holds ( f is one-to-one & g is onto ) let f be Function of X,Y; ::_thesis: for g being Function of Y,X st g * f = id X holds ( f is one-to-one & g is onto ) let g be Function of Y,X; ::_thesis: ( g * f = id X implies ( f is one-to-one & g is onto ) ) assume A1: g * f = id X ; ::_thesis: ( f is one-to-one & g is onto ) thus f is one-to-one ::_thesis: g is onto proof percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: f is one-to-one hence f is one-to-one ; ::_thesis: verum end; suppose Y <> {} ; ::_thesis: f is one-to-one then dom f = X by Def1; hence f is one-to-one by A1, FUNCT_1:31; ::_thesis: verum end; end; end; rng (g * f) = X by A1, RELAT_1:45; then X c= rng g by RELAT_1:26; hence rng g = X by XBOOLE_0:def_10; :: according to FUNCT_2:def_3 ::_thesis: verum end; theorem :: FUNCT_2:24 for X, Y, Z being set for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds ( f is one-to-one & g is one-to-one ) proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds ( f is one-to-one & g is one-to-one ) let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y holds ( f is one-to-one & g is one-to-one ) let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) & g * f is one-to-one & rng f = Y implies ( f is one-to-one & g is one-to-one ) ) assume ( Z <> {} or Y = {} ) ; ::_thesis: ( not g * f is one-to-one or not rng f = Y or ( f is one-to-one & g is one-to-one ) ) then Y = dom g by Def1; hence ( not g * f is one-to-one or not rng f = Y or ( f is one-to-one & g is one-to-one ) ) by FUNCT_1:26; ::_thesis: verum end; theorem Th25: :: FUNCT_2:25 for X, Y being set for f being Function of X,Y st f is one-to-one & rng f = Y holds f " is Function of Y,X proof let X, Y be set ; ::_thesis: for f being Function of X,Y st f is one-to-one & rng f = Y holds f " is Function of Y,X let f be Function of X,Y; ::_thesis: ( f is one-to-one & rng f = Y implies f " is Function of Y,X ) assume that A1: f is one-to-one and A2: rng f = Y ; ::_thesis: f " is Function of Y,X A3: rng (f ") c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f ") or x in X ) assume x in rng (f ") ; ::_thesis: x in X then x in dom f by A1, FUNCT_1:33; hence x in X ; ::_thesis: verum end; dom (f ") = Y by A1, A2, FUNCT_1:33; then reconsider R = f " as Relation of Y,X by A3, RELSET_1:4; R is quasi_total proof percases ( X <> {} or X = {} ) ; :: according to FUNCT_2:def_1 case X <> {} ; ::_thesis: Y = dom R thus Y = dom R by A1, A2, FUNCT_1:33; ::_thesis: verum end; case X = {} ; ::_thesis: R = {} then rng f = {} ; then dom (f ") = {} by A1, FUNCT_1:32; hence R = {} ; ::_thesis: verum end; end; end; hence f " is Function of Y,X ; ::_thesis: verum end; theorem :: FUNCT_2:26 for X, Y, x being set for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds (f ") . (f . x) = x proof let X, Y, x be set ; ::_thesis: for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds (f ") . (f . x) = x let f be Function of X,Y; ::_thesis: ( Y <> {} & f is one-to-one & x in X implies (f ") . (f . x) = x ) assume Y <> {} ; ::_thesis: ( not f is one-to-one or not x in X or (f ") . (f . x) = x ) then dom f = X by Def1; hence ( not f is one-to-one or not x in X or (f ") . (f . x) = x ) by FUNCT_1:34; ::_thesis: verum end; theorem :: FUNCT_2:27 for X being set for Y, Z being non empty set for f being Function of X,Y for g being Function of Y,Z st f is onto & g is onto holds g * f is onto proof let X be set ; ::_thesis: for Y, Z being non empty set for f being Function of X,Y for g being Function of Y,Z st f is onto & g is onto holds g * f is onto let Y, Z be non empty set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st f is onto & g is onto holds g * f is onto let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is onto & g is onto holds g * f is onto let g be Function of Y,Z; ::_thesis: ( f is onto & g is onto implies g * f is onto ) assume that A1: f is onto and A2: g is onto ; ::_thesis: g * f is onto rng f = Y by A1, Def3 .= dom g by Def1 ; then rng (g * f) = rng g by RELAT_1:28 .= Z by A2, Def3 ; hence g * f is onto by Def3; ::_thesis: verum end; theorem :: FUNCT_2:28 for X, Y being set for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds ( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds g = f " proof let X, Y be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds ( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds g = f " let f be Function of X,Y; ::_thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds ( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds g = f " let g be Function of Y,X; ::_thesis: ( X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being set holds ( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) implies g = f " ) assume ( X <> {} & Y <> {} ) ; ::_thesis: ( not rng f = Y or not f is one-to-one or ex y, x being set st ( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " ) then ( dom f = X & dom g = Y ) by Def1; hence ( not rng f = Y or not f is one-to-one or ex y, x being set st ( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " ) by FUNCT_1:32; ::_thesis: verum end; theorem :: FUNCT_2:29 for X, Y being set for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds ( (f ") * f = id X & f * (f ") = id Y ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds ( (f ") * f = id X & f * (f ") = id Y ) let f be Function of X,Y; ::_thesis: ( Y <> {} & rng f = Y & f is one-to-one implies ( (f ") * f = id X & f * (f ") = id Y ) ) assume Y <> {} ; ::_thesis: ( not rng f = Y or not f is one-to-one or ( (f ") * f = id X & f * (f ") = id Y ) ) then dom f = X by Def1; hence ( not rng f = Y or not f is one-to-one or ( (f ") * f = id X & f * (f ") = id Y ) ) by FUNCT_1:39; ::_thesis: verum end; theorem :: FUNCT_2:30 for X, Y being set for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds g = f " proof let X, Y be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds g = f " let f be Function of X,Y; ::_thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds g = f " let g be Function of Y,X; ::_thesis: ( X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one implies g = f " ) assume ( X <> {} & Y <> {} ) ; ::_thesis: ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " ) then ( dom f = X & dom g = Y ) by Def1; hence ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " ) by FUNCT_1:41; ::_thesis: verum end; theorem :: FUNCT_2:31 for X, Y being set for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds f is one-to-one proof let X, Y be set ; ::_thesis: for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds f is one-to-one let f be Function of X,Y; ::_thesis: ( Y <> {} & ex g being Function of Y,X st g * f = id X implies f is one-to-one ) assume Y <> {} ; ::_thesis: ( for g being Function of Y,X holds not g * f = id X or f is one-to-one ) then A1: dom f = X by Def1; given g being Function of Y,X such that A2: g * f = id X ; ::_thesis: f is one-to-one thus f is one-to-one by A2, A1, FUNCT_1:31; ::_thesis: verum end; theorem Th32: :: FUNCT_2:32 for X, Y, Z being set for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds f | Z is Function of Z,Y proof let X, Y, Z be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds f | Z is Function of Z,Y let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & Z c= X implies f | Z is Function of Z,Y ) assume that A1: ( Y = {} implies X = {} ) and A2: Z c= X ; ::_thesis: f | Z is Function of Z,Y dom f = X by A1, Def1; then A3: Z = dom (f | Z) by A2, RELAT_1:62; rng (f | Z) c= Y ; then reconsider R = f | Z as Relation of Z,Y by A3, RELSET_1:4; R is quasi_total proof percases ( Y <> {} or Y = {} ) ; :: according to FUNCT_2:def_1 case Y <> {} ; ::_thesis: Z = dom R dom f = X by A1, Def1; hence Z = dom R by A2, RELAT_1:62; ::_thesis: verum end; case Y = {} ; ::_thesis: R = {} hence R = {} ; ::_thesis: verum end; end; end; hence f | Z is Function of Z,Y ; ::_thesis: verum end; theorem :: FUNCT_2:33 for X, Y, Z being set for f being Function of X,Y st X c= Z holds f | Z = f by RELSET_1:19; theorem :: FUNCT_2:34 for X, Y, x, Z being set for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds (Z |` f) . x = f . x proof let X, Y, x, Z be set ; ::_thesis: for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds (Z |` f) . x = f . x let f be Function of X,Y; ::_thesis: ( Y <> {} & x in X & f . x in Z implies (Z |` f) . x = f . x ) assume that A1: ( Y <> {} & x in X ) and A2: f . x in Z ; ::_thesis: (Z |` f) . x = f . x x in dom f by A1, Def1; then x in dom (Z |` f) by A2, FUNCT_1:54; hence (Z |` f) . x = f . x by FUNCT_1:55; ::_thesis: verum end; theorem :: FUNCT_2:35 for X, Y, P being set for f being Function of X,Y st Y <> {} holds for y being set st ex x being set st ( x in X & x in P & y = f . x ) holds y in f .: P proof let X, Y, P be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds for y being set st ex x being set st ( x in X & x in P & y = f . x ) holds y in f .: P let f be Function of X,Y; ::_thesis: ( Y <> {} implies for y being set st ex x being set st ( x in X & x in P & y = f . x ) holds y in f .: P ) assume Y <> {} ; ::_thesis: for y being set st ex x being set st ( x in X & x in P & y = f . x ) holds y in f .: P then A1: dom f = X by Def1; let y be set ; ::_thesis: ( ex x being set st ( x in X & x in P & y = f . x ) implies y in f .: P ) given x being set such that A2: ( x in X & x in P & y = f . x ) ; ::_thesis: y in f .: P thus y in f .: P by A1, A2, FUNCT_1:def_6; ::_thesis: verum end; theorem :: FUNCT_2:36 for X, Y, P being set for f being Function of X,Y holds f .: P c= Y ; theorem :: FUNCT_2:37 canceled; theorem :: FUNCT_2:38 for X, Y, Q being set for f being Function of X,Y st Y <> {} holds for x being set holds ( x in f " Q iff ( x in X & f . x in Q ) ) proof let X, Y, Q be set ; ::_thesis: for f being Function of X,Y st Y <> {} holds for x being set holds ( x in f " Q iff ( x in X & f . x in Q ) ) let f be Function of X,Y; ::_thesis: ( Y <> {} implies for x being set holds ( x in f " Q iff ( x in X & f . x in Q ) ) ) assume Y <> {} ; ::_thesis: for x being set holds ( x in f " Q iff ( x in X & f . x in Q ) ) then dom f = X by Def1; hence for x being set holds ( x in f " Q iff ( x in X & f . x in Q ) ) by FUNCT_1:def_7; ::_thesis: verum end; theorem :: FUNCT_2:39 for X, Y, Q being set for f being PartFunc of X,Y holds f " Q c= X ; theorem Th40: :: FUNCT_2:40 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds f " Y = X proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds f " Y = X let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f " Y = X ) (rng f) /\ Y = rng f by XBOOLE_1:28; then A1: f " Y = f " (rng f) by RELAT_1:133; assume ( Y <> {} or X = {} ) ; ::_thesis: f " Y = X then dom f = X by Def1; hence f " Y = X by A1, RELAT_1:134; ::_thesis: verum end; theorem :: FUNCT_2:41 for X, Y being set for f being Function of X,Y holds ( ( for y being set st y in Y holds f " {y} <> {} ) iff rng f = Y ) proof let X, Y be set ; ::_thesis: for f being Function of X,Y holds ( ( for y being set st y in Y holds f " {y} <> {} ) iff rng f = Y ) let f be Function of X,Y; ::_thesis: ( ( for y being set st y in Y holds f " {y} <> {} ) iff rng f = Y ) thus ( ( for y being set st y in Y holds f " {y} <> {} ) implies rng f = Y ) ::_thesis: ( rng f = Y implies for y being set st y in Y holds f " {y} <> {} ) proof assume for y being set st y in Y holds f " {y} <> {} ; ::_thesis: rng f = Y then Y c= rng f by FUNCT_1:73; hence rng f = Y by XBOOLE_0:def_10; ::_thesis: verum end; thus ( rng f = Y implies for y being set st y in Y holds f " {y} <> {} ) by FUNCT_1:72; ::_thesis: verum end; theorem Th42: :: FUNCT_2:42 for X, Y, P being set for f being Function of X,Y st ( Y = {} implies X = {} ) & P c= X holds P c= f " (f .: P) proof let X, Y, P be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & P c= X holds P c= f " (f .: P) let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & P c= X implies P c= f " (f .: P) ) assume ( Y <> {} or X = {} ) ; ::_thesis: ( not P c= X or P c= f " (f .: P) ) then dom f = X by Def1; hence ( not P c= X or P c= f " (f .: P) ) by FUNCT_1:76; ::_thesis: verum end; theorem :: FUNCT_2:43 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds f " (f .: X) = X proof let X, Y be set ; ::_thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) holds f " (f .: X) = X let f be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f " (f .: X) = X ) assume ( Y <> {} or X = {} ) ; ::_thesis: f " (f .: X) = X then A1: dom f = X by Def1; then f " (rng f) = X by RELAT_1:134; hence f " (f .: X) = X by A1, RELAT_1:113; ::_thesis: verum end; theorem :: FUNCT_2:44 for X, Y, Z, Q being set for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds f " Q c= (g * f) " (g .: Q) proof let X, Y, Z, Q be set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds f " Q c= (g * f) " (g .: Q) let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st ( Z = {} implies Y = {} ) holds f " Q c= (g * f) " (g .: Q) let g be Function of Y,Z; ::_thesis: ( ( Z = {} implies Y = {} ) implies f " Q c= (g * f) " (g .: Q) ) assume ( Z <> {} or Y = {} ) ; ::_thesis: f " Q c= (g * f) " (g .: Q) then A1: dom g = Y by Def1; rng f c= Y ; hence f " Q c= (g * f) " (g .: Q) by A1, FUNCT_1:90; ::_thesis: verum end; theorem :: FUNCT_2:45 for Y, P being set for f being Function of {},Y holds f .: P = {} ; theorem :: FUNCT_2:46 for Y, Q being set for f being Function of {},Y holds f " Q = {} ; theorem :: FUNCT_2:47 for x, Y being set for f being Function of {x},Y st Y <> {} holds f . x in Y proof let x, Y be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds f . x in Y let f be Function of {x},Y; ::_thesis: ( Y <> {} implies f . x in Y ) assume Y <> {} ; ::_thesis: f . x in Y then A1: dom f = {x} by Def1; rng f c= Y ; then {(f . x)} c= Y by A1, FUNCT_1:4; hence f . x in Y by ZFMISC_1:31; ::_thesis: verum end; theorem Th48: :: FUNCT_2:48 for x, Y being set for f being Function of {x},Y st Y <> {} holds rng f = {(f . x)} proof let x, Y be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds rng f = {(f . x)} let f be Function of {x},Y; ::_thesis: ( Y <> {} implies rng f = {(f . x)} ) assume Y <> {} ; ::_thesis: rng f = {(f . x)} then dom f = {x} by Def1; hence rng f = {(f . x)} by FUNCT_1:4; ::_thesis: verum end; theorem :: FUNCT_2:49 for x, Y, P being set for f being Function of {x},Y st Y <> {} holds f .: P c= {(f . x)} proof let x, Y, P be set ; ::_thesis: for f being Function of {x},Y st Y <> {} holds f .: P c= {(f . x)} let f be Function of {x},Y; ::_thesis: ( Y <> {} implies f .: P c= {(f . x)} ) f .: P c= rng f by RELAT_1:111; hence ( Y <> {} implies f .: P c= {(f . x)} ) by Th48; ::_thesis: verum end; theorem Th50: :: FUNCT_2:50 for X, y, x being set for f being Function of X,{y} st x in X holds f . x = y proof let X, y, x be set ; ::_thesis: for f being Function of X,{y} st x in X holds f . x = y let f be Function of X,{y}; ::_thesis: ( x in X implies f . x = y ) ( x in X implies f . x in {y} ) by Th5; hence ( x in X implies f . x = y ) by TARSKI:def_1; ::_thesis: verum end; theorem Th51: :: FUNCT_2:51 for X, y being set for f1, f2 being Function of X,{y} holds f1 = f2 proof let X, y be set ; ::_thesis: for f1, f2 being Function of X,{y} holds f1 = f2 let f1, f2 be Function of X,{y}; ::_thesis: f1 = f2 for x being set st x in X holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in X implies f1 . x = f2 . x ) assume A1: x in X ; ::_thesis: f1 . x = f2 . x then f1 . x = y by Th50; hence f1 . x = f2 . x by A1, Th50; ::_thesis: verum end; hence f1 = f2 by Th12; ::_thesis: verum end; theorem Th52: :: FUNCT_2:52 for X being set for f being Function of X,X holds dom f = X proof let X be set ; ::_thesis: for f being Function of X,X holds dom f = X ( X = {} implies X = {} ) ; hence for f being Function of X,X holds dom f = X by Def1; ::_thesis: verum end; registration let X, Y be set ; let f be quasi_total PartFunc of X,Y; let g be quasi_total PartFunc of X,X; clusterg * f -> quasi_total for PartFunc of X,Y; coherence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total proof percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total hence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total ; ::_thesis: verum end; supposeA1: Y <> {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total then dom f = X by Def1; then dom (f * g) = g " X by RELAT_1:147 .= dom g by RELSET_1:22 .= X by Th52 ; hence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total by A1, Def1; ::_thesis: verum end; end; end; end; registration let X, Y be set ; let f be quasi_total PartFunc of Y,Y; let g be quasi_total PartFunc of X,Y; clusterg * f -> quasi_total for PartFunc of X,Y; coherence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total proof percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total hence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total ; ::_thesis: verum end; supposeA1: Y <> {} ; ::_thesis: for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total dom f = Y by Th52; then dom (f * g) = g " Y by RELAT_1:147 .= dom g by RELSET_1:22 .= X by A1, Def1 ; hence for b1 being PartFunc of X,Y st b1 = f * g holds b1 is quasi_total by A1, Def1; ::_thesis: verum end; end; end; end; theorem Th53: :: FUNCT_2:53 for X being set for f, g being Relation of X,X st rng f = X & rng g = X holds rng (g * f) = X proof let X be set ; ::_thesis: for f, g being Relation of X,X st rng f = X & rng g = X holds rng (g * f) = X let f, g be Relation of X,X; ::_thesis: ( rng f = X & rng g = X implies rng (g * f) = X ) assume that A1: rng f = X and A2: rng g = X ; ::_thesis: rng (g * f) = X thus rng (g * f) = f .: X by A2, RELAT_1:127 .= X by A1, RELSET_1:22 ; ::_thesis: verum end; theorem :: FUNCT_2:54 for X being set for f, g being Function of X,X st g * f = f & rng f = X holds g = id X proof let X be set ; ::_thesis: for f, g being Function of X,X st g * f = f & rng f = X holds g = id X let f, g be Function of X,X; ::_thesis: ( g * f = f & rng f = X implies g = id X ) dom g = X by Th52; hence ( g * f = f & rng f = X implies g = id X ) by FUNCT_1:23; ::_thesis: verum end; theorem :: FUNCT_2:55 for X being set for f, g being Function of X,X st f * g = f & f is one-to-one holds g = id X proof let X be set ; ::_thesis: for f, g being Function of X,X st f * g = f & f is one-to-one holds g = id X let f, g be Function of X,X; ::_thesis: ( f * g = f & f is one-to-one implies g = id X ) A1: rng g c= X ; ( dom f = X & dom g = X ) by Th52; hence ( f * g = f & f is one-to-one implies g = id X ) by A1, FUNCT_1:28; ::_thesis: verum end; theorem Th56: :: FUNCT_2:56 for X being set for f being Function of X,X holds ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) proof let X be set ; ::_thesis: for f being Function of X,X holds ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) let f be Function of X,X; ::_thesis: ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) dom f = X by Th52; hence ( f is one-to-one iff for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 ) by FUNCT_1:def_4; ::_thesis: verum end; definition let X, Y be set ; let f be X -defined Y -valued Function; attrf is bijective means :Def4: :: FUNCT_2:def 4 ( f is one-to-one & f is onto ); end; :: deftheorem Def4 defines bijective FUNCT_2:def_4_:_ for X, Y being set for f being b1 -defined b2 -valued Function holds ( f is bijective iff ( f is one-to-one & f is onto ) ); registration let X, Y be set ; cluster Function-like bijective -> one-to-one onto for Element of bool [:X,Y:]; coherence for b1 being PartFunc of X,Y st b1 is bijective holds ( b1 is one-to-one & b1 is onto ) by Def4; cluster Function-like one-to-one onto -> bijective for Element of bool [:X,Y:]; coherence for b1 being PartFunc of X,Y st b1 is one-to-one & b1 is onto holds b1 is bijective by Def4; end; registration let X be set ; cluster Relation-like X -defined X -valued Function-like total quasi_total bijective for Element of bool [:X,X:]; existence ex b1 being Function of X,X st b1 is bijective proof take id X ; ::_thesis: id X is bijective thus ( id X is one-to-one & rng (id X) = X ) ; :: according to FUNCT_2:def_3,FUNCT_2:def_4 ::_thesis: verum end; end; definition let X be set ; mode Permutation of X is bijective Function of X,X; end; theorem Th57: :: FUNCT_2:57 for X being set for f being Function of X,X st f is one-to-one & rng f = X holds f is Permutation of X proof let X be set ; ::_thesis: for f being Function of X,X st f is one-to-one & rng f = X holds f is Permutation of X let f be Function of X,X; ::_thesis: ( f is one-to-one & rng f = X implies f is Permutation of X ) assume that A1: f is one-to-one and A2: rng f = X ; ::_thesis: f is Permutation of X f is onto by A2, Def3; hence f is Permutation of X by A1; ::_thesis: verum end; theorem :: FUNCT_2:58 for X being set for f being Function of X,X st f is one-to-one holds for x1, x2 being set st x1 in X & x2 in X & f . x1 = f . x2 holds x1 = x2 by Th56; registration let X be set ; let f, g be onto PartFunc of X,X; clusterg * f -> onto for PartFunc of X,X; coherence for b1 being PartFunc of X,X st b1 = f * g holds b1 is onto proof ( rng f = X & rng g = X ) by Def3; then rng (f * g) = X by Th53; hence for b1 being PartFunc of X,X st b1 = f * g holds b1 is onto by Def3; ::_thesis: verum end; end; registration let X be set ; let f, g be bijective Function of X,X; clusterf * g -> bijective for Function of X,X; coherence for b1 being Function of X,X st b1 = g * f holds b1 is bijective ; end; registration let X be set ; cluster reflexive Function-like total quasi_total -> bijective for Element of bool [:X,X:]; coherence for b1 being Function of X,X st b1 is reflexive & b1 is total holds b1 is bijective proof let f be Function of X,X; ::_thesis: ( f is reflexive & f is total implies f is bijective ) assume A1: ( f is reflexive & f is total ) ; ::_thesis: f is bijective A3: field f = (dom f) \/ (rng f) by RELAT_1:def_6; thus f is one-to-one :: according to FUNCT_2:def_4 ::_thesis: f is onto proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A4: x1 in dom f and A5: x2 in dom f and A6: f . x1 = f . x2 ; ::_thesis: x1 = x2 x1 in field f by A3, A4, XBOOLE_0:def_3; then [x1,x1] in f by A1, RELAT_2:def_1, RELAT_2:def_9; then A7: x1 = f . x1 by A4, FUNCT_1:def_2; x2 in field f by A3, A5, XBOOLE_0:def_3; then [x2,x2] in f by A1, RELAT_2:def_1, RELAT_2:def_9; hence x1 = x2 by A5, A6, A7, FUNCT_1:def_2; ::_thesis: verum end; thus rng f c= X ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: X c= rng f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in rng f ) assume x in X ; ::_thesis: x in rng f then x in dom f by PARTFUN1:def_2; then x in field f by A3, XBOOLE_0:def_3; then [x,x] in f by A1, RELAT_2:def_1, RELAT_2:def_9; hence x in rng f by XTUPLE_0:def_13; ::_thesis: verum end; end; definition let X be set ; let f be Permutation of X; :: original: " redefine funcf " -> Permutation of X; coherence f " is Permutation of X proof dom f = X by Th52; then A1: rng (f ") = X by FUNCT_1:33; rng f = X by Def3; then f " is Function of X,X by Th25; hence f " is Permutation of X by A1, Th57; ::_thesis: verum end; end; theorem :: FUNCT_2:59 for X being set for f, g being Permutation of X st g * f = g holds f = id X proof let X be set ; ::_thesis: for f, g being Permutation of X st g * f = g holds f = id X let f, g be Permutation of X; ::_thesis: ( g * f = g implies f = id X ) A1: rng f c= X ; ( dom f = X & dom g = X ) by Th52; hence ( g * f = g implies f = id X ) by A1, FUNCT_1:28; ::_thesis: verum end; theorem :: FUNCT_2:60 for X being set for f, g being Permutation of X st g * f = id X holds g = f " proof let X be set ; ::_thesis: for f, g being Permutation of X st g * f = id X holds g = f " let f, g be Permutation of X; ::_thesis: ( g * f = id X implies g = f " ) A1: dom f = X by Th52; ( rng f = X & dom g = X ) by Def3, Th52; hence ( g * f = id X implies g = f " ) by A1, FUNCT_1:41; ::_thesis: verum end; theorem :: FUNCT_2:61 for X being set for f being Permutation of X holds ( (f ") * f = id X & f * (f ") = id X ) proof let X be set ; ::_thesis: for f being Permutation of X holds ( (f ") * f = id X & f * (f ") = id X ) let f be Permutation of X; ::_thesis: ( (f ") * f = id X & f * (f ") = id X ) ( dom f = X & rng f = X ) by Def3, Th52; hence ( (f ") * f = id X & f * (f ") = id X ) by FUNCT_1:39; ::_thesis: verum end; theorem Th62: :: FUNCT_2:62 for X, P being set for f being Permutation of X st P c= X holds ( f .: (f " P) = P & f " (f .: P) = P ) proof let X, P be set ; ::_thesis: for f being Permutation of X st P c= X holds ( f .: (f " P) = P & f " (f .: P) = P ) let f be Permutation of X; ::_thesis: ( P c= X implies ( f .: (f " P) = P & f " (f .: P) = P ) ) assume A1: P c= X ; ::_thesis: ( f .: (f " P) = P & f " (f .: P) = P ) dom f = X by Th52; then A2: P c= f " (f .: P) by A1, FUNCT_1:76; ( f " (f .: P) c= P & rng f = X ) by Def3, FUNCT_1:82; hence ( f .: (f " P) = P & f " (f .: P) = P ) by A1, A2, FUNCT_1:77, XBOOLE_0:def_10; ::_thesis: verum end; registration let X be set ; let D be non empty set ; let Z be set ; let f be Function of X,D; let g be Function of D,Z; clusterf * g -> quasi_total for PartFunc of X,Z; coherence for b1 being PartFunc of X,Z st b1 = g * f holds b1 is quasi_total by Th13; end; definition let C be non empty set ; let D be set ; let f be Function of C,D; let c be Element of C; :: original: . redefine funcf . c -> Element of D; coherence f . c is Element of D proof ( not D is empty or D is empty ) ; hence f . c is Element of D by Th5, SUBSET_1:def_1; ::_thesis: verum end; end; scheme :: FUNCT_2:sch 3 FuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } : ex f being Function of F1(),F2() st for x being Element of F1() holds P1[x,f . x] provided A1: for x being Element of F1() ex y being Element of F2() st P1[x,y] proof defpred S1[ set , set ] means ( \$1 in F1() & \$2 in F2() & P1[\$1,\$2] ); A2: for x being set st x in F1() holds ex y being set st ( y in F2() & S1[x,y] ) proof let x be set ; ::_thesis: ( x in F1() implies ex y being set st ( y in F2() & S1[x,y] ) ) assume A3: x in F1() ; ::_thesis: ex y being set st ( y in F2() & S1[x,y] ) then ex y being Element of F2() st P1[x,y] by A1; hence ex y being set st ( y in F2() & S1[x,y] ) by A3; ::_thesis: verum end; consider f being Function of F1(),F2() such that A4: for x being set st x in F1() holds S1[x,f . x] from FUNCT_2:sch_1(A2); take f ; ::_thesis: for x being Element of F1() holds P1[x,f . x] let x be Element of F1(); ::_thesis: P1[x,f . x] thus P1[x,f . x] by A4; ::_thesis: verum end; scheme :: FUNCT_2:sch 4 LambdaD{ F1() -> non empty set , F2() -> non empty set , F3( Element of F1()) -> Element of F2() } : ex f being Function of F1(),F2() st for x being Element of F1() holds f . x = F3(x) proof defpred S1[ Element of F1(), set ] means \$2 = F3(\$1); A1: for x being Element of F1() ex y being Element of F2() st S1[x,y] ; thus ex f being Function of F1(),F2() st for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A1); ::_thesis: verum end; theorem Th63: :: FUNCT_2:63 for X, Y being set for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds f1 = f2 let f1, f2 be Function of X,Y; ::_thesis: ( ( for x being Element of X holds f1 . x = f2 . x ) implies f1 = f2 ) assume for x being Element of X holds f1 . x = f2 . x ; ::_thesis: f1 = f2 then for x being set st x in X holds f1 . x = f2 . x ; hence f1 = f2 by Th12; ::_thesis: verum end; theorem Th64: :: FUNCT_2:64 for X, Y, P being set for f being Function of X,Y for y being set st y in f .: P holds ex x being set st ( x in X & x in P & y = f . x ) proof let X, Y, P be set ; ::_thesis: for f being Function of X,Y for y being set st y in f .: P holds ex x being set st ( x in X & x in P & y = f . x ) let f be Function of X,Y; ::_thesis: for y being set st y in f .: P holds ex x being set st ( x in X & x in P & y = f . x ) let y be set ; ::_thesis: ( y in f .: P implies ex x being set st ( x in X & x in P & y = f . x ) ) assume y in f .: P ; ::_thesis: ex x being set st ( x in X & x in P & y = f . x ) then consider x being set such that A1: x in dom f and A2: ( x in P & y = f . x ) by FUNCT_1:def_6; take x ; ::_thesis: ( x in X & x in P & y = f . x ) thus x in X by A1; ::_thesis: ( x in P & y = f . x ) thus ( x in P & y = f . x ) by A2; ::_thesis: verum end; theorem :: FUNCT_2:65 for X, Y, P being set for f being Function of X,Y for y being set st y in f .: P holds ex c being Element of X st ( c in P & y = f . c ) proof let X, Y, P be set ; ::_thesis: for f being Function of X,Y for y being set st y in f .: P holds ex c being Element of X st ( c in P & y = f . c ) let f be Function of X,Y; ::_thesis: for y being set st y in f .: P holds ex c being Element of X st ( c in P & y = f . c ) let y be set ; ::_thesis: ( y in f .: P implies ex c being Element of X st ( c in P & y = f . c ) ) assume y in f .: P ; ::_thesis: ex c being Element of X st ( c in P & y = f . c ) then consider x being set such that A1: x in X and A2: ( x in P & y = f . x ) by Th64; reconsider c = x as Element of X by A1; take c ; ::_thesis: ( c in P & y = f . c ) thus ( c in P & y = f . c ) by A2; ::_thesis: verum end; begin theorem Th66: :: FUNCT_2:66 for X, Y, f being set st f in Funcs (X,Y) holds f is Function of X,Y proof let X, Y, f be set ; ::_thesis: ( f in Funcs (X,Y) implies f is Function of X,Y ) assume f in Funcs (X,Y) ; ::_thesis: f is Function of X,Y then ( ( not Y = {} or not X <> {} ) & ex f9 being Function st ( f9 = f & dom f9 = X & rng f9 c= Y ) ) by Def2; hence f is Function of X,Y by Def1, RELSET_1:4; ::_thesis: verum end; scheme :: FUNCT_2:sch 5 Lambda1C{ F1() -> set , F2() -> set , P1[ set ], F3( set ) -> set , F4( set ) -> set } : ex f being Function of F1(),F2() st for x being set st x in F1() holds ( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) provided A1: for x being set st x in F1() holds ( ( P1[x] implies F3(x) in F2() ) & ( P1[x] implies F4(x) in F2() ) ) proof A2: now__::_thesis:_(_F2()_=_{}_implies_not_F1()_<>_{}_) set x = the Element of F1(); assume A3: F2() = {} ; ::_thesis: not F1() <> {} assume A4: F1() <> {} ; ::_thesis: contradiction then ( P1[ the Element of F1()] implies F3( the Element of F1()) in F2() ) by A1; hence contradiction by A1, A3, A4; ::_thesis: verum end; consider f being Function such that A5: dom f = F1() and A6: for x being set st x in F1() holds ( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) from PARTFUN1:sch_1(); rng f c= F2() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in F2() ) assume y in rng f ; ::_thesis: y in F2() then consider x being set such that A7: x in dom f and A8: y = f . x by FUNCT_1:def_3; A9: ( P1[x] implies f . x = F4(x) ) by A5, A6, A7; ( P1[x] implies f . x = F3(x) ) by A5, A6, A7; hence y in F2() by A1, A5, A7, A8, A9; ::_thesis: verum end; then f is Function of F1(),F2() by A5, A2, Def1, RELSET_1:4; hence ex f being Function of F1(),F2() st for x being set st x in F1() holds ( ( P1[x] implies f . x = F3(x) ) & ( P1[x] implies f . x = F4(x) ) ) by A6; ::_thesis: verum end; theorem :: FUNCT_2:67 for X, Y being set for f being PartFunc of X,Y st dom f = X holds f is Function of X,Y proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st dom f = X holds f is Function of X,Y let f be PartFunc of X,Y; ::_thesis: ( dom f = X implies f is Function of X,Y ) rng f c= Y ; hence ( dom f = X implies f is Function of X,Y ) by Th2; ::_thesis: verum end; theorem :: FUNCT_2:68 for X, Y being set for f being PartFunc of X,Y st f is total holds f is Function of X,Y ; theorem :: FUNCT_2:69 for X, Y being set for f being PartFunc of X,Y st ( Y = {} implies X = {} ) & f is Function of X,Y holds f is total ; theorem :: FUNCT_2:70 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds <:f,X,Y:> is total ; registration let X be set ; let f be Function of X,X; cluster<:f,X,X:> -> total ; coherence <:f,X,X:> is total ; end; theorem Th71: :: FUNCT_2:71 for X, Y being set for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x let f be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x ) assume A1: ( Y = {} implies X = {} ) ; ::_thesis: ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x then reconsider g = f as Function of X,Y by A1; take g ; ::_thesis: for x being set st x in dom f holds g . x = f . x thus for x being set st x in dom f holds g . x = f . x ; ::_thesis: verum end; supposeA2: Y <> {} ; ::_thesis: ex g being Function of X,Y st for x being set st x in dom f holds g . x = f . x deffunc H1( set ) -> set = f . \$1; defpred S1[ set ] means \$1 in dom f; set y = the Element of Y; deffunc H2( set ) -> Element of Y = the Element of Y; A3: for x being set st x in X holds ( ( S1[x] implies H1(x) in Y ) & ( not S1[x] implies H2(x) in Y ) ) by A2, PARTFUN1:4; consider g being Function of X,Y such that A4: for x being set st x in X holds ( ( S1[x] implies g . x = H1(x) ) & ( not S1[x] implies g . x = H2(x) ) ) from FUNCT_2:sch_5(A3); take g ; ::_thesis: for x being set st x in dom f holds g . x = f . x thus for x being set st x in dom f holds g . x = f . x by A4; ::_thesis: verum end; end; end; theorem :: FUNCT_2:72 for X, Y being set holds Funcs (X,Y) c= PFuncs (X,Y) proof let X, Y be set ; ::_thesis: Funcs (X,Y) c= PFuncs (X,Y) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X,Y) or x in PFuncs (X,Y) ) assume x in Funcs (X,Y) ; ::_thesis: x in PFuncs (X,Y) then ex f being Function st ( x = f & dom f = X & rng f c= Y ) by Def2; hence x in PFuncs (X,Y) by PARTFUN1:def_3; ::_thesis: verum end; theorem :: FUNCT_2:73 for X, Y being set for f, g being Function of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds f = g by PARTFUN1:66; theorem :: FUNCT_2:74 for X being set for f, g being Function of X,X st f tolerates g holds f = g by PARTFUN1:66; theorem Th75: :: FUNCT_2:75 for X, Y being set for f being PartFunc of X,Y for g being Function of X,Y st ( Y = {} implies X = {} ) holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y for g being Function of X,Y st ( Y = {} implies X = {} ) holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) let f be PartFunc of X,Y; ::_thesis: for g being Function of X,Y st ( Y = {} implies X = {} ) holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) let g be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) ) assume ( Y = {} implies X = {} ) ; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) then dom g = X by Def1; hence ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) by PARTFUN1:53; ::_thesis: verum end; theorem :: FUNCT_2:76 for X being set for f being PartFunc of X,X for g being Function of X,X holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) proof let X be set ; ::_thesis: for f being PartFunc of X,X for g being Function of X,X holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) let f be PartFunc of X,X; ::_thesis: for g being Function of X,X holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) let g be Function of X,X; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) ( X = {} implies X = {} ) ; hence ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) by Th75; ::_thesis: verum end; theorem Th77: :: FUNCT_2:77 for X, Y being set for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds ex g being Function of X,Y st f tolerates g proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds ex g being Function of X,Y st f tolerates g let f be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st f tolerates g ) assume A1: ( Y = {} implies X = {} ) ; ::_thesis: ex g being Function of X,Y st f tolerates g then consider g being Function of X,Y such that A2: for x being set st x in dom f holds g . x = f . x by Th71; take g ; ::_thesis: f tolerates g thus f tolerates g by A1, A2, Th75; ::_thesis: verum end; theorem :: FUNCT_2:78 for X being set for f, g being PartFunc of X,X for h being Function of X,X st f tolerates h & g tolerates h holds f tolerates g by PARTFUN1:67; theorem :: FUNCT_2:79 for X, Y being set for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds ex h being Function of X,Y st ( f tolerates h & g tolerates h ) proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds ex h being Function of X,Y st ( f tolerates h & g tolerates h ) let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being Function of X,Y st ( f tolerates h & g tolerates h ) ) assume ( ( Y = {} implies X = {} ) & f tolerates g ) ; ::_thesis: ex h being Function of X,Y st ( f tolerates h & g tolerates h ) then ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) by PARTFUN1:68; hence ex h being Function of X,Y st ( f tolerates h & g tolerates h ) ; ::_thesis: verum end; theorem :: FUNCT_2:80 for X, Y being set for f being PartFunc of X,Y for g being Function of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds g in TotFuncs f by PARTFUN1:def_5; theorem :: FUNCT_2:81 for X being set for f being PartFunc of X,X for g being Function of X,X st f tolerates g holds g in TotFuncs f by PARTFUN1:def_5; theorem Th82: :: FUNCT_2:82 for X, Y being set for f being PartFunc of X,Y for g being set st g in TotFuncs f holds g is Function of X,Y proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y for g being set st g in TotFuncs f holds g is Function of X,Y let f be PartFunc of X,Y; ::_thesis: for g being set st g in TotFuncs f holds g is Function of X,Y let g be set ; ::_thesis: ( g in TotFuncs f implies g is Function of X,Y ) assume g in TotFuncs f ; ::_thesis: g is Function of X,Y then ex g9 being PartFunc of X,Y st ( g9 = g & g9 is total & f tolerates g9 ) by PARTFUN1:def_5; hence g is Function of X,Y ; ::_thesis: verum end; theorem :: FUNCT_2:83 for X, Y being set for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y) proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds TotFuncs f c= Funcs (X,Y) let f be PartFunc of X,Y; ::_thesis: TotFuncs f c= Funcs (X,Y) percases ( ( Y = {} & X <> {} ) or Y <> {} or X = {} ) ; suppose ( Y = {} & X <> {} ) ; ::_thesis: TotFuncs f c= Funcs (X,Y) hence TotFuncs f c= Funcs (X,Y) ; ::_thesis: verum end; supposeA1: ( Y <> {} or X = {} ) ; ::_thesis: TotFuncs f c= Funcs (X,Y) let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in TotFuncs f or g in Funcs (X,Y) ) assume g in TotFuncs f ; ::_thesis: g in Funcs (X,Y) then g is Function of X,Y by Th82; hence g in Funcs (X,Y) by A1, Th8; ::_thesis: verum end; end; end; theorem :: FUNCT_2:84 for X, Y being set holds TotFuncs <:{},X,Y:> = Funcs (X,Y) proof let X, Y be set ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y) percases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ; supposeA1: ( Y = {} & X <> {} ) ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y) then TotFuncs <:{},X,Y:> = {} ; hence TotFuncs <:{},X,Y:> = Funcs (X,Y) by A1; ::_thesis: verum end; supposeA2: ( Y = {} implies X = {} ) ; ::_thesis: TotFuncs <:{},X,Y:> = Funcs (X,Y) for g being set holds ( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) ) proof let g be set ; ::_thesis: ( g in TotFuncs <:{},X,Y:> iff g in Funcs (X,Y) ) thus ( g in TotFuncs <:{},X,Y:> implies g in Funcs (X,Y) ) ::_thesis: ( g in Funcs (X,Y) implies g in TotFuncs <:{},X,Y:> ) proof assume g in TotFuncs <:{},X,Y:> ; ::_thesis: g in Funcs (X,Y) then g is Function of X,Y by Th82; hence g in Funcs (X,Y) by A2, Th8; ::_thesis: verum end; assume A3: g in Funcs (X,Y) ; ::_thesis: g in TotFuncs <:{},X,Y:> then reconsider g9 = g as PartFunc of X,Y by Th66; A4: <:{},X,Y:> tolerates g9 by PARTFUN1:60; g is Function of X,Y by A3, Th66; hence g in TotFuncs <:{},X,Y:> by A2, A4, PARTFUN1:def_5; ::_thesis: verum end; hence TotFuncs <:{},X,Y:> = Funcs (X,Y) by TARSKI:1; ::_thesis: verum end; end; end; theorem :: FUNCT_2:85 for X, Y being set for f being Function of X,Y st ( Y = {} implies X = {} ) holds TotFuncs <:f,X,Y:> = {f} by PARTFUN1:72; theorem :: FUNCT_2:86 for X being set for f being Function of X,X holds TotFuncs <:f,X,X:> = {f} by PARTFUN1:72; theorem :: FUNCT_2:87 for X, y being set for f being PartFunc of X,{y} for g being Function of X,{y} holds TotFuncs f = {g} proof let X, y be set ; ::_thesis: for f being PartFunc of X,{y} for g being Function of X,{y} holds TotFuncs f = {g} let f be PartFunc of X,{y}; ::_thesis: for g being Function of X,{y} holds TotFuncs f = {g} let g be Function of X,{y}; ::_thesis: TotFuncs f = {g} for h being set holds ( h in TotFuncs f iff h = g ) proof let h be set ; ::_thesis: ( h in TotFuncs f iff h = g ) thus ( h in TotFuncs f implies h = g ) ::_thesis: ( h = g implies h in TotFuncs f ) proof assume h in TotFuncs f ; ::_thesis: h = g then h is Function of X,{y} by Th82; hence h = g by Th51; ::_thesis: verum end; f tolerates g by PARTFUN1:61; hence ( h = g implies h in TotFuncs f ) by PARTFUN1:def_5; ::_thesis: verum end; hence TotFuncs f = {g} by TARSKI:def_1; ::_thesis: verum end; theorem :: FUNCT_2:88 for X, Y being set for f, g being PartFunc of X,Y st g c= f holds TotFuncs f c= TotFuncs g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g c= f holds TotFuncs f c= TotFuncs g let f, g be PartFunc of X,Y; ::_thesis: ( g c= f implies TotFuncs f c= TotFuncs g ) assume A1: g c= f ; ::_thesis: TotFuncs f c= TotFuncs g let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in TotFuncs f or h in TotFuncs g ) assume A2: h in TotFuncs f ; ::_thesis: h in TotFuncs g then reconsider h9 = h as PartFunc of X,Y by PARTFUN1:69; A3: h9 is total by A2, PARTFUN1:70; g tolerates h9 by A1, A2, PARTFUN1:58, PARTFUN1:71; hence h in TotFuncs g by A3, PARTFUN1:def_5; ::_thesis: verum end; theorem Th89: :: FUNCT_2:89 for X, Y being set for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds g c= f proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds g c= f let f, g be PartFunc of X,Y; ::_thesis: ( dom g c= dom f & TotFuncs f c= TotFuncs g implies g c= f ) assume A1: dom g c= dom f ; ::_thesis: ( not TotFuncs f c= TotFuncs g or g c= f ) now__::_thesis:_(_not_TotFuncs_f_c=_TotFuncs_g_or_g_c=_f_) percases not ( not ( Y = {} & X <> {} ) & Y = {} & not X = {} ) ; suppose ( Y = {} & X <> {} ) ; ::_thesis: ( not TotFuncs f c= TotFuncs g or g c= f ) hence ( not TotFuncs f c= TotFuncs g or g c= f ) ; ::_thesis: verum end; supposeA2: ( Y = {} implies X = {} ) ; ::_thesis: ( TotFuncs f c= TotFuncs g implies g c= f ) thus ( TotFuncs f c= TotFuncs g implies g c= f ) ::_thesis: verum proof assume A3: TotFuncs f c= TotFuncs g ; ::_thesis: g c= f for x being set st x in dom g holds g . x = f . x proof let x be set ; ::_thesis: ( x in dom g implies g . x = f . x ) consider h being Function of X,Y such that A4: f tolerates h by A2, Th77; h in TotFuncs f by A2, A4, PARTFUN1:def_5; then B5: g tolerates h by A3, PARTFUN1:71; assume x in dom g ; ::_thesis: g . x = f . x then x in (dom f) /\ (dom g) by A1, XBOOLE_0:def_4; hence g . x = f . x by B5, PARTFUN1:def_4, A2, A4, PARTFUN1:67; ::_thesis: verum end; hence g c= f by A1, GRFUNC_1:2; ::_thesis: verum end; end; end; end; hence ( not TotFuncs f c= TotFuncs g or g c= f ) ; ::_thesis: verum end; theorem Th90: :: FUNCT_2:90 for X, Y being set for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds g c= f proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) holds g c= f let f, g be PartFunc of X,Y; ::_thesis: ( TotFuncs f c= TotFuncs g & ( for y being set holds Y <> {y} ) implies g c= f ) assume that A1: TotFuncs f c= TotFuncs g and A2: for y being set holds Y <> {y} ; ::_thesis: g c= f now__::_thesis:_dom_g_c=_dom_f percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: dom g c= dom f hence dom g c= dom f ; ::_thesis: verum end; supposeA3: Y <> {} ; ::_thesis: dom g c= dom f thus dom g c= dom f ::_thesis: verum proof deffunc H1( set ) -> set = f . \$1; defpred S1[ set ] means \$1 in dom f; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom f ) assume that A4: x in dom g and A5: not x in dom f ; ::_thesis: contradiction A6: Y <> {(g . x)} by A2; g . x in Y by A4, PARTFUN1:4; then consider y being set such that A7: y in Y and A8: y <> g . x by A6, ZFMISC_1:35; deffunc H2( set ) -> set = y; A9: for x9 being set st x9 in X holds ( ( S1[x9] implies H1(x9) in Y ) & ( not S1[x9] implies H2(x9) in Y ) ) by A7, PARTFUN1:4; consider h being Function of X,Y such that A10: for x9 being set st x9 in X holds ( ( S1[x9] implies h . x9 = H1(x9) ) & ( not S1[x9] implies h . x9 = H2(x9) ) ) from FUNCT_2:sch_5(A9); f tolerates h proof let x9 be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x9 in (proj1 f) /\ (proj1 h) or f . x9 = h . x9 ) assume x9 in (dom f) /\ (dom h) ; ::_thesis: f . x9 = h . x9 then x9 in dom f by XBOOLE_0:def_4; hence f . x9 = h . x9 by A10; ::_thesis: verum end; then B11: h in TotFuncs f by A3, PARTFUN1:def_5; x in X by A4; then x in dom h by A3, Def1; then A12: x in (dom g) /\ (dom h) by A4, XBOOLE_0:def_4; h . x = y by A4, A5, A10; hence contradiction by A8, B11, A12, PARTFUN1:def_4, A1, PARTFUN1:71; ::_thesis: verum end; end; end; end; hence g c= f by A1, Th89; ::_thesis: verum end; theorem :: FUNCT_2:91 for X, Y being set for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds f = g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g holds f = g let f, g be PartFunc of X,Y; ::_thesis: ( ( for y being set holds Y <> {y} ) & TotFuncs f = TotFuncs g implies f = g ) assume A1: for y being set holds Y <> {y} ; ::_thesis: ( not TotFuncs f = TotFuncs g or f = g ) assume TotFuncs f = TotFuncs g ; ::_thesis: f = g then ( g c= f & f c= g ) by A1, Th90; hence f = g by XBOOLE_0:def_10; ::_thesis: verum end; registration let A, B be non empty set ; cluster Function-like quasi_total -> non empty for Element of bool [:A,B:]; coherence for b1 being Function of A,B holds not b1 is empty by Def1, RELAT_1:38; end; begin scheme :: FUNCT_2:sch 6 LambdaSep1{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F2(), F5( set ) -> Element of F2() } : ex f being Function of F1(),F2() st ( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds f . x = F5(x) ) ) proof defpred S1[ set , set ] means ( ( \$1 = F3() implies \$2 = F4() ) & ( \$1 <> F3() implies \$2 = F5(\$1) ) ); A1: for x being Element of F1() ex y being Element of F2() st S1[x,y] proof let x be Element of F1(); ::_thesis: ex y being Element of F2() st S1[x,y] ( x = F3() implies ex y being Element of F2() st S1[x,y] ) ; hence ex y being Element of F2() st S1[x,y] ; ::_thesis: verum end; consider f being Function of F1(),F2() such that A2: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A1); take f ; ::_thesis: ( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds f . x = F5(x) ) ) thus ( f . F3() = F4() & ( for x being Element of F1() st x <> F3() holds f . x = F5(x) ) ) by A2; ::_thesis: verum end; scheme :: FUNCT_2:sch 7 LambdaSep2{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F2(), F6() -> Element of F2(), F7( set ) -> Element of F2() } : ex f being Function of F1(),F2() st ( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds f . x = F7(x) ) ) provided A1: F3() <> F4() proof defpred S1[ set , set ] means ( ( \$1 = F3() implies \$2 = F5() ) & ( \$1 = F4() implies \$2 = F6() ) & ( \$1 <> F3() & \$1 <> F4() implies \$2 = F7(\$1) ) ); A2: for x being Element of F1() ex y being Element of F2() st S1[x,y] proof let x be Element of F1(); ::_thesis: ex y being Element of F2() st S1[x,y] A3: ( x = F4() implies ex y being Element of F2() st S1[x,y] ) by A1; ( x = F3() implies ex y being Element of F2() st S1[x,y] ) by A1; hence ex y being Element of F2() st S1[x,y] by A3; ::_thesis: verum end; consider f being Function of F1(),F2() such that A4: for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A2); take f ; ::_thesis: ( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds f . x = F7(x) ) ) thus ( f . F3() = F5() & f . F4() = F6() & ( for x being Element of F1() st x <> F3() & x <> F4() holds f . x = F7(x) ) ) by A4; ::_thesis: verum end; theorem :: FUNCT_2:92 for A, B being set for f being Function st f in Funcs (A,B) holds ( dom f = A & rng f c= B ) proof let A, B be set ; ::_thesis: for f being Function st f in Funcs (A,B) holds ( dom f = A & rng f c= B ) let f be Function; ::_thesis: ( f in Funcs (A,B) implies ( dom f = A & rng f c= B ) ) assume f in Funcs (A,B) ; ::_thesis: ( dom f = A & rng f c= B ) then ex g being Function st ( f = g & dom g = A & rng g c= B ) by Def2; hence ( dom f = A & rng f c= B ) ; ::_thesis: verum end; scheme :: FUNCT_2:sch 8 FunctRealEx{ F1() -> non empty set , F2() -> set , F3( set ) -> set } : ex f being Function of F1(),F2() st for x being Element of F1() holds f . x = F3(x) provided A1: for x being Element of F1() holds F3(x) in F2() proof defpred S1[ set , set ] means \$2 = F3(\$1); A2: for x being set st x in F1() holds ex y being set st ( y in F2() & S1[x,y] ) by A1; ex f being Function of F1(),F2() st for x being set st x in F1() holds S1[x,f . x] from FUNCT_2:sch_1(A2); then consider f being Function of F1(),F2() such that A3: for x being set st x in F1() holds f . x = F3(x) ; for x being Element of F1() holds f . x = F3(x) by A3; hence ex f being Function of F1(),F2() st for x being Element of F1() holds f . x = F3(x) ; ::_thesis: verum end; scheme :: FUNCT_2:sch 9 KappaMD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> set } : ex f being Function of F1(),F2() st for x being Element of F1() holds f . x = F3(x) provided A1: for x being Element of F1() holds F3(x) is Element of F2() proof A2: now__::_thesis:_for_x_being_Element_of_F1()_holds_F3(x)_in_F2() let x be Element of F1(); ::_thesis: F3(x) in F2() F3(x) is Element of F2() by A1; hence F3(x) in F2() ; ::_thesis: verum end; consider f being Function of F1(),F2() such that A3: for x being Element of F1() holds f . x = F3(x) from FUNCT_2:sch_8(A2); take f ; ::_thesis: for x being Element of F1() holds f . x = F3(x) thus for x being Element of F1() holds f . x = F3(x) by A3; ::_thesis: verum end; definition let A, B, C be non empty set ; let f be Function of A,[:B,C:]; :: original: pr1 redefine func pr1 f -> Function of A,B means :Def5: :: FUNCT_2:def 5 for x being Element of A holds it . x = (f . x) `1 ; coherence pr1 f is Function of A,B proof A1: dom (pr1 f) = dom f by MCART_1:def_12; A2: rng (pr1 f) c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (pr1 f) or x in B ) assume x in rng (pr1 f) ; ::_thesis: x in B then consider y being set such that A3: ( y in dom (pr1 f) & x = (pr1 f) . y ) by FUNCT_1:def_3; ( x = (f . y) `1 & f . y in [:B,C:] ) by A1, A3, Th5, MCART_1:def_12; hence x in B by MCART_1:10; ::_thesis: verum end; dom (pr1 f) = A by A1, Def1; hence pr1 f is Function of A,B by A2, Th2; ::_thesis: verum end; compatibility for b1 being Function of A,B holds ( b1 = pr1 f iff for x being Element of A holds b1 . x = (f . x) `1 ) proof let IT be Function of A,B; ::_thesis: ( IT = pr1 f iff for x being Element of A holds IT . x = (f . x) `1 ) A4: dom (pr1 f) = dom f by MCART_1:def_12; then A5: dom (pr1 f) = A by Def1; hence ( IT = pr1 f implies for x being Element of A holds IT . x = (f . x) `1 ) by A4, MCART_1:def_12; ::_thesis: ( ( for x being Element of A holds IT . x = (f . x) `1 ) implies IT = pr1 f ) assume for x being Element of A holds IT . x = (f . x) `1 ; ::_thesis: IT = pr1 f then A6: for x being set st x in dom f holds IT . x = (f . x) `1 ; dom IT = dom f by A4, A5, Def1; hence IT = pr1 f by A6, MCART_1:def_12; ::_thesis: verum end; :: original: pr2 redefine func pr2 f -> Function of A,C means :Def6: :: FUNCT_2:def 6 for x being Element of A holds it . x = (f . x) `2 ; coherence pr2 f is Function of A,C proof A7: dom (pr2 f) = dom f by MCART_1:def_13; A8: rng (pr2 f) c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (pr2 f) or x in C ) assume x in rng (pr2 f) ; ::_thesis: x in C then consider y being set such that A9: ( y in dom (pr2 f) & x = (pr2 f) . y ) by FUNCT_1:def_3; ( x = (f . y) `2 & f . y in [:B,C:] ) by A7, A9, Th5, MCART_1:def_13; hence x in C by MCART_1:10; ::_thesis: verum end; dom (pr2 f) = A by A7, Def1; hence pr2 f is Function of A,C by A8, Th2; ::_thesis: verum end; compatibility for b1 being Function of A,C holds ( b1 = pr2 f iff for x being Element of A holds b1 . x = (f . x) `2 ) proof let IT be Function of A,C; ::_thesis: ( IT = pr2 f iff for x being Element of A holds IT . x = (f . x) `2 ) A10: dom (pr2 f) = dom f by MCART_1:def_13; then A11: dom (pr2 f) = A by Def1; hence ( IT = pr2 f implies for x being Element of A holds IT . x = (f . x) `2 ) by A10, MCART_1:def_13; ::_thesis: ( ( for x being Element of A holds IT . x = (f . x) `2 ) implies IT = pr2 f ) assume for x being Element of A holds IT . x = (f . x) `2 ; ::_thesis: IT = pr2 f then A12: for x being set st x in dom f holds IT . x = (f . x) `2 ; dom IT = dom f by A10, A11, Def1; hence IT = pr2 f by A12, MCART_1:def_13; ::_thesis: verum end; end; :: deftheorem Def5 defines pr1 FUNCT_2:def_5_:_ for A, B, C being non empty set for f being Function of A,[:B,C:] for b5 being Function of A,B holds ( b5 = pr1 f iff for x being Element of A holds b5 . x = (f . x) `1 ); :: deftheorem Def6 defines pr2 FUNCT_2:def_6_:_ for A, B, C being non empty set for f being Function of A,[:B,C:] for b5 being Function of A,C holds ( b5 = pr2 f iff for x being Element of A holds b5 . x = (f . x) `2 ); definition let A1 be set ; let B1 be non empty set ; let A2 be set ; let B2 be non empty set ; let f1 be Function of A1,B1; let f2 be Function of A2,B2; :: original: = redefine predf1 = f2 means :: FUNCT_2:def 7 ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ); compatibility ( f1 = f2 iff ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) ) proof A1: dom f1 = A1 by Def1; hence ( f1 = f2 implies ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) ) by Def1; ::_thesis: ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) implies f1 = f2 ) assume that A2: A1 = A2 and A3: for a being Element of A1 holds f1 . a = f2 . a ; ::_thesis: f1 = f2 A4: dom f2 = A2 by Def1; for a being set st a in A1 holds f1 . a = f2 . a by A3; hence f1 = f2 by A1, A4, A2, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem defines = FUNCT_2:def_7_:_ for A1 being set for B1 being non empty set for A2 being set for B2 being non empty set for f1 being Function of A1,B1 for f2 being Function of A2,B2 holds ( f1 = f2 iff ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) ); definition let A, B be set ; let f1, f2 be Function of A,B; :: original: = redefine predf1 = f2 means :: FUNCT_2:def 8 for a being Element of A holds f1 . a = f2 . a; compatibility ( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ) by Th63; end; :: deftheorem defines = FUNCT_2:def_8_:_ for A, B being set for f1, f2 being Function of A,B holds ( f1 = f2 iff for a being Element of A holds f1 . a = f2 . a ); theorem :: FUNCT_2:93 for N being set for f being Function of N,(bool N) ex R being Relation of N st for i being set st i in N holds Im (R,i) = f . i proof let N be set ; ::_thesis: for f being Function of N,(bool N) ex R being Relation of N st for i being set st i in N holds Im (R,i) = f . i let f be Function of N,(bool N); ::_thesis: ex R being Relation of N st for i being set st i in N holds Im (R,i) = f . i deffunc H1( set ) -> set = f . \$1; A1: for i being Element of N st i in [#] N holds H1(i) c= [#] N proof let i be Element of N; ::_thesis: ( i in [#] N implies H1(i) c= [#] N ) assume i in [#] N ; ::_thesis: H1(i) c= [#] N then f . i in bool N by Th5; hence H1(i) c= [#] N ; ::_thesis: verum end; consider R being Relation of ([#] N) such that A2: for i being Element of N st i in [#] N holds Im (R,i) = H1(i) from RELSET_1:sch_3(A1); reconsider R = R as Relation of N ; take R ; ::_thesis: for i being set st i in N holds Im (R,i) = f . i thus for i being set st i in N holds Im (R,i) = f . i by A2; ::_thesis: verum end; theorem Th94: :: FUNCT_2:94 for X being set for A being Subset of X holds (id X) " A = A proof let X be set ; ::_thesis: for A being Subset of X holds (id X) " A = A let A be Subset of X; ::_thesis: (id X) " A = A thus A = (id X) " ((id X) .: A) by Th62 .= (id X) " A by FUNCT_1:92 ; ::_thesis: verum end; theorem :: FUNCT_2:95 for A, B being non empty set for f being Function of A,B for A0 being Subset of A for B0 being Subset of B holds ( f .: A0 c= B0 iff A0 c= f " B0 ) proof let A, B be non empty set ; ::_thesis: for f being Function of A,B for A0 being Subset of A for B0 being Subset of B holds ( f .: A0 c= B0 iff A0 c= f " B0 ) let f be Function of A,B; ::_thesis: for A0 being Subset of A for B0 being Subset of B holds ( f .: A0 c= B0 iff A0 c= f " B0 ) let A0 be Subset of A; ::_thesis: for B0 being Subset of B holds ( f .: A0 c= B0 iff A0 c= f " B0 ) let B0 be Subset of B; ::_thesis: ( f .: A0 c= B0 iff A0 c= f " B0 ) thus ( f .: A0 c= B0 implies A0 c= f " B0 ) ::_thesis: ( A0 c= f " B0 implies f .: A0 c= B0 ) proof assume f .: A0 c= B0 ; ::_thesis: A0 c= f " B0 then A1: f " (f .: A0) c= f " B0 by RELAT_1:143; A0 c= f " (f .: A0) by Th42; hence A0 c= f " B0 by A1, XBOOLE_1:1; ::_thesis: verum end; thus ( A0 c= f " B0 implies f .: A0 c= B0 ) ::_thesis: verum proof assume A0 c= f " B0 ; ::_thesis: f .: A0 c= B0 then A2: f .: A0 c= f .: (f " B0) by RELAT_1:123; f .: (f " B0) c= B0 by FUNCT_1:75; hence f .: A0 c= B0 by A2, XBOOLE_1:1; ::_thesis: verum end; end; theorem :: FUNCT_2:96 for A, B being non empty set for f being Function of A,B for A0 being non empty Subset of A for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds f . c = f0 . c ) holds f | A0 = f0 proof let A, B be non empty set ; ::_thesis: for f being Function of A,B for A0 being non empty Subset of A for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds f . c = f0 . c ) holds f | A0 = f0 let f be Function of A,B; ::_thesis: for A0 being non empty Subset of A for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds f . c = f0 . c ) holds f | A0 = f0 let A0 be non empty Subset of A; ::_thesis: for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds f . c = f0 . c ) holds f | A0 = f0 let f0 be Function of A0,B; ::_thesis: ( ( for c being Element of A st c in A0 holds f . c = f0 . c ) implies f | A0 = f0 ) assume A1: for c being Element of A st c in A0 holds f . c = f0 . c ; ::_thesis: f | A0 = f0 reconsider g = f | A0 as Function of A0,B by Th32; for c being Element of A0 holds g . c = f0 . c proof let c be Element of A0; ::_thesis: g . c = f0 . c thus g . c = f . c by FUNCT_1:49 .= f0 . c by A1 ; ::_thesis: verum end; hence f | A0 = f0 by Th63; ::_thesis: verum end; theorem :: FUNCT_2:97 for f being Function for A0, C being set st C c= A0 holds f .: C = (f | A0) .: C proof let f be Function; ::_thesis: for A0, C being set st C c= A0 holds f .: C = (f | A0) .: C let A0, C be set ; ::_thesis: ( C c= A0 implies f .: C = (f | A0) .: C ) assume A1: C c= A0 ; ::_thesis: f .: C = (f | A0) .: C thus (f | A0) .: C = (f * (id A0)) .: C by RELAT_1:65 .= f .: ((id A0) .: C) by RELAT_1:126 .= f .: C by A1, FUNCT_1:92 ; ::_thesis: verum end; theorem :: FUNCT_2:98 for f being Function for A0, D being set st f " D c= A0 holds f " D = (f | A0) " D proof let f be Function; ::_thesis: for A0, D being set st f " D c= A0 holds f " D = (f | A0) " D let A0, D be set ; ::_thesis: ( f " D c= A0 implies f " D = (f | A0) " D ) assume A1: f " D c= A0 ; ::_thesis: f " D = (f | A0) " D thus (f | A0) " D = (f * (id A0)) " D by RELAT_1:65 .= (id A0) " (f " D) by RELAT_1:146 .= f " D by A1, Th94 ; ::_thesis: verum end; scheme :: FUNCT_2:sch 10 MChoice{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> set } : ex t being Function of F1(),F2() st for a being Element of F1() holds t . a in F3(a) provided A1: for a being Element of F1() holds F2() meets F3(a) proof defpred S1[ set , set ] means \$2 in F3(\$1); A2: for e being set st e in F1() holds ex u being set st ( u in F2() & S1[e,u] ) by A1, XBOOLE_0:3; consider t being Function such that A3: ( dom t = F1() & rng t c= F2() ) and A4: for e being set st e in F1() holds S1[e,t . e] from FUNCT_1:sch_5(A2); reconsider t = t as Function of F1(),F2() by A3, Def1, RELSET_1:4; take t ; ::_thesis: for a being Element of F1() holds t . a in F3(a) let a be Element of F1(); ::_thesis: t . a in F3(a) thus t . a in F3(a) by A4; ::_thesis: verum end; theorem Th99: :: FUNCT_2:99 for X, D being non empty set for p being Function of X,D for i being Element of X holds p /. i = p . i proof let X, D be non empty set ; ::_thesis: for p being Function of X,D for i being Element of X holds p /. i = p . i let p be Function of X,D; ::_thesis: for i being Element of X holds p /. i = p . i let i be Element of X; ::_thesis: p /. i = p . i i in X ; then i in dom p by Def1; hence p /. i = p . i by PARTFUN1:def_6; ::_thesis: verum end; registration let X, D be non empty set ; let p be Function of X,D; let i be Element of X; identifyp /. i with p . i; correctness compatibility p /. i = p . i; by Th99; end; theorem :: FUNCT_2:100 for S, X being set for f being Function of S,X for A being Subset of X st ( X = {} implies S = {} ) holds (f " A) ` = f " (A `) proof let S, X be set ; ::_thesis: for f being Function of S,X for A being Subset of X st ( X = {} implies S = {} ) holds (f " A) ` = f " (A `) let f be Function of S,X; ::_thesis: for A being Subset of X st ( X = {} implies S = {} ) holds (f " A) ` = f " (A `) let A be Subset of X; ::_thesis: ( ( X = {} implies S = {} ) implies (f " A) ` = f " (A `) ) assume A1: ( X = {} implies S = {} ) ; ::_thesis: (f " A) ` = f " (A `) A /\ (A `) = {} by XBOOLE_0:def_7, XBOOLE_1:79; then (f " A) /\ (f " (A `)) = f " ({} X) by FUNCT_1:68 .= {} ; then A2: f " A misses f " (A `) by XBOOLE_0:def_7; (f " A) \/ (f " (A `)) = f " (A \/ (A `)) by RELAT_1:140 .= f " ([#] X) by SUBSET_1:10 .= [#] S by A1, Th40 ; then ((f " A) `) /\ ((f " (A `)) `) = ([#] S) ` by XBOOLE_1:53 .= {} S by XBOOLE_1:37 ; then (f " A) ` misses (f " (A `)) ` by XBOOLE_0:def_7; hence (f " A) ` = f " (A `) by A2, SUBSET_1:25; ::_thesis: verum end; theorem :: FUNCT_2:101 for X, Y, Z being set for D being non empty set for f being Function of X,D st Y c= X & f .: Y c= Z holds f | Y is Function of Y,Z proof let X, Y, Z be set ; ::_thesis: for D being non empty set for f being Function of X,D st Y c= X & f .: Y c= Z holds f | Y is Function of Y,Z let D be non empty set ; ::_thesis: for f being Function of X,D st Y c= X & f .: Y c= Z holds f | Y is Function of Y,Z let f be Function of X,D; ::_thesis: ( Y c= X & f .: Y c= Z implies f | Y is Function of Y,Z ) assume that A1: Y c= X and A2: f .: Y c= Z ; ::_thesis: f | Y is Function of Y,Z dom f = X by Def1; then A3: dom (f | Y) = Y by A1, RELAT_1:62; A4: now__::_thesis:_(_Z_=_{}_implies_Y_=_{}_) assume Z = {} ; ::_thesis: Y = {} then rng (f | Y) = {} by A2, RELAT_1:115; hence Y = {} by A3, RELAT_1:42; ::_thesis: verum end; rng (f | Y) c= Z by A2, RELAT_1:115; hence f | Y is Function of Y,Z by A3, A4, Def1, RELSET_1:4; ::_thesis: verum end; definition let T, S be non empty set ; let f be Function of T,S; let G be Subset-Family of S; funcf " G -> Subset-Family of T means :Def9: :: FUNCT_2:def 9 for A being Subset of T holds ( A in it iff ex B being Subset of S st ( B in G & A = f " B ) ); existence ex b1 being Subset-Family of T st for A being Subset of T holds ( A in b1 iff ex B being Subset of S st ( B in G & A = f " B ) ) proof defpred S1[ Subset of T] means ex B being Subset of S st ( B in G & \$1 = f " B ); ex R being Subset-Family of T st for A being Subset of T holds ( A in R iff S1[A] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of T st for A being Subset of T holds ( A in b1 iff ex B being Subset of S st ( B in G & A = f " B ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of T st ( for A being Subset of T holds ( A in b1 iff ex B being Subset of S st ( B in G & A = f " B ) ) ) & ( for A being Subset of T holds ( A in b2 iff ex B being Subset of S st ( B in G & A = f " B ) ) ) holds b1 = b2 proof let R1, R2 be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds ( A in R1 iff ex B being Subset of S st ( B in G & A = f " B ) ) ) & ( for A being Subset of T holds ( A in R2 iff ex B being Subset of S st ( B in G & A = f " B ) ) ) implies R1 = R2 ) assume that A1: for A being Subset of T holds ( A in R1 iff ex B being Subset of S st ( B in G & A = f " B ) ) and A2: for A being Subset of T holds ( A in R2 iff ex B being Subset of S st ( B in G & A = f " B ) ) ; ::_thesis: R1 = R2 for x being set holds ( x in R1 iff x in R2 ) proof let x be set ; ::_thesis: ( x in R1 iff x in R2 ) thus ( x in R1 implies x in R2 ) ::_thesis: ( x in R2 implies x in R1 ) proof assume A3: x in R1 ; ::_thesis: x in R2 then reconsider x = x as Subset of T ; ex B being Subset of S st ( B in G & x = f " B ) by A1, A3; hence x in R2 by A2; ::_thesis: verum end; assume A4: x in R2 ; ::_thesis: x in R1 then reconsider x = x as Subset of T ; ex B being Subset of S st ( B in G & x = f " B ) by A2, A4; hence x in R1 by A1; ::_thesis: verum end; hence R1 = R2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def9 defines " FUNCT_2:def_9_:_ for T, S being non empty set for f being Function of T,S for G being Subset-Family of S for b5 being Subset-Family of T holds ( b5 = f " G iff for A being Subset of T holds ( A in b5 iff ex B being Subset of S st ( B in G & A = f " B ) ) ); theorem :: FUNCT_2:102 for T, S being non empty set for f being Function of T,S for A, B being Subset-Family of S st A c= B holds f " A c= f " B proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for A, B being Subset-Family of S st A c= B holds f " A c= f " B let f be Function of T,S; ::_thesis: for A, B being Subset-Family of S st A c= B holds f " A c= f " B let A, B be Subset-Family of S; ::_thesis: ( A c= B implies f " A c= f " B ) assume A1: A c= B ; ::_thesis: f " A c= f " B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " A or x in f " B ) assume A2: x in f " A ; ::_thesis: x in f " B then reconsider x = x as Subset of T ; ex C being Subset of S st ( C in B & x = f " C ) proof consider C being Subset of S such that A3: ( C in A & x = f " C ) by A2, Def9; take C ; ::_thesis: ( C in B & x = f " C ) thus ( C in B & x = f " C ) by A1, A3; ::_thesis: verum end; hence x in f " B by Def9; ::_thesis: verum end; definition let T, S be non empty set ; let f be Function of T,S; let G be Subset-Family of T; funcf .: G -> Subset-Family of S means :Def10: :: FUNCT_2:def 10 for A being Subset of S holds ( A in it iff ex B being Subset of T st ( B in G & A = f .: B ) ); existence ex b1 being Subset-Family of S st for A being Subset of S holds ( A in b1 iff ex B being Subset of T st ( B in G & A = f .: B ) ) proof thus ex R being Subset-Family of S st for A being Subset of S holds ( A in R iff ex B being Subset of T st ( B in G & A = f .: B ) ) ::_thesis: verum proof defpred S1[ Subset of S] means ex B being Subset of T st ( B in G & \$1 = f .: B ); ex R being Subset-Family of S st for A being Subset of S holds ( A in R iff S1[A] ) from SUBSET_1:sch_3(); hence ex R being Subset-Family of S st for A being Subset of S holds ( A in R iff ex B being Subset of T st ( B in G & A = f .: B ) ) ; ::_thesis: verum end; end; uniqueness for b1, b2 being Subset-Family of S st ( for A being Subset of S holds ( A in b1 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds ( A in b2 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ) holds b1 = b2 proof let R1, R2 be Subset-Family of S; ::_thesis: ( ( for A being Subset of S holds ( A in R1 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds ( A in R2 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ) implies R1 = R2 ) assume that A1: for A being Subset of S holds ( A in R1 iff ex B being Subset of T st ( B in G & A = f .: B ) ) and A2: for A being Subset of S holds ( A in R2 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ; ::_thesis: R1 = R2 for x being set holds ( x in R1 iff x in R2 ) proof let x be set ; ::_thesis: ( x in R1 iff x in R2 ) thus ( x in R1 implies x in R2 ) ::_thesis: ( x in R2 implies x in R1 ) proof assume A3: x in R1 ; ::_thesis: x in R2 then reconsider x = x as Subset of S ; ex B being Subset of T st ( B in G & x = f .: B ) by A1, A3; hence x in R2 by A2; ::_thesis: verum end; assume A4: x in R2 ; ::_thesis: x in R1 then reconsider x = x as Subset of S ; ex B being Subset of T st ( B in G & x = f .: B ) by A2, A4; hence x in R1 by A1; ::_thesis: verum end; hence R1 = R2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def10 defines .: FUNCT_2:def_10_:_ for T, S being non empty set for f being Function of T,S for G being Subset-Family of T for b5 being Subset-Family of S holds ( b5 = f .: G iff for A being Subset of S holds ( A in b5 iff ex B being Subset of T st ( B in G & A = f .: B ) ) ); theorem :: FUNCT_2:103 for T, S being non empty set for f being Function of T,S for A, B being Subset-Family of T st A c= B holds f .: A c= f .: B proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for A, B being Subset-Family of T st A c= B holds f .: A c= f .: B let f be Function of T,S; ::_thesis: for A, B being Subset-Family of T st A c= B holds f .: A c= f .: B let A, B be Subset-Family of T; ::_thesis: ( A c= B implies f .: A c= f .: B ) assume A1: A c= B ; ::_thesis: f .: A c= f .: B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: A or x in f .: B ) assume A2: x in f .: A ; ::_thesis: x in f .: B then reconsider x = x as Subset of S ; ex C being Subset of T st ( C in B & x = f .: C ) proof consider C being Subset of T such that A3: ( C in A & x = f .: C ) by A2, Def10; take C ; ::_thesis: ( C in B & x = f .: C ) thus ( C in B & x = f .: C ) by A1, A3; ::_thesis: verum end; hence x in f .: B by Def10; ::_thesis: verum end; theorem :: FUNCT_2:104 for T, S being non empty set for f being Function of T,S for B being Subset-Family of S for P being Subset of S st f .: (f " B) is Cover of P holds B is Cover of P proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for B being Subset-Family of S for P being Subset of S st f .: (f " B) is Cover of P holds B is Cover of P let f be Function of T,S; ::_thesis: for B being Subset-Family of S for P being Subset of S st f .: (f " B) is Cover of P holds B is Cover of P let B be Subset-Family of S; ::_thesis: for P being Subset of S st f .: (f " B) is Cover of P holds B is Cover of P let P be Subset of S; ::_thesis: ( f .: (f " B) is Cover of P implies B is Cover of P ) assume f .: (f " B) is Cover of P ; ::_thesis: B is Cover of P then A1: P c= union (f .: (f " B)) by SETFAM_1:def_11; P c= union B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union B ) assume x in P ; ::_thesis: x in union B then consider Y being set such that A2: x in Y and A3: Y in f .: (f " B) by A1, TARSKI:def_4; ex Z being set st ( x in Z & Z in B ) proof reconsider Y = Y as Subset of S by A3; consider Y1 being Subset of T such that A4: Y1 in f " B and A5: Y = f .: Y1 by A3, Def10; consider Y2 being Subset of S such that A6: ( Y2 in B & Y1 = f " Y2 ) by A4, Def9; A7: f .: (f " Y2) c= Y2 by FUNCT_1:75; reconsider Y2 = Y2 as set ; take Y2 ; ::_thesis: ( x in Y2 & Y2 in B ) thus ( x in Y2 & Y2 in B ) by A2, A5, A6, A7; ::_thesis: verum end; hence x in union B by TARSKI:def_4; ::_thesis: verum end; hence B is Cover of P by SETFAM_1:def_11; ::_thesis: verum end; theorem :: FUNCT_2:105 for T, S being non empty set for f being Function of T,S for B being Subset-Family of T for P being Subset of T st B is Cover of P holds f " (f .: B) is Cover of P proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for B being Subset-Family of T for P being Subset of T st B is Cover of P holds f " (f .: B) is Cover of P let f be Function of T,S; ::_thesis: for B being Subset-Family of T for P being Subset of T st B is Cover of P holds f " (f .: B) is Cover of P let B be Subset-Family of T; ::_thesis: for P being Subset of T st B is Cover of P holds f " (f .: B) is Cover of P let P be Subset of T; ::_thesis: ( B is Cover of P implies f " (f .: B) is Cover of P ) assume B is Cover of P ; ::_thesis: f " (f .: B) is Cover of P then A1: P c= union B by SETFAM_1:def_11; P c= union (f " (f .: B)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union (f " (f .: B)) ) assume x in P ; ::_thesis: x in union (f " (f .: B)) then consider Y being set such that A2: x in Y and A3: Y in B by A1, TARSKI:def_4; ex Z being set st ( x in Z & Z in f " (f .: B) ) proof reconsider Y = Y as Subset of T by A3; set Z = f " (f .: Y); take f " (f .: Y) ; ::_thesis: ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) ) dom f = T by Def1; then A4: Y c= f " (f .: Y) by FUNCT_1:76; f .: Y in f .: B by A3, Def10; hence ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) ) by A2, A4, Def9; ::_thesis: verum end; hence x in union (f " (f .: B)) by TARSKI:def_4; ::_thesis: verum end; hence f " (f .: B) is Cover of P by SETFAM_1:def_11; ::_thesis: verum end; theorem :: FUNCT_2:106 for T, S being non empty set for f being Function of T,S for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q let f be Function of T,S; ::_thesis: for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q let Q be Subset-Family of S; ::_thesis: union (f .: (f " Q)) c= union Q let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (f .: (f " Q)) or x in union Q ) thus ( x in union (f .: (f " Q)) implies x in union Q ) ::_thesis: verum proof assume x in union (f .: (f " Q)) ; ::_thesis: x in union Q then consider A being set such that A1: x in A and A2: A in f .: (f " Q) by TARSKI:def_4; reconsider A = A as Subset of S by A2; consider A1 being Subset of T such that A3: A1 in f " Q and A4: A = f .: A1 by A2, Def10; consider A2 being Subset of S such that A5: ( A2 in Q & A1 = f " A2 ) by A3, Def9; f .: (f " A2) c= A2 by FUNCT_1:75; hence x in union Q by A1, A4, A5, TARSKI:def_4; ::_thesis: verum end; end; theorem :: FUNCT_2:107 for T, S being non empty set for f being Function of T,S for P being Subset-Family of T holds union P c= union (f " (f .: P)) proof let T, S be non empty set ; ::_thesis: for f being Function of T,S for P being Subset-Family of T holds union P c= union (f " (f .: P)) let f be Function of T,S; ::_thesis: for P being Subset-Family of T holds union P c= union (f " (f .: P)) let P be Subset-Family of T; ::_thesis: union P c= union (f " (f .: P)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union P or x in union (f " (f .: P)) ) assume x in union P ; ::_thesis: x in union (f " (f .: P)) then consider A being set such that A1: x in A and A2: A in P by TARSKI:def_4; A3: A c= T by A2; reconsider A = A as Subset of T by A2; reconsider A1 = f .: A as Subset of S ; reconsider A2 = f " A1 as Subset of T ; A c= dom f by A3, Def1; then A4: A c= A2 by FUNCT_1:76; A1 in f .: P by A2, Def10; then A2 in f " (f .: P) by Def9; hence x in union (f " (f .: P)) by A1, A4, TARSKI:def_4; ::_thesis: verum end; definition let X, Z be set ; let Y be non empty set ; let f be Function of X,Y; let p be Z -valued Function; assume A1: rng f c= dom p ; funcp /* f -> Function of X,Z equals :Def11: :: FUNCT_2:def 11 p * f; coherence p * f is Function of X,Z proof dom f = X by Def1; then A2: dom (p * f) = X by A1, RELAT_1:27; then A3: p * f is total by PARTFUN1:def_2; rng (p * f) c= Z ; hence p * f is Function of X,Z by A3, A2, RELSET_1:4; ::_thesis: verum end; end; :: deftheorem Def11 defines /* FUNCT_2:def_11_:_ for X, Z being set for Y being non empty set for f being Function of X,Y for p being b2 -valued Function st rng f c= dom p holds p /* f = p * f; theorem Th108: :: FUNCT_2:108 for Z, X being set for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p . (f . x) proof let Z, X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p . (f . x) let Y be non empty set ; ::_thesis: for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p . (f . x) let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p . (f . x) let p be PartFunc of Y,Z; ::_thesis: for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p . (f . x) let x be Element of X; ::_thesis: ( X <> {} & rng f c= dom p implies (p /* f) . x = p . (f . x) ) assume that A1: X <> {} and A2: rng f c= dom p ; ::_thesis: (p /* f) . x = p . (f . x) p /* f = p * f by A2, Def11; hence (p /* f) . x = p . (f . x) by A1, Th15; ::_thesis: verum end; theorem Th109: :: FUNCT_2:109 for Z, X being set for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p /. (f . x) proof let Z, X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p /. (f . x) let Y be non empty set ; ::_thesis: for f being Function of X,Y for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p /. (f . x) let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p /. (f . x) let p be PartFunc of Y,Z; ::_thesis: for x being Element of X st X <> {} & rng f c= dom p holds (p /* f) . x = p /. (f . x) let x be Element of X; ::_thesis: ( X <> {} & rng f c= dom p implies (p /* f) . x = p /. (f . x) ) assume that A1: X <> {} and A2: rng f c= dom p ; ::_thesis: (p /* f) . x = p /. (f . x) A3: f . x in rng f by A1, Th4; thus (p /* f) . x = p . (f . x) by A1, A2, Th108 .= p /. (f . x) by A2, A3, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FUNCT_2:110 for Z, X being set for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for g being Function of X,X st rng f c= dom p holds (p /* f) * g = p /* (f * g) proof let Z, X be set ; ::_thesis: for Y being non empty set for f being Function of X,Y for p being PartFunc of Y,Z for g being Function of X,X st rng f c= dom p holds (p /* f) * g = p /* (f * g) let Y be non empty set ; ::_thesis: for f being Function of X,Y for p being PartFunc of Y,Z for g being Function of X,X st rng f c= dom p holds (p /* f) * g = p /* (f * g) let f be Function of X,Y; ::_thesis: for p being PartFunc of Y,Z for g being Function of X,X st rng f c= dom p holds (p /* f) * g = p /* (f * g) let p be PartFunc of Y,Z; ::_thesis: for g being Function of X,X st rng f c= dom p holds (p /* f) * g = p /* (f * g) let g be Function of X,X; ::_thesis: ( rng f c= dom p implies (p /* f) * g = p /* (f * g) ) A1: rng (f * g) c= rng f by RELAT_1:26; assume A2: rng f c= dom p ; ::_thesis: (p /* f) * g = p /* (f * g) hence (p /* f) * g = (p * f) * g by Def11 .= p * (f * g) by RELAT_1:36 .= p /* (f * g) by A2, A1, Def11, XBOOLE_1:1 ; ::_thesis: verum end; theorem :: FUNCT_2:111 for X, Y being non empty set for f being Function of X,Y holds ( f is constant iff ex y being Element of Y st rng f = {y} ) proof let X, Y be non empty set ; ::_thesis: for f being Function of X,Y holds ( f is constant iff ex y being Element of Y st rng f = {y} ) let f be Function of X,Y; ::_thesis: ( f is constant iff ex y being Element of Y st rng f = {y} ) hereby ::_thesis: ( ex y being Element of Y st rng f = {y} implies f is constant ) consider x being set such that A1: x in dom f by XBOOLE_0:def_1; set y = f . x; reconsider y = f . x as Element of Y by A1, Th5; assume A2: f is constant ; ::_thesis: ex y being Element of Y st rng f = {y} take y = y; ::_thesis: rng f = {y} for y9 being set holds ( y9 in rng f iff y9 = y ) proof let y9 be set ; ::_thesis: ( y9 in rng f iff y9 = y ) hereby ::_thesis: ( y9 = y implies y9 in rng f ) assume y9 in rng f ; ::_thesis: y9 = y then ex x9 being set st ( x9 in dom f & y9 = f . x9 ) by FUNCT_1:def_3; hence y9 = y by A2, A1, FUNCT_1:def_10; ::_thesis: verum end; assume y9 = y ; ::_thesis: y9 in rng f hence y9 in rng f by A1, Th4; ::_thesis: verum end; hence rng f = {y} by TARSKI:def_1; ::_thesis: verum end; given y being Element of Y such that A3: rng f = {y} ; ::_thesis: f is constant let x, x9 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in proj1 f or not x9 in proj1 f or f . x = f . x9 ) assume x in dom f ; ::_thesis: ( not x9 in proj1 f or f . x = f . x9 ) then A4: f . x in rng f by Th4; assume x9 in dom f ; ::_thesis: f . x = f . x9 then A5: f . x9 in rng f by Th4; thus f . x = y by A3, A4, TARSKI:def_1 .= f . x9 by A3, A5, TARSKI:def_1 ; ::_thesis: verum end; theorem :: FUNCT_2:112 for A, B being non empty set for x being Element of A for f being Function of A,B holds f . x in rng f proof let A, B be non empty set ; ::_thesis: for x being Element of A for f being Function of A,B holds f . x in rng f let x be Element of A; ::_thesis: for f being Function of A,B holds f . x in rng f let f be Function of A,B; ::_thesis: f . x in rng f dom f = A by Def1; hence f . x in rng f by FUNCT_1:def_3; ::_thesis: verum end; theorem Th113: :: FUNCT_2:113 for y, A, B being set for f being Function of A,B st y in rng f holds ex x being Element of A st y = f . x proof let y be set ; ::_thesis: for A, B being set for f being Function of A,B st y in rng f holds ex x being Element of A st y = f . x let A, B be set ; ::_thesis: for f being Function of A,B st y in rng f holds ex x being Element of A st y = f . x let f be Function of A,B; ::_thesis: ( y in rng f implies ex x being Element of A st y = f . x ) assume y in rng f ; ::_thesis: ex x being Element of A st y = f . x then consider x being set such that A1: x in A and A2: f . x = y by Th11; reconsider x = x as Element of A by A1; take x ; ::_thesis: y = f . x thus y = f . x by A2; ::_thesis: verum end; theorem :: FUNCT_2:114 for Z being set for A, B being non empty set for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds rng f c= Z proof let Z be set ; ::_thesis: for A, B being non empty set for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds rng f c= Z let A, B be non empty set ; ::_thesis: for f being Function of A,B st ( for x being Element of A holds f . x in Z ) holds rng f c= Z let f be Function of A,B; ::_thesis: ( ( for x being Element of A holds f . x in Z ) implies rng f c= Z ) assume A1: for x being Element of A holds f . x in Z ; ::_thesis: rng f c= Z let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Z ) assume y in rng f ; ::_thesis: y in Z then ex x being Element of A st f . x = y by Th113; hence y in Z by A1; ::_thesis: verum end; theorem :: FUNCT_2:115 for Y, X being non empty set for Z being set for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g . (f . x) proof let Y, X be non empty set ; ::_thesis: for Z being set for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g . (f . x) let Z be set ; ::_thesis: for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g . (f . x) let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g . (f . x) let g be PartFunc of Y,Z; ::_thesis: for x being Element of X st g is total holds (g /* f) . x = g . (f . x) let x be Element of X; ::_thesis: ( g is total implies (g /* f) . x = g . (f . x) ) assume g is total ; ::_thesis: (g /* f) . x = g . (f . x) then dom g = Y by PARTFUN1:def_2; then rng f c= dom g ; hence (g /* f) . x = g . (f . x) by Th108; ::_thesis: verum end; theorem :: FUNCT_2:116 for Y, X being non empty set for Z being set for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g /. (f . x) proof let Y, X be non empty set ; ::_thesis: for Z being set for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g /. (f . x) let Z be set ; ::_thesis: for f being Function of X,Y for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g /. (f . x) let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z for x being Element of X st g is total holds (g /* f) . x = g /. (f . x) let g be PartFunc of Y,Z; ::_thesis: for x being Element of X st g is total holds (g /* f) . x = g /. (f . x) let x be Element of X; ::_thesis: ( g is total implies (g /* f) . x = g /. (f . x) ) assume g is total ; ::_thesis: (g /* f) . x = g /. (f . x) then dom g = Y by PARTFUN1:def_2; then rng f c= dom g ; hence (g /* f) . x = g /. (f . x) by Th109; ::_thesis: verum end; theorem Th117: :: FUNCT_2:117 for X, Y being non empty set for Z, S being set for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) holds (g | S) /* f = g /* f proof let X, Y be non empty set ; ::_thesis: for Z, S being set for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) holds (g | S) /* f = g /* f let Z, S be set ; ::_thesis: for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) holds (g | S) /* f = g /* f let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) holds (g | S) /* f = g /* f let g be PartFunc of Y,Z; ::_thesis: ( rng f c= dom (g | S) implies (g | S) /* f = g /* f ) assume A1: rng f c= dom (g | S) ; ::_thesis: (g | S) /* f = g /* f let x be Element of X; :: according to FUNCT_2:def_8 ::_thesis: ((g | S) /* f) . x = (g /* f) . x A2: dom (g | S) c= dom g by RELAT_1:60; A3: f . x in rng f by Th4; thus ((g | S) /* f) . x = (g | S) . (f . x) by A1, Th108 .= g . (f . x) by A1, A3, FUNCT_1:47 .= (g /* f) . x by A1, A2, Th108, XBOOLE_1:1 ; ::_thesis: verum end; theorem :: FUNCT_2:118 for X, Y being non empty set for Z, S, T being set for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds (g | S) /* f = (g | T) /* f proof let X, Y be non empty set ; ::_thesis: for Z, S, T being set for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds (g | S) /* f = (g | T) /* f let Z, S, T be set ; ::_thesis: for f being Function of X,Y for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds (g | S) /* f = (g | T) /* f let f be Function of X,Y; ::_thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds (g | S) /* f = (g | T) /* f let g be PartFunc of Y,Z; ::_thesis: ( rng f c= dom (g | S) & S c= T implies (g | S) /* f = (g | T) /* f ) assume A1: rng f c= dom (g | S) ; ::_thesis: ( not S c= T or (g | S) /* f = (g | T) /* f ) assume S c= T ; ::_thesis: (g | S) /* f = (g | T) /* f then g | S c= g | T by RELAT_1:75; then A2: dom (g | S) c= dom (g | T) by RELAT_1:11; thus (g | S) /* f = g /* f by A1, Th117 .= (g | T) /* f by A1, A2, Th117, XBOOLE_1:1 ; ::_thesis: verum end; theorem :: FUNCT_2:119 for D, A, B being non empty set for H being Function of D,[:A,B:] for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)] proof let D, A, B be non empty set ; ::_thesis: for H being Function of D,[:A,B:] for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)] let H be Function of D,[:A,B:]; ::_thesis: for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)] let d be Element of D; ::_thesis: H . d = [((pr1 H) . d),((pr2 H) . d)] thus H . d = [((H . d) `1),((H . d) `2)] by MCART_1:21 .= [((H . d) `1),((pr2 H) . d)] by Def6 .= [((pr1 H) . d),((pr2 H) . d)] by Def5 ; ::_thesis: verum end; theorem :: FUNCT_2:120 for A1, A2, B1, B2 being set for f being Function of A1,A2 for g being Function of B1,B2 st f tolerates g holds f /\ g is Function of (A1 /\ B1),(A2 /\ B2) proof let A1, A2, B1, B2 be set ; ::_thesis: for f being Function of A1,A2 for g being Function of B1,B2 st f tolerates g holds f /\ g is Function of (A1 /\ B1),(A2 /\ B2) let f be Function of A1,A2; ::_thesis: for g being Function of B1,B2 st f tolerates g holds f /\ g is Function of (A1 /\ B1),(A2 /\ B2) let g be Function of B1,B2; ::_thesis: ( f tolerates g implies f /\ g is Function of (A1 /\ B1),(A2 /\ B2) ) assume A1: f tolerates g ; ::_thesis: f /\ g is Function of (A1 /\ B1),(A2 /\ B2) A2: ( dom (f /\ g) c= (dom f) /\ (dom g) & (dom f) /\ (dom g) c= A1 /\ B1 ) by RELAT_1:2, XBOOLE_1:27; A3: now__::_thesis:_(_dom_f_=_A1_&_A1_<>_{}_&_dom_g_=_B1_&_B1_<>_{}_implies_(_(_A1_/\_B1_<>_{}_implies_A2_/\_B2_<>_{}_)_&_dom_(f_/\_g)_=_A1_/\_B1_)_) set a = the Element of A1 /\ B1; assume that A4: dom f = A1 and A1 <> {} and A5: dom g = B1 and B1 <> {} ; ::_thesis: ( ( A1 /\ B1 <> {} implies A2 /\ B2 <> {} ) & dom (f /\ g) = A1 /\ B1 ) hereby ::_thesis: dom (f /\ g) = A1 /\ B1 assume A6: A1 /\ B1 <> {} ; ::_thesis: A2 /\ B2 <> {} then the Element of A1 /\ B1 in A1 by XBOOLE_0:def_4; then A7: f . the Element of A1 /\ B1 in rng f by A4, FUNCT_1:def_3; ( f . the Element of A1 /\ B1 = g . the Element of A1 /\ B1 & the Element of A1 /\ B1 in B1 ) by A1, A4, A5, A6, PARTFUN1:def_4, XBOOLE_0:def_4; then f . the Element of A1 /\ B1 in rng g by A5, FUNCT_1:def_3; hence A2 /\ B2 <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum end; thus dom (f /\ g) = A1 /\ B1 ::_thesis: verum proof thus dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: A1 /\ B1 c= dom (f /\ g) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 /\ B1 or a in dom (f /\ g) ) assume A8: a in A1 /\ B1 ; ::_thesis: a in dom (f /\ g) then a in A1 by XBOOLE_0:def_4; then A9: [a,(f . a)] in f by A4, FUNCT_1:def_2; ( f . a = g . a & a in B1 ) by A1, A4, A5, A8, PARTFUN1:def_4, XBOOLE_0:def_4; then [a,(f . a)] in g by A5, FUNCT_1:def_2; then [a,(f . a)] in f /\ g by A9, XBOOLE_0:def_4; hence a in dom (f /\ g) by XTUPLE_0:def_12; ::_thesis: verum end; end; ( rng (f /\ g) c= (rng f) /\ (rng g) & (rng f) /\ (rng g) c= A2 /\ B2 ) by RELAT_1:13, XBOOLE_1:27; then A10: rng (f /\ g) c= A2 /\ B2 by XBOOLE_1:1; A11: ( A2 = {} or A2 <> {} ) ; A12: ( B2 = {} or B2 <> {} ) ; A13: now__::_thesis:_(_(_A2_/\_B2_<>_{}_&_dom_(f_/\_g)_=_A1_/\_B1_)_or_(_A1_/\_B1_=_{}_&_dom_(f_/\_g)_=_A1_/\_B1_)_or_(_A2_/\_B2_=_{}_&_A1_/\_B1_<>_{}_&_f_/\_g_=_{}_)_) percases ( A2 /\ B2 <> {} or A1 /\ B1 = {} or ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ) ; case A2 /\ B2 <> {} ; ::_thesis: dom (f /\ g) = A1 /\ B1 hence dom (f /\ g) = A1 /\ B1 by A12, A3, Def1, A11; ::_thesis: verum end; case A1 /\ B1 = {} ; ::_thesis: dom (f /\ g) = A1 /\ B1 hence dom (f /\ g) = A1 /\ B1 by A2; ::_thesis: verum end; case ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ; ::_thesis: f /\ g = {} hence f /\ g = {} by A12, A3, Def1, A11; ::_thesis: verum end; end; end; dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1; hence f /\ g is Function of (A1 /\ B1),(A2 /\ B2) by A10, A13, Def1, RELSET_1:4; ::_thesis: verum end; registration let A, B be set ; cluster Funcs (A,B) -> functional ; coherence Funcs (A,B) is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in Funcs (A,B) or x is set ) assume x in Funcs (A,B) ; ::_thesis: x is set then ex f being Function st ( x = f & dom f = A & rng f c= B ) by Def2; hence x is set ; ::_thesis: verum end; end; definition let A, B be set ; mode FUNCTION_DOMAIN of A,B -> non empty set means :Def12: :: FUNCT_2:def 12 for x being Element of it holds x is Function of A,B; existence ex b1 being non empty set st for x being Element of b1 holds x is Function of A,B proof take IT = { the Function of A,B}; ::_thesis: for x being Element of IT holds x is Function of A,B let g be Element of IT; ::_thesis: g is Function of A,B thus g is Function of A,B by TARSKI:def_1; ::_thesis: verum end; end; :: deftheorem Def12 defines FUNCTION_DOMAIN FUNCT_2:def_12_:_ for A, B being set for b3 being non empty set holds ( b3 is FUNCTION_DOMAIN of A,B iff for x being Element of b3 holds x is Function of A,B ); registration let A, B be set ; cluster -> functional for FUNCTION_DOMAIN of A,B; coherence for b1 being FUNCTION_DOMAIN of A,B holds b1 is functional proof let F be FUNCTION_DOMAIN of A,B; ::_thesis: F is functional thus for x being set st x in F holds x is Function by Def12; :: according to FUNCT_1:def_13 ::_thesis: verum end; end; theorem :: FUNCT_2:121 for P, Q being set for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q proof let P, Q be set ; ::_thesis: for f being Function of P,Q holds {f} is FUNCTION_DOMAIN of P,Q let f be Function of P,Q; ::_thesis: {f} is FUNCTION_DOMAIN of P,Q for g being Element of {f} holds g is Function of P,Q by TARSKI:def_1; hence {f} is FUNCTION_DOMAIN of P,Q by Def12; ::_thesis: verum end; theorem Th122: :: FUNCT_2:122 for P being set for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B proof let P be set ; ::_thesis: for B being non empty set holds Funcs (P,B) is FUNCTION_DOMAIN of P,B let B be non empty set ; ::_thesis: Funcs (P,B) is FUNCTION_DOMAIN of P,B for f being Element of Funcs (P,B) holds f is Function of P,B by Th66; hence Funcs (P,B) is FUNCTION_DOMAIN of P,B by Def12; ::_thesis: verum end; definition let A be set ; let B be non empty set ; :: original: Funcs redefine func Funcs (A,B) -> FUNCTION_DOMAIN of A,B; coherence Funcs (A,B) is FUNCTION_DOMAIN of A,B by Th122; let F be FUNCTION_DOMAIN of A,B; :: original: Element redefine mode Element of F -> Function of A,B; coherence for b1 being Element of F holds b1 is Function of A,B by Def12; end; registration let I be set ; cluster id I -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = id I holds b1 is total ; end; definition let X, A be non empty set ; let F be Function of X,A; let x be set ; assume A1: x in X ; :: original: /. redefine funcF /. x -> Element of A equals :: FUNCT_2:def 13 F . x; compatibility for b1 being Element of A holds ( b1 = F /. x iff b1 = F . x ) proof let a be Element of A; ::_thesis: ( a = F /. x iff a = F . x ) x in dom F by A1, Def1; hence ( a = F /. x iff a = F . x ) by PARTFUN1:def_6; ::_thesis: verum end; end; :: deftheorem defines /. FUNCT_2:def_13_:_ for X, A being non empty set for F being Function of X,A for x being set st x in X holds F /. x = F . x; theorem :: FUNCT_2:123 for X being non empty set for f being Function of X,X for g being b1 -valued Function holds dom (f * g) = dom g proof let X be non empty set ; ::_thesis: for f being Function of X,X for g being X -valued Function holds dom (f * g) = dom g let f be Function of X,X; ::_thesis: for g being X -valued Function holds dom (f * g) = dom g let g be X -valued Function; ::_thesis: dom (f * g) = dom g dom f = X by Def1; then rng g c= dom f ; hence dom (f * g) = dom g by RELAT_1:27; ::_thesis: verum end; theorem :: FUNCT_2:124 for X being non empty set for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds f = id X proof let X be non empty set ; ::_thesis: for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds f = id X let f be Function of X,X; ::_thesis: ( ( for x being Element of X holds f . x = x ) implies f = id X ) assume A1: for x being Element of X holds f . x = x ; ::_thesis: f = id X let x be Element of X; :: according to FUNCT_2:def_8 ::_thesis: f . x = (id X) . x x = (id X) . x by FUNCT_1:18; hence f . x = (id X) . x by A1; ::_thesis: verum end; definition let O, E be set ; mode Action of O,E is Function of O,(Funcs (E,E)); end; theorem :: FUNCT_2:125 for x, A being set for f, g being Function of {x},A st f . x = g . x holds f = g proof let x, A be set ; ::_thesis: for f, g being Function of {x},A st f . x = g . x holds f = g let f, g be Function of {x},A; ::_thesis: ( f . x = g . x implies f = g ) assume A1: f . x = g . x ; ::_thesis: f = g now__::_thesis:_for_y_being_set_st_y_in_{x}_holds_ f_._y_=_g_._y let y be set ; ::_thesis: ( y in {x} implies f . y = g . y ) assume y in {x} ; ::_thesis: f . y = g . y then y = x by TARSKI:def_1; hence f . y = g . y by A1; ::_thesis: verum end; hence f = g by Th12; ::_thesis: verum end;