:: ALGSTR_0 semantic presentation

definition
attr c1 is strict;
struct addMagma -> 1-sorted ;
aggr addMagma(# carrier, addF #) -> addMagma ;
sel addF c1 -> BinOp of the carrier of c1;
end;

registration
let D be non empty set ;
let o be BinOp of D;
cluster addMagma(# D,o #) -> non empty ;
coherence
not addMagma(# D,o #) is empty by STRUCT_0:def 1;
end;

registration
let T be trivial set ;
let f be BinOp of T;
cluster addMagma(# T,f #) -> trivial ;
coherence
addMagma(# T,f #) is trivial by STRUCT_0:def 9;
end;

registration
let N be non trivial set ;
let b be BinOp of N;
cluster addMagma(# N,b #) -> non trivial ;
coherence
not addMagma(# N,b #) is trivial by STRUCT_0:def 9;
end;

definition
let M be addMagma ;
let x, y be Element of M;
func x + y -> Element of M equals :: ALGSTR_0:def 1
the addF of M . x,y;
coherence
the addF of M . x,y is Element of M ;
end;

:: deftheorem defines + ALGSTR_0:def 1 :
for M being addMagma
for x, y being Element of M holds x + y = the addF of M . x,y;

definition
func Trivial-addMagma -> addMagma equals :: ALGSTR_0:def 2
 addMagma(# 1,op2 #);
coherence
addMagma(# 1,op2 #) is addMagma ;
end;

:: deftheorem defines Trivial-addMagma ALGSTR_0:def 2 :
Trivial-addMagma = addMagma(# 1,op2 #);

registration
cluster Trivial-addMagma -> non empty trivial strict ;
coherence
( Trivial-addMagma is strict & not Trivial-addMagma is empty & Trivial-addMagma is trivial ) by CARD_1:87, STRUCT_0:def 9;
end;

registration
cluster non empty trivial strict addMagma ;
existence
ex b1 being addMagma st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

definition
let M be addMagma ;
let x be Element of M;
attr x is left_add-cancelable means :: ALGSTR_0:def 3
for y, z being Element of M st x + y = x + z holds
y = z;
attr x is right_add-cancelable means :Def4: :: ALGSTR_0:def 4
for y, z being Element of M st y + x = z + x holds
y = z;
end;

:: deftheorem defines left_add-cancelable ALGSTR_0:def 3 :
for M being addMagma
for x being Element of M holds
( x is left_add-cancelable iff for y, z being Element of M st x + y = x + z holds
y = z );

:: deftheorem Def4 defines right_add-cancelable ALGSTR_0:def 4 :
for M being addMagma
for x being Element of M holds
( x is right_add-cancelable iff for y, z being Element of M st y + x = z + x holds
y = z );

definition
let M be addMagma ;
let x be Element of M;
attr x is add-cancelable means :Def5: :: ALGSTR_0:def 5
( x is right_add-cancelable & x is left_add-cancelable );
end;

:: deftheorem Def5 defines add-cancelable ALGSTR_0:def 5 :
for M being addMagma
for x being Element of M holds
( x is add-cancelable iff ( x is right_add-cancelable & x is left_add-cancelable ) );

registration
let M be addMagma ;
cluster left_add-cancelable right_add-cancelable -> add-cancelable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is right_add-cancelable & b1 is left_add-cancelable holds
b1 is add-cancelable by Def5;
cluster add-cancelable -> left_add-cancelable right_add-cancelable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is add-cancelable holds
( b1 is right_add-cancelable & b1 is left_add-cancelable ) by Def5;
end;

definition
let M be addMagma ;
attr M is left_add-cancelable means :Def6: :: ALGSTR_0:def 6
for x being Element of M holds x is left_add-cancelable;
attr M is right_add-cancelable means :Def7: :: ALGSTR_0:def 7
for x being Element of M holds x is right_add-cancelable;
end;

:: deftheorem Def6 defines left_add-cancelable ALGSTR_0:def 6 :
for M being addMagma holds
( M is left_add-cancelable iff for x being Element of M holds x is left_add-cancelable );

:: deftheorem Def7 defines right_add-cancelable ALGSTR_0:def 7 :
for M being addMagma holds
( M is right_add-cancelable iff for x being Element of M holds x is right_add-cancelable );

definition
let M be addMagma ;
attr M is add-cancelable means :Def8: :: ALGSTR_0:def 8
( M is right_add-cancelable & M is left_add-cancelable );
end;

:: deftheorem Def8 defines add-cancelable ALGSTR_0:def 8 :
for M being addMagma holds
( M is add-cancelable iff ( M is right_add-cancelable & M is left_add-cancelable ) );

registration
cluster left_add-cancelable right_add-cancelable -> add-cancelable addMagma ;
coherence
for b1 being addMagma st b1 is right_add-cancelable & b1 is left_add-cancelable holds
b1 is add-cancelable by Def8;
cluster add-cancelable -> left_add-cancelable right_add-cancelable addMagma ;
coherence
for b1 being addMagma st b1 is add-cancelable holds
( b1 is right_add-cancelable & b1 is left_add-cancelable ) by Def8;
end;

registration
cluster Trivial-addMagma -> add-cancelable ;
coherence
Trivial-addMagma is add-cancelable
proof end;
end;

registration
cluster non empty trivial strict add-cancelable addMagma ;
existence
ex b1 being addMagma st
( b1 is add-cancelable & b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

registration
let M be left_add-cancelable addMagma ;
cluster -> left_add-cancelable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is left_add-cancelable by Def6;
end;

registration
let M be right_add-cancelable addMagma ;
cluster -> right_add-cancelable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is right_add-cancelable by Def7;
end;

definition
attr c1 is strict;
struct addLoopStr -> ZeroStr , addMagma ;
aggr addLoopStr(# carrier, addF, ZeroF #) -> addLoopStr ;
end;

registration
let D be non empty set ;
let o be BinOp of D;
let d be Element of D;
cluster addLoopStr(# D,o,d #) -> non empty ;
coherence
not addLoopStr(# D,o,d #) is empty by STRUCT_0:def 1;
end;

registration
let T be trivial set ;
let f be BinOp of T;
let t be Element of T;
cluster addLoopStr(# T,f,t #) -> trivial ;
coherence
addLoopStr(# T,f,t #) is trivial by STRUCT_0:def 9;
end;

registration
let N be non trivial set ;
let b be BinOp of N;
let m be Element of N;
cluster addLoopStr(# N,b,m #) -> non trivial ;
coherence
not addLoopStr(# N,b,m #) is trivial by STRUCT_0:def 9;
end;

definition
func Trivial-addLoopStr -> addLoopStr equals :: ALGSTR_0:def 9
 addLoopStr(# 1,op2 ,op0 #);
coherence
addLoopStr(# 1,op2 ,op0 #) is addLoopStr ;
end;

:: deftheorem defines Trivial-addLoopStr ALGSTR_0:def 9 :
Trivial-addLoopStr = addLoopStr(# 1,op2 ,op0 #);

registration
cluster Trivial-addLoopStr -> non empty trivial strict ;
coherence
( Trivial-addLoopStr is strict & not Trivial-addLoopStr is empty & Trivial-addLoopStr is trivial ) by CARD_1:87, STRUCT_0:def 9;
end;

registration
cluster non empty trivial strict addLoopStr ;
existence
ex b1 being addLoopStr st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

definition
let M be addLoopStr ;
let x be Element of M;
attr x is left_complementable means :Def10: :: ALGSTR_0:def 10
 ex y being Element of M st y + x = 0. M;
attr x is right_complementable means :: ALGSTR_0:def 11
 ex y being Element of M st x + y = 0. M;
end;

:: deftheorem Def10 defines left_complementable ALGSTR_0:def 10 :
for M being addLoopStr
for x being Element of M holds
( x is left_complementable iff ex y being Element of M st y + x = 0. M );

:: deftheorem defines right_complementable ALGSTR_0:def 11 :
for M being addLoopStr
for x being Element of M holds
( x is right_complementable iff ex y being Element of M st x + y = 0. M );

definition
let M be addLoopStr ;
let x be Element of M;
attr x is complementable means :Def12: :: ALGSTR_0:def 12
( x is right_complementable & x is left_complementable );
end;

:: deftheorem Def12 defines complementable ALGSTR_0:def 12 :
for M being addLoopStr
for x being Element of M holds
( x is complementable iff ( x is right_complementable & x is left_complementable ) );

registration
let M be addLoopStr ;
cluster left_complementable right_complementable -> complementable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is right_complementable & b1 is left_complementable holds
b1 is complementable by Def12;
cluster complementable -> left_complementable right_complementable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is complementable holds
( b1 is right_complementable & b1 is left_complementable ) by Def12;
end;

definition
let M be addLoopStr ;
let x be Element of M;
assume A1: ( x is left_complementable & x is right_add-cancelable ) ;
func - x -> Element of M means :: ALGSTR_0:def 13
it + x = 0. M;
existence
ex b1 being Element of M st b1 + x = 0. M by A1, Def10;
uniqueness
for b1, b2 being Element of M st b1 + x = 0. M & b2 + x = 0. M holds
b1 = b2 by A1, Def4;
end;

:: deftheorem defines - ALGSTR_0:def 13 :
for M being addLoopStr
for x being Element of M st x is left_complementable & x is right_add-cancelable holds
for b3 being Element of M holds
( b3 = - x iff b3 + x = 0. M );

definition
let V be addLoopStr ;
let v, w be Element of V;
func v - w -> Element of V equals :: ALGSTR_0:def 14
v + (- w);
correctness
coherence
v + (- w) is Element of V;
;
end;

:: deftheorem defines - ALGSTR_0:def 14 :
for V being addLoopStr
for v, w being Element of V holds v - w = v + (- w);

registration
cluster Trivial-addLoopStr -> add-cancelable ;
coherence
Trivial-addLoopStr is add-cancelable
proof end;
end;

definition
let M be addLoopStr ;
attr M is left_complementable means :Def15: :: ALGSTR_0:def 15
for x being Element of M holds x is left_complementable;
attr M is right_complementable means :Def16: :: ALGSTR_0:def 16
for x being Element of M holds x is right_complementable;
end;

:: deftheorem Def15 defines left_complementable ALGSTR_0:def 15 :
for M being addLoopStr holds
( M is left_complementable iff for x being Element of M holds x is left_complementable );

:: deftheorem Def16 defines right_complementable ALGSTR_0:def 16 :
for M being addLoopStr holds
( M is right_complementable iff for x being Element of M holds x is right_complementable );

definition
let M be addLoopStr ;
attr M is complementable means :Def17: :: ALGSTR_0:def 17
( M is right_complementable & M is left_complementable );
end;

:: deftheorem Def17 defines complementable ALGSTR_0:def 17 :
for M being addLoopStr holds
( M is complementable iff ( M is right_complementable & M is left_complementable ) );

registration
cluster left_complementable right_complementable -> complementable addLoopStr ;
coherence
for b1 being addLoopStr st b1 is right_complementable & b1 is left_complementable holds
b1 is complementable by Def17;
cluster complementable -> left_complementable right_complementable addLoopStr ;
coherence
for b1 being addLoopStr st b1 is complementable holds
( b1 is right_complementable & b1 is left_complementable ) by Def17;
end;

registration
cluster Trivial-addLoopStr -> complementable ;
coherence
Trivial-addLoopStr is complementable
proof end;
end;

registration
cluster non empty trivial add-cancelable strict complementable addLoopStr ;
existence
ex b1 being addLoopStr st
( b1 is complementable & b1 is add-cancelable & b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

registration
let M be left_complementable addLoopStr ;
cluster -> left_complementable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is left_complementable by Def15;
end;

registration
let M be right_complementable addLoopStr ;
cluster -> right_complementable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is right_complementable by Def16;
end;

definition
attr c1 is strict;
struct multMagma -> 1-sorted ;
aggr multMagma(# carrier, multF #) -> multMagma ;
sel multF c1 -> BinOp of the carrier of c1;
end;

registration
let D be non empty set ;
let o be BinOp of D;
cluster multMagma(# D,o #) -> non empty ;
coherence
not multMagma(# D,o #) is empty by STRUCT_0:def 1;
end;

registration
let T be trivial set ;
let f be BinOp of T;
cluster multMagma(# T,f #) -> trivial ;
coherence
multMagma(# T,f #) is trivial by STRUCT_0:def 9;
end;

registration
let N be non trivial set ;
let b be BinOp of N;
cluster multMagma(# N,b #) -> non trivial ;
coherence
not multMagma(# N,b #) is trivial by STRUCT_0:def 9;
end;

definition
let M be multMagma ;
let x, y be Element of M;
func x * y -> Element of M equals :: ALGSTR_0:def 18
the multF of M . x,y;
coherence
the multF of M . x,y is Element of M ;
end;

:: deftheorem defines * ALGSTR_0:def 18 :
for M being multMagma
for x, y being Element of M holds x * y = the multF of M . x,y;

definition
func Trivial-multMagma -> multMagma equals :: ALGSTR_0:def 19
 multMagma(# 1,op2 #);
coherence
multMagma(# 1,op2 #) is multMagma ;
end;

:: deftheorem defines Trivial-multMagma ALGSTR_0:def 19 :
Trivial-multMagma = multMagma(# 1,op2 #);

registration
cluster Trivial-multMagma -> non empty trivial strict ;
coherence
( Trivial-multMagma is strict & not Trivial-multMagma is empty & Trivial-multMagma is trivial ) by CARD_1:87, STRUCT_0:def 9;
end;

registration
cluster non empty trivial strict multMagma ;
existence
ex b1 being multMagma st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

definition
let M be multMagma ;
let x be Element of M;
attr x is left_mult-cancelable means :: ALGSTR_0:def 20
for y, z being Element of M st x * y = x * z holds
y = z;
attr x is right_mult-cancelable means :Def21: :: ALGSTR_0:def 21
for y, z being Element of M st y * x = z * x holds
y = z;
end;

:: deftheorem defines left_mult-cancelable ALGSTR_0:def 20 :
for M being multMagma
for x being Element of M holds
( x is left_mult-cancelable iff for y, z being Element of M st x * y = x * z holds
y = z );

:: deftheorem Def21 defines right_mult-cancelable ALGSTR_0:def 21 :
for M being multMagma
for x being Element of M holds
( x is right_mult-cancelable iff for y, z being Element of M st y * x = z * x holds
y = z );

definition
let M be multMagma ;
let x be Element of M;
attr x is mult-cancelable means :Def22: :: ALGSTR_0:def 22
( x is right_mult-cancelable & x is left_mult-cancelable );
end;

:: deftheorem Def22 defines mult-cancelable ALGSTR_0:def 22 :
for M being multMagma
for x being Element of M holds
( x is mult-cancelable iff ( x is right_mult-cancelable & x is left_mult-cancelable ) );

registration
let M be multMagma ;
cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is right_mult-cancelable & b1 is left_mult-cancelable holds
b1 is mult-cancelable by Def22;
cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable Element of the carrier of M;
coherence
for b1 being Element of M st b1 is mult-cancelable holds
( b1 is right_mult-cancelable & b1 is left_mult-cancelable ) by Def22;
end;

definition
let M be multMagma ;
attr M is left_mult-cancelable means :Def23: :: ALGSTR_0:def 23
for x being Element of M holds x is left_mult-cancelable;
attr M is right_mult-cancelable means :Def24: :: ALGSTR_0:def 24
for x being Element of M holds x is right_mult-cancelable;
end;

:: deftheorem Def23 defines left_mult-cancelable ALGSTR_0:def 23 :
for M being multMagma holds
( M is left_mult-cancelable iff for x being Element of M holds x is left_mult-cancelable );

:: deftheorem Def24 defines right_mult-cancelable ALGSTR_0:def 24 :
for M being multMagma holds
( M is right_mult-cancelable iff for x being Element of M holds x is right_mult-cancelable );

definition
let M be multMagma ;
attr M is mult-cancelable means :Def25: :: ALGSTR_0:def 25
( M is left_mult-cancelable & M is right_mult-cancelable );
end;

:: deftheorem Def25 defines mult-cancelable ALGSTR_0:def 25 :
for M being multMagma holds
( M is mult-cancelable iff ( M is left_mult-cancelable & M is right_mult-cancelable ) );

registration
cluster left_mult-cancelable right_mult-cancelable -> mult-cancelable multMagma ;
coherence
for b1 being multMagma st b1 is right_mult-cancelable & b1 is left_mult-cancelable holds
b1 is mult-cancelable by Def25;
cluster mult-cancelable -> left_mult-cancelable right_mult-cancelable multMagma ;
coherence
for b1 being multMagma st b1 is mult-cancelable holds
( b1 is right_mult-cancelable & b1 is left_mult-cancelable ) by Def25;
end;

registration
cluster Trivial-multMagma -> mult-cancelable ;
coherence
Trivial-multMagma is mult-cancelable
proof end;
end;

registration
cluster non empty trivial strict mult-cancelable multMagma ;
existence
ex b1 being multMagma st
( b1 is mult-cancelable & b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

registration
let M be left_mult-cancelable multMagma ;
cluster -> left_mult-cancelable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is left_mult-cancelable by Def23;
end;

registration
let M be right_mult-cancelable multMagma ;
cluster -> right_mult-cancelable Element of the carrier of M;
coherence
for b1 being Element of M holds b1 is right_mult-cancelable by Def24;
end;

definition
attr c1 is strict;
struct multLoopStr -> OneStr , multMagma ;
aggr multLoopStr(# carrier, multF, OneF #) -> multLoopStr ;
end;

registration
let D be non empty set ;
let o be BinOp of D;
let d be Element of D;
cluster multLoopStr(# D,o,d #) -> non empty ;
coherence
not multLoopStr(# D,o,d #) is empty by STRUCT_0:def 1;
end;

registration
let T be trivial set ;
let f be BinOp of T;
let t be Element of T;
cluster multLoopStr(# T,f,t #) -> trivial ;
coherence
multLoopStr(# T,f,t #) is trivial by STRUCT_0:def 9;
end;

registration
let N be non trivial set ;
let b be BinOp of N;
let m be Element of N;
cluster multLoopStr(# N,b,m #) -> non trivial ;
coherence
not multLoopStr(# N,b,m #) is trivial by STRUCT_0:def 9;
end;

definition
func Trivial-multLoopStr -> multLoopStr equals :: ALGSTR_0:def 26
 multLoopStr(# 1,op2 ,op0 #);
coherence
multLoopStr(# 1,op2 ,op0 #) is multLoopStr ;
end;

:: deftheorem defines Trivial-multLoopStr ALGSTR_0:def 26 :
Trivial-multLoopStr = multLoopStr(# 1,op2 ,op0 #);

registration
cluster Trivial-multLoopStr -> non empty trivial strict ;
coherence
( Trivial-multLoopStr is strict & not Trivial-multLoopStr is empty & Trivial-multLoopStr is trivial ) by CARD_1:87, STRUCT_0:def 9;
end;

registration
cluster non empty trivial strict multLoopStr ;
existence
ex b1 being multLoopStr st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

registration
cluster Trivial-multLoopStr -> mult-cancelable ;
coherence
Trivial-multLoopStr is mult-cancelable
proof end;
end;

definition
let M be multLoopStr ;
let x be Element of M;
attr x is left_invertible means :Def27: :: ALGSTR_0:def 27
 ex y being Element of M st y * x = 1. M;
attr x is right_invertible means :: ALGSTR_0:def 28
 ex y being Element of M st x * y = 1. M;
end;

:: deftheorem Def27 defines left_invertible ALGSTR_0:def 27 :
for M being multLoopStr
for x being Element of M holds
( x is left_invertible iff ex y being Element of M st y * x = 1. M );

:: deftheorem defines right_invertible ALGSTR_0:def 28 :
for M being multLoopStr
for x being Element of M holds
( x is right_invertible iff ex y being Element of M st x * y = 1. M );

definition
let M be multLoopStr ;
let x be Element of M;
attr x is invertible means :Def29: :: ALGSTR_0:def 29
( x is right_invertible & x is left_invertible );
end;

:: deftheorem Def29 defines invertible ALGSTR_0:def 29 :
for M being multLoopStr
for x being Element of M holds
( x is invertible iff ( x is right_invertible & x is left_invertible ) );

registration
let M be multLoopStr ;
cluster left_invertible right_invertible -> invertible Element of the carrier of M;
coherence
for b1 being Element of M st b1 is right_invertible & b1 is left_invertible holds
b1 is invertible by Def29;
cluster invertible -> left_invertible right_invertible Element of the carrier of M;
coherence
for b1 being Element of M st b1 is invertible holds
( b1 is right_invertible & b1 is left_invertible ) by Def29;
end;

definition
let M be multLoopStr ;
let x be Element of M;
assume A1: ( x is left_invertible & x is right_mult-cancelable ) ;
func / x -> Element of M means :: ALGSTR_0:def 30
it * x = 1. M;
existence
ex b1 being Element of M st b1 * x = 1. M by A1, Def27;
uniqueness
for b1, b2 being Element of M st b1 * x = 1. M & b2 * x = 1. M holds
b1 = b2 by A1, Def21;
end;

:: deftheorem defines / ALGSTR_0:def 30 :
for M being multLoopStr
for x being Element of M st x is left_invertible & x is right_mult-cancelable holds
for b3 being Element of M holds
( b3 = / x iff b3 * x = 1. M );

definition
let M be multLoopStr ;
attr M is left_invertible means :Def31: :: ALGSTR_0:def 31
for x being Element of M holds x is left_invertible;
attr M is right_invertible means :Def32: :: ALGSTR_0:def 32
for x being Element of M holds x is right_invertible;
end;

:: deftheorem Def31 defines left_invertible ALGSTR_0:def 31 :
for M being multLoopStr holds
( M is left_invertible iff for x being Element of M holds x is left_invertible );

:: deftheorem Def32 defines right_invertible ALGSTR_0:def 32 :
for M being multLoopStr holds
( M is right_invertible iff for x being Element of M holds x is right_invertible );

definition
let M be multLoopStr ;
attr M is invertible means :Def33: :: ALGSTR_0:def 33
( M is right_invertible & M is left_invertible );
end;

:: deftheorem Def33 defines invertible ALGSTR_0:def 33 :
for M being multLoopStr holds
( M is invertible iff ( M is right_invertible & M is left_invertible ) );

registration
cluster left_invertible right_invertible -> invertible multLoopStr ;
coherence
for b1 being multLoopStr st b1 is right_invertible & b1 is left_invertible holds
b1 is invertible by Def33;
cluster