:: ALGSTR_1 semantic presentation

theorem E1: :: 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 E2: :: 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, E1 ;
end;

theorem E3: :: 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, E1;
hence ex b1 being Element of c1 st b1 + c2 = 0. c1 ;
end;

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

:: deftheorem ALGSTR_1:def 1 :
canceled;

:: deftheorem ALGSTR_1:def 2 :
canceled;

:: deftheorem defines Extract ALGSTR_1:def 3 :
for 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 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 ; :: uses STRUCT_0:def 1
end;
end;

theorem :: ALGSTR_1:4
canceled;

theorem E4: :: 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 :: ALGSTR_1:6
for b1, b2 being Element of L_Trivial holds b1 + b2 = 0. L_Trivial by E4;

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

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

E7: 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 E4;
end;

E8: 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 E4;
end;

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

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

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

:: deftheorem E11 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 :E12: :: 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 :E13: :: 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 :E14: :: 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 :E15: :: ALGSTR_1:def 9
for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b1 + b3 = b2;
end;

:: deftheorem E12 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 E13 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 E14 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 E15 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 :E16: :: 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 E16 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 E16;
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 E16;
end;

theorem E17: :: 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 E16;
hence for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1 + b3 = b2 by E15;
thus for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b3 + b1 = b2 by E18, E14;
thus for b1, b2, b3 being Element of c1 holds
( b1 + b2 = b1 + b3 implies b2 = b3 ) by E18, E12;
let c2, c3, c4 be Element of c1;
thus ( c3 + c2 = c4 + c2 implies c3 = c4 ) by E18, E13;
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 E12, E13, E14, E15; :: uses ALGSTR_1:def 10
end;

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

E19: for b1, b2 being Element of L_Trivial holds b1 + b2 = b2 + b1
by E4;

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 E11, E5, E6, E7, E8, E9, E10, E18, E17, 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 E17; :: uses 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; :: uses 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 E17;
end;
end;

theorem :: ALGSTR_1:8
canceled;

theorem E20: :: 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 E17, 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, E2
.= 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, E3;
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, E3;
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, E11, E17, 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 E19, 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 :: ALGSTR_1:10
canceled;

theorem :: 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 E20, 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 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 ; :: uses STRUCT_0:def 1
end;
end;

theorem :: ALGSTR_1:12
canceled;

theorem :: ALGSTR_1:13
canceled;

theorem :: ALGSTR_1:14
canceled;

theorem :: ALGSTR_1:15
canceled;

theorem :: ALGSTR_1:16
canceled;

theorem :: ALGSTR_1:17
canceled;

theorem E21: :: 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 :: ALGSTR_1:19
for b1, b2 being Element of multL_Trivial holds b1 * b2 = 1. multL_Trivial by E21;

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

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

E24: 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 E21;
end;

E25: 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 E21;
end;

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

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

definition
let c1 be non empty multLoopStr ;
attr a1 is invertible means :E28: :: 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 :E29: :: 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 E28 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 E29 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 E28, E29, E22, E23, E24, E25, E26, E27, 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 E28, E29, E22, E23, E24, E25, E26, E27, GROUP_1:def 2;
end;

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

registration
cluster associative strict multLoopStr ;
existence
ex b1 being multLoop st
( b1 is strict & b1 is associative )
proof
multL_Trivial is associative by E30, 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;

E31: 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;

E32: 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, E31 ;
end;

E33: 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, E31;
hence ex b1 being Element of c1 st b1 * c2 = 1. c1 ;
end;

theorem :: ALGSTR_1:20
canceled;

theorem :: ALGSTR_1:21
canceled;

theorem E34: :: 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 E28, 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, E32
.= 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, E33;
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, E33;
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, E28, E29, 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 E30, GROUP_1:def 4;
end;

E35: for b1, b2 being Element of multL_Trivial holds b1 * b2 = b2 * b1
by E21;

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

theorem :: ALGSTR_1:23
canceled;

theorem :: 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 E34, GROUP_1:def 16;

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

:: deftheorem ALGSTR_1:def 14 :
canceled;

:: deftheorem ALGSTR_1:def 15 :
canceled;

:: deftheorem E36 defines " ALGSTR_1:def 16 :
for b1 being non empty invertible cancelable multLoopStr
for b2, b3 being Element of b1 holds
( b3 = b2 " iff b2 * b3 = 1. b1 );

theorem :: ALGSTR_1:25
canceled;

theorem :: ALGSTR_1:26
for b1 being multGroup
for b2 being Element of b1 holds
( b2 * (b2 " ) = 1. b1 & (b2 " ) * b2 = 1. b1 )
proof
let c1 be multGroup;
let c2 be Element of c1;
thus E37: c2 * (c2 " ) = 1. c1 by E36;
( 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 E34;
hence (c2 " ) * c2 = 1. c1 by E37, E31;
end;

definition
let c1 be non empty invertible cancelable multLoopStr ;
let c2, c3 be Element of c1;
func a2 / a3 -> Element of a1 equals :: ALGSTR_1:def 17
a2 * (a3 " );
correctness
coherence
c2 * (c3 " ) is Element of c1;
;
end;

:: deftheorem defines / ALGSTR_1:def 17 :
for b1 being non empty invertible cancelable multLoopStr
for b2, b3 being Element of b1 holds b2 / b3 = b2 * (b3 " );

definition
canceled;
canceled;
canceled;
func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 21
 multLoopStr_0 REAL ,multreal ,1,0;
correctness
coherence
multLoopStr_0 REAL ,multreal ,1,0 is strict multLoopStr_0 ;
;
end;

:: deftheorem ALGSTR_1:def 18 :
canceled;

:: deftheorem ALGSTR_1:def 19 :
canceled;

:: deftheorem ALGSTR_1:def 20 :
canceled;

:: deftheorem defines multEX_0 ALGSTR_1:def 21 :
multEX_0 = multLoopStr_0 REAL ,multreal ,1,0;

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

E37: for b1, b2 being Element of multEX_0
for b3, b4 being Real holds
( ( b1 = b3 & b2 = b4 ) implies ( b1 * b2 = b3 * b4 ) )
proof
let c1, c2 be Element of multEX_0 ;
let c3, c4 be Real;
assume ( c1 = c3 & c2 = c4 ) ;
hence c1 * c2 = multreal . c3,c4
.= c3 * c4 by BINOP_2:def 11 ;

end;

E38: now
let c1, c2 be Element of multEX_0 ;
assume E39: c2 = 1 ;
reconsider c3 = c1 as Real ;
thus c1 * c2 = multreal . c3,1 by E39
.= c3 * 1 by BINOP_2:def 11
.= c1 ;
thus c2 * c1 = multreal . 1,c3 by E39
.= 1 * c3 by BINOP_2:def 11
.= c1 ;
end;

registration
cluster multEX_0 -> non empty unital strict ;
coherence
multEX_0 is unital
proof
reconsider c1 = 1 as Element of multEX_0 ;
take c1 ; :: uses GROUP_1:def 2
thus for b1 being Element of the carrier of multEX_0 holds
( b1 * c1 = b1 & c1 * b1 = b1 ) by E38;
end;
end;

E39: 0 = 0. multEX_0
;

E40: 1 = 1. multEX_0
proof
reconsider c1 = 1 as Element of multEX_0 ;
for b1 being Element of multEX_0 holds
( b1 * c1 = b1 & c1 * b1 = b1 ) by E38;
hence 1 =