:: Binary Operations Applied to Functions
::  by Andrzej Trybulec
::
:: Received September 4, 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 FUNCT_1, FUNCT_3, PARTFUN1, RELAT_1, ZFMISC_1, XBOOLE_0, TARSKI,
      SUBSET_1, BINOP_1, MCART_1, FUNCOP_1, WELLORD1, MSUALG_4, FUNCT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, WELLORD1;
 constructors PARTFUN1, BINOP_1, FUNCT_3, RELSET_1, WELLORD1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1;
 requirements SUBSET, BOOLE;


begin

reserve f,g,h for Function,
  A for set;

theorem :: FUNCOP_1:1
  delta A = <:id A, id A:>;

reserve F for Function,
  B,x,y,y1,y2,z for set;

definition
  let f;
  func f~ -> Function means
:: FUNCOP_1:def 1

  dom it = dom f & for x being object st x in dom f holds
(for y,z being object st f.x = [y,z] holds it.x = [z,y]) &
   (f.x = it.x or ex y,z being object st f.x =[y,z]);
  involutiveness;
end;

theorem :: FUNCOP_1:2
  <:f,g:> = <:g,f:>~;

theorem :: FUNCOP_1:3
  (f|A)~ = f~|A;

theorem :: FUNCOP_1:4
  (delta A)~ = delta A;

theorem :: FUNCOP_1:5
  <:f,g:>|A = <:f|A,g:>;

theorem :: FUNCOP_1:6
  <:f,g:>|A = <:f,g|A:>;

definition
  let A be set, z be object;
  func A --> z -> set equals
:: FUNCOP_1:def 2
  [:A, {z}:];
end;

registration
  let A be set, z be object;
  cluster A --> z -> Function-like Relation-like;
end;

reserve x,z for object;

theorem :: FUNCOP_1:7
  x in A implies (A --> z).x = z;

registration
  let A be non empty set, x be object, a be Element of A;
  reduce (A --> x).a to x;
end;

theorem :: FUNCOP_1:8
  A <> {} implies rng (A --> x) = {x};

theorem :: FUNCOP_1:9
  rng f = {x} implies f = (dom f) --> x;

registration
  let x be object;
  cluster {} --> x -> empty;
end;

registration
  let x be object;
  let A be empty set;
  cluster A --> x -> empty;
end;

registration
  let x be object;
  let A be non empty set;
  cluster A --> x -> non empty;
end;

theorem :: FUNCOP_1:10
  dom ({} --> x) = {} & rng ({} --> x) = {};

theorem :: FUNCOP_1:11
  (for z st z in dom f holds f.z = x) implies f = dom f --> x;

theorem :: FUNCOP_1:12
  (A --> x)|B = A /\ B --> x;

theorem :: FUNCOP_1:13
  dom (A --> x) = A & rng (A --> x) c= {x};

registration
  let X be set, a be object;
  reduce dom (X --> a) to X;
end;

registration let D be set;
  cluster D --> {} -> empty-yielding;
end;

theorem :: FUNCOP_1:14
  x in B implies (A --> x)"B = A;

theorem :: FUNCOP_1:15
  (A --> x)"{x} = A;

theorem :: FUNCOP_1:16
  not x in B implies (A --> x)"B = {};

theorem :: FUNCOP_1:17
  x in dom h implies h*(A --> x) = A --> h.x;

theorem :: FUNCOP_1:18
  A <> {} & x in dom h implies dom(h*(A --> x)) <> {};

theorem :: FUNCOP_1:19
  (A --> x)*h = h"A --> x;

theorem :: FUNCOP_1:20
  (A --> [x,y])~ = A --> [y,x];

definition
  let F,f,g;
  func F.:(f,g) -> set equals
:: FUNCOP_1:def 3
  F * <:f,g:>;
end;

registration
  let F,f,g;
  cluster F.:(f,g) -> Function-like Relation-like;
end;

theorem :: FUNCOP_1:21
  for h st dom h = dom(F.:(f,g)) & for z being set st z in dom (F.:(f,g)
  ) holds h.z = F.(f.z,g.z) holds h = F.:(f,g);

theorem :: FUNCOP_1:22
  x in dom (F.:(f,g)) implies (F.:(f,g)).x = F.(f.x,g.x);

theorem :: FUNCOP_1:23
  f|A = g|A implies (F.:(f,h))|A = (F.:(g,h))|A;

theorem :: FUNCOP_1:24
  f|A = g|A implies (F.:(h,f))|A = (F.:(h,g))|A;

theorem :: FUNCOP_1:25
  F.:(f,g)*h = F.:(f*h, g*h);

definition
  let F,f,x;
  func F[:](f,x) -> set equals
:: FUNCOP_1:def 4
  F * <:f, dom f --> x:>;
end;

registration
  let F,f,x;
  cluster F[:](f,x) -> Function-like Relation-like;
end;

theorem :: FUNCOP_1:26
  F[:](f,x) = F.:(f, dom f --> x);

theorem :: FUNCOP_1:27
  x in dom (F[:](f,z)) implies (F[:](f,z)).x = F.(f.x,z);

theorem :: FUNCOP_1:28
  f|A = g|A implies (F[:](f,x))|A = (F[:](g,x))|A;

theorem :: FUNCOP_1:29
  F[:](f,x)*h = F[:](f*h,x);

theorem :: FUNCOP_1:30
  F[:](f,x)*id A = F[:](f|A,x);

definition
  let F,x,g;
  func F[;](x,g) -> set equals
:: FUNCOP_1:def 5
  F * <:dom g --> x, g:>;
end;

registration
  let F,x,g;
  cluster F[;](x,g) -> Function-like Relation-like;
end;

theorem :: FUNCOP_1:31
  F[;](x,g) = F.:(dom g --> x, g);

theorem :: FUNCOP_1:32
  x in dom (F[;](z,f)) implies (F[;](z,f)).x = F.(z,f.x);

theorem :: FUNCOP_1:33
  f|A = g|A implies (F[;](x,f))|A = (F[;](x,g))|A;

theorem :: FUNCOP_1:34
  F[;](x,f)*h = F[;](x,f*h);

theorem :: FUNCOP_1:35
  F[;](x,f)*id A = F[;](x,f|A);

reserve X for non empty set,
  Y for set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:36
  F.:(f,g) is Function of Y,X;

definition
  let X be non empty set, Z be set;
  let F be BinOp of X, f,g be Function of Z,X;
  redefine func F.:(f,g) -> Function of Z,X;
end;

reserve Y for non empty set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:37
  for z being Element of Y holds (F.:(f,g)).z = F.(f.z,g.z);

theorem :: FUNCOP_1:38
  for h being Function of Y,X holds (for z being Element of Y
  holds h.z = F.(f.z,g.z)) implies h = F.:(f,g);

theorem :: FUNCOP_1:39
  for g being Function of X,X holds F.:(id X, g)*f = F.:(f,g*f);

theorem :: FUNCOP_1:40
  for g being Function of X,X holds F.:(g, id X)*f = F.:(g*f,f);

theorem :: FUNCOP_1:41
  F.:(id X, id X)*f = F.:(f,f);

theorem :: FUNCOP_1:42
  for g being Function of X,X holds F.:(id X, g).x = F.(x,g.x);

theorem :: FUNCOP_1:43
  for g being Function of X,X holds F.:(g, id X).x = F.(g.x,x);

theorem :: FUNCOP_1:44
  F.:(id X, id X).x = F.(x,x);

theorem :: FUNCOP_1:45
  x in B implies A --> x is Function of A,B;

definition
  let I be set, i be object;
  redefine func I --> i -> Function of I,{i};
end;

definition
  let B be non empty set, A be set, b be Element of B;
  redefine func A --> b -> Function of A,B;
end;

theorem :: FUNCOP_1:46
  A --> x is Function of A,X;

reserve Y for set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:47
  F[:](f,x) is Function of Y,X;

definition
  let X be non empty set, Z be set;
  let F be BinOp of X, f be Function of Z,X, x be Element of X;
  redefine func F[:](f,x) -> Function of Z,X;
end;

reserve Y for non empty set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:48
  for y being Element of Y holds (F[:](f,x)).y = F.(f.y,x);

theorem :: FUNCOP_1:49
  (for y being Element of Y holds g.y = F.(f.y,x)) implies g = F
  [:](f,x);

theorem :: FUNCOP_1:50
  F[:](id X, x)*f = F[:](f,x);

theorem :: FUNCOP_1:51
  F[:](id X, x).x = F.(x,x);

reserve Y for set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:52
  F[;](x,g) is Function of Y,X;

definition
  let X be non empty set, Z be set;
  let F be BinOp of X, x be Element of X;
  let g be Function of Z,X;
  redefine func F[;](x,g) -> Function of Z,X;
end;

reserve Y for non empty set,
  F for BinOp of X,
  f,g,h for Function of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:53
  for y being Element of Y holds (F[;](x,f)).y = F.(x,f.y);

theorem :: FUNCOP_1:54
  (for y being Element of Y holds g.y = F.(x,f.y)) implies g = F
  [;](x,f);

reserve Y for set,
  F for BinOp of X,
  f,g,h for Function
  of Y,X,
  x,x1,x2 for Element of X;

theorem :: FUNCOP_1:55
  F[;](x, id X)*f = F[;](x,f);

theorem :: FUNCOP_1:56
  F[;](x, id X).x = F.(x,x);

theorem :: FUNCOP_1:57
  for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] for x
  being Element of X holds f~.x =[(f.x)`2,(f.x)`1];

definition
  let X,Y,Z be non empty set;
  let f be Function of X, [:Y,Z:];
  redefine func rng f -> Relation of Y,Z;
end;

definition
  let X,Y,Z be non empty set;
  let f be Function of X, [:Y,Z:];
  redefine func f~ -> Function of X, [:Z,Y:];
end;

theorem :: FUNCOP_1:58
  for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] holds
  rng (f~) = (rng f)~;

reserve y for Element of Y;

theorem :: FUNCOP_1:59
  F is associative implies F[:](F[;](x1,f),x2) = F[;](x1,F[:](f,x2));

theorem :: FUNCOP_1:60
  F is associative implies F.:(F[:](f,x),g) = F.:(f,F[;](x,g));

theorem :: FUNCOP_1:61
  F is associative implies F.:(F.:(f,g),h) = F.:(f,F.:(g,h));

theorem :: FUNCOP_1:62
  F is associative implies F[;](F.(x1,x2),f) = F[;](x1,F[;](x2,f));

theorem :: FUNCOP_1:63
  F is associative implies F[:](f, F.(x1,x2)) = F[:](F[:](f,x1),x2);

theorem :: FUNCOP_1:64
  F is commutative implies F[;](x,f) = F[:](f,x);

theorem :: FUNCOP_1:65
  F is commutative implies F.:(f,g) = F.:(g,f);

theorem :: FUNCOP_1:66
  F is idempotent implies F.:(f,f) = f;

reserve Y for non empty set,
  F for BinOp of X,
  f for Function of Y,X,
  x for Element of X,
  y for Element of Y;

theorem :: FUNCOP_1:67
  F is idempotent implies F[;](f.y,f).y = f.y;

theorem :: FUNCOP_1:68
  F is idempotent implies F[:](f,f.y).y = f.y;

:: Addendum, 2002.07.08

theorem :: FUNCOP_1:69
  for F,f,g being Function st [:rng f, rng g:] c= dom F holds dom(F.:(f,
  g)) = dom f /\ dom g;

:: from PRALG_1, 2004.07.23

definition
  let IT be Function;
  attr IT is Function-yielding means
:: FUNCOP_1:def 6

  for x being object st x in dom IT holds IT.x is Function;
end;

registration
  cluster Function-yielding for Function;
end;

registration
  let B be Function-yielding Function, j be object;
  cluster B.j -> Function-like Relation-like;
end;

registration
  let F be Function-yielding Function, f be Function;
  cluster F * f -> Function-yielding;
end;

:: missing, 2005.11.13, A.T.

registration
  let B;
  let c be non empty set;
  cluster B --> c -> non-empty;
end;

:: missing, 2005.12.20, A.T.

theorem :: FUNCOP_1:70
  ([:X,Y:] --> z).(x,y) = z;

:: from CAT_1, 2007.02.11, A.T.

reserve a,b,c for set;

definition
  let a,b,c be object;
  func (a,b).-->c -> Function equals
:: FUNCOP_1:def 7
  {[a,b]} --> c;
end;

theorem :: FUNCOP_1:71
 for a,b,c being object holds
  ((a,b).-->c).(a,b) = c;

:: from CQC_LANG, 2007.03.13, A.T.

definition
  let x,y,a,b be object;
  func IFEQ(x,y,a,b) -> object equals
:: FUNCOP_1:def 8

  a if x = y otherwise b;
end;

definition
  let x,y be object; let a,b be set;
  redefine func IFEQ(x,y,a,b) -> set;
end;

definition
  let D be set;
  let x,y be object, a,b be Element of D;
  redefine func IFEQ(x,y,a,b) -> Element of D;
end;

definition
  let x,y be object;
  func x .--> y -> set equals
:: FUNCOP_1:def 9
  {x} --> y;
end;

registration
  let x,y be object;
  cluster x .--> y -> Function-like Relation-like;
end;

registration
  let x,y be object;
  cluster x .--> y -> one-to-one;
end;

theorem :: FUNCOP_1:72
  for x,y be object holds (x .--> y).x = y;

:: from SCMFSA6A, 2007.07.22, A.T.

theorem :: FUNCOP_1:73
  for a,b being object, f being Function holds a.-->b c= f iff a in dom f &
  f.a = b;

:: from FUNCT_2, 2007.11.22, A.T., :: from CAT_4

notation
  let o,m,r be object;
  synonym (o,m) :-> r for (o,m) .--> r;
end;

definition
  let o,m,r be object;
  redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
:: FUNCOP_1:def 10
  not contradiction;
end;

:: missing, 2008.03.20, A.T.

reserve x,y,z for object;

theorem :: FUNCOP_1:74
  x in dom(x .--> y);

theorem :: FUNCOP_1:75
  z in dom(x .--> y) implies z = x;

:: missing, 2008.04.15, A.T.

theorem :: FUNCOP_1:76
  not x in A implies (x .--> y)|A = {};

:: from CAT_1, (new notation), 2008.06.30. A.T.

notation
  let x,y be object;
  synonym x :-> y for x .--> y;
end;

definition
  let m,o be object;
  redefine func m :-> o -> Function of {m}, {o};
end;

theorem :: FUNCOP_1:77
  for x being Element of {a} for y being Element of {b} holds
  ((a,b):->c).(x,y) = c;

:: from MSUHOM_1, ALTCAT_1, 2008.07.06, A.T.

registration
  let f be Function-yielding Function, C be set;
  cluster f|C -> Function-yielding;
end;

:: from CIRCCOMB, 2008.07.06, A.T.

registration
  let A be set;
  let f be Function;
  cluster A --> f -> Function-yielding;
end;

:: from SEQM_3, 2008.07.17, A.T.

registration
  let X be set, a be object;
  cluster X --> a -> constant;
end;
:: from YELLOW_6, 2008.07.17, A.T.

registration
  cluster non empty constant for Function;
  let X be set, Y be non empty set;
  cluster constant for Function of X,Y;
end;
:: missing, 2008.07.17, A.T.

registration
  let f be constant Function, X be set;
  cluster f|X -> constant;
end;
:: missing, 2008.08.14, A.T.

theorem :: FUNCOP_1:78
  for f being non empty constant Function ex y st for x st x in dom f
  holds f.x = y;
:: from YELLOW_6, 2008.12.26, A.T.

theorem :: FUNCOP_1:79
  for X being non empty set, x being set holds the_value_of (X --> x) =
  x;

:: from CIRCCMB3, 2008.12.26, A.T.

theorem :: FUNCOP_1:80
  for f being constant Function holds f = (dom f) --> the_value_of f;

:: missing, 2009.01.21, A.T.

registration
  let X be set, Y be non empty set;
  cluster total for PartFunc of X,Y;
end;

:: new, 2009.02.14, A.T.

registration
  let I be set, A be object;
  cluster I --> A -> I-defined;
end;

registration
  let I, A be object;
  cluster I .--> A -> {I}-defined;
end;

:: BORSUK_1:6, 2009.06.11, A.K.

theorem :: FUNCOP_1:81
  (A --> x).:B c= {x};

registration
  let I be set, f be Function;
  cluster I .--> f -> Function-yielding;
end;

:: 2009.10.03, A.T.

registration let I be set;
 cluster total for I-defined non-empty Function;
end;

theorem :: FUNCOP_1:82
  x .--> y is_isomorphism_of {[x,x]},{[y,y]};

theorem :: FUNCOP_1:83
  {[x,x]}, {[y,y]} are_isomorphic;

registration
  let I be set, A be object;
  cluster I --> A -> total for I-defined Function;
end;

theorem :: FUNCOP_1:84
  for f being Function st x in dom f
   holds x .--> f.x c= f;

registration let A be non empty set;
 let x be set, i be Element of A;
 cluster x .--> i -> A-valued;
end;

reserve Y for set,
        f,g for Function of Y,X,
        x for Element of X,
        y for Element of Y;

:: missing, 2010.02.10, A.T.

theorem :: FUNCOP_1:85
  F is associative implies F.:(F[;](x,f),g) = F[;](x,F.:(f,g));

registration let A be set, B be non empty set, x be Element of B;
 cluster A --> x -> B-valued;
end;

registration let A be non empty set, x be Element of A, y be object;
  cluster x .--> y -> A-defined;
end;

theorem :: FUNCOP_1:86
 for x,y,A being set st x in A
 holds (x .--> y)|A = x .--> y;

:: missing, 2011.02.06, A.K.

registration
  let Y be functional set;
  cluster Y-valued -> Function-yielding for Function;
end;

:: from MSUALG_4, 2011.04.16, A.T.

definition
  let IT be Function;
  attr IT is Relation-yielding means
:: FUNCOP_1:def 11
  for x be set st x in dom IT holds IT.x is Relation;
end;

registration
 cluster Function-yielding -> Relation-yielding for Function;
end;

registration
 cluster empty -> Function-yielding for Function;
end;

:: from CIRCCOMB, 2011.04.19, A.T.

theorem :: FUNCOP_1:87
  for X,Y being set, x,y being object
  holds X --> x tolerates Y --> y iff x = y or X misses Y;

reserve x,y,z,A for set;

theorem :: FUNCOP_1:88
 rng(x .--> y) = {y};

theorem :: FUNCOP_1:89
  z in A implies (A --> x)*(y .--> z) = y .--> x;

registration
  let f be Function-yielding Function;
  let a,b be object;
  cluster f.(a,b) -> Function-like Relation-like;
end;

registration
  let Y be set;
  let X,Z be non empty set;
  cluster -> Function-yielding for Function of X, Funcs(Y,Z);
end;