:: by Czes{\l}aw Byli\'nski

::

:: Received April 14, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: deftheorem defines . BINOP_1:def 1 :

for f being Function

for a, b being set holds f . (a,b) = f . [a,b];

for f being Function

for a, b being set holds f . (a,b) = f . [a,b];

definition

let A, B be non empty set ;

let C be set ;

let 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

f . (a,b) is Element of C

end;
let C be set ;

let 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

f . (a,b) is Element of C

proof end;

theorem Th1: :: BINOP_1:1

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

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 end;

theorem :: BINOP_1:2

for X, Y, Z being set

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

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 end;

definition
end;

definition

let A be set ;

let f be BinOp of A;

let a, b be Element of A;

:: original: .

redefine func f . (a,b) -> Element of A;

coherence

f . (a,b) is Element of A

end;
let f be BinOp of A;

let a, b be Element of A;

:: original: .

redefine func f . (a,b) -> Element of A;

coherence

f . (a,b) is Element of A

proof end;

scheme :: BINOP_1:sch 1

FuncEx2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , P_{1}[ set , set , set ] } :

FuncEx2{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x, y being set st x in F_{1}() & y in F_{2}() holds

P_{1}[x,y,f . (x,y)]

providedfor x, y being set st x in F

P

A1:
for x, y being set st x in F_{1}() & y in F_{2}() holds

ex z being set st

( z in F_{3}() & P_{1}[x,y,z] )

ex z being set st

( z in F

proof end;

scheme :: BINOP_1:sch 3

FuncEx2D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ set , set , set ] } :

FuncEx2D{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x being Element of F_{1}()

for y being Element of F_{2}() holds P_{1}[x,y,f . (x,y)]

providedfor x being Element of F

for y being Element of F

A1:
for x being Element of F_{1}()

for y being Element of F_{2}() ex z being Element of F_{3}() st P_{1}[x,y,z]

for y being Element of F

proof end;

scheme :: BINOP_1:sch 4

Lambda2D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( Element of F_{1}(), Element of F_{2}()) -> Element of F_{3}() } :

Lambda2D{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x being Element of F_{1}()

for y being Element of F_{2}() holds f . (x,y) = F_{4}(x,y)

for x being Element of F

for y being Element of F

proof end;

definition

let A be set ;

let o be BinOp of A;

end;
let o be BinOp of A;

attr o is commutative means :Def2: :: BINOP_1:def 2

for a, b being Element of A holds o . (a,b) = o . (b,a);

for a, b being Element of A holds o . (a,b) = o . (b,a);

attr o is associative means :: BINOP_1:def 3

for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c);

for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c);

:: deftheorem Def2 defines commutative BINOP_1:def 2 :

for A being set

for o being BinOp of A holds

( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) );

for A being set

for o being BinOp of A holds

( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) );

:: deftheorem defines associative BINOP_1:def 3 :

for A being set

for o being BinOp of A holds

( o is associative iff for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c) );

for A being set

for o being BinOp of A holds

( o is associative iff for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c) );

:: deftheorem defines idempotent BINOP_1:def 4 :

for A being set

for o being BinOp of A holds

( o is idempotent iff for a being Element of A holds o . (a,a) = a );

for A being set

for o being BinOp of A holds

( o is idempotent iff for a being Element of A holds o . (a,a) = a );

registration

for b_{1} being BinOp of {} holds

( b_{1} is empty & b_{1} is associative & b_{1} is commutative )
end;

cluster Function-like V18([:{},{}:], {} ) -> empty commutative associative for Element of bool [:[:{},{}:],{}:];

coherence for b

( b

proof end;

definition

let A be set ;

let e be Element of A;

let o be BinOp of A;

end;
let e be Element of A;

let o be BinOp of A;

pred e is_a_left_unity_wrt o means :Def5: :: BINOP_1:def 5

for a being Element of A holds o . (e,a) = a;

for a being Element of A holds o . (e,a) = a;

pred e is_a_right_unity_wrt o means :Def6: :: BINOP_1:def 6

for a being Element of A holds o . (a,e) = a;

for a being Element of A holds o . (a,e) = a;

:: deftheorem Def5 defines is_a_left_unity_wrt BINOP_1:def 5 :

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

:: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def 6 :

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

definition

let A be set ;

let e be Element of A;

let o be BinOp of A;

end;
let e be Element of A;

let o be BinOp of A;

pred e is_a_unity_wrt o means :: BINOP_1:def 7

( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o );

( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o );

:: deftheorem defines is_a_unity_wrt BINOP_1:def 7 :

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_unity_wrt o iff ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) );

for A being set

for e being Element of A

for o being BinOp of A holds

( e is_a_unity_wrt o iff ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) );

theorem Th3: :: BINOP_1:3

for A being set

for o being BinOp of A

for e being Element of A holds

( e is_a_unity_wrt o iff for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) )

for o being BinOp of A

for e being Element of A holds

( e is_a_unity_wrt o iff for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) )

proof end;

theorem Th4: :: BINOP_1:4

for A being set

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )

proof end;

theorem Th5: :: BINOP_1:5

for A being set

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a )

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a )

proof end;

theorem Th6: :: BINOP_1:6

for A being set

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff e is_a_left_unity_wrt o )

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff e is_a_left_unity_wrt o )

proof end;

theorem Th7: :: BINOP_1:7

for A being set

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff e is_a_right_unity_wrt o )

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_unity_wrt o iff e is_a_right_unity_wrt o )

proof end;

theorem :: BINOP_1:8

for A being set

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )

for o being BinOp of A

for e being Element of A st o is commutative holds

( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )

proof end;

theorem Th9: :: BINOP_1:9

for A being set

for o being BinOp of A

for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds

e1 = e2

for o being BinOp of A

for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds

e1 = e2

proof end;

theorem Th10: :: BINOP_1:10

for A being set

for o being BinOp of A

for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds

e1 = e2

for o being BinOp of A

for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds

e1 = e2

proof end;

definition

let A be set ;

let o be BinOp of A;

assume A1: ex e being Element of A st e is_a_unity_wrt o ;

existence

ex b_{1} being Element of A st b_{1} is_a_unity_wrt o
by A1;

uniqueness

for b_{1}, b_{2} being Element of A st b_{1} is_a_unity_wrt o & b_{2} is_a_unity_wrt o holds

b_{1} = b_{2}
by Th10;

end;
let o be BinOp of A;

assume A1: ex e being Element of A st e is_a_unity_wrt o ;

existence

ex b

uniqueness

for b

b

:: deftheorem defines the_unity_wrt BINOP_1:def 8 :

for A being set

for o being BinOp of A st ex e being Element of A st e is_a_unity_wrt o holds

for b_{3} being Element of A holds

( b_{3} = the_unity_wrt o iff b_{3} is_a_unity_wrt o );

for A being set

for o being BinOp of A st ex e being Element of A st e is_a_unity_wrt o holds

for b

( b

definition

let A be set ;

let o9, o be BinOp of A;

end;
let o9, o be BinOp of A;

pred o9 is_left_distributive_wrt o means :Def9: :: BINOP_1:def 9

for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c)));

for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c)));

pred o9 is_right_distributive_wrt o means :Def10: :: BINOP_1:def 10

for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)));

for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)));

:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def 9 :

for A being set

for o9, o being BinOp of A holds

( o9 is_left_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))) );

for A being set

for o9, o being BinOp of A holds

( o9 is_left_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))) );

:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def 10 :

for A being set

for o9, o being BinOp of A holds

( o9 is_right_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))) );

for A being set

for o9, o being BinOp of A holds

( o9 is_right_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))) );

definition

let A be set ;

let o9, o be BinOp of A;

end;
let o9, o be BinOp of A;

pred o9 is_distributive_wrt o means :: BINOP_1:def 11

( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o );

( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o );

:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :

for A being set

for o9, o being BinOp of A holds

( o9 is_distributive_wrt o iff ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) );

for A being set

for o9, o being BinOp of A holds

( o9 is_distributive_wrt o iff ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) );

theorem Th11: :: BINOP_1:11

for A being set

for o9, o being BinOp of A holds

( 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))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )

for o9, o being BinOp of A holds

( 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))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )

proof end;

theorem Th12: :: BINOP_1:12

for A being non empty set

for o, o9 being BinOp of A st o9 is commutative holds

( 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))) )

for o, o9 being BinOp of A st o9 is commutative holds

( 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 end;

theorem Th13: :: BINOP_1:13

for A being non empty set

for o, o9 being BinOp of A st o9 is commutative holds

( 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))) )

for o, o9 being BinOp of A st o9 is commutative holds

( 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 end;

theorem Th14: :: BINOP_1:14

for A being non empty set

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o )

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o )

proof end;

theorem Th15: :: BINOP_1:15

for A being non empty set

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o )

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o )

proof end;

theorem :: BINOP_1:16

for A being non empty set

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )

for o, o9 being BinOp of A st o9 is commutative holds

( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )

proof end;

definition

let A be set ;

let u be UnOp of A;

let o be BinOp of A;

end;
let u be UnOp of A;

let o be BinOp of A;

pred u is_distributive_wrt o means :Def12: :: BINOP_1:def 12

for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b));

for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b));

:: deftheorem Def12 defines is_distributive_wrt BINOP_1:def 12 :

for A being set

for u being UnOp of A

for o being BinOp of A holds

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

for A being set

for u being UnOp of A

for o being BinOp of A holds

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

definition

canceled;

canceled;

canceled;

let A be non empty set ;

let e be Element of A;

let o be BinOp of A;

compatibility

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

by Def5;

compatibility

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

by Def6;

end;
canceled;

canceled;

let A be non empty set ;

let e be Element of A;

let o be BinOp of A;

redefine pred e is_a_left_unity_wrt o means :: BINOP_1:def 16

for a being Element of A holds o . (e,a) = a;

correctness for a being Element of A holds o . (e,a) = a;

compatibility

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

by Def5;

redefine pred e is_a_right_unity_wrt o means :: BINOP_1:def 17

for a being Element of A holds o . (a,e) = a;

correctness for a being Element of A holds o . (a,e) = a;

compatibility

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

by Def6;

:: deftheorem defines is_a_left_unity_wrt BINOP_1:def 16 :

for A being non empty set

for e being Element of A

for o being BinOp of A holds

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

for A being non empty set

for e being Element of A

for o being BinOp of A holds

( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

:: deftheorem defines is_a_right_unity_wrt BINOP_1:def 17 :

for A being non empty set

for e being Element of A

for o being BinOp of A holds

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

for A being non empty set

for e being Element of A

for o being BinOp of A holds

( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

definition

let A be non empty set ;

let o9, o be BinOp of A;

compatibility

( o9 is_left_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))) );

by Def9;

compatibility

( o9 is_right_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))) );

by Def10;

end;
let o9, o be BinOp of A;

redefine pred o9 is_left_distributive_wrt o means :: BINOP_1:def 18

for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c)));

correctness for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c)));

compatibility

( o9 is_left_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))) );

by Def9;

redefine pred o9 is_right_distributive_wrt o means :: BINOP_1:def 19

for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)));

correctness for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)));

compatibility

( o9 is_right_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))) );

by Def10;

:: deftheorem defines is_left_distributive_wrt BINOP_1:def 18 :

for A being non empty set

for o9, o being BinOp of A holds

( o9 is_left_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))) );

for A being non empty set

for o9, o being BinOp of A holds

( o9 is_left_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))) );

:: deftheorem defines is_right_distributive_wrt BINOP_1:def 19 :

for A being non empty set

for o9, o being BinOp of A holds

( o9 is_right_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))) );

for A being non empty set

for o9, o being BinOp of A holds

( o9 is_right_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))) );

definition

let A be non empty set ;

let u be UnOp of A;

let o be BinOp of A;

compatibility

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

by Def12;

end;
let u be UnOp of A;

let o be BinOp of A;

redefine pred u is_distributive_wrt o means :: BINOP_1:def 20

for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b));

correctness for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b));

compatibility

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

by Def12;

:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :

for A being non empty set

for u being UnOp of A

for o being BinOp of A holds

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

for A being non empty set

for u being UnOp of A

for o being BinOp of A holds

( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

:: FUNCT_2, 2005.12.13, A.T.

theorem :: BINOP_1:17

for X, Y, Z, x, y being set

for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds

f . (x,y) in Z

for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds

f . (x,y) in Z

proof end;

:: from TOPALG_3, 2005.12.14, A.T.

theorem :: BINOP_1:18

for x, y, X, Y, Z being set

for f being Function of [:X,Y:],Z

for g being Function st Z <> {} & x in X & y in Y holds

(g * f) . (x,y) = g . (f . (x,y))

for f being Function of [:X,Y:],Z

for g being Function st Z <> {} & x in X & y in Y holds

(g * f) . (x,y) = g . (f . (x,y))

proof end;

:: missing, 2005.12.17, A.T.

theorem :: BINOP_1:19

for X, Y being set

for f being Function st dom f = [:X,Y:] holds

( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

for f being Function st dom f = [:X,Y:] holds

( f is constant iff for x1, x2, y1, y2 being set st x1 in X & x2 in X & y1 in Y & y2 in Y holds

f . (x1,y1) = f . (x2,y2) )

proof end;

:: from PARTFUN1, 2006.12.05, AT

theorem :: BINOP_1:20

for X, Y, Z being set

for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds

f1 . (x,y) = f2 . (x,y) ) holds

f1 = f2

for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds

f1 . (x,y) = f2 . (x,y) ) holds

f1 = f2

proof end;

scheme :: BINOP_1:sch 5

PartFuncEx2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , P_{1}[ set , set , set ] } :

PartFuncEx2{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x, y being set holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & ex z being set st P_{1}[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds

P_{1}[x,y,f . (x,y)] ) )

provided( ( for x, y being set holds

( [x,y] in dom f iff ( x in F

P

A1:
for x, y, z being set st x in F_{1}() & y in F_{2}() & P_{1}[x,y,z] holds

z in F_{3}()
and

A2: for x, y, z1, z2 being set st x in F_{1}() & y in F_{2}() & P_{1}[x,y,z1] & P_{1}[x,y,z2] holds

z1 = z2

z in F

A2: for x, y, z1, z2 being set st x in F

z1 = z2

proof end;

scheme :: BINOP_1:sch 6

LambdaR2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( set , set ) -> set , P_{1}[ set , set ] } :

LambdaR2{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x, y being set holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )

provided
( ( for x, y being set holds

( [x,y] in dom f iff ( x in F

f . (x,y) = F

proof end;

:: from GRCAT_1, 2006.12.05, AT

scheme :: BINOP_1:sch 7

PartLambda2{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( set , set ) -> set , P_{1}[ set , set ] } :

PartLambda2{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x, y being set holds

( [x,y] in dom f iff ( x in F_{1}() & y in F_{2}() & P_{1}[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )

provided
( ( for x, y being set holds

( [x,y] in dom f iff ( x in F

f . (x,y) = F

proof end;

scheme :: BINOP_1:sch 8

Sch8{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> set , F_{4}( set , set ) -> set , P_{1}[ set , set ] } :

Sch8{ F

ex f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() st

( ( for x being Element of F_{1}()

for y being Element of F_{2}() holds

( [x,y] in dom f iff P_{1}[x,y] ) ) & ( for x being Element of F_{1}()

for y being Element of F_{2}() st [x,y] in dom f holds

f . (x,y) = F_{4}(x,y) ) )

provided( ( for x being Element of F

for y being Element of F

( [x,y] in dom f iff P

for y being Element of F

f . (x,y) = F

A1:
for x being Element of F_{1}()

for y being Element of F_{2}() st P_{1}[x,y] holds

F_{4}(x,y) in F_{3}()

for y being Element of F

F

proof end;

:: 2007.11.22, A.T.

definition

let A be set ;

let f be BinOp of A;

let x, y be Element of A;

:: original: .

redefine func f . (x,y) -> Element of A;

coherence

f . (x,y) is Element of A

end;
let f be BinOp of A;

let x, y be Element of A;

:: original: .

redefine func f . (x,y) -> Element of A;

coherence

f . (x,y) is Element of A

proof end;

definition

let X, Y, Z be set ;

let f1, f2 be Function of [:X,Y:],Z;

( f1 = f2 iff for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y) ) by Th1;

end;
let f1, f2 be Function of [:X,Y:],Z;

:: original: =

redefine pred f1 = f2 means :: BINOP_1:def 21

for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y);

compatibility redefine pred f1 = f2 means :: BINOP_1:def 21

for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y);

( f1 = f2 iff for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y) ) by Th1;

:: deftheorem defines = BINOP_1:def 21 :

for X, Y, Z being set

for f1, f2 being Function of [:X,Y:],Z holds

( f1 = f2 iff for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y) );

for X, Y, Z being set

for f1, f2 being Function of [:X,Y:],Z holds

( f1 = f2 iff for x, y being set st x in X & y in Y holds

f1 . (x,y) = f2 . (x,y) );

:: let A be non empty set, o be BinOp of A;

:: redefine attr o is commutative means

:: for a,b being Element of A holds o.(a,b ) = o.(b,a);

:: correctness by Def2;

:: redefine attr o is associative means

:: for a,b,c being Element of A holds o.(a,o.(b,c)) = o.(o.(a,b),c);

:: correctness by Def3;

:: redefine attr o is idempotent means

:: for a being Element of A holds o.(a,a) = a;

:: correctness by Def4;

:: end;