begin
Lm1:
( ( for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr) = a ) & ( for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr) + a = a ) )
by Th4;
Lm2:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b
Lm3:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b
Lm4:
( ( for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds
x = y ) & ( for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds
x = y ) )
by Th4;
Lm5:
for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)
by Th4;
Lm6:
for a, b being Element of Trivial-addLoopStr holds a + b = b + a
by Th4;
Lm7:
( ( for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr) = a ) & ( for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr) * a = a ) )
by Th9;
Lm8:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b
Lm9:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b
Lm10:
for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th9;
Lm11:
for L being non empty multLoopStr
for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L holds
b * a = 1. L
Lm12:
for L being non empty multLoopStr
for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
(1. L) * a = a * (1. L)
Lm13:
for L being non empty multLoopStr st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
for a being Element of L ex x being Element of L st x * a = 1. L
Lm14:
for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th9;
Lm16:
0 = 0. multEX_0
;
Lm17:
1 = 1_ multEX_0
;
Lm18:
for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st a * x = b
Lm19:
for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st x * a = b
Lm20:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y
Lm21:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y
Lm22:
for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0
Lm23:
for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0
Lm24:
for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
Lm25:
for a, b being Element of multEX_0 holds a * b = b * a