:: ALGSTR_1 semantic presentation

theorem Th1: :: ALGSTR_1:1
for b1 being non empty LoopStr
for b2, b3 being Element of b1 holds
( ( for b4 being Element of b1 holds b4 + (0. b1) = b4 ) & ( for b4 being Element of b1 holds
ex b5 being Element of b1 st b4 + b5 = 0. b1 ) & ( for b4, b5, b6 being Element of b1 holds (b4 + b5) + b6 = b4 + (b5 + b6) ) & b2 + b3 = 0. b1 implies b3 + b2 = 0. b1 )
proof
let c1 be non empty LoopStr ;
let c2, c3 be Element of c1;
assume E2: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) ) ;
assume E3: c2 + c3 = 0. c1 ;
consider c4 being Element of c1 such that
E4: c3 + c4 = 0. c1 by E2;
thus c3 + c2 = (c3 + c2) + (c3 + c4) by E2, E4
.= ((c3 + c2) + c3) + c4 by E2
.= (c3 + (0. c1)) + c4 by E2, E3
.= 0. c1 by E2, E4 ;
end;

theorem Th2: :: ALGSTR_1:2
for b1 being non empty LoopStr
for b2 being Element of b1 holds
( ( for b3 being Element of b1 holds b3 + (0. b1) = b3 ) & ( for b3 being Element of b1 holds
ex b4 being Element of b1 st b3 + b4 = 0. b1 ) & ( for b3, b4, b5 being Element of b1 holds (b3 + b4) + b5 = b3 + (b4 + b5) ) implies (0. b1) + b2 = b2 + (0. b1) )
proof
let c1 be non empty LoopStr ;
let c2 be Element of c1;
assume E3: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) ) ;
then consider c3 being Element of c1 such that
E4: c2 + c3 = 0. c1 ;
thus (0. c1) + c2 = c2 + (c3 + c2) by E3, E4
.= c2 + (0. c1) by E3, E4, Th1 ;
end;

theorem Th3: :: ALGSTR_1:3
for b1 being non empty LoopStr holds
( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) implies for b2 being Element of b1 holds
ex b3 being Element of b1 st b3 + b2 = 0. b1 )
proof
let c1 be non empty LoopStr ;
assume E4: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) ) ;
let c2 be Element of c1;
consider c3 being Element of c1 such that
E5: c2 + c3 = 0. c1 by E4;
c3 + c2 = 0. c1 by E4, E5, Th1;
hence ex b1 being Element of c1 st b1 + c2 = 0. c1 ;
end;

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

:: deftheorem Def1 ALGSTR_1:def 1 :
canceled;

:: deftheorem Def2 ALGSTR_1:def 2 :
canceled;

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

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

:: deftheorem Def4 defines L_Trivial ALGSTR_1:def 4 :
L_Trivial = LoopStr(# {{} },op2 ,(Extract {} ) #);

registration
cluster L_Trivial -> non empty strict ;
coherence
not L_Trivial is empty
proof
thus not the carrier of L_Trivial is empty ; :: according to STRUCT_0:def 1
end;
end;

theorem Th4: :: ALGSTR_1:4
canceled;

theorem Th5: :: ALGSTR_1:5
for b1, b2 being Element of L_Trivial holds b1 = b2
proof
let c1, c2 be Element of L_Trivial ;
thus c1 = {} by TARSKI:def 1
.= c2 by TARSKI:def 1 ;
end;

theorem Th6: :: ALGSTR_1:6
for b1, b2 being Element of L_Trivial holds b1 + b2 = 0. L_Trivial by Th5;

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

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

Lemma7: for b1, b2 being Element of L_Trivial holds
ex b3 being Element of L_Trivial st b1 + b3 = b2
proof
let c1, c2 be Element of L_Trivial ;
take c3 = 0. L_Trivial ;
thus c1 + c3 = c2 by Th5;
end;

Lemma8: for b1, b2 being Element of L_Trivial holds
ex b3 being Element of L_Trivial st b3 + b1 = b2
proof
let c1, c2 be Element of L_Trivial ;
take c3 = 0. L_Trivial ;
thus c3 + c1 = c2 by Th5;
end;

Lemma9: for b1, b2, b3 being Element of L_Trivial holds
( b1 + b2 = b1 + b3 implies b2 = b3 )
by Th5;

Lemma10: for b1, b2, b3 being Element of L_Trivial holds
( b2 + b1 = b3 + b1 implies b2 = b3 )
by Th5;

definition
let c1 be non empty LoopStr ;
attr a1 is left_zeroed means :Def5: :: ALGSTR_1:def 5
for b1 being Element of a1 holds (0. a1) + b1 = b1;
end;

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

definition
let c1 be non empty LoopStr ;
attr a1 is add-left-cancelable means :Def6: :: ALGSTR_1:def 6
for b1, b2, b3 being Element of a1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 );
attr a1 is add-right-cancelable means :Def7: :: ALGSTR_1:def 7
for b1, b2, b3 being Element of a1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 );
attr a1 is add-left-invertible means :Def8: :: ALGSTR_1:def 8
for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b3 + b1 = b2;
attr a1 is add-right-invertible means :Def9: :: ALGSTR_1:def 9
for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b1 + b3 = b2;
end;

:: deftheorem Def6 defines add-left-cancelable ALGSTR_1:def 6 :
for b1 being non empty LoopStr holds
( b1 is add-left-cancelable iff for b2, b3, b4 being Element of b1 holds
( b2 + b3 = b2 + b4 implies b3 = b4 ) );

:: deftheorem Def7 defines add-right-cancelable ALGSTR_1:def 7 :
for b1 being non empty LoopStr holds
( b1 is add-right-cancelable iff for b2, b3, b4 being Element of b1 holds
( b3 + b2 = b4 + b2 implies b3 = b4 ) );

:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :
for b1 being non empty LoopStr holds
( b1 is add-left-invertible iff for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b4 + b2 = b3 );

:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :
for b1 being non empty LoopStr holds
( b1 is add-right-invertible iff for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b2 + b4 = b3 );

definition
let c1 be non empty LoopStr ;
attr a1 is Loop-like means :Def10: :: ALGSTR_1:def 10
( a1 is add-left-cancelable & a1 is add-right-cancelable & a1 is add-left-invertible & a1 is add-right-invertible );
end;

:: deftheorem Def10 defines Loop-like ALGSTR_1:def 10 :
for b1 being non empty LoopStr holds
( b1 is Loop-like iff ( b1 is add-left-cancelable & b1 is add-right-cancelable & b1 is add-left-invertible & b1 is add-right-invertible ) );

registration
cluster non empty Loop-like -> non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible LoopStr ;
coherence
for b1 being non empty LoopStr holds
( b1 is Loop-like implies ( b1 is add-left-cancelable & b1 is add-right-cancelable & b1 is add-left-invertible & b1 is add-right-invertible ) ) by Def10;
cluster non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible -> non empty Loop-like LoopStr ;
coherence
for b1 being non empty LoopStr holds
( b1 is add-left-cancelable & b1 is add-right-cancelable & b1 is add-left-invertible & b1 is add-right-invertible implies b1 is Loop-like ) by Def10;
end;

theorem Th7: :: ALGSTR_1:7
for b1 being non empty LoopStr holds
( b1 is Loop-like iff ( ( for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b2 + b4 = b3 ) & ( for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b4 + b2 = b3 ) & ( for b2, b3, b4 being Element of b1 holds
( b2 + b3 = b2 + b4 implies b3 = b4 ) ) & ( for b2, b3, b4 being Element of b1 holds
( b3 + b2 = b4 + b2 implies b3 = b4 ) ) ) )
proof
let c1 be non empty LoopStr ;
hereby
assume c1 is Loop-like ;
then E18: ( c1 is add-left-cancelable & c1 is add-right-cancelable & c1 is add-left-invertible & c1 is add-right-invertible ) by Def10;
hence for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2 by Def9;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2 by E18, Def8;
thus for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 ) by E18, Def6;
let c2, c3, c4 be Element of c1;
thus ( c3 + c2 = c4 + c2 implies c3 = c4 ) by E18, Def7;
end;
assume ( ( for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2 ) & ( for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2 ) & ( for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 ) ) ) ;
hence ( c1 is add-left-cancelable & c1 is add-right-cancelable & c1 is add-left-invertible & c1 is add-right-invertible ) by Def6, Def7, Def8, Def9; :: according to ALGSTR_1:def 10
end;

Lemma18: for b1, b2, b3 being Element of L_Trivial holds (b1 + b2) + b3 = b1 + (b2 + b3)
by Th5;

Lemma19: for b1, b2 being Element of L_Trivial holds b1 + b2 = b2 + b1
by Th5;

registration
cluster L_Trivial -> non empty strict add-associative right_zeroed left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like ;
coherence
( L_Trivial is add-associative & L_Trivial is Loop-like & L_Trivial is right_zeroed & L_Trivial is left_zeroed ) by Def5, Lemma5, Lemma6, Lemma7, Lemma8, Lemma9, Lemma10, Lemma18, Th7, RLVECT_1:def 6, RLVECT_1:def 7;
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
ex b1 being non empty LoopStr st
( b1 is strict & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like )
proof
take L_Trivial ;
thus ( L_Trivial is strict & L_Trivial is left_zeroed & L_Trivial is right_zeroed & L_Trivial is Loop-like ) ;
end;
end;

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

registration
cluster strict add-associative LoopStr ;
existence
ex b1 being Loop st
( b1 is strict & b1 is add-associative )
proof
take L_Trivial ;
thus ( L_Trivial is strict & L_Trivial is add-associative ) ;
end;
end;

definition
mode Group is add-associative Loop;
end;

registration
cluster non empty Loop-like -> non empty right_complementable LoopStr ;
coherence
for b1 being non empty LoopStr holds
( b1 is Loop-like implies b1 is right_complementable )
proof
let c1 be non empty LoopStr ;
assume c1 is Loop-like ;
hence for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 by Th7; :: according to RLVECT_1:def 8
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
for b1 being non empty LoopStr holds
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable implies ( b1 is left_zeroed & b1 is Loop-like ) )
proof
let c1 be non empty LoopStr ;
assume E20: ( c1 is add-associative & c1 is right_zeroed & c1 is right_complementable ) ;
then reconsider c2 = c1 as non empty add-associative right_zeroed right_complementable LoopStr ;
thus for b1 being Element of c1 holds (0. c1) + b1 = b1 by E20, RLVECT_1:10; :: according to ALGSTR_1:def 5
now
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2 by E20, RLVECT_1:20;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2
proof
let c3, c4 be Element of c1;
reconsider c5 = c3, c6 = c4 as Element of c2 ;
reconsider c7 = c6 + (- c5) as Element of c1 ;
take c7 ;
(c6 + (- c5)) + c5 = c6 + ((- c5) + c5) by RLVECT_1:def 6
.= c6 + (0. c2) by RLVECT_1:16
.= c4 by RLVECT_1:10 ;
hence c7 + c3 = c4 ;
end;
thus ( ( for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 ) ) ) by E20, RLVECT_1:21;
end;
hence c1 is Loop-like by Th7;
end;
end;

theorem Th8: :: ALGSTR_1:8
canceled;

theorem Th9: :: ALGSTR_1:9
for b1 being non empty LoopStr holds
( b1 is Group iff ( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) ) )
proof
let c1 be non empty LoopStr ;
thus ( c1 is Group implies ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) ) ) by Th7, RLVECT_1:def 6, RLVECT_1:def 7;
assume E21: ( ( for b1 being Element of c1 holds b1 + (0. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 + b2 = 0. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 + b2) + b3 = b1 + (b2 + b3) ) ) ;
now
thus E22: for b1 being Element of c1 holds (0. c1) + b1 = b1
proof
let c2 be Element of c1;
thus (0. c1) + c2 = c2 + (0. c1) by E21, Th2
.= c2 by E21 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E23: c2 + c4 = 0. c1 by E21;
take c5 = c4 + c3;
thus c2 + c5 = (0. c1) + c3 by E21, E23
.= c3 by E22 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E23: c4 + c2 = 0. c1 by E21, Th3;
take c5 = c3 + c4;
thus c5 + c2 = c3 + (0. c1) by E21, E23
.= c3 by E21 ;
end;
thus for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E23: c5 + c2 = 0. c1 by E21, Th3;
assume c2 + c3 = c2 + c4 ;
then (c5 + c2) + c3 = c5 + (c2 + c4) by E21
.= (c5 + c2) + c4 by E21 ;
hence c3 = (0. c1) + c4 by E22, E23
.= c4 by E22 ;

end;
thus for b1, b2, b3 being Element of c1 holds
( b2 + b1 = b3 + b1 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E23: c2 + c5 = 0. c1 by E21;
assume c3 + c2 = c4 + c2 ;
then c3 + (c2 + c5) = (c4 + c2) + c5 by E21
.= c4 + (c2 + c5) by E21 ;
hence c3 = c4 + (0. c1) by E21, E23
.= c4 by E21 ;

end;
end;
hence c1 is Group by E21, Def5, Th7, RLVECT_1:def 6, RLVECT_1:def 7;
end;

registration
cluster L_Trivial -> non empty strict Abelian add-associative right_zeroed right_complementable left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like ;
coherence
L_Trivial is Abelian by Lemma19, RLVECT_1:def 5;
end;

registration
cluster strict Abelian right_complementable LoopStr ;
existence
ex b1 being Group st
( b1 is strict & b1 is Abelian )
proof
take L_Trivial ;
thus ( L_Trivial is strict & L_Trivial is Abelian ) ;
end;
end;

theorem Th10: :: ALGSTR_1:10
canceled;

theorem Th11: :: ALGSTR_1:11
for b1 being non empty LoopStr holds
( b1 is Abelian Group iff ( ( for b2 being Element of b1 holds b2 + (0. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 + b3 = 0. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4) ) & ( for b2, b3 being Element of b1 holds b2 + b3 = b3 + b2 ) ) ) by Th9, RLVECT_1:def 5;

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

:: deftheorem Def11 defines multL_Trivial ALGSTR_1:def 11 :
multL_Trivial = multLoopStr(# {{} },op2 ,(Extract {} ) #);

registration
cluster multL_Trivial -> non empty strict ;
coherence
not multL_Trivial is empty
proof
thus not the carrier of multL_Trivial is empty ; :: according to STRUCT_0:def 1
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 b1, b2 being Element of multL_Trivial holds b1 = b2
proof
let c1, c2 be Element of multL_Trivial ;
thus c1 = {} by TARSKI:def 1
.= c2 by TARSKI:def 1 ;
end;

theorem Th19: :: ALGSTR_1:19
for b1, b2 being Element of multL_Trivial holds b1 * b2 = 1. multL_Trivial by Th18;

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

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

Lemma24: for b1, b2 being Element of multL_Trivial holds
ex b3 being Element of multL_Trivial st b1 * b3 = b2
proof
let c1, c2 be Element of multL_Trivial ;
take c3 = 1. multL_Trivial ;
thus c1 * c3 = c2 by Th18;
end;

Lemma25: for b1, b2 being Element of multL_Trivial holds
ex b3 being Element of multL_Trivial st b3 * b1 = b2
proof
let c1, c2 be Element of multL_Trivial ;
take c3 = 1. multL_Trivial ;
thus c3 * c1 = c2 by Th18;
end;

Lemma26: for b1, b2, b3 being Element of multL_Trivial holds
( b1 * b2 = b1 * b3 implies b2 = b3 )
by Th18;

Lemma27: for b1, b2, b3 being Element of multL_Trivial holds
( b2 * b1 = b3 * b1 implies b2 = b3 )
by Th18;

definition
let c1 be non empty multLoopStr ;
attr a1 is invertible means :Def12: :: ALGSTR_1:def 12
( ( for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b1 * b3 = b2 ) & ( for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b3 * b1 = b2 ) );
attr a1 is cancelable means :Def13: :: ALGSTR_1:def 13
( ( for b1, b2, b3 being Element of a1 holds
( b1 * b2 = b1 * b3 implies b2 = b3 ) ) & ( for b1, b2, b3 being Element of a1 holds
( b2 * b1 = b3 * b1 implies b2 = b3 ) ) );
end;

:: deftheorem Def12 defines invertible ALGSTR_1:def 12 :
for b1 being non empty multLoopStr holds
( b1 is invertible iff ( ( for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b2 * b4 = b3 ) & ( for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b4 * b2 = b3 ) ) );

:: deftheorem Def13 defines cancelable ALGSTR_1:def 13 :
for b1 being non empty multLoopStr holds
( b1 is cancelable iff ( ( for b2, b3, b4 being Element of b1 holds
( b2 * b3 = b2 * b4 implies b3 = b4 ) ) & ( for b2, b3, b4 being Element of b1 holds
( b3 * b2 = b4 * b2 implies b3 = b4 ) ) ) );

registration
cluster non empty unital strict invertible cancelable multLoopStr ;
existence
ex b1 being non empty multLoopStr st
( b1 is strict & b1 is unital & b1 is invertible & b1 is cancelable )
proof
( multL_Trivial is unital & multL_Trivial is invertible & multL_Trivial is cancelable ) by Def12, Def13, Lemma22, Lemma23, Lemma24, Lemma25, Lemma26, Lemma27, GROUP_1:def 2;
hence ex b1 being non empty multLoopStr st
( b1 is strict & b1 is unital & b1 is invertible & b1 is cancelable ) ;
end;
end;

definition
mode multLoop is non empty unital invertible cancelable multLoopStr ;
end;

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

Lemma30: for b1, b2, b3 being Element of multL_Trivial holds (b1 * b2) * b3 = b1 * (b2 * b3)
by Th18;

registration
cluster associative strict multLoopStr ;
existence
ex b1 being multLoop st
( b1 is strict & b1 is associative )
proof
multL_Trivial is associative by Lemma30, GROUP_1:def 4;
hence ex b1 being multLoop st
( b1 is strict & b1 is associative ) ;
end;
end;

definition
mode multGroup is associative multLoop;
end;

Lemma31: for b1 being non empty multLoopStr
for b2, b3 being Element of b1 holds
( ( for b4 being Element of b1 holds b4 * (1. b1) = b4 ) & ( for b4 being Element of b1 holds
ex b5 being Element of b1 st b4 * b5 = 1. b1 ) & ( for b4, b5, b6 being Element of b1 holds (b4 * b5) * b6 = b4 * (b5 * b6) ) & b2 * b3 = 1. b1 implies b3 * b2 = 1. b1 )
proof
let c1 be non empty multLoopStr ;
let c2, c3 be Element of c1;
assume E32: ( ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 * b2 = 1. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) ) ;
assume E33: c2 * c3 = 1. c1 ;
consider c4 being Element of c1 such that
E34: c3 * c4 = 1. c1 by E32;
thus c3 * c2 = (c3 * c2) * (c3 * c4) by E32, E34
.= ((c3 * c2) * c3) * c4 by E32
.= (c3 * (1. c1)) * c4 by E32, E33
.= 1. c1 by E32, E34 ;
end;

Lemma32: for b1 being non empty multLoopStr
for b2 being Element of b1 holds
( ( for b3 being Element of b1 holds b3 * (1. b1) = b3 ) & ( for b3 being Element of b1 holds
ex b4 being Element of b1 st b3 * b4 = 1. b1 ) & ( for b3, b4, b5 being Element of b1 holds (b3 * b4) * b5 = b3 * (b4 * b5) ) implies (1. b1) * b2 = b2 * (1. b1) )
proof
let c1 be non empty multLoopStr ;
let c2 be Element of c1;
assume E33: ( ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 * b2 = 1. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) ) ;
then consider c3 being Element of c1 such that
E34: c2 * c3 = 1. c1 ;
thus (1. c1) * c2 = c2 * (c3 * c2) by E33, E34
.= c2 * (1. c1) by E33, E34, Lemma31 ;
end;

Lemma33: for b1 being non empty multLoopStr holds
( ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 * b3 = 1. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4) ) implies for b2 being Element of b1 holds
ex b3 being Element of b1 st b3 * b2 = 1. b1 )
proof
let c1 be non empty multLoopStr ;
assume E34: ( ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 * b2 = 1. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) ) ;
let c2 be Element of c1;
consider c3 being Element of c1 such that
E35: c2 * c3 = 1. c1 by E34;
c3 * c2 = 1. c1 by E34, E35, Lemma31;
hence ex b1 being Element of c1 st b1 * c2 = 1. c1 ;
end;

theorem Th20: :: ALGSTR_1:20
canceled;

theorem Th21: :: ALGSTR_1:21
canceled;

theorem Th22: :: ALGSTR_1:22
for b1 being non empty multLoopStr holds
( b1 is multGroup iff ( ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 * b3 = 1. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4) ) ) )
proof
let c1 be non empty multLoopStr ;
thus ( c1 is multGroup implies ( ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 * b2 = 1. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) ) ) by Def12, GROUP_1:def 4, VECTSP_1:def 13;
assume E35: ( ( for b1 being Element of c1 holds b1 * (1. c1) = b1 ) & ( for b1 being Element of c1 holds
ex b2 being Element of c1 st b1 * b2 = 1. c1 ) & ( for b1, b2, b3 being Element of c1 holds (b1 * b2) * b3 = b1 * (b2 * b3) ) ) ;
now
thus E36: for b1 being Element of c1 holds (1. c1) * b1 = b1
proof
let c2 be Element of c1;
thus (1. c1) * c2 = c2 * (1. c1) by E35, Lemma32
.= c2 by E35 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 * b3 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E37: c2 * c4 = 1. c1 by E35;
take c5 = c4 * c3;
thus c2 * c5 = (1. c1) * c3 by E35, E37
.= c3 by E36 ;
end;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 * b1 = b2
proof
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E37: c4 * c2 = 1. c1 by E35, Lemma33;
take c5 = c3 * c4;
thus c5 * c2 = c3 * (1. c1) by E35, E37
.= c3 by E35 ;
end;
thus for b1, b2, b3 being Element of c1 holds
( b1 * b2 = b1 * b3 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E37: c5 * c2 = 1. c1 by E35, Lemma33;
assume c2 * c3 = c2 * c4 ;
then (c5 * c2) * c3 = c5 * (c2 * c4) by E35
.= (c5 * c2) * c4 by E35 ;
hence c3 = (1. c1) * c4 by E36, E37
.= c4 by E36 ;

end;
thus for b1, b2, b3 being Element of c1 holds
( b2 * b1 = b3 * b1 implies b2 = b3 )
proof
let c2, c3, c4 be Element of c1;
consider c5 being Element of c1 such that
E37: c2 * c5 = 1. c1 by E35;
assume c3 * c2 = c4 * c2 ;
then c3 * (c2 * c5) = (c4 * c2) * c5 by E35
.= c4 * (c2 * c5) by E35 ;
hence c3 = c4 * (1. c1) by E35, E37
.= c4 by E35 ;

end;
end;
hence c1 is multGroup by E35, Def12, Def13, GROUP_1:def 4, GROUP_1:def 2;
end;

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

Lemma35: for b1, b2 being Element of multL_Trivial holds b1 * b2 = b2 * b1
by Th18;

registration
cluster commutative strict multLoopStr ;
existence
ex b1 being multGroup st
( b1 is strict & b1 is commutative )
proof
multL_Trivial is commutative by Lemma35, GROUP_1:def 16;
hence ex b1 being multGroup st
( b1 is strict & b1 is commutative ) ;
end;
end;

theorem Th23: :: ALGSTR_1:23
canceled;

theorem Th24: :: ALGSTR_1:24
for b1 being non empty multLoopStr holds
( b1 is commutative multGroup iff ( ( for b2 being Element of b1 holds b2 * (1. b1) = b2 ) & ( for b2 being Element of b1 holds
ex b3 being Element of b1 st b2 * b3 = 1. b1 ) & ( for b2, b3, b4 being Element of b1 holds (b2 * b3) * b4 = b2 * (b3 * b4) ) & ( for b2, b3 being Element of b1 holds b2 * b3 = b3 * b2 ) ) ) by Th22, GROUP_1:def 16;

definition
let c1 be non empty invertible cancelable multLoopStr ;
let c2 be Element of c1;
canceled;
canceled;
func c2 " -> Element of a1 means :Def16: :: ALGSTR_1:def 16
a2 * a3 = 1. a1;
existence
ex b1 being Element of c1 st c2 * b1 = 1. c1 by Def12;
uniqueness
for b1, b2 being Element of c1 holds
( c2 * b1 = 1. c1 & c2 * b2 = 1. c1 implies b1 = b2 ) by Def13;
end;

:: deftheorem Def14 ALGSTR_1:def 14 :