theorem
for
L being non
empty doubleLoopStr holds
(
L is
rightQuasi-Field iff ( ( for
a being
Element of
L holds
a + (0. L) = a ) & ( for
a being
Element of
L ex
x being
Element of
L st
a + x = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(a + b) + c = a + (b + c) ) & ( for
a,
b being
Element of
L holds
a + b = b + a ) &
0. L <> 1. L & ( for
a being
Element of
L holds
a * (1. L) = a ) & ( for
a being
Element of
L holds
(1. L) * a = a ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
a * x = b ) & ( for
a,
b being
Element of
L st
a <> 0. L holds
ex
x being
Element of
L st
x * a = b ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
a * x = a * y holds
x = y ) & ( for
a,
x,
y being
Element of
L st
a <> 0. L &
x * a = y * a holds
x = y ) & ( for
a being
Element of
L holds
a * (0. L) = 0. L ) & ( for
a being
Element of
L holds
(0. L) * a = 0. L ) & ( for
a,
b,
c being
Element of
L holds
(b + c) * a = (b * a) + (c * a) ) ) )