The abstract of the Mizar article:

Three-Argument Operations and Four-Argument Operations

by

Michal Muzalewski, and

Wojciech Skaba

Received October 2, 1990

MML identifier: MULTOP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, MULTOP_1;
 notation XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, MCART_1, DOMAIN_1;
 constructors FUNCT_2, DOMAIN_1, MEMBERED, XBOOLE_0;
 clusters RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: THREE ARGUMENT OPERATIONS

definition
  let f be Function;
  let a,b,c be set;
  func f.(a,b,c) -> set equals
:: MULTOP_1:def 1
    f.[a,b,c];
end;

 reserve A,B,C,D,E for non empty set,
         a for Element of A, b for Element of B,
         c for Element of C, d for Element of D,
         X,Y,Z,S,x,y,z,s,t for set;

definition
  let A,B,C,D;
  let f be Function of [:A,B,C:],D;
  let a,b,c;
  redefine func f.(a,b,c) -> Element of D;
end;

canceled;

theorem :: MULTOP_1:2
   for f1,f2 being Function of [:X,Y,Z:],D st
    for x,y,z st x in X & y in Y & z in Z holds f1.[x,y,z] = f2.[x,y,z]
       holds f1 = f2;

theorem :: MULTOP_1:3
   for f1,f2 being Function of [:A,B,C:],D
       st for a,b,c holds f1.[a,b,c] = f2.[a,b,c]
       holds f1 = f2;

theorem :: MULTOP_1:4
    for f1,f2 being Function of [:A,B,C:],D st
    for a being Element of A
    for b being Element of B
    for c being Element of C
   holds
     f1.(a,b,c) = f2.(a,b,c)
     holds f1 = f2;

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

scheme FuncEx3D
  { X,Y,Z,T() -> non empty set, P[set,set,set,set] } :
 ex f being Function of [:X(),Y(),Z():],T() st
   for x being Element of X()
   for y being Element of Y()
   for z being Element of Z()
    holds P[x,y,z,f.[x,y,z]]
provided
 for x being Element of X()
    for y being Element of Y()
    for z being Element of Z()
      ex t being Element of T() st P[x,y,z,t];

scheme TriOpEx
  { A()->non empty set,
    P[ Element of A(), Element of A(), Element of A(), Element of A()] }:
    ex o being TriOp of A() st
    for a,b,c being Element of A() holds P[a,b,c,o.(a,b,c)]
      provided
 for x,y,z being Element of A() ex t being Element of A() st P[x,y,z,t];

scheme Lambda3D
  { X, Y, Z, T()->non empty set,
    F( Element of X(), Element of Y(), Element of Z()) -> Element of T()
  }:
 ex f being Function of [:X(),Y(),Z():],T()
  st for x being Element of X()
     for y being Element of Y()
     for z being Element of Z()
       holds f.[x,y,z]=F(x,y,z);

scheme TriOpLambda
  { A,B,C,D()->non empty set,
    O( Element of A(), Element of B(), Element of C()) -> Element of D()
  }:
 ex o being Function of [:A(),B(),C():],D() st
    for a being Element of A(),
        b being Element of B(),
        c being Element of C() holds o.(a,b,c) = O(a,b,c);

:: FOUR ARGUMENT OPERATIONS

definition
  let f be Function;
  let a,b,c,d be set;
  func f.(a,b,c,d) -> set equals
:: MULTOP_1:def 2
    f.[a,b,c,d];
end;

definition
  let A,B,C,D,E;
  let f be Function of [:A,B,C,D:],E;
  let a,b,c,d;
  redefine func f.(a,b,c,d) -> Element of E;
end;

canceled;

theorem :: MULTOP_1:6
   for f1,f2 being Function of [:X,Y,Z,S:],D st
   for x,y,z,s st x in X & y in Y & z in Z & s in S
     holds f1.[x,y,z,s] = f2.[x,y,z,s]
       holds
         f1 = f2;

theorem :: MULTOP_1:7
   for f1,f2 being Function of [:A,B,C,D:],E
      st for a,b,c,d holds f1.[a,b,c,d] = f2.[a,b,c,d]
       holds f1 = f2;

theorem :: MULTOP_1:8
    for f1,f2 being Function of [:A,B,C,D:],E st
    for a,b,c,d holds f1.(a,b,c,d) = f2.(a,b,c,d)
     holds f1 = f2;

definition let A;
 mode QuaOp of A is Function of [:A,A,A,A:],A;
end;

scheme FuncEx4D
  { X, Y, Z, S, T() -> non empty set, P[set,set,set,set,set] }:
 ex f being Function of [:X(),Y(),Z(),S():],T() st
   for x being Element of X()
   for y being Element of Y()
   for z being Element of Z()
   for s being Element of S()
    holds P[x,y,z,s,f.[x,y,z,s]]
provided
 for x being Element of X()
    for y being Element of Y()
    for z being Element of Z()
    for s being Element of S()
      ex t being Element of T() st P[x,y,z,s,t];

scheme QuaOpEx
  { A()->non empty set,
    P[ Element of A(), Element of A(),
       Element of A(), Element of A(), Element of A()] }:
    ex o being QuaOp of A() st
    for a,b,c,d being Element of A() holds P[a,b,c,d,o.(a,b,c,d)]
      provided
 for x,y,z,s being Element of A()
      ex t being Element of A() st P[x,y,z,s,t];

scheme Lambda4D
  { X, Y, Z, S, T() -> non empty set,
    F( Element of X(), Element of Y(),
       Element of Z(), Element of S()) -> Element of T() }:
 ex f being Function of [:X(),Y(),Z(),S():],T()
  st for x being Element of X()
     for y being Element of Y()
     for z being Element of Z()
     for s being Element of S()
       holds f.[x,y,z,s]=F(x,y,z,s);

scheme QuaOpLambda
  { A()->non empty set, O( Element of A(), Element of A(),
       Element of A(), Element of A()) -> Element of A() }:
 ex o being QuaOp of A() st
    for a,b,c,d being Element of A() holds o.(a,b,c,d) = O(a,b,c,d);