:: Three-Argument Operations and Four-Argument Operations :: by Michal Muzalewski and Wojciech Skaba :: :: Received October 2, 1990 :: 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, XBOOLE_0, SUBSET_1, ZFMISC_1, MULTOP_1; notations XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FUNCT_1, FUNCT_2, MCART_1, DOMAIN_1; constructors FUNCT_2, DOMAIN_1, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1; requirements SUBSET, BOOLE; begin :: THREE ARGUMENT OPERATIONS definition let f be Function; let a,b,c be object; 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 for set,x,y,z,s,t for object; 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; theorem :: MULTOP_1:1 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:2 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:3 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 :: MULTOP_1:sch 1 FuncEx3D { X,Y,Z,T() -> non empty set, P[object,object,object,object] } : 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 :: MULTOP_1:sch 2 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 :: MULTOP_1:sch 3 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 :: MULTOP_1:sch 4 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; theorem :: MULTOP_1:4 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:5 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:6 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 :: MULTOP_1:sch 5 FuncEx4D { X, Y, Z, S, T() -> non empty set, P[object,object,object,object,object] }: 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 :: MULTOP_1:sch 6 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 :: MULTOP_1:sch 7 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 :: MULTOP_1:sch 8 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);