:: From Loops to Abelian Multiplicative Groups with Zero
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem Th1: :: ALGSTR_1:1

for L being non empty addLoopStr
for a, b being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L holds
b + a = 0. L

proof end;

theorem :: ALGSTR_1:2

for L being non empty addLoopStr
for a being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds
(0. L) + a = a + (0. L)

proof end;

theorem :: ALGSTR_1:3

for L being non empty addLoopStr st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds
for a being Element of L ex x being Element of L st x + a = 0. L

proof end;

definition

let x be set ;
canceled;
canceled;
func Extract x -> Element of {x} equals :: ALGSTR_1:def 3
x;
coherence
x is Element of {x} by TARSKI:def 1;

end;

:: deftheorem ALGSTR_1:def 1 :
canceled;

:: deftheorem ALGSTR_1:def 2 :
canceled;

:: deftheorem defines Extract ALGSTR_1:def 3 :
for x being set holds Extract x = x;

theorem :: ALGSTR_1:4

canceled;

theorem Th5: :: ALGSTR_1:5

for a, b being Element of Trivial-addLoopStr holds a = b

proof end;

theorem :: ALGSTR_1:6

for a, b being Element of Trivial-addLoopStr holds a + b = 0. Trivial-addLoopStr by Th5;

Lm1: ( ( for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr) = a ) & ( for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr) + a = a ) )
by Th5;

Lm2: for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b

proof end;

Lm3: for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b

proof end;

Lm4: ( ( for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds
x = y ) & ( for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds
x = y ) )
by Th5;

definition

let IT be non empty addLoopStr ;
canceled;
attr IT is left_zeroed means :Def5: :: ALGSTR_1:def 5
for a being Element of IT holds (0. IT) + a = a;

end;

:: deftheorem ALGSTR_1:def 4 :
canceled;

:: deftheorem Def5 defines left_zeroed ALGSTR_1:def 5 :
for IT being non empty addLoopStr holds
( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );

definition

let L be non empty addLoopStr ;
canceled;
canceled;
attr L is add-left-invertible means :Def8: :: ALGSTR_1:def 8
for a, b being Element of L ex x being Element of L st x + a = b;
attr L is add-right-invertible means :Def9: :: ALGSTR_1:def 9
for a, b being Element of L ex x being Element of L st a + x = b;

end;

:: deftheorem ALGSTR_1:def 6 :
canceled;

:: deftheorem ALGSTR_1:def 7 :
canceled;

:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :
for L being non empty addLoopStr holds
( L is add-left-invertible iff for a, b being Element of L ex x being Element of L st x + a = b );

:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :
for L being non empty addLoopStr holds
( L is add-right-invertible iff for a, b being Element of L ex x being Element of L st a + x = b );

definition

let IT be non empty addLoopStr ;
canceled;
canceled;
attr IT is Loop-like means :Def12: :: ALGSTR_1:def 12
( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible );

end;

:: deftheorem ALGSTR_1:def 10 :
canceled;

:: deftheorem ALGSTR_1:def 11 :
canceled;

:: deftheorem Def12 defines Loop-like ALGSTR_1:def 12 :
for IT being non empty addLoopStr holds
( IT is Loop-like iff ( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible ) );

registration

cluster non empty Loop-like -> non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Loop-like holds
( b₁ is left_add-cancelable & b₁ is right_add-cancelable & b₁ is add-left-invertible & b₁ is add-right-invertible ) by Def12;
cluster non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible -> non empty Loop-like addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is left_add-cancelable & b₁ is right_add-cancelable & b₁ is add-left-invertible & b₁ is add-right-invertible holds
b₁ is Loop-like by Def12;

end;

theorem Th7: :: ALGSTR_1:7

for L being non empty addLoopStr holds
( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) ) )

proof end;

Lm5: for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)
by Th5;

Lm6: for a, b being Element of Trivial-addLoopStr holds a + b = b + a
by Th5;

registration

cluster Trivial-addLoopStr -> add-associative right_zeroed left_zeroed Loop-like ;
coherence
( Trivial-addLoopStr is add-associative & Trivial-addLoopStr is Loop-like & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is left_zeroed ) by Def5, Lm1, Lm2, Lm3, Lm4, Lm5, Th7, RLVECT_1:def 6, RLVECT_1:def 7;

end;

registration

cluster non empty strict right_zeroed left_zeroed Loop-like addLoopStr ;
existence
ex b₁ being non empty addLoopStr st
( b₁ is strict & b₁ is left_zeroed & b₁ is right_zeroed & b₁ is Loop-like )

proof end;

end;

definition

mode Loop is non empty right_zeroed left_zeroed Loop-like addLoopStr ;

end;

registration

cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ;
existence
ex b₁ being Loop st
( b₁ is strict & b₁ is add-associative )

proof end;

end;

registration

cluster non empty Loop-like -> non empty add-left-invertible addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Loop-like holds
b₁ is add-left-invertible ;
cluster non empty right_complementable add-associative right_zeroed -> non empty left_zeroed Loop-like addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable holds
( b₁ is left_zeroed & b₁ is Loop-like )

proof end;

end;

theorem :: ALGSTR_1:8

canceled;

theorem Th9: :: ALGSTR_1:9

for L being non empty addLoopStr holds
( L is AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) )

proof end;

registration

cluster Trivial-addLoopStr -> Abelian ;
coherence
Trivial-addLoopStr is Abelian by Lm6, RLVECT_1:def 5;

end;

registration

cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ;
existence
ex b₁ being AddGroup st
( b₁ is strict & b₁ is Abelian )

proof end;

end;

theorem :: ALGSTR_1:10

canceled;

theorem :: ALGSTR_1:11

for L being non empty addLoopStr holds
( L is Abelian AddGroup iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) ) ) by Th9, RLVECT_1:def 5;

registration

cluster Trivial-multLoopStr -> non empty ;
coherence
not Trivial-multLoopStr is empty ;

end;

theorem :: ALGSTR_1:12

canceled;

theorem :: ALGSTR_1:13

canceled;

theorem :: ALGSTR_1:14

canceled;

theorem :: ALGSTR_1:15

canceled;

theorem :: ALGSTR_1:16

canceled;

theorem :: ALGSTR_1:17

canceled;

theorem Th18: :: ALGSTR_1:18

for a, b being Element of Trivial-multLoopStr holds a = b

proof end;

theorem :: ALGSTR_1:19

for a, b being Element of Trivial-multLoopStr holds a * b = 1. Trivial-multLoopStr by Th18;

Lm7: ( ( for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr) = a ) & ( for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr) * a = a ) )
by Th18;

Lm8: for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b

proof end;

Lm9: for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b

proof end;

definition

let IT be non empty multLoopStr ;
canceled;
attr IT is invertible means :Def14: :: ALGSTR_1:def 14
( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) );
canceled;

end;

:: deftheorem ALGSTR_1:def 13 :
canceled;

:: deftheorem Def14 defines invertible ALGSTR_1:def 14 :
for IT being non empty multLoopStr holds
( IT is invertible iff ( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) ) );

:: deftheorem ALGSTR_1:def 15 :
canceled;

notation

let L be non empty multLoopStr ;
synonym cancelable L for mult-cancelable ;

end;

registration

cluster non empty cancelable strict well-unital invertible multLoopStr ;
existence
ex b₁ being non empty multLoopStr st
( b₁ is strict & b₁ is well-unital & b₁ is invertible & b₁ is cancelable )

proof end;

end;

definition

mode multLoop is non empty cancelable well-unital invertible multLoopStr ;

end;

registration

cluster Trivial-multLoopStr -> cancelable well-unital invertible ;
coherence
( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Def14, Lm7, Lm8, Lm9, VECTSP_1:def 16;

end;

Lm10: for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th18;

registration

cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative right_unital well-unital left_unital invertible multLoopStr ;
existence
ex b₁ being multLoop st
( b₁ is strict & b₁ is associative )

proof end;

end;

definition

mode multGroup is associative multLoop;

end;

Lm11: for L being non empty multLoopStr
for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L holds
b * a = 1. L

proof end;

Lm12: for L being non empty multLoopStr
for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
(1. L) * a = a * (1. L)

proof end;

Lm13: for L being non empty multLoopStr st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
for a being Element of L ex x being Element of L st x * a = 1. L

proof end;

theorem :: ALGSTR_1:20

canceled;

theorem :: ALGSTR_1:21

canceled;

theorem Th22: :: ALGSTR_1:22

for L being non empty multLoopStr holds
( L is multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) ) )

proof end;

registration

cluster Trivial-multLoopStr -> associative ;
coherence
Trivial-multLoopStr is associative by Lm10, GROUP_1:def 4;

end;

Lm14: for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th18;

registration

cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative commutative right_unital well-unital left_unital invertible multLoopStr ;
existence
ex b₁ being multGroup st
( b₁ is strict & b₁ is commutative )

proof end;

end;

theorem :: ALGSTR_1:23

canceled;

theorem :: ALGSTR_1:24

for L being non empty multLoopStr holds
( L is commutative multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th22, GROUP_1:def 16;

notation

let L be non empty cancelable invertible multLoopStr ;
let x be Element of L;
synonym x " for / x;

end;

registration

let L be non empty cancelable invertible multLoopStr ;
cluster -> left_invertible Element of the carrier of L;
coherence
for b₁ being Element of L holds b₁ is left_invertible

proof end;

end;

theorem :: ALGSTR_1:25

canceled;

theorem :: ALGSTR_1:26

for G being multGroup
for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )

proof end;

definition

canceled;
canceled;
canceled;
let L be non empty cancelable invertible multLoopStr ;
let a, b be Element of L;
func a / b -> Element of L equals :: ALGSTR_1:def 19
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;

end;

:: deftheorem ALGSTR_1:def 16 :
canceled;

:: deftheorem ALGSTR_1:def 17 :
canceled;

:: deftheorem ALGSTR_1:def 18 :
canceled;

:: deftheorem defines / ALGSTR_1:def 19 :
for L being non empty cancelable invertible multLoopStr
for a, b being Element of L holds a / b = a * (b ");

definition

canceled;
canceled;
canceled;
func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 23
multLoopStr_0(# REAL,multreal,0,1 #);
correctness
coherence
multLoopStr_0(# REAL,multreal,0,1 #) is strict multLoopStr_0 ;
;

end;

:: deftheorem ALGSTR_1:def 20 :
canceled;

:: deftheorem ALGSTR_1:def 21 :
canceled;

:: deftheorem ALGSTR_1:def 22 :
canceled;

:: deftheorem defines multEX_0 ALGSTR_1:def 23 :
multEX_0 = multLoopStr_0(# REAL,multreal,0,1 #);

registration

cluster multEX_0 -> non empty strict ;
coherence
not multEX_0 is empty ;

end;

Lm15: now

let x, e be Element of multEX_0; :: thesis: ( e = 1 implies ( x * e = x & e * x = x ) )
reconsider a = x as Real ;
assume A1: e = 1 ; :: thesis: ( x * e = x & e * x = x )
hence x * e = a * 1 by BINOP_2:def 11
.= x ;
:: thesis: e * x = x
thus e * x = 1 * a by A1, BINOP_2:def 11
.= x ; :: thesis: verum

end;

registration

cluster multEX_0 -> strict well-unital ;
coherence
multEX_0 is well-unital

proof end;

end;

Lm16: 0 = 0. multEX_0
;

Lm17: 1 = 1_ multEX_0
;

theorem :: ALGSTR_1:27

canceled;

theorem :: ALGSTR_1:28

canceled;

theorem :: ALGSTR_1:29

canceled;

theorem :: ALGSTR_1:30

canceled;

theorem :: ALGSTR_1:31

canceled;

theorem Th32: :: ALGSTR_1:32

for q, p being Real st q <> 0 holds
ex y being Real st p = q * y

proof end;

theorem Th33: :: ALGSTR_1:33

for q, p being Real st q <> 0 holds
ex y being Real st p = y * q

proof end;

Lm18: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st a * x = b

proof end;

Lm19: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st x * a = b

proof end;

Lm20: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y

proof end;

Lm21: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y

proof end;

Lm22: for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0

proof end;

Lm23: for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0

proof end;

definition

let IT be non empty multLoopStr_0 ;
attr IT is almost_invertible means :Def24: :: ALGSTR_1:def 24
( ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st x * a = b ) );

end;

:: deftheorem Def24 defines almost_invertible ALGSTR_1:def 24 :
for IT being non empty multLoopStr_0 holds
( IT is almost_invertible iff ( ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st x * a = b ) ) );

definition

let IT be non empty multLoopStr_0 ;
canceled;
attr IT is multLoop_0-like means :Def26: :: ALGSTR_1:def 26
( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) );

end;

:: deftheorem ALGSTR_1:def 25 :
canceled;

:: deftheorem Def26 defines multLoop_0-like ALGSTR_1:def 26 :
for IT being non empty multLoopStr_0 holds
( IT is multLoop_0-like iff ( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) ) );

theorem Th34: :: ALGSTR_1:34

for L being non empty multLoopStr_0 holds
( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

proof end;

registration

cluster non empty multLoop_0-like -> non empty almost_cancelable almost_invertible multLoopStr_0 ;
coherence
for b₁ being non empty multLoopStr_0 st b₁ is multLoop_0-like holds
( b₁ is almost_invertible & b₁ is almost_cancelable ) by Def26;

end;

registration

cluster non empty non degenerated strict well-unital multLoop_0-like multLoopStr_0 ;
existence
ex b₁ being non empty multLoopStr_0 st
( b₁ is strict & b₁ is well-unital & b₁ is multLoop_0-like & not b₁ is degenerated )

proof end;

end;

definition

mode multLoop_0 is non empty non degenerated well-unital multLoop_0-like multLoopStr_0 ;

end;

registration

cluster multEX_0 -> strict well-unital multLoop_0-like ;
coherence
( multEX_0 is well-unital & multEX_0 is multLoop_0-like ) by Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Th34;

end;

Lm24: for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)

proof end;

registration

cluster non empty non degenerated strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative right_unital well-unital left_unital almost_invertible multLoop_0-like multLoopStr_0 ;
existence
ex b₁ being multLoop_0 st
( b₁ is strict & b₁ is associative & not b₁ is degenerated )

proof end;

end;

definition

mode multGroup_0 is non degenerated associative multLoop_0;

end;

theorem :: ALGSTR_1:35

canceled;

theorem :: ALGSTR_1:36

canceled;

registration

cluster multEX_0 -> strict associative ;
coherence
multEX_0 is associative by Lm24, GROUP_1:def 4;

end;

Lm25: for a, b being Element of multEX_0 holds a * b = b * a

proof end;

registration

cluster non empty non degenerated strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative commutative right_unital well-unital left_unital almost_invertible multLoop_0-like multLoopStr_0 ;
existence
ex b₁ being multGroup_0 st
( b₁ is strict & b₁ is commutative )

proof end;

end;

theorem :: ALGSTR_1:37

canceled;

theorem :: ALGSTR_1:38

canceled;

definition

let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let x be Element of L;
assume A1: x <> 0. L ;
redefine func x " means :Def27: :: ALGSTR_1:def 27
it * x = 1. L;
compatibility
for b₁ being Element of the carrier of L holds
( b₁ = x " iff b₁ * x = 1. L )

proof end;

end;

:: deftheorem Def27 defines " ALGSTR_1:def 27 :
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for x being Element of L st x <> 0. L holds
for b₃ being Element of the carrier of L holds
( b₃ = x " iff b₃ * x = 1. L );

theorem :: ALGSTR_1:39

canceled;

theorem :: ALGSTR_1:40

for G being non empty almost_cancelable associative well-unital almost_invertible multLoopStr_0
for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G & a * (a ") = 1. G )

proof end;

definition

let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let a, b be Element of L;
func a / b -> Element of L equals :: ALGSTR_1:def 28
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;

end;

:: deftheorem defines / ALGSTR_1:def 28 :
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for a, b being Element of L holds a / b = a * (b ");

registration

cluster non empty trivial -> non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is trivial holds
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable )

proof end;

cluster non empty trivial -> non empty right-distributive well-unital doubleLoopStr ;
coherence
for b₁ being non empty doubleLoopStr st b₁ is trivial holds
( b₁ is well-unital & b₁ is right-distributive )

proof end;

end;

registration

cluster non empty trivial -> non empty Group-like associative commutative multMagma ;
coherence
for b₁ being non empty multMagma st b₁ is trivial holds
( b₁ is Group-like & b₁ is associative & b₁ is commutative )

proof end;

end;