:: Binary Operations
:: by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 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; :: redefines . (BINOP_1, definition)
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 :: redefines is_a_left_unity_wrt (BINOP_1, definition)
for a being Element of A holds o .(e,a) = a;
correctness;
redefine pred e is_a_right_unity_wrt o means :: redefines is_a_right_unity_wrt (BINOP_1, definition)
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 :: redefines is_left_distributive_wrt (BINOP_1, definition)
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 :: redefines is_right_distributive_wrt (BINOP_1, definition)
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 :: redefines is_distributive_wrt (BINOP_1, definition)
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; :: redefines . (BINOP_1, definition)
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 :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
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;