:: BINOP_1 semantic presentation

begin

definition
let f be Function;
let a, b be set ;
funcf . (a,b) ->  set  equals :: BINOP_1:def 1
f . [a,b];
correctness
coherence
f . [a,b] is set ;
;
end;

:: deftheorem  defines . BINOP_1:def_1_:_
 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 funcf . (a,b) ->  Element of C;
coherence
 f . (a,b) is Element of C
proof
reconsider ab = [a,b] as Element of [:A,B:] by ZFMISC_1:def_2;
 f . ab is Element of C ;
hence  f . (a,b) is Element of C ; ::_thesis: verum
end;
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
proof
let X, Y, Z be set ; ::_thesis: 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
let f1, f2 be Function of [:X,Y:],Z; ::_thesis: ( ( for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ) implies f1 = f2 )
assume A1: for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ; ::_thesis: f1 = f2
 for z being set st z in [:X,Y:] holds
f1 . z = f2 . z
proof
let z be set ; ::_thesis: ( z in [:X,Y:] implies f1 . z = f2 . z )
assume  z in [:X,Y:] ; ::_thesis: f1 . z = f2 . z
then consider x, y being set  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  f1 . z = f2 . z by A1, A2; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:12; ::_thesis: verum
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
proof
let X, Y, Z be set ; ::_thesis: 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
let f1, f2 be Function of [:X,Y:],Z; ::_thesis: ( ( for a being Element of X
for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) implies f1 = f2 )
assume  for a being Element of X
for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ; ::_thesis: f1 = f2
then  for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ;
hence  f1 = f2 by Th1; ::_thesis: verum
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;

definition
let A be set ;
let f be BinOp of A;
let a, b be Element of A;
:: original: .
redefine funcf . (a,b) ->  Element of A;
coherence
 f . (a,b) is Element of A
proof
percases ( A <> {} or A = {} ) ;
suppose A <> {} ; ::_thesis: f . (a,b) is Element of A
then reconsider A = A as non empty set ;
reconsider f = 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  f . (a,b) is Element of A ; ::_thesis: verum
end;
supposeA1: A = {} ; ::_thesis: f . (a,b) is Element of A
then  not [a,b] in dom f ;
then  f . (a,b) = {} by FUNCT_1:def_2;
hence  f . (a,b) is Element of A by A1, SUBSET_1:def_1; ::_thesis: verum
end;
end;
end;
end;


scheme :: BINOP_1:sch 1
FuncEx2{ F1() ->  set , F2() ->  set , F3() ->  set , P1[ set , set , set ] } :
 ex f being Function of [:F1(),F2():],F3() st
for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
provided
A1: for x, y being set st x in F1() & y in F2() holds
ex z being set st
( z in F3() & P1[x,y,z] )
proof
defpred S1[ set , set ] means  for x1, y1 being set st $1 = [x1,y1] holds
P1[x1,y1,$2];
A2: for x being set st x in [:F1(),F2():] holds
ex z being set st
( z in F3() & S1[x,z] )
proof
let x be set ; ::_thesis: ( x in [:F1(),F2():] implies ex z being set st
( z in F3() & S1[x,z] ) )
assume  x in [:F1(),F2():] ; ::_thesis: ex z being set st
( z in F3() & S1[x,z] )
then consider x1, y1 being set  such that
A3: ( x1 in F1() & y1 in F2() ) and
A4: x = [x1,y1] by ZFMISC_1:def_2;
consider z being set  such that
A5: z in F3() and
A6: P1[x1,y1,z] by A1, A3;
take  z ; ::_thesis: ( z in F3() & S1[x,z] )
thus  z in F3() by A5; ::_thesis: S1[x,z]
let x2, y2 be set ; ::_thesis: ( x = [x2,y2] implies P1[x2,y2,z] )
assume A7: x = [x2,y2] ; ::_thesis: P1[x2,y2,z]
then  x1 = x2 by A4, XTUPLE_0:1;
hence  P1[x2,y2,z] by A4, A6, A7, XTUPLE_0:1; ::_thesis: verum
end;
consider f being Function of [:F1(),F2():],F3() such that
A8: for x being set st x in [:F1(),F2():] holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
take  f ; ::_thesis: for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
let x, y be set ; ::_thesis: ( x in F1() & y in F2() implies P1[x,y,f . (x,y)] )
assume  ( x in F1() & y in F2() ) ; ::_thesis: P1[x,y,f . (x,y)]
then  [x,y] in [:F1(),F2():] by ZFMISC_1:def_2;
hence  P1[x,y,f . (x,y)] by A8; ::_thesis: verum
end;

scheme :: BINOP_1:sch 2
Lambda2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set } :
 ex f being Function of [:F1(),F2():],F3() st
for x, y being set st x in F1() & y in F2() holds
f . (x,y) = F4(x,y)
provided
A1: for x, y being set st x in F1() & y in F2() holds
F4(x,y) in F3()
proof
defpred S1[ set , set , set ] means $3 = F4($1,$2);
A2: for x, y being set st x in F1() & y in F2() holds
ex z being set st
( z in F3() & S1[x,y,z] ) by A1;
thus  ex f being Function of [:F1(),F2():],F3() st
for x, y being set st x in F1() & y in F2() holds
S1[x,y,f . (x,y)] from BINOP_1:sch_1(A2); ::_thesis: verum
end;

scheme :: BINOP_1:sch 3
FuncEx2D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , P1[ set , set , set ] } :
 ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds P1[x,y,f . (x,y)]
provided
A1: for x being Element of F1()
for y being Element of F2() ex z being Element of F3() st P1[x,y,z]
proof
defpred S1[ set , set ] means  for x being Element of F1()
for y being Element of F2() st $1 = [x,y] holds
P1[x,y,$2];
A2: for p being Element of [:F1(),F2():] ex z being Element of F3() st S1[p,z]
proof
let p be Element of [:F1(),F2():]; ::_thesis: ex z being Element of F3() st S1[p,z]
consider x1, y1 being set  such that
A3: x1 in F1() and
A4: y1 in F2() and
A5: p = [x1,y1] by ZFMISC_1:def_2;
reconsider y1 = y1 as Element of F2() by A4;
reconsider x1 = x1 as Element of F1() by A3;
consider z being Element of F3() such that
A6: P1[x1,y1,z] by A1;
take  z ; ::_thesis: S1[p,z]
let x be Element of F1(); ::_thesis: for y being Element of F2() st p = [x,y] holds
P1[x,y,z]
let y be Element of F2(); ::_thesis: ( p = [x,y] implies P1[x,y,z] )
assume A7: p = [x,y] ; ::_thesis: P1[x,y,z]
then  x1 = x by A5, XTUPLE_0:1;
hence  P1[x,y,z] by A5, A6, A7, XTUPLE_0:1; ::_thesis: verum
end;
consider f being Function of [:F1(),F2():],F3() such that
A8: for p being Element of [:F1(),F2():] holds S1[p,f . p] from FUNCT_2:sch_3(A2);
take  f ; ::_thesis: for x being Element of F1()
for y being Element of F2() holds P1[x,y,f . (x,y)]
let x be Element of F1(); ::_thesis: for y being Element of F2() holds P1[x,y,f . (x,y)]
let y be Element of F2(); ::_thesis: P1[x,y,f . (x,y)]
reconsider xy = [x,y] as Element of [:F1(),F2():] by ZFMISC_1:def_2;
 P1[x,y,f . xy] by A8;
hence  P1[x,y,f . (x,y)] ; ::_thesis: verum
end;

scheme :: BINOP_1:sch 4
Lambda2D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( Element of F1(), Element of F2()) ->  Element of F3() } :
 ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
proof
defpred S1[ Element of F1(), Element of F2(), set ] means $3 = F4($1,$2);
A1: for x being Element of F1()
for y being Element of F2() ex z being Element of F3() st S1[x,y,z] ;
thus  ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;

definition
let A be set ;
let o be BinOp of A;
attro is commutative  means :Def2: :: BINOP_1:def 2
 for a, b being Element of A holds o . (a,b) = o . (b,a);
attro 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);
attro is idempotent  means :: BINOP_1:def 4
 for a being Element of A holds o . (a,a) = a;
end;

:: 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) );

:: 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) );

:: 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 );

registration
cluster Function-like V18([:{},{}:], {} )  ->  empty commutative associative for Element of bool [:[:{},{}:],{}:];
coherence
 for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proof
let f be BinOp of {}; ::_thesis: ( f is empty & f is associative & f is commutative )
thus  f is empty ; ::_thesis: ( f is associative & f is commutative )
A1: f c= [:(dom f),(rng f):] ;
hereby  :: according to BINOP_1:def_3 ::_thesis: f is commutative
let a, b, c be Element of {} ; ::_thesis: f . (a,(f . (b,c))) = f . ((f . (a,b)),c)
thus f . (a,(f . (b,c))) = {} by A1, FUNCT_1:def_2
.= f . ((f . (a,b)),c) by A1, FUNCT_1:def_2 ; ::_thesis: verum
end;
let a, b be Element of {} ; :: according to BINOP_1:def_2 ::_thesis: f . (a,b) = f . (b,a)
thus f . (a,b) = {} by A1, FUNCT_1:def_2
.= f . (b,a) by A1, FUNCT_1:def_2 ; ::_thesis: verum
end;
end;

definition
let A be set ;
let e be Element of A;
let o be BinOp of A;
prede is_a_left_unity_wrt o means :Def5: :: BINOP_1:def 5
 for a being Element of A holds o . (e,a) = a;
prede is_a_right_unity_wrt o means :Def6: :: BINOP_1:def 6
 for a being Element of A holds o . (a,e) = a;
end;

:: 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 );

:: 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 );

definition
let A be set ;
let e be Element of A;
let o be BinOp of A;
prede is_a_unity_wrt o means :: BINOP_1:def 7
( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o );
end;

:: 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 ) );

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 ) )
proof
let A be set ; ::_thesis: 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 ) )
let o be BinOp of A; ::_thesis: 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 ) )
let e be Element of A; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
thus  ( e is_a_unity_wrt o implies for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ) ::_thesis: ( ( for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ) implies e is_a_unity_wrt o )
proof
assume  ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) ; :: according to BINOP_1:def_7 ::_thesis: for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a )
hence  for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) by Def5, Def6; ::_thesis: verum
end;
assume  for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ; ::_thesis: e is_a_unity_wrt o
hence  ( ( for a being Element of A holds o . (e,a) = a ) & ( for a being Element of A holds o . (a,e) = a ) ) ; :: according to BINOP_1:def_5,BINOP_1:def_6,BINOP_1:def_7 ::_thesis: verum
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 )
proof
let A be set ; ::_thesis: 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 )
let o be BinOp of A; ::_thesis: 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 )
let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) )
assume A1: o is commutative ; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )
now__::_thesis:_(_(_(_for_a_being_Element_of_A_holds_
(_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_implies_for_a_being_Element_of_A_holds_o_._(e,a)_=_a_)_&_(_(_for_a_being_Element_of_A_holds_o_._(e,a)_=_a_)_implies_for_a_being_Element_of_A_holds_
(_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_)
thus  ( ( for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ) implies for a being Element of A holds o . (e,a) = a ) ; ::_thesis: ( ( for a being Element of A holds o . (e,a) = a ) implies for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
assume A2: for a being Element of A holds o . (e,a) = a ; ::_thesis: for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a )
let a be Element of A; ::_thesis: ( o . (e,a) = a & o . (a,e) = a )
thus  o . (e,a) = a by A2; ::_thesis: o . (a,e) = a
thus o . (a,e) = o . (e,a) by A1, Def2
.= a by A2 ; ::_thesis: verum
end;
hence  ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) by Th3; ::_thesis: verum
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 )
proof
let A be set ; ::_thesis: 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 )
let o be BinOp of A; ::_thesis: 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 )
let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) )
assume A1: o is commutative ; ::_thesis: ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a )
now__::_thesis:_(_(_(_for_a_being_Element_of_A_holds_
(_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_implies_for_a_being_Element_of_A_holds_o_._(a,e)_=_a_)_&_(_(_for_a_being_Element_of_A_holds_o_._(a,e)_=_a_)_implies_for_a_being_Element_of_A_holds_
(_o_._(e,a)_=_a_&_o_._(a,e)_=_a_)_)_)
thus  ( ( for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ) implies for a being Element of A holds o . (a,e) = a ) ; ::_thesis: ( ( for a being Element of A holds o . (a,e) = a ) implies for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
assume A2: for a being Element of A holds o . (a,e) = a ; ::_thesis: for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a )
let a be Element of A; ::_thesis: ( o . (e,a) = a & o . (a,e) = a )
thus o . (e,a) = o . (a,e) by A1, Def2
.= a by A2 ; ::_thesis: o . (a,e) = a
thus  o . (a,e) = a by A2; ::_thesis: verum
end;
hence  ( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) by Th3; ::_thesis: verum
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 )
proof
let A be set ; ::_thesis: 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 )
let o be BinOp of A; ::_thesis: 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 )
let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) )
 ( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a ) by Def5;
hence  ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) ) by Th4; ::_thesis: verum
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 )
proof
let A be set ; ::_thesis: 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 )
let o be BinOp of A; ::_thesis: 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 )
let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) )
 ( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a ) by Def6;
hence  ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_right_unity_wrt o ) ) by Th5; ::_thesis: verum
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 )
proof
let A be set ; ::_thesis: 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 )
let o be BinOp of A; ::_thesis: 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 )
let e be Element of A; ::_thesis: ( o is commutative implies ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) )
assume A1: o is commutative ; ::_thesis: ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )
then  ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) by Th6;
hence  ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) by A1, Th7; ::_thesis: verum
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
proof
let A be set ; ::_thesis: 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
let o be BinOp of A; ::_thesis: 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
let e1, e2 be Element of A; ::_thesis: ( e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2 )
assume that
A1: e1 is_a_left_unity_wrt o and
A2: e2 is_a_right_unity_wrt o ; ::_thesis: e1 = e2
thus e1 = o . (e1,e2) by A2, Def6
.= e2 by A1, Def5 ; ::_thesis: verum
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
proof
let A be set ; ::_thesis: 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
let o be BinOp of A; ::_thesis: for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds
e1 = e2
let e1, e2 be Element of A; ::_thesis: ( e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2 )
assume that
 e1 is_a_left_unity_wrt o and
A1: ( e1 is_a_right_unity_wrt o & e2 is_a_left_unity_wrt o ) and
 e2 is_a_right_unity_wrt o ; :: according to BINOP_1:def_7 ::_thesis: e1 = e2
thus  e1 = e2 by A1, Th9; ::_thesis: verum
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 ;
func the_unity_wrt o ->  Element of A means :: BINOP_1:def 8
it is_a_unity_wrt o;
existence
 ex b1 being Element of A st b1 is_a_unity_wrt o by A1;
uniqueness
 for b1, b2 being Element of A st b1 is_a_unity_wrt o & b2 is_a_unity_wrt o holds
b1 = b2 by Th10;
end;

:: 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 b3 being Element of A holds
( b3 = the_unity_wrt o iff b3 is_a_unity_wrt o );

definition
let A be set ;
let o9, o be BinOp of A;
predo9 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)));
predo9 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)));
end;

:: 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))) );

:: 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))) );

definition
let A be set ;
let o9, o be BinOp of A;
predo9 is_distributive_wrt o means :: BINOP_1:def 11
( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o );
end;

:: 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 ) );

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))) ) )
proof
let A be set ; ::_thesis: 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))) ) )
let o9, o be BinOp of A; ::_thesis: ( 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))) ) )
thus  ( o9 is_distributive_wrt o implies 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))) ) ) ::_thesis: ( ( 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 o9 is_distributive_wrt o )
proof
assume  ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) ; :: according to BINOP_1:def_11 ::_thesis: 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))) )
hence  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))) ) by Def9, Def10; ::_thesis: verum
end;
assume  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))) ) ; ::_thesis: o9 is_distributive_wrt o
hence  ( ( 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 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) ; :: according to BINOP_1:def_9,BINOP_1:def_10,BINOP_1:def_11 ::_thesis: verum
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))) )
proof
let A be non empty set ; ::_thesis: 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))) )
let o, o9 be BinOp of A; ::_thesis: ( 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))) ) )
assume A1: o9 is commutative ; ::_thesis: ( 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 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))) ) ; ::_thesis: ( ( for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) implies 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))) ) )
assume A2: for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ; ::_thesis: 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))) )
let a, b, c be Element of A; ::_thesis: ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
thus  o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) by A2; ::_thesis: o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)))
thus o9 . ((o . (a,b)),c) = o9 . (c,(o . (a,b))) by A1, Def2
.= o . ((o9 . (c,a)),(o9 . (c,b))) by A2
.= o . ((o9 . (a,c)),(o9 . (c,b))) by A1, Def2
.= o . ((o9 . (a,c)),(o9 . (b,c))) by A1, Def2 ; ::_thesis: verum
end;
hence  ( 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))) ) by Th11; ::_thesis: verum
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))) )
proof
let A be non empty set ; ::_thesis: 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))) )
let o, o9 be BinOp of A; ::_thesis: ( 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))) ) )
assume A1: o9 is commutative ; ::_thesis: ( 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 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))) ) ; ::_thesis: ( ( for a, b, c being Element of A holds 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))) & 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))) ; ::_thesis: 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))) )
let a, b, c be Element of A; ::_thesis: ( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
thus o9 . (a,(o . (b,c))) = o9 . ((o . (b,c)),a) by A1, Def2
.= o . ((o9 . (b,a)),(o9 . (c,a))) by A2
.= o . ((o9 . (a,b)),(o9 . (c,a))) by A1, Def2
.= o . ((o9 . (a,b)),(o9 . (a,c))) by A1, Def2 ; ::_thesis: o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)))
thus  o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) by A2; ::_thesis: verum
end;
hence  ( 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))) ) by Th11; ::_thesis: verum
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 )
proof
let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o )
let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) )
 ( 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;
hence  ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) ) by Th12; ::_thesis: verum
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 )
proof
let A be non empty set ; ::_thesis: for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o )
let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) )
 ( 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;
hence  ( o9 is commutative implies ( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) ) by Th13; ::_thesis: verum
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 )
proof
let A be non empty set ; ::_thesis: 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 )
let o, o9 be BinOp of A; ::_thesis: ( o9 is commutative implies ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) )
assume A1: o9 is commutative ; ::_thesis: ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )
then  ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) by Th14;
hence  ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) by A1, Th15; ::_thesis: verum
end;

definition
let A be set ;
let u be UnOp of A;
let o be BinOp of A;
predu 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));
end;

:: 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)) );

definition
canceled;
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
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
compatibility
( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );
by Def6;
end;

:: deftheorem  BINOP_1:def_13_:_
canceled;

:: deftheorem  BINOP_1:def_14_:_
canceled;

:: deftheorem  BINOP_1:def_15_:_
canceled;

:: 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 );

:: 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 );

definition
let A be non empty set ;
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
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
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;

:: 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))) );

:: 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))) );

definition
let A be non empty set ;
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
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;

:: 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)) );

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
proof
let X, Y, Z, x, y be set ; ::_thesis: for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds
f . (x,y) in Z
let f be Function of [:X,Y:],Z; ::_thesis: ( x in X & y in Y & Z <> {} implies f . (x,y) in Z )
assume  ( x in X & y in Y ) ; ::_thesis: ( not Z <> {} or f . (x,y) in Z )
then  [x,y] in [:X,Y:] by ZFMISC_1:87;
hence  ( not Z <> {} or f . (x,y) in Z ) by FUNCT_2:5; ::_thesis: verum
end;

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))
proof
let x, y, X, Y, Z be set ; ::_thesis: 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))
let f be Function of [:X,Y:],Z; ::_thesis: for g being Function st Z <> {} & x in X & y in Y holds
(g * f) . (x,y) = g . (f . (x,y))
let g be Function; ::_thesis: ( Z <> {} & x in X & y in Y implies (g * f) . (x,y) = g . (f . (x,y)) )
assume A1: Z <> {} ; ::_thesis: ( not x in X or not y in Y or (g * f) . (x,y) = g . (f . (x,y)) )
assume  ( x in X & y in Y ) ; ::_thesis: (g * f) . (x,y) = g . (f . (x,y))
then  [x,y] in [:X,Y:] by ZFMISC_1:87;
hence  (g * f) . (x,y) = g . (f . (x,y)) by A1, FUNCT_2:15; ::_thesis: verum
end;

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) )
proof
let X, Y be set ; ::_thesis: 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) )
let f be Function; ::_thesis: ( dom f = [:X,Y:] implies ( 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) ) )
assume A1: dom f = [:X,Y:] ; ::_thesis: ( 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) )
hereby  ::_thesis: ( ( 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) ) implies f is constant )
assume A2: f is constant ; ::_thesis: 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)
let x1, x2, y1, y2 be set ; ::_thesis: ( x1 in X & x2 in X & y1 in Y & y2 in Y implies f . (x1,y1) = f . (x2,y2) )
assume  ( x1 in X & x2 in X & y1 in Y & y2 in Y ) ; ::_thesis: f . (x1,y1) = f . (x2,y2)
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, FUNCT_1:def_10; ::_thesis: verum
end;
assume A3: 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) ; ::_thesis: f is constant
let x be set ; :: according to FUNCT_1:def_10 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or f . x = f . b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume  x in dom f ; ::_thesis: ( not y in dom f or f . x = f . y )
then consider x1, y1 being set  such that
A4: ( x1 in X & y1 in Y ) and
A5: x = [x1,y1] by A1, ZFMISC_1:84;
assume  y in dom f ; ::_thesis: f . x = f . y
then consider x2, y2 being set  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 ; ::_thesis: verum
end;

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
proof
let X, Y, Z be set ; ::_thesis: 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
let f1, f2 be PartFunc of [:X,Y:],Z; ::_thesis: ( dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds
f1 . (x,y) = f2 . (x,y) ) implies f1 = f2 )
assume that
A1: dom f1 = dom f2 and
A2: for x, y being set st [x,y] in dom f1 holds
f1 . (x,y) = f2 . (x,y) ; ::_thesis: f1 = f2
 for z being set st z in dom f1 holds
f1 . z = f2 . z
proof
let z be set ; ::_thesis: ( z in dom f1 implies f1 . z = f2 . z )
assume A3: z in dom f1 ; ::_thesis: f1 . z = f2 . z
then consider x, y being set  such that
A4: z = [x,y] by RELAT_1:def_1;
 f1 . (x,y) = f2 . (x,y) by A2, A3, A4;
hence  f1 . z = f2 . z by A4; ::_thesis: verum
end;
hence  f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum
end;

scheme :: BINOP_1:sch 5
PartFuncEx2{ F1() ->  set , F2() ->  set , F3() ->  set , P1[ set , set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds
P1[x,y,f . (x,y)] ) )
provided
A1: for x, y, z being set st x in F1() & y in F2() & P1[x,y,z] holds
z in F3() and
A2: for x, y, z1, z2 being set st x in F1() & y in F2() & P1[x,y,z1] & P1[x,y,z2] holds
z1 = z2
proof
defpred S1[ set , set ] means  for x1, y1 being set st $1 = [x1,y1] holds
P1[x1,y1,$2];
A3: for x, z being set st x in [:F1(),F2():] & S1[x,z] holds
z in F3()
proof
let x, z be set ; ::_thesis: ( x in [:F1(),F2():] & S1[x,z] implies z in F3() )
assume  x in [:F1(),F2():] ; ::_thesis: ( not S1[x,z] or z in F3() )
then A4: ex x1, y1 being set st
( x1 in F1() & y1 in F2() & x = [x1,y1] ) by ZFMISC_1:def_2;
assume  for x1, y1 being set st x = [x1,y1] holds
P1[x1,y1,z] ; ::_thesis: z in F3()
hence  z in F3() by A1, A4; ::_thesis: verum
end;
A5: for x, z1, z2 being set st x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] holds
z1 = z2
proof
let x, z1, z2 be set ; ::_thesis: ( x in [:F1(),F2():] & S1[x,z1] & S1[x,z2] implies z1 = z2 )
assume that
A6: x in [:F1(),F2():] and
A7: ( ( for x1, y1 being set st x = [x1,y1] holds
P1[x1,y1,z1] ) & ( for x1, y1 being set st x = [x1,y1] holds
P1[x1,y1,z2] ) ) ; ::_thesis: z1 = z2
consider x1, y1 being set  such that
A8: ( x1 in F1() & y1 in F2() ) and
A9: x = [x1,y1] by A6, ZFMISC_1:def_2;
 ( P1[x1,y1,z1] & P1[x1,y1,z2] ) by A7, A9;
hence  z1 = z2 by A2, A8; ::_thesis: verum
end;
consider f being PartFunc of [:F1(),F2():],F3() such that
A10: for x being set holds
( x in dom f iff ( x in [:F1(),F2():] & ex z being set st S1[x,z] ) ) and
A11: for x being set st x in dom f holds
S1[x,f . x] from PARTFUN1:sch_2(A3, A5);
take  f ; ::_thesis: ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds
P1[x,y,f . (x,y)] ) )
thus  for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ::_thesis: for x, y being set st [x,y] in dom f holds
P1[x,y,f . (x,y)]
proof
let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) )
thus  ( [x,y] in dom f implies ( x in F1() & y in F2() & ex z being set st P1[x,y,z] ) ) ::_thesis: ( x in F1() & y in F2() & ex z being set st P1[x,y,z] implies [x,y] in dom f )
proof
assume A12: [x,y] in dom f ; ::_thesis: ( x in F1() & y in F2() & ex z being set st P1[x,y,z] )
hence  ( x in F1() & y in F2() ) by ZFMISC_1:87; ::_thesis: ex z being set st P1[x,y,z]
consider z being set  such that
A13: for x1, y1 being set st [x,y] = [x1,y1] holds
P1[x1,y1,z] by A10, A12;
take  z ; ::_thesis: P1[x,y,z]
thus  P1[x,y,z] by A13; ::_thesis: verum
end;
assume  ( x in F1() & y in F2() ) ; ::_thesis: ( for z being set holds P1[x,y,z] or [x,y] in dom f )
then A14: [x,y] in [:F1(),F2():] by ZFMISC_1:def_2;
given z being set  such that A15: P1[x,y,z] ; ::_thesis: [x,y] in dom f
now__::_thesis:_ex_z_being_set_st_
for_x1,_y1_being_set_st_[x,y]_=_[x1,y1]_holds_
P1[x1,y1,z]
take z = z; ::_thesis: for x1, y1 being set st [x,y] = [x1,y1] holds
P1[x1,y1,z]
let x1, y1 be set ; ::_thesis: ( [x,y] = [x1,y1] implies P1[x1,y1,z] )
assume A16: [x,y] = [x1,y1] ; ::_thesis: P1[x1,y1,z]
then  x = x1 by XTUPLE_0:1;
hence  P1[x1,y1,z] by A15, A16, XTUPLE_0:1; ::_thesis: verum
end;
hence  [x,y] in dom f by A10, A14; ::_thesis: verum
end;
thus  for x, y being set st [x,y] in dom f holds
P1[x,y,f . (x,y)] by A11; ::_thesis: verum
end;

scheme :: BINOP_1:sch 6
LambdaR2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x, y being set st P1[x,y] holds
F4(x,y) in F3()
proof
defpred S1[ set , set , set ] means ( P1[$1,$2] & $3 = F4($1,$2) );
A2: for x, y, z1, z2 being set st x in F1() & y in F2() & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2 ;
A3: for x, y, z being set st x in F1() & y in F2() & S1[x,y,z] holds
z in F3() by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A4: for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & ex z being set st S1[x,y,z] ) ) and
A5: for x, y being set st [x,y] in dom f holds
S1[x,y,f . (x,y)] from BINOP_1:sch_5(A3, A2);
take  f ; ::_thesis: ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
thus  for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ::_thesis: for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) )
thus  ( [x,y] in dom f implies ( x in F1() & y in F2() & P1[x,y] ) ) ::_thesis: ( x in F1() & y in F2() & P1[x,y] implies [x,y] in dom f )
proof
assume A6: [x,y] in dom f ; ::_thesis: ( x in F1() & y in F2() & P1[x,y] )
then  ex z being set st
( P1[x,y] & z = F4(x,y) ) by A4;
hence  ( x in F1() & y in F2() & P1[x,y] ) by A4, A6; ::_thesis: verum
end;
assume that
A7: ( x in F1() & y in F2() ) and
A8: P1[x,y] ; ::_thesis: [x,y] in dom f
 ex z being set st
( P1[x,y] & z = F4(x,y) ) by A8;
hence  [x,y] in dom f by A4, A7; ::_thesis: verum
end;
thus  for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) by A5; ::_thesis: verum
end;

scheme :: BINOP_1:sch 7
PartLambda2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x, y being set st x in F1() & y in F2() & P1[x,y] holds
F4(x,y) in F3()
proof
defpred S1[ set , set ] means ( $1 in F1() & $2 in F2() & P1[$1,$2] );
A2: for x, y being set st S1[x,y] holds
F4(x,y) in F3() by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A3: ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & S1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) from BINOP_1:sch_6(A2);
take  f ; ::_thesis: ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
thus  ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) by A3; ::_thesis: verum
end;

scheme :: BINOP_1:sch 8
Sch8{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x being Element of F1()
for y being Element of F2() st P1[x,y] holds
F4(x,y) in F3()
proof
A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds
F4(x,y) in F3() by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A3: ( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) from BINOP_1:sch_7(A2);
take  f ; ::_thesis: ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
thus  ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) by A3; ::_thesis: verum
end;

definition
let A be set ;
let f be BinOp of A;
let x, y be Element of A;
:: original: .
redefine funcf . (x,y) ->  Element of A;
coherence
 f . (x,y) is Element of A
proof
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: f . (x,y) is Element of A
then  dom f = {} ;
then  f . (x,y) = {} by FUNCT_1:def_2;
hence  f . (x,y) is Element of A ; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: f . (x,y) is Element of A
then reconsider A = A as non empty set ;
reconsider f = f as BinOp of A ;
reconsider x = x, y = y as Element of A ;
 f . (x,y) is Element of A ;
hence  f . (x,y) is Element of A ; ::_thesis: verum
end;
end;
end;
end;

definition
let X, Y, Z be set ;
let f1, f2 be Function of [:X,Y:],Z;
:: original: =
redefine predf1 = 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
 ( 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;

:: 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) );