:: ALGSTR_0 semantic presentation

begin


definition
attrc1 is strict ;
struct addMagma  ->  1-sorted ;
aggraddMagma(# 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 ;
end;

registration
let T be trivial set ;
let f be BinOp of T;
cluster addMagma(# T,f #) ->  trivial ;
coherence
 addMagma(# T,f #) is trivial ;
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 ;
end;

definition
let M be addMagma ;
let x, y be Element of M;
funcx + 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  -> 1 -element strict ;
coherence
 ( Trivial-addMagma is 1 -element & Trivial-addMagma is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for addMagma ;
existence
 ex b1 being addMagma st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-addMagma ; ::_thesis: ( Trivial-addMagma is strict & Trivial-addMagma is 1 -element )
thus  ( Trivial-addMagma is strict & Trivial-addMagma is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let M be addMagma ;
let x be Element of M;
attrx is left_add-cancelable  means :: ALGSTR_0:def 3
 for y, z being Element of M st x + y = x + z holds
y = z;
attrx 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;
attrx 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 for 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 for 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 ;
attrM is left_add-cancelable  means :Def6: :: ALGSTR_0:def 6
 for x being Element of M holds x is left_add-cancelable ;
attrM 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 ;
attrM 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 for 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 for 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
set M = Trivial-addMagma ;
thus  Trivial-addMagma is right_add-cancelable :: according to ALGSTR_0:def_8 ::_thesis: Trivial-addMagma is left_add-cancelable
proof
let x, y, z be Element of Trivial-addMagma; :: according to ALGSTR_0:def_4,ALGSTR_0:def_7 ::_thesis: ( y + x = z + x implies y = z )
assume  y + x = z + x ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of Trivial-addMagma; :: according to ALGSTR_0:def_3,ALGSTR_0:def_6 ::_thesis: ( x + y = x + z implies y = z )
assume  x + y = x + z ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element strict add-cancelable for addMagma ;
existence
 ex b1 being addMagma st
( b1 is add-cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-addMagma ; ::_thesis: ( Trivial-addMagma is add-cancelable & Trivial-addMagma is strict & Trivial-addMagma is 1 -element )
thus  ( Trivial-addMagma is add-cancelable & Trivial-addMagma is strict & Trivial-addMagma is 1 -element ) ; ::_thesis: verum
end;
end;

registration
let M be left_add-cancelable addMagma ;
cluster  ->  left_add-cancelable for 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 for Element of the carrier of M;
coherence
 for b1 being Element of M holds b1 is right_add-cancelable by Def7;
end;

definition
attrc1 is strict ;
struct addLoopStr  ->  ZeroStr , addMagma ;
aggraddLoopStr(# 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 ;
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 ;
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 ;
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  -> 1 -element strict ;
coherence
 ( Trivial-addLoopStr is 1 -element & Trivial-addLoopStr is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for addLoopStr ;
existence
 ex b1 being addLoopStr st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr is strict & Trivial-addLoopStr is 1 -element )
thus  ( Trivial-addLoopStr is strict & Trivial-addLoopStr is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let M be addLoopStr ;
let x be Element of M;
attrx is left_complementable  means :Def10: :: ALGSTR_0:def 10
 ex y being Element of M st y + x = 0. M;
attrx 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;
attrx 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 for 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 for 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;
funcv - 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
set M = Trivial-addLoopStr ;
thus  Trivial-addLoopStr is right_add-cancelable :: according to ALGSTR_0:def_8 ::_thesis: Trivial-addLoopStr is left_add-cancelable
proof
let x, y, z be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def_4,ALGSTR_0:def_7 ::_thesis: ( y + x = z + x implies y = z )
assume  y + x = z + x ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def_3,ALGSTR_0:def_6 ::_thesis: ( x + y = x + z implies y = z )
assume  x + y = x + z ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

definition
let M be addLoopStr ;
attrM is left_complementable  means :Def15: :: ALGSTR_0:def 15
 for x being Element of M holds x is left_complementable ;
attrM 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 ;
attrM 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 for 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 for 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
set M = Trivial-addLoopStr ;
thus  Trivial-addLoopStr is right_complementable :: according to ALGSTR_0:def_17 ::_thesis: Trivial-addLoopStr is left_complementable
proof
let x be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take  x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. Trivial-addLoopStr
thus  x + x = 0. Trivial-addLoopStr by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def_15 ::_thesis: x is left_complementable
take  x ; :: according to ALGSTR_0:def_10 ::_thesis: x + x = 0. Trivial-addLoopStr
thus  x + x = 0. Trivial-addLoopStr by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element add-cancelable strict complementable for addLoopStr ;
existence
 ex b1 being addLoopStr st
( b1 is complementable & b1 is add-cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr is complementable & Trivial-addLoopStr is add-cancelable & Trivial-addLoopStr is strict & Trivial-addLoopStr is 1 -element )
thus  ( Trivial-addLoopStr is complementable & Trivial-addLoopStr is add-cancelable & Trivial-addLoopStr is strict & Trivial-addLoopStr is 1 -element ) ; ::_thesis: verum
end;
end;

registration
let M be left_complementable addLoopStr ;
cluster  ->  left_complementable for 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 for Element of the carrier of M;
coherence
 for b1 being Element of M holds b1 is right_complementable by Def16;
end;

begin

definition
attrc1 is strict ;
struct multMagma  ->  1-sorted ;
aggrmultMagma(# 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 ;
end;

registration
let T be trivial set ;
let f be BinOp of T;
cluster multMagma(# T,f #) ->  trivial ;
coherence
 multMagma(# T,f #) is trivial ;
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 ;
end;

definition
let M be multMagma ;
let x, y be Element of M;
funcx * 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  -> 1 -element strict ;
coherence
 ( Trivial-multMagma is 1 -element & Trivial-multMagma is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for multMagma ;
existence
 ex b1 being multMagma st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-multMagma ; ::_thesis: ( Trivial-multMagma is strict & Trivial-multMagma is 1 -element )
thus  ( Trivial-multMagma is strict & Trivial-multMagma is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let M be multMagma ;
let x be Element of M;
attrx is left_mult-cancelable  means :: ALGSTR_0:def 20
 for y, z being Element of M st x * y = x * z holds
y = z;
attrx 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;
attrx 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 for 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 for 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 ;
attrM is left_mult-cancelable  means :Def23: :: ALGSTR_0:def 23
 for x being Element of M holds x is left_mult-cancelable ;
attrM 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 ;
attrM 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 for 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 for 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
set M = Trivial-multMagma ;
thus  Trivial-multMagma is left_mult-cancelable :: according to ALGSTR_0:def_25 ::_thesis: Trivial-multMagma is right_mult-cancelable
proof
let x, y, z be Element of Trivial-multMagma; :: according to ALGSTR_0:def_20,ALGSTR_0:def_23 ::_thesis: ( x * y = x * z implies y = z )
assume  x * y = x * z ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of Trivial-multMagma; :: according to ALGSTR_0:def_21,ALGSTR_0:def_24 ::_thesis: ( y * x = z * x implies y = z )
assume  y * x = z * x ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element strict mult-cancelable for multMagma ;
existence
 ex b1 being multMagma st
( b1 is mult-cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-multMagma ; ::_thesis: ( Trivial-multMagma is mult-cancelable & Trivial-multMagma is strict & Trivial-multMagma is 1 -element )
thus  ( Trivial-multMagma is mult-cancelable & Trivial-multMagma is strict & Trivial-multMagma is 1 -element ) ; ::_thesis: verum
end;
end;

registration
let M be left_mult-cancelable multMagma ;
cluster  ->  left_mult-cancelable for 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 for Element of the carrier of M;
coherence
 for b1 being Element of M holds b1 is right_mult-cancelable by Def24;
end;

definition
attrc1 is strict ;
struct multLoopStr  ->  OneStr , multMagma ;
aggrmultLoopStr(# 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 ;
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 ;
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 ;
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  -> 1 -element strict ;
coherence
 ( Trivial-multLoopStr is 1 -element & Trivial-multLoopStr is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for multLoopStr ;
existence
 ex b1 being multLoopStr st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-multLoopStr ; ::_thesis: ( Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element )
thus  ( Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element ) ; ::_thesis: verum
end;
end;

registration
cluster Trivial-multLoopStr  ->  mult-cancelable ;
coherence
 Trivial-multLoopStr is mult-cancelable
proof
set M = Trivial-multLoopStr ;
thus  Trivial-multLoopStr is left_mult-cancelable :: according to ALGSTR_0:def_25 ::_thesis: Trivial-multLoopStr is right_mult-cancelable
proof
let x, y, z be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def_20,ALGSTR_0:def_23 ::_thesis: ( x * y = x * z implies y = z )
assume  x * y = x * z ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def_21,ALGSTR_0:def_24 ::_thesis: ( y * x = z * x implies y = z )
assume  y * x = z * x ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

definition
let M be multLoopStr ;
let x be Element of M;
attrx is left_invertible  means :Def27: :: ALGSTR_0:def 27
 ex y being Element of M st y * x = 1. M;
attrx 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;
attrx 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 for 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 for 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 ;
attrM is left_invertible  means :Def31: :: ALGSTR_0:def 31
 for x being Element of M holds x is left_invertible ;
attrM 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 ;
attrM 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 for multLoopStr ;
coherence
 for b1 being multLoopStr st b1 is right_invertible & b1 is left_invertible holds
b1 is invertible by Def33;
cluster invertible  ->  left_invertible right_invertible for multLoopStr ;
coherence
 for b1 being multLoopStr st b1 is invertible holds
( b1 is right_invertible & b1 is left_invertible ) by Def33;
end;

registration
cluster Trivial-multLoopStr  ->  invertible ;
coherence
 Trivial-multLoopStr is invertible
proof
set M = Trivial-multLoopStr ;
thus  Trivial-multLoopStr is right_invertible :: according to ALGSTR_0:def_33 ::_thesis: Trivial-multLoopStr is left_invertible
proof
let x be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def_32 ::_thesis: x is right_invertible
take  x ; :: according to ALGSTR_0:def_28 ::_thesis: x * x = 1. Trivial-multLoopStr
thus  x * x = 1. Trivial-multLoopStr by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def_31 ::_thesis: x is left_invertible
take  x ; :: according to ALGSTR_0:def_27 ::_thesis: x * x = 1. Trivial-multLoopStr
thus  x * x = 1. Trivial-multLoopStr by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element mult-cancelable strict invertible for multLoopStr ;
existence
 ex b1 being multLoopStr st
( b1 is invertible & b1 is mult-cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-multLoopStr ; ::_thesis: ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element )
thus  ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element ) ; ::_thesis: verum
end;
end;

registration
let M be left_invertible multLoopStr ;
cluster  ->  left_invertible for Element of the carrier of M;
coherence
 for b1 being Element of M holds b1 is left_invertible by Def31;
end;

registration
let M be right_invertible multLoopStr ;
cluster  ->  right_invertible for Element of the carrier of M;
coherence
 for b1 being Element of M holds b1 is right_invertible by Def32;
end;

begin

definition
attrc1 is strict ;
struct multLoopStr_0  ->  multLoopStr , ZeroOneStr ;
aggrmultLoopStr_0(# carrier, multF, ZeroF, OneF #) ->  multLoopStr_0 ;
end;

registration
let D be non empty set ;
let o be BinOp of D;
let d, e be Element of D;
cluster multLoopStr_0(# D,o,d,e #) ->  non empty ;
coherence
 not multLoopStr_0(# D,o,d,e #) is empty ;
end;

registration
let T be trivial set ;
let f be BinOp of T;
let s, t be Element of T;
cluster multLoopStr_0(# T,f,s,t #) ->  trivial ;
coherence
 multLoopStr_0(# T,f,s,t #) is trivial ;
end;

registration
let N be non trivial set ;
let b be BinOp of N;
let m, n be Element of N;
cluster multLoopStr_0(# N,b,m,n #) ->  non trivial ;
coherence
 not multLoopStr_0(# N,b,m,n #) is trivial ;
end;

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

:: deftheorem  defines Trivial-multLoopStr_0 ALGSTR_0:def_34_:_
 Trivial-multLoopStr_0 = multLoopStr_0(# 1,op2,op0,op0 #);

registration
cluster Trivial-multLoopStr_0  -> 1 -element strict ;
coherence
 ( Trivial-multLoopStr_0 is 1 -element & Trivial-multLoopStr_0 is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for multLoopStr_0 ;
existence
 ex b1 being multLoopStr_0 st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-multLoopStr_0 ; ::_thesis: ( Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element )
thus  ( Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let M be multLoopStr_0 ;
let x be Element of M;
funcx "  ->  Element of M means :: ALGSTR_0:def 35
it * x = 1. M if ( x is left_invertible & x is right_mult-cancelable )
otherwise it = 0. M;
existence
 ( ( x is left_invertible & x is right_mult-cancelable implies ex b1 being Element of M st b1 * x = 1. M ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) implies ex b1 being Element of M st b1 = 0. M ) ) by Def27;
uniqueness
 for b1, b2 being Element of M holds
( ( x is left_invertible & x is right_mult-cancelable & b1 * x = 1. M & b2 * x = 1. M implies b1 = b2 ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) & b1 = 0. M & b2 = 0. M implies b1 = b2 ) ) by Def21;
consistency
 for b1 being Element of M holds verum ;
end;

:: deftheorem  defines " ALGSTR_0:def_35_:_
 for M being multLoopStr_0
for x, b3 being Element of M holds
( ( x is left_invertible & x is right_mult-cancelable implies ( b3 = x " iff b3 * x = 1. M ) ) & ( ( not x is left_invertible or not x is right_mult-cancelable ) implies ( b3 = x " iff b3 = 0. M ) ) );

definition
let M be multLoopStr_0 ;
attrM is almost_left_cancelable  means :: ALGSTR_0:def 36
 for x being Element of M st x <> 0. M holds
x is left_mult-cancelable ;
attrM is almost_right_cancelable  means :: ALGSTR_0:def 37
 for x being Element of M st x <> 0. M holds
x is right_mult-cancelable ;
end;

:: deftheorem  defines almost_left_cancelable ALGSTR_0:def_36_:_
 for M being multLoopStr_0 holds
( M is almost_left_cancelable iff for x being Element of M st x <> 0. M holds
x is left_mult-cancelable );

:: deftheorem  defines almost_right_cancelable ALGSTR_0:def_37_:_
 for M being multLoopStr_0 holds
( M is almost_right_cancelable iff for x being Element of M st x <> 0. M holds
x is right_mult-cancelable );

definition
let M be multLoopStr_0 ;
attrM is almost_cancelable  means :Def38: :: ALGSTR_0:def 38
( M is almost_left_cancelable & M is almost_right_cancelable );
end;

:: deftheorem Def38 defines almost_cancelable ALGSTR_0:def_38_:_
 for M being multLoopStr_0 holds
( M is almost_cancelable iff ( M is almost_left_cancelable & M is almost_right_cancelable ) );

registration
cluster almost_left_cancelable almost_right_cancelable  ->  almost_cancelable for multLoopStr_0 ;
coherence
 for b1 being multLoopStr_0 st b1 is almost_right_cancelable & b1 is almost_left_cancelable holds
b1 is almost_cancelable by Def38;
cluster almost_cancelable  ->  almost_left_cancelable almost_right_cancelable for multLoopStr_0 ;
coherence
 for b1 being multLoopStr_0 st b1 is almost_cancelable holds
( b1 is almost_right_cancelable & b1 is almost_left_cancelable ) by Def38;
end;

registration
cluster Trivial-multLoopStr_0  ->  almost_cancelable ;
coherence
 Trivial-multLoopStr_0 is almost_cancelable
proof
set M = Trivial-multLoopStr_0 ;
thus  Trivial-multLoopStr_0 is almost_left_cancelable :: according to ALGSTR_0:def_38 ::_thesis: Trivial-multLoopStr_0 is almost_right_cancelable
proof
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_36 ::_thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is left_mult-cancelable )
assume  x <> 0. Trivial-multLoopStr_0 ; ::_thesis: x is left_mult-cancelable
let y, z be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_20 ::_thesis: ( x * y = x * z implies y = z )
assume  x * y = x * z ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_37 ::_thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is right_mult-cancelable )
assume  x <> 0. Trivial-multLoopStr_0 ; ::_thesis: x is right_mult-cancelable
let y, z be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_21 ::_thesis: ( y * x = z * x implies y = z )
assume  y * x = z * x ; ::_thesis: y = z
thus  y = z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element strict almost_cancelable for multLoopStr_0 ;
existence
 ex b1 being multLoopStr_0 st
( b1 is almost_cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-multLoopStr_0 ; ::_thesis: ( Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element )
thus  ( Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element ) ; ::_thesis: verum
end;
end;

definition
let M be multLoopStr_0 ;
attrM is almost_left_invertible  means :: ALGSTR_0:def 39
 for x being Element of M st x <> 0. M holds
x is left_invertible ;
attrM is almost_right_invertible  means :: ALGSTR_0:def 40
 for x being Element of M st x <> 0. M holds
x is right_invertible ;
end;

:: deftheorem  defines almost_left_invertible ALGSTR_0:def_39_:_
 for M being multLoopStr_0 holds
( M is almost_left_invertible iff for x being Element of M st x <> 0. M holds
x is left_invertible );

:: deftheorem  defines almost_right_invertible ALGSTR_0:def_40_:_
 for M being multLoopStr_0 holds
( M is almost_right_invertible iff for x being Element of M st x <> 0. M holds
x is right_invertible );

definition
let M be multLoopStr_0 ;
attrM is almost_invertible  means :Def41: :: ALGSTR_0:def 41
( M is almost_right_invertible & M is almost_left_invertible );
end;

:: deftheorem Def41 defines almost_invertible ALGSTR_0:def_41_:_
 for M being multLoopStr_0 holds
( M is almost_invertible iff ( M is almost_right_invertible & M is almost_left_invertible ) );

registration
cluster almost_left_invertible almost_right_invertible  ->  almost_invertible for multLoopStr_0 ;
coherence
 for b1 being multLoopStr_0 st b1 is almost_right_invertible & b1 is almost_left_invertible holds
b1 is almost_invertible by Def41;
cluster almost_invertible  ->  almost_left_invertible almost_right_invertible for multLoopStr_0 ;
coherence
 for b1 being multLoopStr_0 st b1 is almost_invertible holds
( b1 is almost_right_invertible & b1 is almost_left_invertible ) by Def41;
end;

registration
cluster Trivial-multLoopStr_0  ->  almost_invertible ;
coherence
 Trivial-multLoopStr_0 is almost_invertible
proof
set M = Trivial-multLoopStr_0 ;
thus  Trivial-multLoopStr_0 is almost_right_invertible :: according to ALGSTR_0:def_41 ::_thesis: Trivial-multLoopStr_0 is almost_left_invertible
proof
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_40 ::_thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is right_invertible )
assume  x <> 0. Trivial-multLoopStr_0 ; ::_thesis: x is right_invertible
take  x ; :: according to ALGSTR_0:def_28 ::_thesis: x * x = 1. Trivial-multLoopStr_0
thus  x * x = 1. Trivial-multLoopStr_0 by STRUCT_0:def_10; ::_thesis: verum
end;
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def_39 ::_thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is left_invertible )
assume  x <> 0. Trivial-multLoopStr_0 ; ::_thesis: x is left_invertible
take  x ; :: according to ALGSTR_0:def_27 ::_thesis: x * x = 1. Trivial-multLoopStr_0
thus  x * x = 1. Trivial-multLoopStr_0 by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element strict almost_cancelable almost_invertible for multLoopStr_0 ;
existence
 ex b1 being multLoopStr_0 st
( b1 is almost_invertible & b1 is almost_cancelable & b1 is strict & b1 is 1 -element )
proof
take  Trivial-multLoopStr_0 ; ::_thesis: ( Trivial-multLoopStr_0 is almost_invertible & Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element )
thus  ( Trivial-multLoopStr_0 is almost_invertible & Trivial-multLoopStr_0 is almost_cancelable & Trivial-multLoopStr_0 is strict & Trivial-multLoopStr_0 is 1 -element ) ; ::_thesis: verum
end;
end;

begin

definition
attrc1 is strict ;
struct doubleLoopStr  ->  addLoopStr , multLoopStr_0 ;
aggrdoubleLoopStr(# carrier, addF, multF, OneF, ZeroF #) ->  doubleLoopStr ;
end;

registration
let D be non empty set ;
let o, o1 be BinOp of D;
let d, e be Element of D;
cluster doubleLoopStr(# D,o,o1,d,e #) ->  non empty ;
coherence
 not doubleLoopStr(# D,o,o1,d,e #) is empty ;
end;

registration
let T be trivial set ;
let f, f1 be BinOp of T;
let s, t be Element of T;
cluster doubleLoopStr(# T,f,f1,s,t #) ->  trivial ;
coherence
 doubleLoopStr(# T,f,f1,s,t #) is trivial ;
end;

registration
let N be non trivial set ;
let b, b1 be BinOp of N;
let m, n be Element of N;
cluster doubleLoopStr(# N,b,b1,m,n #) ->  non trivial ;
coherence
 not doubleLoopStr(# N,b,b1,m,n #) is trivial ;
end;

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

:: deftheorem  defines Trivial-doubleLoopStr ALGSTR_0:def_42_:_
 Trivial-doubleLoopStr = doubleLoopStr(# 1,op2,op2,op0,op0 #);

registration
cluster Trivial-doubleLoopStr  -> 1 -element strict ;
coherence
 ( Trivial-doubleLoopStr is 1 -element & Trivial-doubleLoopStr is strict ) by CARD_1:49;
end;

registration
cluster1 -element strict for doubleLoopStr ;
existence
 ex b1 being doubleLoopStr st
( b1 is strict & b1 is 1 -element )
proof
take  Trivial-doubleLoopStr ; ::_thesis: ( Trivial-doubleLoopStr is strict & Trivial-doubleLoopStr is 1 -element )
thus  ( Trivial-doubleLoopStr is strict & Trivial-doubleLoopStr is 1 -element ) ; ::_thesis: verum
end;
end;