let L be non empty doubleLoopStr ; ( 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) ) ) )
thus
( L is rightQuasi-Field implies ( ( 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) ) ) )
by ALGSTR_1:6, ALGSTR_1:16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 3; ( ( 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) ) implies L is rightQuasi-Field )
assume that
A1:
for a being Element of L holds a + (0. L) = a
and
A2:
for a being Element of L ex x being Element of L st a + x = 0. L
and
A3:
for a, b, c being Element of L holds (a + b) + c = a + (b + c)
and
A4:
for a, b being Element of L holds a + b = b + a
and
A5:
( 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) ) )
; L is rightQuasi-Field
A6:
for a, b being Element of L ex x being Element of L st x + a = b
A8:
for a being Element of L holds (0. L) + a = a
A9:
for a, x, y being Element of L st a + x = a + y holds
x = y
A11:
for a, x, y being Element of L st x + a = y + a holds
x = y
proof
let a,
x,
y be
Element of
L;
( x + a = y + a implies x = y )
consider z being
Element of
L such that A12:
a + z = 0. L
by A2;
assume
x + a = y + a
;
x = y
then x + (a + z) =
(y + a) + z
by A3
.=
y + (a + z)
by A3
;
hence x =
y + (0. L)
by A1, A12
.=
y
by A1
;
verum
end;
for a, b being Element of L ex x being Element of L st a + x = b
hence
L is rightQuasi-Field
by A1, A3, A4, A5, A8, A6, A9, A11, ALGSTR_1:6, ALGSTR_1:16, ALGSTR_1:def 2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 3, VECTSP_1:def 6; verum