:: Binary Operations
::  by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies FUNCT_1, BOOLE, RELAT_1, BINOP_1, SEQM_3, PARTFUN1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2;
 constructors FUNCT_2;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1;
 requirements SUBSET, BOOLE;
 definitions FUNCT_1;
 theorems RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, XBOOLE_1, SUBSET_1;
 schemes FUNCT_2, PARTFUN1;

begin

definition
  let f be Function;
  let a,b be set;
  func f.(a,b) -> set equals

  f.[a,b];
  correctness;
end;

reserve A for set;

definition
  let A,B be non empty set, C be set, f be Function of [:A,B:],C;
  let a be Element of A;
  let b be Element of B;
  redefine func f.(a,b) -> Element of C;
  coherence
  proof
    reconsider ab = [a,b] as Element of [:A,B:] by ZFMISC_1:def 2;
    f.ab is Element of C;
    hence thesis;
  end;
end;

reserve X,Y,Z,x,x1,x2,y,y1,y2,z,z1,z2 for set;

theorem Th1:
  for X,Y,Z being set for f1,f2 being Function of [:X,Y:],Z
  st for x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y)
  holds f1 = f2
proof
  let X,Y,Z be set;
  let f1,f2 be Function of [:X,Y:],Z such that
A1: for x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y);
  for z being set st z in [:X,Y:] holds f1.z = f2.z
  proof
    let z be set;
    assume z in [:X,Y:];
    then consider x,y being set such that
A2: x in X & y in Y and
A3: z = [x,y] by ZFMISC_1:def 2;
    f1.(x,y) = f1.z & f2.(x,y) = f2.z by A3;
    hence thesis by A1,A2;
  end;
  hence thesis by FUNCT_2:18;
end;

theorem
  for f1,f2 being Function of [:X,Y:],Z st
  for a being Element of X for b being Element of Y holds f1.(a,b) = f2.(a,b)
  holds f1 = f2
proof
  let f1,f2 be Function of [:X,Y:],Z;
  assume for a being Element of X for b being Element of Y
  holds f1.(a,b) = f2.(a,b);
  then for x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y);
  hence f1 = f2 by Th1;
end;

definition
  let A be set;
  mode UnOp of A is Function of A,A;
  mode BinOp of A is Function of [:A,A:],A;
end;

reserve u for UnOp of A,
  o,o' for BinOp of A,
  a,b,c,e,e1,e2 for Element of A;

scheme FuncEx2{X, Y, Z() -> set, P[set,set,set]}:
  ex f being Function of [:X(),Y():],Z() st
  for x,y st x in X() & y in Y() holds P[x,y,f.(x,y)]
provided
A1: for x,y st x in X() & y in Y() ex z st z in Z() & P[x,y,z]
proof
  defpred R[set,set] means for x1,y1 st $1 = [x1,y1] holds P[x1,y1,$2];
A2: for x st x in [:X(),Y():] ex z st z in Z() & R[x,z]
  proof
    let x;
    assume x in [:X(),Y():];
    then consider x1,y1 such that
A3: x1 in X() & y1 in Y() and
A4: x = [x1,y1] by ZFMISC_1:def 2;
    consider z such that
A5: z in Z() and
A6: P[x1,y1,z] by A1,A3;
    take z;
    thus z in Z() by A5;
    let x2,y2;
    assume x = [x2,y2];
    then x1 = x2 & y1 = y2 by A4,ZFMISC_1:33;
    hence thesis by A6;
  end;
  consider f being Function of [:X(),Y():],Z() such that
A7: for x st x in [:X(),Y():] holds R[x,f.x] from FUNCT_2:sch 1(A2);
  take f;
  let x,y;
  assume x in X() & y in Y();
  then [x,y] in [:X(),Y():] by ZFMISC_1:def 2;
  hence thesis by A7;
end;

scheme Lambda2{X, Y, Z() -> set, F(set,set)->set}:
  ex f being Function of [:X(),Y():],Z()
  st for x,y st x in X() & y in Y() holds f.(x,y) = F(x,y)
provided
A1: for x,y st x in X() & y in Y() holds F(x,y) in Z()
proof
  defpred P[set,set,set] means $3 = F($1,$2);
A2: for x,y st x in X() & y in Y() ex z st z in Z() & P[x,y,z] by A1;
  thus ex f being Function of [:X(),Y():],Z() st
  for x,y st x in X() & y in Y() holds P[x,y,f.(x,y)] from FuncEx2(A2);
end;

scheme FuncEx2D{X, Y, Z() -> non empty set, P[set,set,set]}:
  ex f being Function of [:X(),Y():],Z() st
  for x being Element of X() for y being Element of Y() holds P[x,y,f.(x,y)]
provided
A1: for x being Element of X() for y being Element of Y()
ex z being Element of Z() st P[x,y,z]
proof
  defpred R[set,set] means for x being (Element of X()),y being Element of Y()
  st $1 = [x,y] holds P[x,y,$2];
A2: for p being Element of [:X(),Y():] ex z being Element of Z() st R[p,z]
  proof
    let p be Element of [:X(),Y():];
    consider x1,y1 such that
A3: x1 in X() and
A4: y1 in Y() and
A5: p = [x1,y1] by ZFMISC_1:def 2;
    reconsider x1 as Element of X() by A3;
    reconsider y1 as Element of Y() by A4;
    consider z being Element of Z() such that
A6: P[x1,y1,z] by A1;
    take z;
    let x be Element of X(),y be Element of Y();
    assume p = [x,y];
    then x1 = x & y1 = y by A5,ZFMISC_1:33;
    hence P[x,y,z] by A6;
  end;
  consider f being Function of [:X(),Y():],Z() such that
A7: for p being Element of [:X(),Y():] holds R[p,f.p] from FUNCT_2:sch 3(A2);
  take f;
  let x be Element of X();
  let y be Element of Y();
  reconsider xy = [x,y] as Element of [:X(),Y():] by ZFMISC_1:def 2;
  P[x,y,f.xy] by A7;
  hence thesis;
end;

scheme Lambda2D{X, Y, Z() -> non empty set,
  F(Element of X(),Element of Y()) -> Element of Z()}:
  ex f being Function of [:X(),Y():],Z()
  st for x being Element of X() for y being Element of Y() holds f.(x,y)=F(x,y)
proof
  defpred P[Element of X(),Element of Y(),set] means $3 = F($1,$2);
A1: for x being Element of X() for y being Element of Y()
  ex z being Element of Z() st P[x,y,z];
  thus ex f being Function of [:X(),Y():],Z()
  st for x being Element of X() for y being Element of Y() holds
  P[x,y,f.(x,y)] from FuncEx2D(A1);
end;

definition
  let A,o;
  attr o is commutative means
  :Def2:
  for a,b holds o.(a,b) = o.(b,a);
  attr o is associative means
  :Def3:
  for a,b,c holds o.(a,o.(b,c)) = o.(o.(a,b),c);
  attr o is idempotent means
  :Def4:
  for a holds o.(a,a) = a;
end;

registration
  cluster -> empty associative commutative BinOp of {};
  coherence
  proof
    let f be BinOp of {};
 [:{},{}:] = {} by ZFMISC_1:113;
    then
A2: f c= [:dom f, rng f:] & dom f = {} & rng f c= {};
    thus f is empty;
    hereby
      let a,b,c be Element of {};
      thus f.(a,f.(b,c)) = {} by A2,FUNCT_1:def 4
        .= f.(f.(a,b),c) by A2,FUNCT_1:def 4;
    end;
    let a,b be Element of {};
    thus f.(a,b) = {} by A2,FUNCT_1:def 4
      .= f.(b,a) by A2,FUNCT_1:def 4;
  end;
end;

definition
  let A,e,o;
  pred e is_a_left_unity_wrt o means
  :Def5:
  for a holds o.(e,a) = a;
  pred e is_a_right_unity_wrt o means
  :Def6:
  for a holds o.(a,e) = a;
end;

definition
  let A,e,o;
  pred e is_a_unity_wrt o means
  e is_a_left_unity_wrt o & e is_a_right_unity_wrt o;
end;

canceled 8;

theorem Th11:
  e is_a_unity_wrt o iff for a holds o.(e,a) = a & o.(a,e) = a
proof
  thus e is_a_unity_wrt o implies for a holds o.(e,a) = a & o.(a,e) = a
  proof
    assume e is_a_left_unity_wrt o & e is_a_right_unity_wrt o;
    hence thesis by Def5,Def6;
  end;
  assume for a holds o.(e,a) = a & o.(a,e) = a;
  hence (for a holds o.(e,a) = a) & (for a holds o.(a,e) = a);
end;

theorem Th12:
  o is commutative implies (e is_a_unity_wrt o iff for a holds o.(e,a) = a)
proof
  assume
A1: o is commutative;
  now
    thus (for a holds o.(e,a) = a & o.(a,e) = a)
    implies (for a holds o.(e,a) = a);
    assume
A2: for a holds o.(e,a) = a;
    let a;
    thus o.(e,a) = a by A2;
    thus o.(a,e) = o.(e,a) by A1,Def2
      .= a by A2;
  end;
  hence thesis by Th11;
end;

theorem Th13:
  o is commutative implies (e is_a_unity_wrt o iff for a holds o.(a,e) = a)
proof
  assume
A1: o is commutative;
  now
    thus (for a holds o.(e,a) = a & o.(a,e) = a)
    implies (for a holds o.(a,e) = a);
    assume
A2: for a holds o.(a,e) = a;
    let a;
    thus o.(e,a) = o.(a,e) by A1,Def2
      .= a by A2;
    thus o.(a,e) = a by A2;
  end;
  hence thesis by Th11;
end;

theorem Th14:
  o is commutative implies (e is_a_unity_wrt o iff e is_a_left_unity_wrt o)
proof e is_a_left_unity_wrt o iff for a holds o.(e,a) = a by Def5;
  hence thesis by Th12;
end;

theorem Th15:
  o is commutative implies (e is_a_unity_wrt o iff e is_a_right_unity_wrt o)
proof e is_a_right_unity_wrt o iff for a holds o.(a,e) = a by Def6;
  hence thesis by Th13;
end;

theorem
  o is commutative implies
  (e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o)
proof
  assume
A1: o is commutative;
  then e is_a_unity_wrt o iff e is_a_left_unity_wrt o by Th14;
  hence thesis by A1,Th15;
end;

theorem Th17:
  e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2
proof
  assume that
A1: e1 is_a_left_unity_wrt o and
A2: e2 is_a_right_unity_wrt o;
  thus e1 = o.(e1,e2) by A2,Def6
    .= e2 by A1,Def5;
end;

theorem Th18:
  e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2
proof
  assume e1 is_a_left_unity_wrt o & e1 is_a_right_unity_wrt o &
  e2 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o;
  hence thesis by Th17;
end;

definition
  let A,o;
  assume
A1: ex e st e is_a_unity_wrt o;
  func the_unity_wrt o -> Element of A means

  it is_a_unity_wrt o;
  existence by A1;
  uniqueness by Th18;
end;

definition
  let A,o',o;
  pred o' is_left_distributive_wrt o means
  :Def9:
  for a,b,c holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c));
  pred o' is_right_distributive_wrt o means
  :Def10:
  for a,b,c holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));
end;

definition
  let A,o',o;
  pred o' is_distributive_wrt o means
  o' is_left_distributive_wrt o & o' is_right_distributive_wrt o;
end;

canceled 4;

theorem Th23:
  o' is_distributive_wrt o iff for a,b,c holds
  o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
  o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))
proof
  thus o' is_distributive_wrt o implies for a,b,c holds
  o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
  o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))
  proof
    assume o' is_left_distributive_wrt o & o' is_right_distributive_wrt o;
    hence thesis by Def9,Def10;
  end;
  assume for a,b,c holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
  o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));
  hence (for a,b,c holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c))) &
  ( for a,b,c holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)));
end;

theorem Th24:
  for A being non empty set, o,o' being BinOp of A holds
  o' is commutative implies (o' is_distributive_wrt o iff
  for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)))
proof
  let A be non empty set, o,o' be BinOp of A;
  assume
A1: o' is commutative;
  (for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
  o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))) iff
  (for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)))
  proof
    thus (for a,b,c being Element of A holds
    o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
    o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))) implies
    (for a,b,c being Element of A holds
    o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)));
    assume
A2: for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c));
    let a,b,c be Element of A;
    thus o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) by A2;
    thus o'.(o.(a,b),c) = o'.(c,o.(a,b)) by A1,Def2
      .= o.(o'.(c,a),o'.(c,b)) by A2
      .= o.(o'.(a,c),o'.(c,b)) by A1,Def2
      .= o.(o'.(a,c),o'.(b,c)) by A1,Def2;
  end;
  hence thesis by Th23;
end;

theorem Th25:
  for A being non empty set, o,o' being BinOp of A holds
  o' is commutative implies (o' is_distributive_wrt o iff
  for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)))
proof
  let A be non empty set, o,o' be BinOp of A;
  assume
A1: o' is commutative;
  (for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
  o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))) iff
  (for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)))
  proof
    thus (for a,b,c being Element of A holds
    o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
    o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))) implies
    (for a,b,c being Element of A holds
    o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)));
    assume
A2: for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));
    let a,b,c be Element of A;
    thus o'.(a,o.(b,c)) = o'.(o.(b,c),a) by A1,Def2
      .= o.(o'.(b,a),o'.(c,a)) by A2
      .= o.(o'.(a,b),o'.(c,a)) by A1,Def2
      .= o.(o'.(a,b),o'.(a,c)) by A1,Def2;
    thus o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)) by A2;
  end;
  hence thesis by Th23;
end;

theorem Th26:
  for A being non empty set, o,o' being BinOp of A holds
  o' is commutative implies
  (o' is_distributive_wrt o iff o' is_left_distributive_wrt o)
proof
  let A be non empty set, o,o' be BinOp of A;
  o' is_left_distributive_wrt o iff
  for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c))
  by Def9;
  hence thesis by Th24;
end;

theorem Th27:
  for A being non empty set, o,o' being BinOp of A holds
  o' is commutative implies
  (o' is_distributive_wrt o iff o' is_right_distributive_wrt o)
proof
  let A be non empty set, o,o' be BinOp of A;
  o' is_right_distributive_wrt o iff
  for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))
  by Def10;
  hence thesis by Th25;
end;

theorem
  for A being non empty set, o,o' being BinOp of A holds
  o' is commutative implies
  (o' is_right_distributive_wrt o iff o' is_left_distributive_wrt o)
proof
  let A be non empty set, o,o' be BinOp of A;
  assume
A1: o' is commutative;
  then o' is_distributive_wrt o iff o' is_left_distributive_wrt o by Th26;
  hence thesis by A1,Th27;
end;

definition
  let A,u,o;
  pred u is_distributive_wrt o means
  :Def12:
  for a,b holds u.(o.(a,b)) = o.((u.a),(u.b));
end;

definition
  let A be non empty set, o be BinOp of A;
  redefine attr o is commutative means
  for a,b being Element of A holds o.(a,b) = o.(b,a);
  correctness by Def2;
  attr o is associative means
  for a,b,c being Element of A holds o.(a,o.(b,c)) = o.(o.(a,b),c);
  correctness by Def3;
  attr o is idempotent means

  for a being Element of A holds o.(a,a) = a;
  correctness by Def4;
end;

definition
  let A be non empty set, e be Element of A, o be BinOp of A;
  redefine pred e is_a_left_unity_wrt o means
  for a being Element of A holds o.(e,a) = a;
  correctness by Def5;
  pred e is_a_right_unity_wrt o means
  for a being Element of A holds o.(a,e) = a;
  correctness by Def6;
end;

definition
  let A be non empty set, o',o be BinOp of A;
  redefine pred o' is_left_distributive_wrt o means
  for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c));
  correctness by Def9;
  pred o' is_right_distributive_wrt o means
  for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));
  correctness by Def10;
end;

definition
  let A be non empty set, u be UnOp of A, o be BinOp of A;
  redefine pred u is_distributive_wrt o means
  for a,b being Element of A holds u.(o.(a,b)) = o.((u.a),(u.b));
  correctness by Def12;
end;

:: FUNCT_2, 2005.12.13, A.T.

theorem
  for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {}
  holds f.(x,y) in Z
proof
  let f be Function of [:X,Y:],Z;
  assume x in X & y in Y;
  then [x,y] in [:X,Y:] by ZFMISC_1:106;
  hence thesis by FUNCT_2:7;
end;

:: from TOPALG_3, 2005.12.14, A.T.

theorem
  for x, y, X, Y, Z being set, f being Function of [:X,Y:],Z, g being Function
  st Z <> {} & x in X & y in Y holds (g*f).(x,y) = g.(f.(x,y))
proof
  let x, y, X, Y, Z be set, f be Function of [:X,Y:],Z,
  g be Function such that
A1: Z <> {};
  assume x in X & y in Y;
  then [x,y] in [:X,Y:] by ZFMISC_1:106;
  hence (g*f).(x,y) = g.(f.(x,y)) by A1,FUNCT_2:21;
end;

:: missing, 2005.12.17, A.T.

theorem
  for f being Function st dom f = [:X,Y:] holds f is constant iff
  for x1,x2,y1,y2 st x1 in X & x2 in X & y1 in Y & y2 in Y
  holds f.(x1,y1)=f.(x2,y2)
proof
  let f be Function such that
A1: dom f = [:X,Y:];
  hereby
    assume
A2: f is constant;
    let x1,x2,y1,y2;
    assume x1 in X & x2 in X & y1 in Y & y2 in Y;
    then [x1,y1] in [:X,Y:] & [x2,y2] in [:X,Y:]by ZFMISC_1:106;
    hence f.(x1,y1)=f.(x2,y2) by A1,A2,FUNCT_1:def 16;
  end;
  assume
A3: for x1,x2,y1,y2 st x1 in X & x2 in X & y1 in Y & y2 in Y
  holds f.(x1,y1)=f.(x2,y2);
  let x,y;
  assume x in dom f;
  then consider x1,y1 such that
A4: x1 in X & y1 in Y & x = [x1,y1] by A1,ZFMISC_1:103;
  assume y in dom f;
  then consider x2,y2 such that
A5: x2 in X & y2 in Y & y = [x2,y2] by A1,ZFMISC_1:103;
  thus f.x = f.(x1,y1) by A4
    .= f.(x2,y2) by A3,A4,A5
    .= f.y by A5;
end;

:: from PARTFUN1, 2006.12.05, AT

theorem
  for f1,f2 being PartFunc of [:X,Y:],Z
  st dom f1 = dom f2 & for x,y st [x,y] in dom f1 holds f1.(x,y)=f2.(x,y)
  holds f1 = f2
proof
  let f1,f2 be PartFunc of [:X,Y:],Z such that
A1: dom f1 = dom f2 and
A2: for x,y st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y);
  z in dom f1 implies f1.z = f2.z
  proof
    assume
A3: z in dom f1;
    then consider x,y such that
A4: z = [x,y] by RELAT_1:def 1;
    f1.(x,y) = f2.(x,y) by A2,A3,A4;
    hence thesis by A4;
  end;
  hence thesis by A1,FUNCT_1:9;
end;

scheme PartFuncEx2{X,Y,Z()->set,P[set,set,set]}:
  ex f being PartFunc of [:X(),Y():],Z() st
  (for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st P[x,y,z]) &
  (for x,y st [x,y] in dom f holds P[x,y,f.(x,y)])
provided
A1: for x,y,z st x in X() & y in Y() & P[x,y,z] holds z in Z()
and
A2: for x,y,z1,z2 st x in X() & y in Y() & P[x,y,z1] & P[x,y,z2] holds z1 = z2
proof
  defpred Q[set,set] means for x1,y1 st $1 = [x1,y1] holds P[x1,y1,$2];
A3: for x,z st x in [:X(),Y():] & Q[x,z] holds z in Z()
  proof
    let x,z;
    assume x in [:X(),Y():];
    then consider x1,y1 such that
A4: x1 in X() & y1 in Y() and
A5: x = [x1,y1] by ZFMISC_1:def 2;
    assume for x1,y1 st x = [x1,y1] holds P[x1,y1,z];
    hence z in Z() by A1,A4,A5;
  end;
A6: for x,z1,z2 st x in [:X(),Y():] & Q[x,z1] & Q[x,z2] holds z1 = z2
  proof
    let x,z1,z2 such that
A7: x in [:X(),Y():] and
A8: (for x1,y1 st x = [x1,y1] holds P[x1,y1,z1]) and
A9: (for x1,y1 st x = [x1,y1] holds P[x1,y1,z2]);
    consider x1,y1 such that
A10: x1 in X() & y1 in Y() and
A11: x = [x1,y1] by A7,ZFMISC_1:def 2;
    P[x1,y1,z1] & P[x1,y1,z2] by A8,A9,A11;
    hence thesis by A2,A10;
  end;
  consider f being PartFunc of [:X(),Y():],Z() such that
A12: for x holds x in dom f iff x in [:X(),Y():] & ex z st Q[x,z] and
A13: for x st x in dom f holds Q[x,f.x] from PARTFUN1:sch 2(A3,A6);
  take f;
  thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st P[x,y,z
  ]
  proof
    let x,y;
    thus [x,y] in dom f implies x in X() & y in Y() & ex z st P[x,y,z]
    proof
      assume
A14:  [x,y] in dom f;
      hence x in X() & y in Y() by ZFMISC_1:106;
      consider z such that
A15:  for x1,y1 st [x,y] = [x1,y1] holds P[x1,y1,z] by A12,A14;
      take z;
      thus thesis by A15;
    end;
    assume x in X() & y in Y();
    then
A16: [x,y] in [:X(),Y():] by ZFMISC_1:def 2;
    given z such that
A17: P[x,y,z];
    now
      take z;
      let x1,y1;
      assume [x,y] = [x1,y1];
      then x=x1 & y=y1 by ZFMISC_1:33;
      hence P[x1,y1,z] by A17;
    end;
    hence thesis by A12,A16;
  end;
  thus thesis by A13;
end;

scheme LambdaR2{X,Y,Z()->set,F(set,set)->set,P[set,set]}:
  ex f being PartFunc of [:X(),Y():],Z()
  st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y]) &
  (for x,y st [x,y] in dom f holds f.(x,y) = F(x,y))
provided
A1: for x,y st P[x,y] holds F(x,y) in Z()
proof
  defpred Q[set,set,set] means P[$1,$2] & $3 = F($1,$2);
A2: for x,y,z st x in X() & y in Y() & Q[x,y,z] holds z in Z() by A1;
A3: for x,y,z1,z2 st x in X() & y in Y() & Q[x,y,z1] & Q[x,y,z2] holds z1 = z2;
  consider f being PartFunc of [:X(),Y():],Z() such that
A4: for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st Q[x,y,z] and
A5: for x,y st [x,y] in dom f holds Q[x,y,f.(x,y)] from PartFuncEx2(A2,A3);
  take f;
  thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y]
  proof
    let x,y;
    thus [x,y] in dom f implies x in X() & y in Y() & P[x,y]
    proof
      assume [x,y] in dom f;
      then x in X() & y in Y() & ex z st P[x,y] & z = F(x,y) by A4;
      hence thesis;
    end;
    assume x in X() & y in Y() & P[x,y];
    then x in X() & y in Y() & ex z st P[x,y] & z = F(x,y);
    hence thesis by A4;
  end;
  thus thesis by A5;
end;

:: from GRCAT_1, 2006.12.05, AT

scheme PartLambda2{X,Y,Z()->set,F(set,set)->set,P[set,set]}:
  ex f being PartFunc of [:X(),Y():],Z()
  st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y])
  & for x,y st [x,y] in dom f holds f.(x,y) = F(x,y)
provided
A1: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z()
proof
  defpred R[set,set] means $1 in X() & $2 in Y() & P[$1,$2];
A2: for x,y st R[x,y] holds F(x,y) in Z() by A1;
  consider f being PartFunc of [:X(),Y():],Z() such that
A3: for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y] and
A4: for x,y st [x,y] in dom f holds f.(x,y) = F(x,y) from LambdaR2(A2);
  take f;
  thus thesis by A3,A4;
end;

scheme {X,Y()->non empty set,Z()->set,F(set,set)->set,
  P[set,set]}: ex f being PartFunc of [:X(),Y():],Z()
  st (for x being Element of X(), y being Element of Y() holds
  [x,y] in dom f iff P[x,y])
  & for x being Element of X(), y being Element of Y() st [x,y] in dom f
  holds f.(x,y) = F(x,y)
provided
A1: for x being Element of X(), y being Element of Y() st P[x,y] holds
F(x,y) in Z()
proof
A2: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z() by A1;
  consider f being PartFunc of [:X(),Y():],Z() such that
A3: for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y] and
A4: for x,y st [x,y] in dom f holds f.(x,y) = F(x,y) from PartLambda2(A2);
  take f;
  thus thesis by A3,A4;
end;

:: 2007.11.22, A.T.

definition
  let A be set, f be BinOp of A, x,y be Element of A;
  redefine func f.(x,y) -> Element of A;
  coherence
  proof per cases;
    suppose
A1:   A = {};
      then [:A,A:] = {} by ZFMISC_1:113;
      then dom f = {};
      then f.(x,y) = {} by FUNCT_1:def 4;
      hence thesis by A1,SUBSET_1:def 2;
    end;
    suppose A <> {};
      then reconsider A as non empty set;
      reconsider f as BinOp of A;
      reconsider x,y as Element of A;
      f.(x,y) is Element of A;
      hence thesis;
    end;
  end;
end;