:: Binary Operations :: by Czes{\l}aw Byli\'nski :: :: Received April 14, 1989 :: Copyright (c) 1990-2017 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, ZFMISC_1, SUBSET_1, TARSKI, RELAT_1, PARTFUN1, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2; constructors FUNCT_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1; requirements SUBSET, BOOLE; definitions FUNCT_1; expansions FUNCT_1; theorems RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, SUBSET_1, XTUPLE_0, TARSKI; schemes FUNCT_2, PARTFUN1; begin definition let f be Function; let a,b be object; 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 for set,x,x1,x2,y,y1,y2,z,z1,z2 for object; 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 object st z in [:X,Y:] holds f1.z = f2.z proof let z be object; assume z in [:X,Y:]; then consider x,y being object 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:12; 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 thesis 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,o9 for BinOp of A, a,b,c,e,e1,e2 for Element of A; scheme FuncEx2{X, Y, Z() -> set, P[object,object,object]}: 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[object,object] means for x1,y1 st \$1 = [x1,y1] holds P[x1,y1,\$2]; A2: for x being object st x in [:X(),Y():] ex z being object st z in Z() & R[x,z] proof let x be object; assume x in [:X(),Y():]; then consider x1,y1 being object 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 A7: x = [x2,y2]; then x1 = x2 by A4,XTUPLE_0:1; hence thesis by A4,A6,A7,XTUPLE_0:1; end; consider f being Function of [:X(),Y():],Z() such that A8: for x being object 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 A8; end; scheme Lambda2{X, Y, Z() -> set, F(object,object)->object}: 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[object,object,object] 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[object,object,object]}: 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 being object such that A3: x1 in X() and A4: y1 in Y() and A5: p = [x1,y1] by ZFMISC_1:def 2; reconsider y1 as Element of Y() by A4; reconsider x1 as Element of X() by A3; 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 A7: p = [x,y]; then x1 = x by A5,XTUPLE_0:1; hence thesis by A5,A6,A7,XTUPLE_0:1; end; consider f being Function of [:X(),Y():],Z() such that A8: 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 A8; 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 for a,b holds o.(a,b) = o.(b,a); attr o is associative means for a,b,c holds o.(a,o.(b,c)) = o.(o.(a,b ),c); attr o is idempotent means for a holds o.(a,a) = a; end; registration cluster -> empty associative commutative for BinOp of {}; coherence proof let f be BinOp of {}; thus f is empty; A1: f c= [:dom f, rng f:]; hereby let a,b,c be Element of {}; thus f.(a,f.(b,c)) = {} by A1,FUNCT_1:def 2 .= f.(f.(a,b),c) by A1,FUNCT_1:def 2; end; let a,b be Element of {}; thus f.(a,b) = {} by A1,FUNCT_1:def 2 .= f.(b,a) by A1,FUNCT_1:def 2; end; end; definition let A; let e be object; let o; pred e is_a_left_unity_wrt o means for a holds o.(e,a) = a; pred e is_a_right_unity_wrt o means for a holds o.(a,e) = a; end; definition let A; let e be object; let o; pred e is_a_unity_wrt o means e is_a_left_unity_wrt o & e is_a_right_unity_wrt o; end; theorem Th3: 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; 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 Th4: 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 .= a by A2; end; hence thesis by Th3; end; theorem Th5: 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 .= a by A2; thus o.(a,e) = a by A2; end; hence thesis by Th3; end; theorem Th6: o is commutative implies (e is_a_unity_wrt o iff e is_a_left_unity_wrt o) by Th4; theorem Th7: o is commutative implies (e is_a_unity_wrt o iff e is_a_right_unity_wrt o) by Th5; 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 Th6; hence thesis by A1,Th7; end; theorem Th9: 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 .= e2 by A1; end; theorem Th10: e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2 by Th9; 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 Th10; end; definition let A,o9,o; pred o9 is_left_distributive_wrt o means for a,b,c holds o9.(a,o.(b,c )) = o.(o9.(a,b),o9.(a,c)); pred o9 is_right_distributive_wrt o means for a,b,c holds o9.(o.(a,b ),c) = o.(o9.(a,c),o9.(b,c)); end; definition let A,o9,o; pred o9 is_distributive_wrt o means o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o; end; theorem Th11: o9 is_distributive_wrt o iff for a,b,c holds o9.(a,o.(b,c)) = o. (o9.(a,b),o9.(a,c)) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)) proof thus o9 is_distributive_wrt o implies for a,b,c holds o9.(a,o.(b,c)) = o.(o9 .(a,b),o9.(a,c)) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)) proof assume o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o; hence thesis; end; assume for a,b,c holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c)) & o9.(o.(a,b) ,c) = o.(o9.(a,c),o9.(b,c)); hence (for a,b,c holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c))) & for a,b,c holds o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)); end; theorem Th12: for A being non empty set, o,o9 being BinOp of A holds o9 is commutative implies (o9 is_distributive_wrt o iff for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c))) proof let A be non empty set, o,o9 be BinOp of A; assume A1: o9 is commutative; (for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c )) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c))) iff for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c)) proof thus (for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.( a,c)) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c))) implies for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c)); assume A2: for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9 .(a,c)); let a,b,c be Element of A; thus o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c)) by A2; thus o9.(o.(a,b),c) = o9.(c,o.(a,b)) by A1 .= o.(o9.(c,a),o9.(c,b)) by A2 .= o.(o9.(a,c),o9.(c,b)) by A1 .= o.(o9.(a,c),o9.(b,c)) by A1; end; hence thesis by Th11; end; theorem Th13: for A being non empty set, o,o9 being BinOp of A holds o9 is commutative implies (o9 is_distributive_wrt o iff for a,b,c being Element of A holds o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c))) proof let A be non empty set, o,o9 be BinOp of A; assume A1: o9 is commutative; (for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c )) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c))) iff for a,b,c being Element of A holds o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)) proof thus (for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.( a,c)) & o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c))) implies for a,b,c being Element of A holds o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)); assume A2: for a,b,c being Element of A holds o9.(o.(a,b),c) = o.(o9.(a,c),o9 .(b,c)); let a,b,c be Element of A; thus o9.(a,o.(b,c)) = o9.(o.(b,c),a) by A1 .= o.(o9.(b,a),o9.(c,a)) by A2 .= o.(o9.(a,b),o9.(c,a)) by A1 .= o.(o9.(a,b),o9.(a,c)) by A1; thus thesis by A2; end; hence thesis by Th11; end; theorem Th14: for A being non empty set, o,o9 being BinOp of A holds o9 is commutative implies (o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) by Th12; theorem Th15: for A being non empty set, o,o9 being BinOp of A holds o9 is commutative implies (o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o) by Th13; theorem for A being non empty set, o,o9 being BinOp of A holds o9 is commutative implies (o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o) proof let A be non empty set, o,o9 be BinOp of A; assume A1: o9 is commutative; then o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o by Th14; hence thesis by A1,Th15; end; definition let A,u,o; pred u is_distributive_wrt o means for a,b holds u.(o.(a,b)) = o.((u .a),(u.b)); end; definition ::\$CD 3 let A be non empty set, e be object, 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; redefine pred e is_a_right_unity_wrt o means for a being Element of A holds o.(a,e) = a; correctness; end; definition let A be non empty set, o9,o be BinOp of A; redefine pred o9 is_left_distributive_wrt o means for a,b,c being Element of A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c)); correctness; redefine pred o9 is_right_distributive_wrt o means for a,b,c being Element of A holds o9.(o.(a,b),c) = o.(o9.(a,c),o9.(b,c)); correctness; 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; 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:87; hence thesis by FUNCT_2:5; end; :: from TOPALG_3, 2005.12.14, A.T. theorem for x, y being object, 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)) by FUNCT_2:15,ZFMISC_1:87; :: 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:87; hence f.(x1,y1)=f.(x2,y2) by A1,A2; 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 be object; assume x in dom f; then consider x1,y1 being object such that A4: x1 in X & y1 in Y and A5: x = [x1,y1] by A1,ZFMISC_1:84; assume y in dom f; then consider x2,y2 being object such that A6: x2 in X & y2 in Y and A7: y = [x2,y2] by A1,ZFMISC_1:84; thus f.x = f.(x1,y1) by A5 .= f.(x2,y2) by A3,A4,A6 .= f.y by A7; 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 being object 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 being object st [x,y] in dom f1 holds f1.(x,y) = f2.(x,y); for z being object holds z in dom f1 implies f1.z = f2.z proof let z be object; assume A3: z in dom f1; then consider x,y being object 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; end; scheme PartFuncEx2{X,Y,Z()->set,P[object,object,object]}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y being object holds [x,y] in dom f iff x in X() & y in Y() & ex z being object st P[x,y,z]) & for x,y being object st [x,y] in dom f holds P[x,y,f.(x,y)] provided A1: for x,y,z being object st x in X() & y in Y() & P[x,y,z] holds z in Z() and A2: for x,y,z1,z2 being object st x in X() & y in Y() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 proof defpred Q[object,object] means for x1,y1 being object st \$1 = [x1,y1] holds P[x1,y1,\$2]; A3: for x,z being object st x in [:X(),Y():] & Q[x,z] holds z in Z() proof let x,z be object; assume x in [:X(),Y():]; then A4: ex x1,y1 being object st x1 in X() & y1 in Y() & x = [x1,y1] by ZFMISC_1:def 2; assume for x1,y1 being object st x = [x1,y1] holds P[x1,y1,z]; hence thesis by A1,A4; end; A5: for x,z1,z2 being object st x in [:X(),Y():] & Q[x,z1] & Q[x,z2] holds z1 = z2 proof let x,z1,z2 be object such that A6: x in [:X(),Y():] and A7: ( for x1,y1 being object st x = [x1,y1] holds P[x1,y1,z1])& for x1,y1 being object st x = [ x1,y1] holds P[x1,y1,z2]; consider x1,y1 being object such that A8: x1 in X() & y1 in Y() and A9: x = [x1,y1] by A6,ZFMISC_1:def 2; ( P[x1,y1,z1])& P[x1,y1,z2] by A7,A9; hence thesis by A2,A8; end; consider f being PartFunc of [:X(),Y():],Z() such that A10: for x being object holds x in dom f iff x in [:X(),Y():] & ex z being object st Q[x,z] and A11: for x being object st x in dom f holds Q[x,f.x] from PARTFUN1:sch 2(A3,A5); take f; thus for x,y being object holds [x,y] in dom f iff x in X() & y in Y() & ex z being object st P[x,y,z ] proof let x,y be object; thus [x,y] in dom f implies x in X() & y in Y() & ex z being object st P[x,y,z] proof assume A12: [x,y] in dom f; hence x in X() & y in Y() by ZFMISC_1:87; consider z being object such that A13: for x1,y1 being object st [x,y] = [x1,y1] holds P[x1,y1,z] by A10,A12; take z; thus thesis by A13; end; assume x in X() & y in Y(); then A14: [x,y] in [:X(),Y():] by ZFMISC_1:def 2; given z being object such that A15: P[x,y,z]; now take z; let x1,y1 be object; assume A16: [x,y] = [x1,y1]; then x=x1 by XTUPLE_0:1; hence P[x1,y1,z] by A15,A16,XTUPLE_0:1; end; hence thesis by A10,A14; end; thus thesis by A11; end; scheme LambdaR2{X,Y,Z()->set,F(object,object)->object, P[object,object]}: 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[object,object,object] means P[\$1,\$2] & \$3 = F(\$1,\$2); A2: for x,y,z1,z2 being object st x in X() & y in Y() & Q[x,y,z1] & Q[x,y,z2] holds z1 = z2; A3: for x,y,z being object st x in X() & y in Y() & Q[x,y,z] holds z in Z() by A1; consider f being PartFunc of [:X(),Y():],Z() such that A4: for x,y being object holds [x,y] in dom f iff x in X() & y in Y() & ex z being object st Q[x,y,z] and A5: for x,y being object st [x,y] in dom f holds Q[x,y,f.(x,y)] from PartFuncEx2(A3, A2 ); 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 A6: [x,y] in dom f; then ex z being object st P[x,y] & z = F(x,y) by A4; hence thesis by A4,A6; end; assume that A7: x in X() & y in Y() and A8: P[x,y]; ex z being object st P[x,y] & z = F(x,y) by A8; hence thesis by A4,A7; end; thus thesis by A5; end; :: from GRCAT_1, 2006.12.05, AT scheme PartLambda2{X,Y,Z()->set,F(object,object)->object, P[object,object]}: 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[object,object] 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])& 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; end; scheme {X,Y()->non empty set,Z()->set,F(object,object)->object, P[object,object]}: 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])& 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; end; definition let A be set, f be BinOp of A; let a,b be Element of A; redefine func f.(a,b) -> Element of A; coherence proof per cases; suppose A <> {}; then reconsider A as non empty set; reconsider f as BinOp of A; reconsider ab = [a,b] as Element of [:A,A:] by ZFMISC_1:def 2; f.ab is Element of A; hence thesis; end; suppose A1: A = {}; then not [a,b] in dom f; then f.(a,b) = {} by FUNCT_1:def 2; hence thesis by A1,SUBSET_1:def 1; end; end; end; definition let X,Y,Z be set; let f1,f2 being Function of [:X,Y:],Z; redefine pred f1 = f2 means for x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y); compatibility by Th1; end; scheme {X, Y, Z() -> set, P[object,object,object]}: ex f being Function of [:X(),Y():],Z() st for x,y being set st x in X() & y in Y() holds P[x,y,f.(x,y)] provided A1: for x,y being set st x in X() & y in Y() ex z being set st z in Z() & P[x,y,z]; A2: for x,y being object st x in X() & y in Y() ex z being object st z in Z() & P[x,y,z] proof let x,y be object such that A3: x in X() & y in Y(); reconsider x,y as set by TARSKI:1; consider z being set such that A4: z in Z() & P[x,y,z] by A3,A1; take z; z in Z() & P[x,y,z] by A4; hence thesis; end; consider f being Function of [:X(),Y():],Z() such that A5: for x,y being object st x in X() & y in Y() holds P[x,y,f.(x,y)] from FuncEx2(A2); take f; thus thesis by A5; end;