:: ALGSTR_1 semantic presentation

theorem Th1: :: ALGSTR_1:1

for b₁ being non empty LoopStr
for b₂, b₃ being Element of b₁ st ( for b₄ being Element of b₁ holds b₄ + (0. b₁) = b₄ ) & ( for b₄ being Element of b₁ ex b₅ being Element of b₁ st b₄ + b₅ = 0. b₁ ) & ( for b₄, b₅, b₆ being Element of b₁ holds (b₄ + b₅) + b₆ = b₄ + (b₅ + b₆) ) & b₂ + b₃ = 0. b₁ holds
b₃ + b₂ = 0. b₁

proof end;

theorem Th2: :: ALGSTR_1:2

for b₁ being non empty LoopStr
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ + (0. b₁) = b₃ ) & ( for b₃ being Element of b₁ ex b₄ being Element of b₁ st b₃ + b₄ = 0. b₁ ) & ( for b₃, b₄, b₅ being Element of b₁ holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅) ) holds
(0. b₁) + b₂ = b₂ + (0. b₁)

proof end;

theorem Th3: :: ALGSTR_1:3

for b₁ being non empty LoopStr st ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) holds
for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₃ + b₂ = 0. b₁

proof end;

definition

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

end;

:: deftheorem Def1 ALGSTR_1:def 1 :

:: deftheorem Def2 ALGSTR_1:def 2 :

:: deftheorem Def3 defines Extract ALGSTR_1:def 3 :

definition

func L_Trivial -> strict LoopStr equals :: ALGSTR_1:def 4
LoopStr(# {{} },op2 ,(Extract {} ) #);
correctness ;

end;

:: deftheorem Def4 defines L_Trivial ALGSTR_1:def 4 :

registration

cluster L_Trivial -> non empty strict ;
coherence

proof end;

end;

theorem Th4: :: ALGSTR_1:4

canceled;

theorem Th5: :: ALGSTR_1:5

for b₁, b₂ being Element of L_Trivial holds b₁ = b₂

proof end;

theorem Th6: :: ALGSTR_1:6

for b₁, b₂ being Element of L_Trivial holds b₁ + b₂ = 0. L_Trivial by Th5;

Lemma5: for b₁ being Element of L_Trivial holds b₁ + (0. L_Trivial ) = b₁
by Th5;

Lemma6: for b₁ being Element of L_Trivial holds (0. L_Trivial ) + b₁ = b₁
by Th5;

Lemma7: for b₁, b₂ being Element of L_Trivial ex b₃ being Element of L_Trivial st b₁ + b₃ = b₂

proof end;

Lemma8: for b₁, b₂ being Element of L_Trivial ex b₃ being Element of L_Trivial st b₃ + b₁ = b₂

proof end;

Lemma9: for b₁, b₂, b₃ being Element of L_Trivial st b₁ + b₂ = b₁ + b₃ holds
b₂ = b₃
by Th5;

Lemma10: for b₁, b₂, b₃ being Element of L_Trivial st b₂ + b₁ = b₃ + b₁ holds
b₂ = b₃
by Th5;

definition

let c₁ be non empty LoopStr ;
attr a₁ is left_zeroed means :Def5: :: ALGSTR_1:def 5
for b₁ being Element of a₁ holds (0. a₁) + b₁ = b₁;

end;

:: deftheorem Def5 defines left_zeroed ALGSTR_1:def 5 :

definition

let c₁ be non empty LoopStr ;
attr a₁ is add-left-cancelable means :Def6: :: ALGSTR_1:def 6
for b₁, b₂, b₃ being Element of a₁ st b₁ + b₂ = b₁ + b₃ holds
b₂ = b₃;
attr a₁ is add-right-cancelable means :Def7: :: ALGSTR_1:def 7
for b₁, b₂, b₃ being Element of a₁ st b₂ + b₁ = b₃ + b₁ holds
b₂ = b₃;
attr a₁ is add-left-invertible means :Def8: :: ALGSTR_1:def 8
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st b₃ + b₁ = b₂;
attr a₁ is add-right-invertible means :Def9: :: ALGSTR_1:def 9
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st b₁ + b₃ = b₂;

end;

:: deftheorem Def6 defines add-left-cancelable ALGSTR_1:def 6 :

:: deftheorem Def7 defines add-right-cancelable ALGSTR_1:def 7 :

:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :

:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :

definition

let c₁ be non empty LoopStr ;
attr a₁ is Loop-like means :Def10: :: ALGSTR_1:def 10
( a₁ is add-left-cancelable & a₁ is add-right-cancelable & a₁ is add-left-invertible & a₁ is add-right-invertible );

end;

:: deftheorem Def10 defines Loop-like ALGSTR_1:def 10 :

registration

cluster non empty Loop-like -> non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible LoopStr ;
coherence by Def10;
cluster non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible -> non empty Loop-like LoopStr ;
coherence by Def10;

end;

theorem Th7: :: ALGSTR_1:7

for b₁ being non empty LoopStr holds
( b₁ is Loop-like iff ( ( for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₂ + b₄ = b₃ ) & ( for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₄ + b₂ = b₃ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ + b₃ = b₂ + b₄ holds
b₃ = b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₃ + b₂ = b₄ + b₂ holds
b₃ = b₄ ) ) )

proof end;

Lemma18: for b₁, b₂, b₃ being Element of L_Trivial holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)
by Th5;

Lemma19: for b₁, b₂ being Element of L_Trivial holds b₁ + b₂ = b₂ + b₁
by Th5;

registration end;

registration

cluster non empty strict right_zeroed left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like LoopStr ;
existence

proof end;

end;

definition

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

end;

registration

cluster strict add-associative LoopStr ;
existence

proof end;

end;

definition

mode Group is add-associative Loop;

end;

registration

cluster non empty Loop-like -> non empty right_complementable LoopStr ;
coherence

proof end;

cluster non empty add-associative right_zeroed right_complementable -> non empty left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like LoopStr ;
coherence

proof end;

end;

theorem Th8: :: ALGSTR_1:8

canceled;

theorem Th9: :: ALGSTR_1:9

for b₁ being non empty LoopStr holds
( b₁ is Group iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) ) )

proof end;

registration end;

registration

cluster strict Abelian right_complementable LoopStr ;
existence

proof end;

end;

theorem Th10: :: ALGSTR_1:10

canceled;

theorem Th11: :: ALGSTR_1:11

for b₁ being non empty LoopStr holds
( b₁ is Abelian Group iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) ) ) by Th9, RLVECT_1:def 5;

definition

func multL_Trivial -> strict multLoopStr equals :: ALGSTR_1:def 11
multLoopStr(# {{} },op2 ,(Extract {} ) #);
correctness ;

end;

:: deftheorem Def11 defines multL_Trivial ALGSTR_1:def 11 :

registration

cluster multL_Trivial -> non empty strict ;
coherence

proof end;

end;

theorem Th12: :: ALGSTR_1:12

canceled;

theorem Th13: :: ALGSTR_1:13

canceled;

theorem Th14: :: ALGSTR_1:14

canceled;

theorem Th15: :: ALGSTR_1:15

canceled;

theorem Th16: :: ALGSTR_1:16

canceled;

theorem Th17: :: ALGSTR_1:17

canceled;

theorem Th18: :: ALGSTR_1:18

for b₁, b₂ being Element of multL_Trivial holds b₁ = b₂

proof end;

theorem Th19: :: ALGSTR_1:19

for b₁, b₂ being Element of multL_Trivial holds b₁ * b₂ = 1. multL_Trivial by Th18;

Lemma22: for b₁ being Element of multL_Trivial holds b₁ * (1. multL_Trivial ) = b₁
by Th18;

Lemma23: for b₁ being Element of multL_Trivial holds (1. multL_Trivial ) * b₁ = b₁
by Th18;

Lemma24: for b₁, b₂ being Element of multL_Trivial ex b₃ being Element of multL_Trivial st b₁ * b₃ = b₂

proof end;

Lemma25: for b₁, b₂ being Element of multL_Trivial ex b₃ being Element of multL_Trivial st b₃ * b₁ = b₂

proof end;

Lemma26: for b₁, b₂, b₃ being Element of multL_Trivial st b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃
by Th18;

Lemma27: for b₁, b₂, b₃ being Element of multL_Trivial st b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃
by Th18;

definition

let c₁ be non empty multLoopStr ;
attr a₁ is invertible means :Def12: :: ALGSTR_1:def 12
( ( for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st b₁ * b₃ = b₂ ) & ( for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st b₃ * b₁ = b₂ ) );
attr a₁ is cancelable means :Def13: :: ALGSTR_1:def 13
( ( for b₁, b₂, b₃ being Element of a₁ st b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃ ) & ( for b₁, b₂, b₃ being Element of a₁ st b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃ ) );

end;

:: deftheorem Def12 defines invertible ALGSTR_1:def 12 :

:: deftheorem Def13 defines cancelable ALGSTR_1:def 13 :

registration

cluster non empty unital strict invertible cancelable multLoopStr ;
existence

proof end;

end;

definition

mode multLoop is non empty unital invertible cancelable multLoopStr ;

end;

registration

cluster multL_Trivial -> non empty unital strict invertible cancelable ;
coherence by Def12, Def13, Lemma22, Lemma23, Lemma24, Lemma25, Lemma26, Lemma27, GROUP_1:def 2;

end;

Lemma30: for b₁, b₂, b₃ being Element of multL_Trivial holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)
by Th18;

registration

cluster associative strict multLoopStr ;
existence

proof end;

end;

definition

mode multGroup is associative multLoop;

end;

Lemma31: for b₁ being non empty multLoopStr
for b₂, b₃ being Element of b₁ st ( for b₄ being Element of b₁ holds b₄ * (1. b₁) = b₄ ) & ( for b₄ being Element of b₁ ex b₅ being Element of b₁ st b₄ * b₅ = 1. b₁ ) & ( for b₄, b₅, b₆ being Element of b₁ holds (b₄ * b₅) * b₆ = b₄ * (b₅ * b₆) ) & b₂ * b₃ = 1. b₁ holds
b₃ * b₂ = 1. b₁

proof end;

Lemma32: for b₁ being non empty multLoopStr
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₃ * (1. b₁) = b₃ ) & ( for b₃ being Element of b₁ ex b₄ being Element of b₁ st b₃ * b₄ = 1. b₁ ) & ( for b₃, b₄, b₅ being Element of b₁ holds (b₃ * b₄) * b₅ = b₃ * (b₄ * b₅) ) holds
(1. b₁) * b₂ = b₂ * (1. b₁)

proof end;

Lemma33: for b₁ being non empty multLoopStr st ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) holds
for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₃ * b₂ = 1. b₁

proof end;

theorem Th20: :: ALGSTR_1:20

canceled;

theorem Th21: :: ALGSTR_1:21

canceled;

theorem Th22: :: ALGSTR_1:22

for b₁ being non empty multLoopStr holds
( b₁ is multGroup iff ( ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) ) )

proof end;

registration

cluster multL_Trivial -> non empty unital associative strict invertible cancelable ;
coherence by Lemma30, GROUP_1:def 4;

end;

Lemma35: for b₁, b₂ being Element of multL_Trivial holds b₁ * b₂ = b₂ * b₁
by Th18;

registration

cluster commutative strict multLoopStr ;
existence

proof end;

end;

theorem Th23: :: ALGSTR_1:23

canceled;

theorem Th24: :: ALGSTR_1:24

for b₁ being non empty multLoopStr holds
( b₁ is commutative multGroup iff ( ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂ ) ) ) by Th22, GROUP_1:def 16;

definition

let c₁ be non empty invertible cancelable multLoopStr ;
let c₂ be Element of c₁;
canceled;
canceled;
func c₂ " -> Element of a₁ means :Def16: :: ALGSTR_1:def 16
a₂ * a₃ = 1. a₁;
existence by Def12;
uniqueness by Def13;

end;

:: deftheorem Def14 ALGSTR_1:def 14 :

:: deftheorem Def15 ALGSTR_1:def 15 :

:: deftheorem Def16 defines " ALGSTR_1:def 16 :

theorem Th25: :: ALGSTR_1:25

canceled;

theorem Th26: :: ALGSTR_1:26

for b₁ being multGroup
for b₂ being Element of b₁ holds
( b₂ * (b₂ " ) = 1. b₁ & (b₂ " ) * b₂ = 1. b₁ )

proof end;

definition

let c₁ be non empty invertible cancelable multLoopStr ;
let c₂, c₃ be Element of c₁;
func c₂ / c₃ -> Element of a₁ equals :: ALGSTR_1:def 17
a₂ * (a₃ " );
correctness ;

end;

:: deftheorem Def17 defines / ALGSTR_1:def 17 :

definition

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

end;

:: deftheorem Def18 ALGSTR_1:def 18 :

:: deftheorem Def19 ALGSTR_1:def 19 :

:: deftheorem Def20 ALGSTR_1:def 20 :

:: deftheorem Def21 defines multEX_0 ALGSTR_1:def 21 :

registration

cluster multEX_0 -> non empty strict ;
coherence

proof end;

end;

Lemma37: for b₁, b₂ being Element of multEX_0
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ * b₄
by BINOP_2:def 11;

E38: now

let c₁, c₂ be Element of multEX_0 ;
assume E39: c₂ = 1 ;
reconsider c₃ = c₁ as Real ;
thus c₁ * c₂ = multreal . c₃,1 by E39
.= c₃ * 1 by BINOP_2:def 11
.= c₁ ;
thus c₂ * c₁ = multreal . 1,c₃ by E39
.= 1 * c₃ by BINOP_2:def 11
.= c₁ ;

end;

registration

cluster multEX_0 -> non empty unital strict ;
coherence

proof end;

end;

Lemma39: 0 = 0. multEX_0
;

Lemma40: 1 = 1. multEX_0

proof end;

theorem Th27: :: ALGSTR_1:27

canceled;

theorem Th28: :: ALGSTR_1:28

canceled;

theorem Th29: :: ALGSTR_1:29

canceled;

theorem Th30: :: ALGSTR_1:30

canceled;

theorem Th31: :: ALGSTR_1:31

canceled;

theorem Th32: :: ALGSTR_1:32

for b₁, b₂ being Real st b₁ <> 0 holds
ex b₃ being Real st b₂ = b₁ * b₃

proof end;

theorem Th33: :: ALGSTR_1:33

for b₁, b₂ being Real st b₁ <> 0 holds
ex b₃ being Real st b₂ = b₃ * b₁

proof end;

Lemma43: for b₁, b₂ being Element of multEX_0 st b₁ <> 0. multEX_0 holds
ex b₃ being Element of multEX_0 st b₁ * b₃ = b₂

proof end;

Lemma44: for b₁, b₂ being Element of multEX_0 st b₁ <> 0. multEX_0 holds
ex b₃ being Element of multEX_0 st b₃ * b₁ = b₂

proof end;

Lemma45: for b₁, b₂, b₃ being Element of multEX_0 st b₁ <> 0. multEX_0 & b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃

proof end;

Lemma46: for b₁, b₂, b₃ being Element of multEX_0 st b₁ <> 0. multEX_0 & b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃

proof end;

Lemma47: for b₁ being Element of multEX_0 holds b₁ * (0. multEX_0 ) = 0. multEX_0

proof end;

Lemma48: for b₁ being Element of multEX_0 holds (0. multEX_0 ) * b₁ = 0. multEX_0

proof end;

definition

let c₁ be non empty multLoopStr_0 ;
attr a₁ is almost_invertible means :Def22: :: ALGSTR_1:def 22
( ( for b₁, b₂ being Element of a₁ st b₁ <> 0. a₁ holds
ex b₃ being Element of a₁ st b₁ * b₃ = b₂ ) & ( for b₁, b₂ being Element of a₁ st b₁ <> 0. a₁ holds
ex b₃ being Element of a₁ st b₃ * b₁ = b₂ ) );
attr a₁ is almost_cancelable means :Def23: :: ALGSTR_1:def 23
( ( for b₁, b₂, b₃ being Element of a₁ st b₁ <> 0. a₁ & b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃ ) & ( for b₁, b₂, b₃ being Element of a₁ st b₁ <> 0. a₁ & b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃ ) );

end;

:: deftheorem Def22 defines almost_invertible ALGSTR_1:def 22 :

:: deftheorem Def23 defines almost_cancelable ALGSTR_1:def 23 :

definition

let c₁ be non empty multLoopStr_0 ;
attr a₁ is multLoop_0-like means :Def24: :: ALGSTR_1:def 24
( a₁ is almost_invertible & a₁ is almost_cancelable & ( for b₁ being Element of a₁ holds b₁ * (0. a₁) = 0. a₁ ) & ( for b₁ being Element of a₁ holds (0. a₁) * b₁ = 0. a₁ ) );

end;

:: deftheorem Def24 defines multLoop_0-like ALGSTR_1:def 24 :

theorem Th34: :: ALGSTR_1:34

for b₁ being non empty multLoopStr_0 holds
( b₁ is multLoop_0-like iff ( ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₂ * b₄ = b₃ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₄ * b₂ = b₃ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) ) )

proof end;

registration

cluster non empty multLoop_0-like -> non empty almost_invertible almost_cancelable multLoopStr_0 ;
coherence by Def24;

end;

registration

cluster non empty unital strict non degenerated almost_invertible almost_cancelable multLoop_0-like multLoopStr_0 ;
existence

proof end;

end;

definition

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

end;

registration

cluster multEX_0 -> non empty unital strict almost_invertible almost_cancelable multLoop_0-like ;
coherence by Lemma43, Lemma44, Lemma45, Lemma46, Lemma47, Lemma48, Th34;

end;

Lemma53: for b₁, b₂, b₃ being Element of multEX_0 holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof end;

registration

cluster associative strict multLoopStr_0 ;
existence

proof end;

end;

definition

mode multGroup_0 is associative non degenerated multLoop_0;

end;

Lemma54: for b₁ being non empty multLoopStr_0
for b₂, b₃ being Element of b₁ st 0. b₁ <> 1. b₁ & ( for b₄ being Element of b₁ holds b₄ * (1. b₁) = b₄ ) & ( for b₄ being Element of b₁ st b₄ <> 0. b₁ holds
ex b₅ being Element of b₁ st b₄ * b₅ = 1. b₁ ) & ( for b₄, b₅, b₆ being Element of b₁ holds (b₄ * b₅) * b₆ = b₄ * (b₅ * b₆) ) & ( for b₄ being Element of b₁ holds b₄ * (0. b₁) = 0. b₁ ) & b₂ * b₃ = 1. b₁ holds
b₃ * b₂ = 1. b₁

proof end;

Lemma55: for b₁ being non empty multLoopStr_0
for b₂ being Element of b₁ st 0. b₁ <> 1. b₁ & ( for b₃ being Element of b₁ holds b₃ * (1. b₁) = b₃ ) & ( for b₃ being Element of b₁ st b₃ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₃ * b₄ = 1. b₁ ) & ( for b₃, b₄, b₅ being Element of b₁ holds (b₃ * b₄) * b₅ = b₃ * (b₄ * b₅) ) & ( for b₃ being Element of b₁ holds b₃ * (0. b₁) = 0. b₁ ) holds
(1. b₁) * b₂ = b₂ * (1. b₁)

proof end;

Lemma56: for b₁ being non empty multLoopStr_0 st 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) holds
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₃ * b₂ = 1. b₁

proof end;

theorem Th35: :: ALGSTR_1:35

canceled;

theorem Th36: :: ALGSTR_1:36

for b₁ being non empty multLoopStr_0 holds
( b₁ is multGroup_0 iff ( 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) ) )

proof end;

registration

cluster multEX_0 -> non empty unital associative strict almost_invertible almost_cancelable multLoop_0-like ;
coherence by Lemma53, GROUP_1:def 4;

end;

Lemma58: for b₁, b₂ being Element of multEX_0 holds b₁ * b₂ = b₂ * b₁

proof end;

registration

cluster commutative strict multLoopStr_0 ;
existence

proof end;

end;

theorem Th37: :: ALGSTR_1:37

canceled;

theorem Th38: :: ALGSTR_1:38

for b₁ being non empty multLoopStr_0 holds
( b₁ is commutative multGroup_0 iff ( 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) & ( for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂ ) ) ) by Th36, GROUP_1:def 16;

definition

let c₁ be non empty almost_invertible almost_cancelable multLoopStr_0 ;
let c₂ be Element of c₁;
assume E59: c₂ <> 0. c₁ ;
func c₂ " -> Element of a₁ means :Def25: :: ALGSTR_1:def 25
a₂ * a₃ = 1. a₁;
existence by E59, Def22;
uniqueness by E59, Def23;

end;

:: deftheorem Def25 defines " ALGSTR_1:def 25 :

theorem Th39: :: ALGSTR_1:39

canceled;

theorem Th40: :: ALGSTR_1:40

for b₁ being non empty unital associative almost_invertible almost_cancelable multLoopStr_0
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
( b₂ * (b₂ " ) = 1. b₁ & (b₂ " ) * b₂ = 1. b₁ )

proof end;

definition

let c₁ be non empty almost_invertible almost_cancelable multLoopStr_0 ;
let c₂, c₃ be Element of c₁;
func c₂ / c₃ -> Element of a₁ equals :: ALGSTR_1:def 26
a₂ * (a₃ " );
correctness ;

end;

:: deftheorem Def26 defines / ALGSTR_1:def 26 :