:: BINOP_1 semantic presentation

definition
let c1 be Function;
let c2, c3 be set ;
func a1 . a2,a3 -> set equals :: BINOP_1:def 1
a1 . [a2,a3];
correctness
coherence
c1 . [c2,c3] is set ;
;
end;

:: deftheorem defines . BINOP_1:def 1 :
for b1 being Function
for b2, b3 being set holds b1 . b2,b3 = b1 . [b2,b3];

definition
let c1, c2 be non empty set ;
let c3 be set ;
let c4 be Function of [:c1,c2:],c3;
let c5 be Element of c1;
let c6 be Element of c2;
redefine func . as a4 . a5,a6 -> Element of a3;
coherence
c4 . c5,c6 is Element of c3
proof
reconsider c7 = [c5,c6] as Element of [:c1,c2:] by ZFMISC_1:def 2;
c4 . c7 is Element of c3 ;
hence c4 . c5,c6 is Element of c3 ;
end;
end;

theorem :: BINOP_1:1
canceled;

theorem :: BINOP_1:2
for b1, b2, b3 being non empty set
for b4, b5 being Function of [:b1,b2:],b3 holds
( for b6 being Element of b1
for b7 being Element of b2 holds b4 . b6,b7 = b5 . b6,b7 implies b4 = b5 )
proof
let c1, c2, c3 be non empty set ;
let c4, c5 be Function of [:c1,c2:],c3;
assume E1: for b1 being Element of c1
for b2 being Element of c2 holds c4 . b1,b2 = c5 . b1,b2 ;
for b1 being Element of c1
for b2 being Element of c2 holds c4 . [b1,b2] = c5 . [b1,b2]
proof
let c6 be Element of c1;
let c7 be Element of c2;
( c4 . c6,c7 = c4 . [c6,c7] & c5 . c6,c7 = c5 . [c6,c7] ) ;
hence c4 . [c6,c7] = c5 . [c6,c7] by E1;
end;
hence c4 = c5 by FUNCT_2:120;
end;

definition
let c1 be set ;
mode UnOp is Function of a1,a1;
mode BinOp is Function of [:a1,a1:],a1;
end;

scheme :: BINOP_1:sch 1
s1{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1()] } :
ex b1 being BinOp of F1() st
for b2, b3 being Element of F1() holds P1[b2,b3,b1 . b2,b3]
provided
E1: for b1, b2 being Element of F1() holds
ex b3 being Element of F1() st P1[b1,b2,b3]
proof
defpred S1[ Element of F1(), Element of F1(), set ] means for b1 being Element of F1() holds
( b1 = a3 implies P1[a1,a2,b1] );
E2: for b1, b2 being Element of F1() holds
ex b3 being Element of F1() st
S1[b1,b2,b3]
proof
let c1, c2 be Element of F1();
consider c3 being Element of F1() such that
E3: P1[c1,c2,c3] by E1;
take c3 ;
thus S1[c1,c2,c3] by E3;
end;
consider c1 being Function of [:F1(),F1():],F1() such that
E3: for b1, b2 being Element of F1() holds
S1[b1,b2,c1 . [b1,b2]] from FUNCT_2:sch 7(E2);
 take c2 = c1;
let c3, c4 be Element of F1();
c2 . c3,c4 = c2 . [c3,c4] ;
hence P1[c3,c4,c2 . c3,c4] by E3;
end;

scheme :: BINOP_1:sch 2
s2{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> Element of F1() } :
ex b1 being BinOp of F1() st
for b2, b3 being Element of F1() holds b1 . b2,b3 = F2(b2,b3)
provided
proof
consider c1 being Function of [:F1(),F1():],F1() such that
E1: for b1, b2 being Element of F1() holds c1 . [b1,b2] = F2(b1,b2) from FUNCT_2:sch 8();
 take c1 ;
let c2, c3 be Element of F1();
c1 . c2,c3 = c1 . [c2,c3] ;
hence c1 . c2,c3 = F2(c2,c3) by E1;
end;

definition
let c1 be set ;
let c2 be BinOp of c1;
attr a2 is commutative means :E1: :: BINOP_1:def 2
for b1, b2 being Element of a1 holds a2 . b1,b2 = a2 . b2,b1;
attr a2 is associative means :E2: :: BINOP_1:def 3
for b1, b2, b3 being Element of a1 holds a2 . b1,(a2 . b2,b3) = a2 . (a2 . b1,b2),b3;
attr a2 is idempotent means :E3: :: BINOP_1:def 4
for b1 being Element of a1 holds a2 . b1,b1 = b1;
end;

:: deftheorem E1 defines commutative BINOP_1:def 2 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is commutative iff for b3, b4 being Element of b1 holds b2 . b3,b4 = b2 . b4,b3 );

:: deftheorem E2 defines associative BINOP_1:def 3 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is associative iff for b3, b4, b5 being Element of b1 holds b2 . b3,(b2 . b4,b5) = b2 . (b2 . b3,b4),b5 );

:: deftheorem E3 defines idempotent BINOP_1:def 4 :
for b1 being set
for b2 being BinOp of b1 holds
( b2 is idempotent iff for b3 being Element of b1 holds b2 . b3,b3 = b3 );

registration
cluster -> empty commutative associative M4([:{} ,{} :], {} );
coherence
for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proof
let c1 be BinOp of {} ;
E4: [:{} ,{} :] = {} by ZFMISC_1:113;
then E5: ( c1 c= [:(dom c1),(rng c1):] & dom c1 = {} & rng c1 c= {} ) by FUNCT_2:def 1, RELAT_1:21, RELSET_1:12;
thus c1 is empty by E4, XBOOLE_1:3;
hereby :: uses BINOP_1:def 3
let c2, c3, c4 be Element of {} ;
thus c1 . c2,(c1 . c3,c4) = c1 . [c2,(c1 . c3,c4)]
.= {} by E5, FUNCT_1:def 4
.= c1 . [(c1 . c2,c3),c4] by E5, FUNCT_1:def 4
.= c1 . (c1 . c2,c3),c4 ;
end; let c2, c3 be Element of {} ; :: uses BINOP_1:def 2
thus c1 . c2,c3 = c1 . [c2,c3]
.= {} by E5, FUNCT_1:def 4
.= c1 . [c3,c2] by E5, FUNCT_1:def 4
.= c1 . c3,c2 ;
end;
end;

definition
let c1 be set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
pred a2 is_a_left_unity_wrt a3 means :E4: :: BINOP_1:def 5
for b1 being Element of a1 holds a3 . a2,b1 = b1;
pred a2 is_a_right_unity_wrt a3 means :E5: :: BINOP_1:def 6
for b1 being Element of a1 holds a3 . b1,a2 = b1;
end;

:: deftheorem E4 defines is_a_left_unity_wrt BINOP_1:def 5 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_left_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b2,b4 = b4 );

:: deftheorem E5 defines is_a_right_unity_wrt BINOP_1:def 6 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_right_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b4,b2 = b4 );

definition
let c1 be set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
pred a2 is_a_unity_wrt a3 means :: BINOP_1:def 7
( a2 is_a_left_unity_wrt a3 & a2 is_a_right_unity_wrt a3 );
end;

:: deftheorem defines is_a_unity_wrt BINOP_1:def 7 :
for b1 being set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_unity_wrt b3 iff ( b2 is_a_left_unity_wrt b3 & b2 is_a_right_unity_wrt b3 ) );

theorem :: BINOP_1:3
canceled;

theorem :: BINOP_1:4
canceled;

theorem :: BINOP_1:5
canceled;

theorem :: BINOP_1:6
canceled;

theorem :: BINOP_1:7
canceled;

theorem :: BINOP_1:8
canceled;

theorem :: BINOP_1:9
canceled;

theorem :: BINOP_1:10
canceled;

theorem E6: :: BINOP_1:11
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds
( b2 . b3,b4 = b4 & b2 . b4,b3 = b4 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
thus ( c3 is_a_unity_wrt c2 implies for b1 being Element of c1 holds
( c2 . c3,b1 = b1 & c2 . b1,c3 = b1 ) )
proof
assume ( c3 is_a_left_unity_wrt c2 & c3 is_a_right_unity_wrt c2 ) ; :: uses BINOP_1:def 7
hence for b1 being Element of c1 holds
( c2 . c3,b1 = b1 & c2 . b1,c3 = b1 ) by E4, E5;
end;
assume for b1 being Element of c1 holds
( c2 . c3,b1 = b1 & c2 . b1,c3 = b1 ) ;
hence ( for b1 being Element of c1 holds c2 . c3,b1 = b1 & for b1 being Element of c1 holds c2 . b1,c3 = b1 ) ; :: uses BINOP_1:def 5,BINOP_1:def 6,BINOP_1:def 7
end;

theorem E7: :: BINOP_1:12
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is commutative implies ( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds b2 . b3,b4 = b4 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
assume E8: c2 is commutative ;
now
thus ( for b1 being Element of c1 holds
( c2 . c3,b1 = b1 & c2 . b1,c3 = b1 ) implies for b1 being Element of c1 holds c2 . c3,b1 = b1 ) ;
assume E9: for b1 being Element of c1 holds c2 . c3,b1 = b1 ;
let c4 be Element of c1;
thus c2 . c3,c4 = c4 by E9;
thus c2 . c4,c3 = c2 . c3,c4 by E8, E1
.= c4 by E9 ;
end;
hence ( c3 is_a_unity_wrt c2 iff for b1 being Element of c1 holds c2 . c3,b1 = b1 ) by E6;
end;

theorem E8: :: BINOP_1:13
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is commutative implies ( b3 is_a_unity_wrt b2 iff for b4 being Element of b1 holds b2 . b4,b3 = b4 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
assume E9: c2 is commutative ;
now
thus ( for b1 being Element of c1 holds
( c2 . c3,b1 = b1 & c2 . b1,c3 = b1 ) implies for b1 being Element of c1 holds c2 . b1,c3 = b1 ) ;
assume E10: for b1 being Element of c1 holds c2 . b1,c3 = b1 ;
let c4 be Element of c1;
thus c2 . c3,c4 = c2 . c4,c3 by E9, E1
.= c4 by E10 ;
thus c2 . c4,c3 = c4 by E10;
end;
hence ( c3 is_a_unity_wrt c2 iff for b1 being Element of c1 holds c2 . b1,c3 = b1 ) by E6;
end;

theorem E9: :: BINOP_1:14
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is commutative implies ( b3 is_a_unity_wrt b2 iff b3 is_a_left_unity_wrt b2 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
( c3 is_a_left_unity_wrt c2 iff for b1 being Element of c1 holds c2 . c3,b1 = b1 ) by E4;
hence ( c2 is commutative implies ( c3 is_a_unity_wrt c2 iff c3 is_a_left_unity_wrt c2 ) ) by E7;
end;

theorem E10: :: BINOP_1:15
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is commutative implies ( b3 is_a_unity_wrt b2 iff b3 is_a_right_unity_wrt b2 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
( c3 is_a_right_unity_wrt c2 iff for b1 being Element of c1 holds c2 . b1,c3 = b1 ) by E5;
hence ( c2 is commutative implies ( c3 is_a_unity_wrt c2 iff c3 is_a_right_unity_wrt c2 ) ) by E8;
end;

theorem :: BINOP_1:16
for b1 being set
for b2 being BinOp of b1
for b3 being Element of b1 holds
( b2 is commutative implies ( b3 is_a_left_unity_wrt b2 iff b3 is_a_right_unity_wrt b2 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3 be Element of c1;
assume E11: c2 is commutative ;
then ( c3 is_a_unity_wrt c2 iff c3 is_a_left_unity_wrt c2 ) by E9;
hence ( c3 is_a_left_unity_wrt c2 iff c3 is_a_right_unity_wrt c2 ) by E11, E10;
end;

theorem E11: :: BINOP_1:17
for b1 being set
for b2 being BinOp of b1
for b3, b4 being Element of b1 holds
( ( b3 is_a_left_unity_wrt b2 & b4 is_a_right_unity_wrt b2 ) implies ( b3 = b4 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3, c4 be Element of c1;
assume that E12: c3 is_a_left_unity_wrt c2
and E13: c4 is_a_right_unity_wrt c2 ;
thus c3 = c2 . c3,c4 by E13, E5
.= c4 by E12, E4 ;
end;

theorem E12: :: BINOP_1:18
for b1 being set
for b2 being BinOp of b1
for b3, b4 being Element of b1 holds
( ( b3 is_a_unity_wrt b2 & b4 is_a_unity_wrt b2 ) implies ( b3 = b4 ) )
proof
let c1 be set ;
let c2 be BinOp of c1;
let c3, c4 be Element of c1;
assume ( c3 is_a_left_unity_wrt c2 & c3 is_a_right_unity_wrt c2 & c4 is_a_left_unity_wrt c2 & c4 is_a_right_unity_wrt c2 ) ; :: uses BINOP_1:def 7
hence c3 = c4 by E11;
end;

definition
let c1 be set ;
let c2 be BinOp of c1;
assume E13: ex b1 being Element of c1 st b1 is_a_unity_wrt c2 ;
func the_unity_wrt a2 -> Element of a1 means :: BINOP_1:def 8
a3 is_a_unity_wrt a2;
existence
ex b1 being Element of c1 st b1 is_a_unity_wrt c2 by E13;
uniqueness
for b1, b2 being Element of c1 holds
( ( b1 is_a_unity_wrt c2 & b2 is_a_unity_wrt c2 ) implies ( b1 = b2 ) ) by E12;
end;

:: deftheorem defines the_unity_wrt BINOP_1:def 8 :
for b1 being set
for b2 being BinOp of b1 holds
( ex b3 being Element of b1 st b3 is_a_unity_wrt b2 implies for b3 being Element of b1 holds
( b3 = the_unity_wrt b2 iff b3 is_a_unity_wrt b2 ) );

definition
let c1 be set ;
let c2, c3 be BinOp of c1;
pred a2 is_left_distributive_wrt a3 means :E13: :: BINOP_1:def 9
for b1, b2, b3 being Element of a1 holds a2 . b1,(a3 . b2,b3) = a3 . (a2 . b1,b2),(a2 . b1,b3);
pred a2 is_right_distributive_wrt a3 means :E14: :: BINOP_1:def 10
for b1, b2, b3 being Element of a1 holds a2 . (a3 . b1,b2),b3 = a3 . (a2 . b1,b3),(a2 . b2,b3);
end;

:: deftheorem E13 defines is_left_distributive_wrt BINOP_1:def 9 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_left_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) );

:: deftheorem E14 defines is_right_distributive_wrt BINOP_1:def 10 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_right_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) );

definition
let c1 be set ;
let c2, c3 be BinOp of c1;
pred a2 is_distributive_wrt a3 means :: BINOP_1:def 11
( a2 is_left_distributive_wrt a3 & a2 is_right_distributive_wrt a3 );
end;

:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff ( b2 is_left_distributive_wrt b3 & b2 is_right_distributive_wrt b3 ) );

theorem :: BINOP_1:19
canceled;

theorem :: BINOP_1:20
canceled;

theorem :: BINOP_1:21
canceled;

theorem :: BINOP_1:22
canceled;

theorem E15: :: BINOP_1:23
for b1 being set
for b2, b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds
( b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) & b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) ) )
proof
let c1 be set ;
let c2, c3 be BinOp of c1;
thus ( c2 is_distributive_wrt c3 implies for b1, b2, b3 being Element of c1 holds
( c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) & c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) ) )
proof
assume ( c2 is_left_distributive_wrt c3 & c2 is_right_distributive_wrt c3 ) ; :: uses BINOP_1:def 11
hence for b1, b2, b3 being Element of c1 holds
( c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) & c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) ) by E13, E14;
end;
assume for b1, b2, b3 being Element of c1 holds
( c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) & c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) ) ;
hence ( for b1, b2, b3 being Element of c1 holds c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) & for b1, b2, b3 being Element of c1 holds c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) ) ; :: uses BINOP_1:def 9,BINOP_1:def 10,BINOP_1:def 11
end;

theorem E16: :: BINOP_1:24
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b3 is commutative implies ( b3 is_distributive_wrt b2 iff for b4, b5, b6 being Element of b1 holds b3 . b4,(b2 . b5,b6) = b2 . (b3 . b4,b5),(b3 . b4,b6) ) )
proof
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
assume E17: c3 is commutative ;
( for b1, b2, b3 being Element of c1 holds
( c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) & c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) iff for b1, b2, b3 being Element of c1 holds c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) )
proof
thus ( for b1, b2, b3 being Element of c1 holds
( c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) & c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) implies for b1, b2, b3 being Element of c1 holds c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) ) ;
assume E18: for b1, b2, b3 being Element of c1 holds c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) ;
let c4, c5, c6 be Element of c1;
thus c3 . c4,(c2 . c5,c6) = c2 . (c3 . c4,c5),(c3 . c4,c6) by E18;
thus c3 . (c2 . c4,c5),c6 = c3 . c6,(c2 . c4,c5) by E17, E1
.= c2 . (c3 . c6,c4),(c3 . c6,c5) by E18
.= c2 . (c3 . c4,c6),(c3 . c6,c5) by E17, E1
.= c2 . (c3 . c4,c6),(c3 . c5,c6) by E17, E1 ;
end;
hence ( c3 is_distributive_wrt c2 iff for b1, b2, b3 being Element of c1 holds c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) ) by E15;
end;

theorem E17: :: BINOP_1:25
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b3 is commutative implies ( b3 is_distributive_wrt b2 iff for b4, b5, b6 being Element of b1 holds b3 . (b2 . b4,b5),b6 = b2 . (b3 . b4,b6),(b3 . b5,b6) ) )
proof
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
assume E18: c3 is commutative ;
( for b1, b2, b3 being Element of c1 holds
( c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) & c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) iff for b1, b2, b3 being Element of c1 holds c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) )
proof
thus ( for b1, b2, b3 being Element of c1 holds
( c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) & c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) implies for b1, b2, b3 being Element of c1 holds c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) ;
assume E19: for b1, b2, b3 being Element of c1 holds c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ;
let c4, c5, c6 be Element of c1;
thus c3 . c4,(c2 . c5,c6) = c3 . (c2 . c5,c6),c4 by E18, E1
.= c2 . (c3 . c5,c4),(c3 . c6,c4) by E19
.= c2 . (c3 . c4,c5),(c3 . c6,c4) by E18, E1
.= c2 . (c3 . c4,c5),(c3 . c4,c6) by E18, E1 ;
thus c3 . (c2 . c4,c5),c6 = c2 . (c3 . c4,c6),(c3 . c5,c6) by E19;
end;
hence ( c3 is_distributive_wrt c2 iff for b1, b2, b3 being Element of c1 holds c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) by E15;
end;

theorem E18: :: BINOP_1:26
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b3 is commutative implies ( b3 is_distributive_wrt b2 iff b3 is_left_distributive_wrt b2 ) )
proof
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
( c3 is_left_distributive_wrt c2 iff for b1, b2, b3 being Element of c1 holds c3 . b1,(c2 . b2,b3) = c2 . (c3 . b1,b2),(c3 . b1,b3) ) by E13;
hence ( c3 is commutative implies ( c3 is_distributive_wrt c2 iff c3 is_left_distributive_wrt c2 ) ) by E16;
end;

theorem E19: :: BINOP_1:27
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b3 is commutative implies ( b3 is_distributive_wrt b2 iff b3 is_right_distributive_wrt b2 ) )
proof
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
( c3 is_right_distributive_wrt c2 iff for b1, b2, b3 being Element of c1 holds c3 . (c2 . b1,b2),b3 = c2 . (c3 . b1,b3),(c3 . b2,b3) ) by E14;
hence ( c3 is commutative implies ( c3 is_distributive_wrt c2 iff c3 is_right_distributive_wrt c2 ) ) by E17;
end;

theorem :: BINOP_1:28
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b3 is commutative implies ( b3 is_right_distributive_wrt b2 iff b3 is_left_distributive_wrt b2 ) )
proof
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
assume E20: c3 is commutative ;
then ( c3 is_distributive_wrt c2 iff c3 is_left_distributive_wrt c2 ) by E18;
hence ( c3 is_right_distributive_wrt c2 iff c3 is_left_distributive_wrt c2 ) by E20, E19;
end;

definition
let c1 be set ;
let c2 be UnOp of c1;
let c3 be BinOp of c1;
pred a2 is_distributive_wrt a3 means :E20: :: BINOP_1:def 12
for b1, b2 being Element of a1 holds a2 . (a3 . b1,b2) = a3 . (a2 . b1),(a2 . b2);
end;

:: deftheorem E20 defines is_distributive_wrt BINOP_1:def 12 :
for b1 being set
for b2 being UnOp of b1
for b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5 being Element of b1 holds b2 . (b3 . b4,b5) = b3 . (b2 . b4),(b2 . b5) );

definition
let c1 be non empty set ;
let c2 be BinOp of c1;
means :: BINOP_1:def 13
for b1, b2 being Element of a1 holds a2 . b1,b2 = a2 . b2,b1;
correctness
compatibility
( c2 is commutative iff for b1, b2 being Element of c1 holds c2 . b1,b2 = c2 . b2,b1 );
by E1;
means :: BINOP_1:def 14
for b1, b2, b3 being Element of a1 holds a2 . b1,(a2 . b2,b3) = a2 . (a2 . b1,b2),b3;
correctness
compatibility
( c2 is associative iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c2 . b2,b3) = c2 . (c2 . b1,b2),b3 );
by E2;
means :: BINOP_1:def 15
for b1 being Element of a1 holds a2 . b1,b1 = b1;
correctness
compatibility
( c2 is idempotent iff for b1 being Element of c1 holds c2 . b1,b1 = b1 );
by E3;
end;

:: deftheorem defines commutative BINOP_1:def 13 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is commutative iff for b3, b4 being Element of b1 holds b2 . b3,b4 = b2 . b4,b3 );

:: deftheorem defines associative BINOP_1:def 14 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is associative iff for b3, b4, b5 being Element of b1 holds b2 . b3,(b2 . b4,b5) = b2 . (b2 . b3,b4),b5 );

:: deftheorem defines idempotent BINOP_1:def 15 :
for b1 being non empty set
for b2 being BinOp of b1 holds
( b2 is idempotent iff for b3 being Element of b1 holds b2 . b3,b3 = b3 );

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
means :: BINOP_1:def 16
for b1 being Element of a1 holds a3 . a2,b1 = b1;
correctness
compatibility
( c2 is_a_left_unity_wrt c3 iff for b1 being Element of c1 holds c3 . c2,b1 = b1 );
by E4;
means :: BINOP_1:def 17
for b1 being Element of a1 holds a3 . b1,a2 = b1;
correctness
compatibility
( c2 is_a_right_unity_wrt c3 iff for b1 being Element of c1 holds c3 . b1,c2 = b1 );
by E5;
end;

:: deftheorem defines is_a_left_unity_wrt BINOP_1:def 16 :
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_left_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b2,b4 = b4 );

:: deftheorem defines is_a_right_unity_wrt BINOP_1:def 17 :
for b1 being non empty set
for b2 being Element of b1
for b3 being BinOp of b1 holds
( b2 is_a_right_unity_wrt b3 iff for b4 being Element of b1 holds b3 . b4,b2 = b4 );

definition
let c1 be non empty set ;
let c2, c3 be BinOp of c1;
means :: BINOP_1:def 18
for b1, b2, b3 being Element of a1 holds a2 . b1,(a3 . b2,b3) = a3 . (a2 . b1,b2),(a2 . b1,b3);
correctness
compatibility
( c2 is_left_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) );
by E13;
means :: BINOP_1:def 19
for b1, b2, b3 being Element of a1 holds a2 . (a3 . b1,b2),b3 = a3 . (a2 . b1,b3),(a2 . b2,b3);
correctness
compatibility
( c2 is_right_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) );
by E14;
end;

:: deftheorem defines is_left_distributive_wrt BINOP_1:def 18 :
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b2 is_left_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . b4,(b3 . b5,b6) = b3 . (b2 . b4,b5),(b2 . b4,b6) );

:: deftheorem defines is_right_distributive_wrt BINOP_1:def 19 :
for b1 being non empty set
for b2, b3 being BinOp of b1 holds
( b2 is_right_distributive_wrt b3 iff for b4, b5, b6 being Element of b1 holds b2 . (b3 . b4,b5),b6 = b3 . (b2 . b4,b6),(b2 . b5,b6) );

definition
let c1 be non empty set ;
let c2 be UnOp of c1;
let c3 be BinOp of c1;
means :: BINOP_1:def 20
for b1, b2 being Element of a1 holds a2 . (a3 . b1,b2) = a3 . (a2 . b1),(a2 . b2);
correctness
compatibility
( c2 is_distributive_wrt c3 iff for b1, b2 being Element of c1 holds c2 . (c3 . b1,b2) = c3 . (c2 . b1),(c2 . b2) );
by E20;
end;

:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :
for b1 being non empty set
for b2 being UnOp of b1
for b3 being BinOp of b1 holds
( b2 is_distributive_wrt b3 iff for b4, b5 being Element of b1 holds b2 . (b3 . b4,b5) = b3 . (b2 . b4),(b2 . b5) );