begin
theorem Th1:
theorem
theorem
:: deftheorem ALGSTR_1:def 1 :
canceled;
:: deftheorem ALGSTR_1:def 2 :
canceled;
:: deftheorem defines Extract ALGSTR_1:def 3 :
theorem
canceled;
theorem Th5:
theorem
Lm1:
( ( for a being Element of holds a + (0. Trivial-addLoopStr ) = a ) & ( for a being Element of holds (0. Trivial-addLoopStr ) + a = a ) )
by Th5;
Lm2:
for a, b being Element of ex x being Element of st a + x = b
Lm3:
for a, b being Element of ex x being Element of st x + a = b
Lm4:
( ( for a, x, y being Element of st a + x = a + y holds
x = y ) & ( for a, x, y being Element of st x + a = y + a holds
x = y ) )
by Th5;
:: deftheorem ALGSTR_1:def 4 :
canceled;
:: deftheorem Def5 defines left_zeroed ALGSTR_1:def 5 :
:: deftheorem ALGSTR_1:def 6 :
canceled;
:: deftheorem ALGSTR_1:def 7 :
canceled;
:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :
:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :
:: deftheorem ALGSTR_1:def 10 :
canceled;
:: deftheorem ALGSTR_1:def 11 :
canceled;
:: deftheorem Def12 defines Loop-like ALGSTR_1:def 12 :
theorem Th7:
Lm5:
for a, b, c being Element of holds (a + b) + c = a + (b + c)
by Th5;
Lm6:
for a, b being Element of holds a + b = b + a
by Th5;
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem
Lm7:
( ( for a being Element of holds a * (1. Trivial-multLoopStr ) = a ) & ( for a being Element of holds (1. Trivial-multLoopStr ) * a = a ) )
by Th18;
Lm8:
for a, b being Element of ex x being Element of st a * x = b
Lm9:
for a, b being Element of ex x being Element of st x * a = b
:: deftheorem ALGSTR_1:def 13 :
canceled;
:: deftheorem Def14 defines invertible ALGSTR_1:def 14 :
:: deftheorem ALGSTR_1:def 15 :
canceled;
Lm10:
for a, b, c being Element of holds (a * b) * c = a * (b * c)
by Th18;
Lm11:
for L being non empty multLoopStr
for a, b being Element of st ( for a being Element of holds a * (1. L) = a ) & ( for a being Element of ex x being Element of st a * x = 1. L ) & ( for a, b, c being Element of 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 st ( for a being Element of holds a * (1. L) = a ) & ( for a being Element of ex x being Element of st a * x = 1. L ) & ( for a, b, c being Element of 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 holds a * (1. L) = a ) & ( for a being Element of ex x being Element of st a * x = 1. L ) & ( for a, b, c being Element of holds (a * b) * c = a * (b * c) ) holds
for a being Element of ex x being Element of st x * a = 1. L
theorem
canceled;
theorem
canceled;
theorem Th22:
Lm14:
for a, b being Element of holds a * b = b * a
by Th18;
theorem
canceled;
theorem
theorem
canceled;
theorem
:: deftheorem ALGSTR_1:def 16 :
canceled;
:: deftheorem ALGSTR_1:def 17 :
canceled;
:: deftheorem ALGSTR_1:def 18 :
canceled;
:: deftheorem defines / ALGSTR_1:def 19 :
:: deftheorem ALGSTR_1:def 20 :
canceled;
:: deftheorem ALGSTR_1:def 21 :
canceled;
:: deftheorem ALGSTR_1:def 22 :
canceled;
:: deftheorem defines multEX_0 ALGSTR_1:def 23 :
Lm16:
0 = 0. multEX_0
;
Lm17:
1 = 1_ multEX_0
;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th32:
theorem Th33:
Lm18:
for a, b being Element of st a <> 0. multEX_0 holds
ex x being Element of st a * x = b
Lm19:
for a, b being Element of st a <> 0. multEX_0 holds
ex x being Element of st x * a = b
Lm20:
for a, x, y being Element of st a <> 0. multEX_0 & a * x = a * y holds
x = y
Lm21:
for a, x, y being Element of st a <> 0. multEX_0 & x * a = y * a holds
x = y
Lm22:
for a being Element of holds a * (0. multEX_0 ) = 0. multEX_0
Lm23:
for a being Element of holds (0. multEX_0 ) * a = 0. multEX_0
:: deftheorem Def24 defines almost_invertible ALGSTR_1:def 24 :
:: deftheorem ALGSTR_1:def 25 :
canceled;
:: deftheorem Def26 defines multLoop_0-like ALGSTR_1:def 26 :
theorem Th34:
Lm24:
for a, b, c being Element of holds (a * b) * c = a * (b * c)
theorem
canceled;
theorem
canceled;
Lm25:
for a, b being Element of holds a * b = b * a
theorem
canceled;
theorem
canceled;
:: deftheorem Def27 defines " ALGSTR_1:def 27 :
theorem
canceled;
theorem
:: deftheorem defines / ALGSTR_1:def 28 :