binop_1.miz
begin
definition
let f be
Function;
let a,b be
object;
::
BINOP_1:def1
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;
:: original:
.
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 ::
BINOP_1:1
Th1: for X,Y,Z be
set holds for f1,f2 be
Function of
[:X, Y:], Z st for x,y be
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 be
set st x
in X & y
in Y holds (f1
. (x,y))
= (f2
. (x,y));
for z be
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 be
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 ::
BINOP_1:2
for f1,f2 be
Function of
[:X, Y:], Z st for a be
Element of X holds for b be
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 be
Element of X holds for b be
Element of Y holds (f1
. (a,b))
= (f2
. (a,b));
then for x,y be
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 ::
BINOP_1:sch1
FuncEx2 { X,Y,Z() ->
set , P[
object,
object,
object] } :
ex f be
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() holds ex z st z
in Z() & P[x, y, z];
defpred
R[
object,
object] means for x1, y1 st $1
=
[x1, y1] holds P[x1, y1, $2];
A2: for x be
object st x
in
[:X(), Y():] holds ex z be
object st z
in Z() &
R[x, z]
proof
let x be
object;
assume x
in
[:X(), Y():];
then
consider x1,y1 be
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 be
Function of
[:X(), Y():], Z() such that
A8: for x be
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 ::
BINOP_1:sch2
Lambda2 { X,Y,Z() ->
set , F(
object,
object) ->
object } :
ex f be
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();
defpred
P[
object,
object,
object] means $3
= F($1,$2);
A2: for x, y st x
in X() & y
in Y() holds ex z st z
in Z() &
P[x, y, z] by
A1;
thus ex f be
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 ::
BINOP_1:sch3
FuncEx2D { X,Y,Z() -> non
empty
set , P[
object,
object,
object] } :
ex f be
Function of
[:X(), Y():], Z() st for x be
Element of X() holds for y be
Element of Y() holds P[x, y, (f
. (x,y))]
provided
A1: for x be
Element of X() holds for y be
Element of Y() holds ex z be
Element of Z() st P[x, y, z];
defpred
R[
set,
set] means for x be
Element of X(), y be
Element of Y() st $1
=
[x, y] holds P[x, y, $2];
A2: for p be
Element of
[:X(), Y():] holds ex z be
Element of Z() st
R[p, z]
proof
let p be
Element of
[:X(), Y():];
consider x1,y1 be
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 be
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 be
Function of
[:X(), Y():], Z() such that
A8: for p be
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 ::
BINOP_1:sch4
Lambda2D { X,Y,Z() -> non
empty
set , F(
Element of X(),
Element of Y()) ->
Element of Z() } :
ex f be
Function of
[:X(), Y():], Z() st for x be
Element of X() holds for y be
Element of Y() holds (f
. (x,y))
= F(x,y);
defpred
P[
Element of X(),
Element of Y(),
set] means $3
= F($1,$2);
A1: for x be
Element of X() holds for y be
Element of Y() holds ex z be
Element of Z() st
P[x, y, z];
thus ex f be
Function of
[:X(), Y():], Z() st for x be
Element of X() holds for y be
Element of Y() holds
P[x, y, (f
. (x,y))] from
FuncEx2D(
A1);
end;
definition
let A, o;
::
BINOP_1:def2
attr o is
commutative means for a, b holds (o
. (a,b))
= (o
. (b,a));
::
BINOP_1:def3
attr o is
associative means for a, b, c holds (o
. (a,(o
. (b,c))))
= (o
. ((o
. (a,b)),c));
::
BINOP_1:def4
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;
::
BINOP_1:def5
pred e
is_a_left_unity_wrt o means for a holds (o
. (e,a))
= a;
::
BINOP_1:def6
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;
::
BINOP_1:def7
pred e
is_a_unity_wrt o means e
is_a_left_unity_wrt o & e
is_a_right_unity_wrt o;
end
theorem ::
BINOP_1:3
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 ::
BINOP_1:4
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 ::
BINOP_1:5
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 ::
BINOP_1:6
Th6: o is
commutative implies (e
is_a_unity_wrt o iff e
is_a_left_unity_wrt o) by
Th4;
theorem ::
BINOP_1:7
Th7: o is
commutative implies (e
is_a_unity_wrt o iff e
is_a_right_unity_wrt o) by
Th5;
theorem ::
BINOP_1:8
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 ::
BINOP_1:9
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 ::
BINOP_1:10
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;
::
BINOP_1:def8
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;
::
BINOP_1:def9
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))));
::
BINOP_1:def10
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;
::
BINOP_1:def11
pred o9
is_distributive_wrt o means o9
is_left_distributive_wrt o & o9
is_right_distributive_wrt o;
end
theorem ::
BINOP_1:11
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 ::
BINOP_1:12
Th12: for A be non
empty
set, o,o9 be
BinOp of A holds o9 is
commutative implies (o9
is_distributive_wrt o iff for a,b,c be
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 be
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 be
Element of A holds (o9
. (a,(o
. (b,c))))
= (o
. ((o9
. (a,b)),(o9
. (a,c))))
proof
thus (for a,b,c be
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 be
Element of A holds (o9
. (a,(o
. (b,c))))
= (o
. ((o9
. (a,b)),(o9
. (a,c))));
assume
A2: for a,b,c be
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 ::
BINOP_1:13
Th13: for A be non
empty
set, o,o9 be
BinOp of A holds o9 is
commutative implies (o9
is_distributive_wrt o iff for a,b,c be
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 be
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 be
Element of A holds (o9
. ((o
. (a,b)),c))
= (o
. ((o9
. (a,c)),(o9
. (b,c))))
proof
thus (for a,b,c be
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 be
Element of A holds (o9
. ((o
. (a,b)),c))
= (o
. ((o9
. (a,c)),(o9
. (b,c))));
assume
A2: for a,b,c be
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 ::
BINOP_1:14
Th14: for A be non
empty
set, o,o9 be
BinOp of A holds o9 is
commutative implies (o9
is_distributive_wrt o iff o9
is_left_distributive_wrt o) by
Th12;
theorem ::
BINOP_1:15
Th15: for A be non
empty
set, o,o9 be
BinOp of A holds o9 is
commutative implies (o9
is_distributive_wrt o iff o9
is_right_distributive_wrt o) by
Th13;
theorem ::
BINOP_1:16
for A be non
empty
set, o,o9 be
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;
::
BINOP_1:def12
pred u
is_distributive_wrt o means for a, b holds (u
. (o
. (a,b)))
= (o
. ((u
. a),(u
. b)));
end
definition
::$Canceled
let A be non
empty
set, e be
object, o be
BinOp of A;
:: original:
is_a_left_unity_wrt
redefine
::
BINOP_1:def16
pred e
is_a_left_unity_wrt o means for a be
Element of A holds (o
. (e,a))
= a;
correctness ;
:: original:
is_a_right_unity_wrt
redefine
::
BINOP_1:def17
pred e
is_a_right_unity_wrt o means for a be
Element of A holds (o
. (a,e))
= a;
correctness ;
end
definition
let A be non
empty
set, o9,o be
BinOp of A;
:: original:
is_left_distributive_wrt
redefine
::
BINOP_1:def18
pred o9
is_left_distributive_wrt o means for a,b,c be
Element of A holds (o9
. (a,(o
. (b,c))))
= (o
. ((o9
. (a,b)),(o9
. (a,c))));
correctness ;
:: original:
is_right_distributive_wrt
redefine
::
BINOP_1:def19
pred o9
is_right_distributive_wrt o means for a,b,c be
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;
:: original:
is_distributive_wrt
redefine
::
BINOP_1:def20
pred u
is_distributive_wrt o means for a,b be
Element of A holds (u
. (o
. (a,b)))
= (o
. ((u
. a),(u
. b)));
correctness ;
end
theorem ::
BINOP_1:17
for f be
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;
theorem ::
BINOP_1:18
for x,y be
object, X,Y,Z be
set, f be
Function of
[:X, Y:], Z, g be
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;
theorem ::
BINOP_1:19
for f be
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 be
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 be
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;
theorem ::
BINOP_1:20
for f1,f2 be
PartFunc of
[:X, Y:], Z st (
dom f1)
= (
dom f2) & for x,y be
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 be
object st
[x, y]
in (
dom f1) holds (f1
. (x,y))
= (f2
. (x,y));
for z be
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 be
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 ::
BINOP_1:sch5
PartFuncEx2 { X,Y,Z() ->
set , P[
object,
object,
object] } :
ex f be
PartFunc of
[:X(), Y():], Z() st (for x,y be
object holds
[x, y]
in (
dom f) iff x
in X() & y
in Y() & ex z be
object st P[x, y, z]) & for x,y be
object st
[x, y]
in (
dom f) holds P[x, y, (f
. (x,y))]
provided
A1: for x,y,z be
object st x
in X() & y
in Y() & P[x, y, z] holds z
in Z()
and
A2: for x,y,z1,z2 be
object st x
in X() & y
in Y() & P[x, y, z1] & P[x, y, z2] holds z1
= z2;
defpred
Q[
object,
object] means for x1,y1 be
object st $1
=
[x1, y1] holds P[x1, y1, $2];
A3: for x,z be
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 be
object st x1
in X() & y1
in Y() & x
=
[x1, y1] by
ZFMISC_1:def 2;
assume for x1,y1 be
object st x
=
[x1, y1] holds P[x1, y1, z];
hence thesis by
A1,
A4;
end;
A5: for x,z1,z2 be
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 be
object st x
=
[x1, y1] holds P[x1, y1, z1]) & for x1,y1 be
object st x
=
[x1, y1] holds P[x1, y1, z2];
consider x1,y1 be
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 be
PartFunc of
[:X(), Y():], Z() such that
A10: for x be
object holds x
in (
dom f) iff x
in
[:X(), Y():] & ex z be
object st
Q[x, z] and
A11: for x be
object st x
in (
dom f) holds
Q[x, (f
. x)] from
PARTFUN1:sch 2(
A3,
A5);
take f;
thus for x,y be
object holds
[x, y]
in (
dom f) iff x
in X() & y
in Y() & ex z be
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 be
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 be
object such that
A13: for x1,y1 be
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 be
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 ::
BINOP_1:sch6
LambdaR2 { X,Y,Z() ->
set , F(
object,
object) ->
object , P[
object,
object] } :
ex f be
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();
defpred
Q[
object,
object,
object] means P[$1, $2] & $3
= F($1,$2);
A2: for x,y,z1,z2 be
object st x
in X() & y
in Y() &
Q[x, y, z1] &
Q[x, y, z2] holds z1
= z2;
A3: for x,y,z be
object st x
in X() & y
in Y() &
Q[x, y, z] holds z
in Z() by
A1;
consider f be
PartFunc of
[:X(), Y():], Z() such that
A4: for x,y be
object holds
[x, y]
in (
dom f) iff x
in X() & y
in Y() & ex z be
object st
Q[x, y, z] and
A5: for x,y be
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 be
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 be
object st P[x, y] & z
= F(x,y) by
A8;
hence thesis by
A4,
A7;
end;
thus thesis by
A5;
end;
scheme ::
BINOP_1:sch7
PartLambda2 { X,Y,Z() ->
set , F(
object,
object) ->
object , P[
object,
object] } :
ex f be
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();
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 be
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 ::
BINOP_1:sch8
{ X,Y() -> non
empty
set , Z() ->
set , F(
object,
object) ->
object , P[
object,
object] } :
ex f be
PartFunc of
[:X(), Y():], Z() st (for x be
Element of X(), y be
Element of Y() holds
[x, y]
in (
dom f) iff P[x, y]) & for x be
Element of X(), y be
Element of Y() st
[x, y]
in (
dom f) holds (f
. (x,y))
= F(x,y)
provided
A1: for x be
Element of X(), y be
Element of Y() st P[x, y] holds F(x,y)
in Z();
A2: for x, y st x
in X() & y
in Y() & P[x, y] holds F(x,y)
in Z() by
A1;
consider f be
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;
:: original:
.
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 be
Function of
[:X, Y:], Z;
:: original:
=
redefine
::
BINOP_1:def21
pred f1
= f2 means for x,y be
set st x
in X & y
in Y holds (f1
. (x,y))
= (f2
. (x,y));
compatibility by
Th1;
end
scheme ::
BINOP_1:sch9
{ X,Y,Z() ->
set , P[
object,
object,
object] } :
ex f be
Function of
[:X(), Y():], Z() st for x,y be
set st x
in X() & y
in Y() holds P[x, y, (f
. (x,y))]
provided
A1: for x,y be
set st x
in X() & y
in Y() holds ex z be
set st z
in Z() & P[x, y, z];
A2: for x,y be
object st x
in X() & y
in Y() holds ex z be
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 be
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 be
Function of
[:X(), Y():], Z() such that
A5: for x,y be
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;