:: Functions from a Set to a Set
::  by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ZFMISC_1,
      RELAT_2, MCART_1, SETFAM_1, FUNCT_2, GROUP_9;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1,
      RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1;
 constructors RELAT_2, PARTFUN1, MCART_1, SETFAM_1, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1,
      GRFUNC_1, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin :: Function from a set into a set

reserve P,Q,X,Y,Z for set, p,x,x9,x1,x2,y,z for object;

definition
  let X,Y;
  let R be Relation of X,Y;
  attr R is quasi_total means
:: FUNCT_2:def 1

  X = dom R if Y <> {} otherwise R = {};
end;

registration
  let X,Y;
  cluster quasi_total for PartFunc of X,Y;
end;

registration
  let X,Y;
  cluster total -> quasi_total for Relation of X,Y;
end;

definition
  let X,Y;
  mode Function of X,Y is quasi_total PartFunc of X,Y;
end;

registration let X be empty set, Y be set;
 cluster quasi_total -> total for Relation of X,Y;
end;

registration let X be set, Y be non empty set;
 cluster quasi_total -> total for Relation of X,Y;
end;

registration let X be set;
 cluster quasi_total -> total for Relation of X,X;
end;

registration let X be set;
 cluster quasi_total -> total for Relation of [:X,X:],X;
end;

theorem :: FUNCT_2:1
  for f being Function holds f is Function of dom f, rng f;

theorem :: FUNCT_2:2
  for f being Function st rng f c= Y holds f is Function of dom f, Y;

theorem :: FUNCT_2:3
  for f being Function st dom f = X & for x st x in X holds f.x in Y
  holds f is Function of X,Y;

theorem :: FUNCT_2:4
  for f being Function of X,Y st Y <> {} & x in X holds f.x in rng f;

theorem :: FUNCT_2:5
  for f being Function of X,Y st Y <> {} & x in X holds f.x in Y;

theorem :: FUNCT_2:6
  for f being Function of X,Y st (Y = {} implies X = {}) & rng f c= Z
  holds f is Function of X,Z;

theorem :: FUNCT_2:7
  for f being Function of X,Y st (Y = {} implies X = {}) & Y c= Z holds
  f is Function of X,Z;

scheme :: FUNCT_2:sch 1
  FuncEx1{X, Y() -> set, P[object,object]}:
 ex f being Function of X(),Y() st
   for x being object st x in X() holds P[x,f.x]
provided
 for x being object st x in X() ex y being object st y in Y() & P[x,y];

scheme :: FUNCT_2:sch 2
  Lambda1{X, Y() -> set, F(object)->object}:
 ex f being Function of X(),Y() st
  for x being object st x in X() holds f.x = F(x)
provided
 for x being object st x in X() holds F(x) in Y();

definition
  let X,Y;
  func Funcs(X,Y) -> set means
:: FUNCT_2:def 2

  x in it iff ex f being Function st x = f & dom f = X & rng f c= Y;
end;

theorem :: FUNCT_2:8
  for f being Function of X,Y st Y = {} implies X = {} holds f in Funcs(X,Y);

theorem :: FUNCT_2:9
  for f being Function of X,X holds f in Funcs(X,X);

registration
  let X be set, Y be non empty set;
  cluster Funcs(X,Y) -> non empty;
end;

registration
  let X be set;
  cluster Funcs(X,X) -> non empty;
end;

registration
  let X be non empty set, Y be empty set;
  cluster Funcs(X,Y) -> empty;
end;

theorem :: FUNCT_2:10
  for f being Function of X,Y st for y being object st y in Y
   ex x being object st x in X & y = f.x
  holds rng f = Y;

theorem :: FUNCT_2:11
  for f being Function of X,Y st y in rng f
    ex x being object st x in X & f.x = y;

theorem :: FUNCT_2:12
  for f1,f2 being Function of X,Y st
  for x being object st x in X holds f1.x = f2.x
  holds f1 = f2;

theorem :: FUNCT_2:13
  for f being quasi_total Relation of X,Y for g being quasi_total
  Relation of Y,Z st Y = {} implies Z = {} or X = {} holds f*g is quasi_total;

theorem :: FUNCT_2:14
  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;

theorem :: FUNCT_2:15
  for x being object
  for f being Function of X,Y, g being Function st Y <> {} & x in
  X holds (g*f).x = g.(f.x);

theorem :: FUNCT_2:16
  for f being Function of X,Y st Y <> {} holds rng f = Y iff for Z st Z
  <> {} for g,h being Function of Y,Z st g*f = h*f holds g = h;

theorem :: FUNCT_2:17
  for f being Relation of X,Y holds (id X)*f = f & f*(id Y) = f;

theorem :: FUNCT_2:18
  for f being Function of X,Y for g being Function of Y,X st f*g = id Y
  holds rng f = Y;

theorem :: FUNCT_2:19
  for f being Function of X,Y st Y = {} implies X = {} holds f is
  one-to-one iff
  for x1,x2 being object st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2;

theorem :: FUNCT_2:20
  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;

theorem :: FUNCT_2:21
  for f being Function of X,Y st X <> {} & Y <> {} holds f is one-to-one
  iff for Z for g,h being Function of Z,X st f*g = f*h holds g = h;

theorem :: FUNCT_2:22
  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;

definition
  let Y be set;
  let f be Y-valued Relation;
  attr f is onto means
:: FUNCT_2:def 3

  rng f = Y;
end;

theorem :: FUNCT_2:23
  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;

theorem :: FUNCT_2:24
  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;

theorem :: FUNCT_2:25
  for f being Function of X,Y st f is one-to-one & rng f = Y holds
  f" is Function of Y,X;

theorem :: FUNCT_2:26
  for f being Function of X,Y st Y <> {} & f is one-to-one & x in X
  holds (f").(f.x) = x;

theorem :: FUNCT_2:27
  for X be set, Y,Z be non empty set for f be Function of X,Y
  for g be Function of Y,Z holds f is onto & g is onto implies g*f is onto;

theorem :: FUNCT_2:28
  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 object holds y in Y & g.y = x iff x in X
  & f.x = y holds g = f";

theorem :: FUNCT_2:29
  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;

theorem :: FUNCT_2:30
  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";

theorem :: FUNCT_2:31
  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;

theorem :: FUNCT_2:32
  for f being Function of X,Y st (Y = {} implies X = {}) & Z c= X
  holds f|Z is Function of Z,Y;

theorem :: FUNCT_2:33
  for f being Function of X,Y st X c= Z holds f|Z = f;

theorem :: FUNCT_2:34
  for f being Function of X,Y st Y <> {} & x in X & f.x in Z holds (Z|`f)
  .x = f.x;

theorem :: FUNCT_2:35
  for f being Function of X,Y st Y <> {} for y holds (ex x st x in X & x
  in P & y = f.x) implies y in f.:P;

theorem :: FUNCT_2:36
  for f being Function of X,Y holds f.:P c= Y;

::$CT

theorem :: FUNCT_2:38
  for f being Function of X,Y st Y <> {} for x holds x in f"Q iff x in X
  & f.x in Q;

theorem :: FUNCT_2:39
  for f being PartFunc of X,Y holds f"Q c= X;

theorem :: FUNCT_2:40
  for f being Function of X,Y st Y = {} implies X = {} holds f"Y = X;

theorem :: FUNCT_2:41
  for f being Function of X,Y holds
(for y being object st y in Y holds f"{y} <> {})
  iff rng f = Y;

theorem :: FUNCT_2:42
  for f being Function of X,Y st (Y = {} implies X = {}) & P c= X
  holds P c= f"(f.:P);

theorem :: FUNCT_2:43
  for f being Function of X,Y st Y = {} implies X = {} holds f"(f.:X) = X;

theorem :: FUNCT_2:44
  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);

theorem :: FUNCT_2:45
  for f being Function of {},Y holds f.:P = {};

theorem :: FUNCT_2:46
  for f being Function of {},Y holds f"Q = {};

theorem :: FUNCT_2:47
  for x being object
  for f being Function of {x},Y st Y <> {} holds f.x in Y;

theorem :: FUNCT_2:48
  for x being object
  for f being Function of {x},Y st Y <> {} holds rng f = {f.x};

theorem :: FUNCT_2:49
  for x being object
  for f being Function of {x},Y st Y <> {} holds f.:P c= {f.x};

theorem :: FUNCT_2:50
  for y being object
  for f being Function of X,{y} st x in X holds f.x = y;

theorem :: FUNCT_2:51
  for y being object
  for f1,f2 being Function of X,{y} holds f1 = f2;

theorem :: FUNCT_2:52
  for f being Function of X,X holds dom f = X;

registration
  let X,Y be set;
  let f be quasi_total PartFunc of X,Y;
  let g be quasi_total PartFunc of X,X;
  cluster f*g -> quasi_total for PartFunc of X,Y;
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;
  cluster f*g -> quasi_total for PartFunc of X,Y;
end;

theorem :: FUNCT_2:53
  for f,g being Relation of X,X st rng f = X & rng g = X holds rng (g*f) = X;

theorem :: FUNCT_2:54
  for f,g being Function of X,X st g*f = f & rng f = X holds g = id X;

theorem :: FUNCT_2:55
  for f,g being Function of X,X st f*g = f & f is one-to-one holds g = id X;

theorem :: FUNCT_2:56
  for f being Function of X,X holds f is one-to-one iff
  for x1,x2 being object
  st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2;

definition
  let X, Y;
  let f be X-defined Y-valued Function;
  attr f is bijective means
:: FUNCT_2:def 4

  f is one-to-one onto;
end;

registration
  let X, Y be set;
  cluster bijective -> one-to-one onto for PartFunc of X,Y;
  cluster one-to-one onto -> bijective for PartFunc of X,Y;
end;

registration
  let X;
  cluster bijective for Function of X,X;
end;

definition
  let X;
  mode Permutation of X is bijective Function of X,X;
end;

theorem :: FUNCT_2:57
  for f being Function of X, X st f is one-to-one & rng f = X
  holds f is Permutation of X;

theorem :: FUNCT_2:58
  for f being Function of X,X st f is one-to-one holds for x1,x2 st x1
  in X & x2 in X & f.x1 = f.x2 holds x1 = x2;

registration
  let X;
  let f,g be onto PartFunc of X,X;
  cluster f*g -> onto for PartFunc of X,X;
end;

registration
  let X;
  let f,g be bijective Function of X,X;
  cluster g*f -> bijective for Function of X,X;
end;

registration
  let X;
  cluster reflexive total -> bijective for Function of X,X;
end;

definition
  let X;
  let f be Permutation of X;
  redefine func f" -> Permutation of X;
end;

theorem :: FUNCT_2:59
  for f,g being Permutation of X st g*f = g holds f = id X;

theorem :: FUNCT_2:60
  for f,g being Permutation of X st g*f = id X holds g = f";

theorem :: FUNCT_2:61
  for f being Permutation of X holds (f")*f =id X & f*(f") = id X;

theorem :: FUNCT_2:62
  for f being Permutation of X st P c= X holds f.:(f"P) = P & f"(f .:P) = P;

reserve D for non empty set;

registration
  let X,D,Z;
  let f be Function of X,D;
  let g be Function of D,Z;
  cluster g*f -> quasi_total for PartFunc of X,Z;
end;

definition
  let C be non empty set, D be set;
  let f be Function of C,D;
  let c be Element of C;
  redefine func f.c -> Element of D;
end;

scheme :: FUNCT_2:sch 3
  FuncExD{C, D() -> non empty set, P[object,object]}:
 ex f being Function of C(),D()
  st for x being Element of C() holds P[x,f.x]
provided
 for x being Element of C() ex y being Element of D() st P[x,y];

scheme :: FUNCT_2:sch 4
  LambdaD{C, D() -> non empty set, F(Element of C()) -> Element of D()}: ex f
being Function of C(),D() st for x being Element of C() holds f.x = F(x);

theorem :: FUNCT_2:63
  for f1,f2 being Function of X,Y st for x being Element of X
  holds f1.x = f2.x holds f1 = f2;

theorem :: FUNCT_2:64
  for P being set for f being Function of X,Y
   for y holds y in f.:P implies ex x st x in X & x in P & y = f.x;

theorem :: FUNCT_2:65
  for f being Function of X,Y for y st y in f.:P ex c being Element of X
  st c in P & y = f.c;

begin :: PARTFUN1

theorem :: FUNCT_2:66
  for f being set st f in Funcs(X,Y) holds f is Function of X,Y;

scheme :: FUNCT_2:sch 5
  Lambda1C{A, B() -> set, C[object], F, G(object)->object}:
  ex f being
  Function of A(),B() st
 for x being object st x in A() holds (C[ x] implies f.x = F(x)) & (
  not C[ x] implies f.x = G(x))
provided
 for x being object st x in A()
  holds (C[ x] implies F(x) in B()) & (not C[ x]
implies G(x) in B());

theorem :: FUNCT_2:67
  for f being PartFunc of X,Y st dom f = X holds f is Function of X,Y;

theorem :: FUNCT_2:68
  for f being PartFunc of X,Y st f is total holds f is Function of X,Y;

theorem :: FUNCT_2:69
  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 f being Function of X,Y st (Y = {} implies X = {}) holds
  <:f,X,Y:> is total;

registration
  let X; let f be Function of X,X;
  cluster <:f,X,X:> -> total;
end;

theorem :: FUNCT_2:71
  for f being PartFunc of X,Y st Y = {} implies X = {} ex g being
  Function of X,Y st for x being object st x in dom f holds g.x = f.x;

theorem :: FUNCT_2:72
  Funcs(X,Y) c= PFuncs(X,Y);

theorem :: FUNCT_2:73
  for f,g being Function of X,Y st (Y = {} implies X = {}) & f
  tolerates g holds f = g;

theorem :: FUNCT_2:74
  for f,g being Function of X,X st f tolerates g holds f = g;

theorem :: FUNCT_2:75
  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 object st x in dom f holds f.x = g.x;

theorem :: FUNCT_2:76
  for f being PartFunc of X,X for g being Function of X,X holds f
  tolerates g iff for x being object st x in dom f holds f.x = g.x;

theorem :: FUNCT_2:77
  for f being PartFunc of X,Y st Y = {} implies X = {} ex g being
  Function of X,Y st f tolerates g;

theorem :: FUNCT_2:78
  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;

theorem :: FUNCT_2:79
  for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates
  g ex h being Function of X,Y st f tolerates h & g tolerates h;

theorem :: FUNCT_2:80
  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;

theorem :: FUNCT_2:81
  for f being PartFunc of X,X for g being Function of X,X st f tolerates
  g holds g in TotFuncs f;

theorem :: FUNCT_2:82
  for f being PartFunc of X,Y for g being set st g in TotFuncs(f)
  holds g is Function of X,Y;

theorem :: FUNCT_2:83
  for f being PartFunc of X,Y holds TotFuncs f c= Funcs(X,Y);

theorem :: FUNCT_2:84
  TotFuncs <:{},X,Y:> = Funcs(X,Y);

theorem :: FUNCT_2:85
  for f being Function of X,Y st Y = {} implies X = {} holds
  TotFuncs <:f,X,Y:> = {f};

theorem :: FUNCT_2:86
  for f being Function of X,X holds TotFuncs <:f,X,X:> = {f};

theorem :: FUNCT_2:87
  for f being PartFunc of X,{y} for g being Function of X,{y} holds
  TotFuncs f = {g};

theorem :: FUNCT_2:88
  for f,g being PartFunc of X,Y st g c= f holds TotFuncs f c= TotFuncs g;

theorem :: FUNCT_2:89
  for f,g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c=
  TotFuncs g holds g c= f;

theorem :: FUNCT_2:90
  for f,g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & (
  for y holds Y <> {y}) holds g c= f;

theorem :: FUNCT_2:91
  for f,g being PartFunc of X,Y st (for y holds Y <> {y}) & TotFuncs f =
  TotFuncs g holds f = g;

:: from WAYBEL_1

registration
  let A,B be non empty set;
  cluster -> non empty for Function of A,B;
end;

begin :: Addenda
:: from RLVECT_2

scheme :: FUNCT_2:sch 6
  LambdaSep1{D, R() -> non empty set, A() -> Element of D(), B() -> Element of
R(), F(object) -> Element of R()}:
ex f being Function of D(),R() st f.A() = B() &
  for x being Element of D() st x <> A() holds f.x = F(x);

scheme :: FUNCT_2:sch 7
  LambdaSep2{D, R() -> non empty set, A1, A2() -> Element of D(), B1, B2() ->
Element of R(), F(object) -> Element of R()}:
ex f being Function of D(),R() st f.
A1() = B1() & f.A2() = B2() & for x being Element of D() st x <> A1() & x <> A2
  () holds f.x = F(x)
provided
 A1() <> A2();

:: from ALTCAT_1, PRALG_3

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;

:: from SUPINF_2

scheme :: FUNCT_2:sch 8
  FunctRealEx{X()->non empty set,Y()->set,F(object)->object}:
 ex f being Function of
  X(),Y() st for x being Element of X() holds f.x = F(x)
provided
 for x being Element of X() holds F(x) in Y();

:: from YELLOW_2

scheme :: FUNCT_2:sch 9
  KappaMD{X, Y() -> non empty set, F(object) -> object}:
  ex f being Function of X(),
  Y() st for x being Element of X() holds f.x = F(x)
provided
 for x being Element of X() holds F(x) is Element of Y();

definition
  let A,B,C be non empty set;
  let f be Function of A, [:B,C:];
  redefine func pr1 f -> Function of A,B means
:: FUNCT_2:def 5

  for x being Element of A holds it.x = (f.x)`1;
  redefine func pr2 f -> Function of A,C means
:: FUNCT_2:def 6

  for x being Element of A holds it .x = (f.x)`2;
end;

definition
  let A1 be set, B1 be non empty set, A2 be set, B2 be non empty set, f1 be
  Function of A1,B1, f2 be Function of A2,B2;
  redefine pred f1 = f2 means
:: FUNCT_2:def 7
  A1 = A2 & for a being Element of A1 holds f1.a = f2.a;
end;

definition
  let A,B be set, f1,f2 be Function of A,B;
  redefine pred f1 = f2 means
:: FUNCT_2:def 8
  for a being Element of A holds f1.a = f2.a;
end;

:: missing, 2006.11.05, A.T.

theorem :: FUNCT_2:93
  for N being set, 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;

:: Moved from BORSUK_1 by AK on 27.12.2006

theorem :: FUNCT_2:94
  for A being Subset of X holds (id X)"A = A;

:: Moved from TMAP_1 by AK on 27.12.2006

reserve A,B for non empty set;

theorem :: FUNCT_2:95
  for f being Function of A,B, A0 being Subset of A, B0 being Subset of
  B holds f.:A0 c= B0 iff A0 c= f"B0;

theorem :: FUNCT_2:96
  for f being Function of A,B, A0 being non empty Subset of A, 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;

theorem :: FUNCT_2:97
  for f being Function, A0, C being set st C c= A0 holds f.:C = (f|A0).: C;

theorem :: FUNCT_2:98
  for f being Function, A0, D being set st f"D c= A0 holds f"D = (f|A0)" D;

scheme :: FUNCT_2:sch 10
  MChoice{A()-> non empty set, B()-> non empty set, F(object) -> set}:
 ex t being
  Function of A(),B() st for a being Element of A() holds t.a in F(a)
provided
 for a being Element of A() holds B() meets F(a);

:: Moved from FINSEQ_4 by AK on 2007.10.09

theorem :: FUNCT_2:99
  for X, D be non empty set, p be Function of X,D, i be Element
  of X holds p/.i = p.i;

registration
  let X, D be non empty set, p be Function of X,D, i be Element of X;
  identify p/.i with p.i;
end;

:: from JCT_MISC, 2008.06.01, A.T.

theorem :: FUNCT_2:100
  for S,X being set, f being Function of S,X, A being Subset of X st X =
  {} implies S = {} holds (f"A)` = f"(A`);

:: from CAT_1, 2008.07.01, A.T.

theorem :: FUNCT_2:101
  for X,Y,Z being set, D being non empty set, f being Function of X,D st
  Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z;

:: from WEIERSTR, 2008.07.07, A.T.

definition
  let T,S be non empty set;
  let f be Function of T,S;
  let G be Subset-Family of S;
  func f"G -> Subset-Family of T means
:: 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;
end;

theorem :: FUNCT_2:102
  for T,S being non empty set, f being Function of T,S, A,B being
  Subset-Family of S st A c= B holds f"A c= f"B;

definition
  let T,S be set;
  let f be Function of T,S;
  let G be Subset-Family of T;
  func f.:G -> Subset-Family of S means
:: 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;
end;

theorem :: FUNCT_2:103
  for T,S being set, f being Function of T,S, A,B being Subset-Family of T
  st A c= B holds f.:A c= f.:B;

theorem :: FUNCT_2:104
  for T,S being non empty set, f being Function of T,S, B being
  Subset-Family of S, P being Subset of S st f.:(f"B) is Cover of P holds B is
  Cover of P;

theorem :: FUNCT_2:105
  for T,S being non empty set, f being Function of T,S, B being
  Subset-Family of T, P being Subset of T st B is Cover of P holds f"(f.:B) is
  Cover of P;

theorem :: FUNCT_2:106
  for T,S being non empty set, f being Function of T,S, Q being
  Subset-Family of S holds union(f.:(f"(Q))) c= union Q;

theorem :: FUNCT_2:107
  for T,S being non empty set, f being Function of T,S, P being
  Subset-Family of T holds union P c= union(f"(f.:P));

:: Generalized RFUNCT_2:def 1,CFCONT_1:def 1,NFCONT_1:def 7,def 8
::  NCFCONT1:def 9,def 10,def 11,def 12,def 13,def 14
:: 2008.08.15, A.T.

definition
  let X,Z be set, Y be non empty set;
  let f be Function of X,Y;
  let p be Z-valued Function;
  assume
 rng f c= dom p;
  func p/*f -> Function of X,Z equals
:: FUNCT_2:def 11

  p*f;
end;

reserve Y for non empty set,
  f for Function of X,Y,
  p for PartFunc of Y,Z,
  x for Element of X;

theorem :: FUNCT_2:108
  X <> {} & rng f c= dom p implies (p/*f).x = p.(f.x);

theorem :: FUNCT_2:109
  X <> {} & rng f c= dom p implies (p/*f).x = p/.(f.x);

reserve g for Function of X,X;

theorem :: FUNCT_2:110
  rng f c= dom p implies (p/*f)*g = p/*(f*g);

:: from RAMSEY_1, 2008.09.12,A.T.

theorem :: FUNCT_2:111
  for X,Y being non empty set, f being Function of X,Y holds f is
  constant iff ex y being Element of Y st rng f = {y};

:: from ISOCAT_2, 2008.09.14, A.T.

theorem :: FUNCT_2:112
  for A,B being non empty set, x being Element of A, f being Function of
  A,B holds f.x in rng f;

:: missing, 2008.09.14, A.T.

theorem :: FUNCT_2:113
  for A,B being set, f being Function of A,B st y in rng f ex x
  being Element of A st y = f.x;

:: from RFUNCT_2, 2008.09.14, A.T.

theorem :: FUNCT_2:114
  for A,B being non empty set, f being Function of A,B st for x being
  Element of A holds f.x in Z holds rng f c= Z;

reserve X,Y for non empty set,
  Z,S,T for set,
  f for Function of X,Y,
  g for PartFunc of Y,Z,
  x for Element of X;

theorem :: FUNCT_2:115
  g is total implies (g/*f).x = g.(f.x);

theorem :: FUNCT_2:116
  g is total implies (g/*f).x = g/.(f.x);

theorem :: FUNCT_2:117
  rng f c= dom (g|S) implies (g|S)/*f = g/*f;

theorem :: FUNCT_2:118
  rng f c= dom (g|S) & S c= T implies (g|S)/*f = (g|T)/*f;

:: missing, 2009.01.09, A.T.

theorem :: FUNCT_2:119
  for H being Function of D, [:A,B:], d being Element of D holds H.d = [
  pr1 H.d,pr2 H.d];

:: from YELLOW20, 2009.01.21, A.T.

theorem :: FUNCT_2:120
  for A1,A2, B1,B2 being set for f being Function of A1,A2, g being
Function of B1,B2 st f tolerates g holds f /\ g is Function of A1 /\ B1, A2 /\
  B2;

:: from FRAENKEL, 2009.05.06, A.K.

registration
  let A, B be set;
  cluster Funcs(A,B) -> functional;
end;

definition
  let A, B be set;
  mode FUNCTION_DOMAIN of A,B -> non empty set means
:: FUNCT_2:def 12

    for x being Element of it holds x is Function of A,B;
end;

registration
  let A, B be set;
  cluster -> functional for FUNCTION_DOMAIN of A,B;
end;

theorem :: FUNCT_2:121
  for f being Function of P,Q holds { f } is FUNCTION_DOMAIN of P,Q;

theorem :: FUNCT_2:122
  Funcs(P,B) is FUNCTION_DOMAIN of P,B;

definition
  let A be set, B be non empty set;
  redefine func Funcs(A,B) -> FUNCTION_DOMAIN of A,B;
  let F be FUNCTION_DOMAIN of A,B;
  redefine mode Element of F -> Function of A,B;
end;

registration
  let I be set;
  cluster id I -> total for I-defined Function;
end;

:: from CAT_3, 2009.09.14

definition
  let X,A;
  let F be Function of X,A;
  let x be set;
  assume
 x in X;
  redefine func F/.x equals
:: FUNCT_2:def 13
  F.x;
end;

theorem :: FUNCT_2:123
  for X being set, Y being non empty set
  for f being Function of X, Y, g being X-valued Function
   holds dom(f*g) = dom g;

theorem :: FUNCT_2:124
  for X being non empty set, f being Function of X,X st for x being
  Element of X holds f.x = x holds f = id X;

:: Moved from GROUP_9, AK

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 being set, A being set
   for f,g being Function of {x}, A st f.x = g.x
   holds f = g;

theorem :: FUNCT_2:126
  for A being set holds id A in Funcs(A,A);

theorem :: FUNCT_2:127
  Funcs({},{}) = { id {} };

theorem :: FUNCT_2:128
  for A,B,C being set, f,g being Function st f in Funcs(A,B) & g in
  Funcs(B,C) holds g*f in Funcs(A,C);

theorem :: FUNCT_2:129
  for A,B,C being set st Funcs(A,B) <> {} & Funcs(B,C) <> {} holds
  Funcs(A,C) <> {};

theorem :: FUNCT_2:130
  for A being set holds {} is Function of A,{};

scheme :: FUNCT_2:sch 11
  Lambda1{X, Y() -> set, F(object)->object}:
 ex f being Function of X(),Y() st
   for x being set st x in X() holds f.x = F(x)
provided
 for x being set st x in X() holds F(x) in Y();