let L be non empty doubleLoopStr ; :: thesis: ( L is leftQuasi-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 a * (b + c) = (a * b) + (a * c) ) ) )

thus ( L is leftQuasi-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 a * (b + c) = (a * b) + (a * c) ) ) ) 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 2; :: thesis: ( ( 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 a * (b + c) = (a * b) + (a * c) ) implies L is leftQuasi-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 a * (b + c) = (a * b) + (a * c) ) ) ; :: thesis: L is leftQuasi-Field

A6: for a being Element of L holds (0. L) + a = a

x = y

x = y

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 a * (b + c) = (a * b) + (a * c) ) ) )

thus ( L is leftQuasi-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 a * (b + c) = (a * b) + (a * c) ) ) ) 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 2; :: thesis: ( ( 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 a * (b + c) = (a * b) + (a * c) ) implies L is leftQuasi-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 a * (b + c) = (a * b) + (a * c) ) ) ; :: thesis: L is leftQuasi-Field

A6: for a being Element of L holds (0. L) + a = a

proof

A7:
for a, b being Element of L ex x being Element of L st a + x = b
let a be Element of L; :: thesis: (0. L) + a = a

thus (0. L) + a = a + (0. L) by A4

.= a by A1 ; :: thesis: verum

end;thus (0. L) + a = a + (0. L) by A4

.= a by A1 ; :: thesis: verum

proof

A9:
for a, b being Element of L ex x being Element of L st x + a = b
let a, b be Element of L; :: thesis: ex x being Element of L st a + x = b

consider y being Element of L such that

A8: a + y = 0. L by A2;

take x = y + b; :: thesis: a + x = b

thus a + x = (0. L) + b by A3, A8

.= b by A6 ; :: thesis: verum

end;consider y being Element of L such that

A8: a + y = 0. L by A2;

take x = y + b; :: thesis: a + x = b

thus a + x = (0. L) + b by A3, A8

.= b by A6 ; :: thesis: verum

proof

A11:
for a, x, y being Element of L st a + x = a + y holds
let a, b be Element of L; :: thesis: ex x being Element of L st x + a = b

consider x being Element of L such that

A10: a + x = b by A7;

take x ; :: thesis: x + a = b

thus x + a = b by A4, A10; :: thesis: verum

end;consider x being Element of L such that

A10: a + x = b by A7;

take x ; :: thesis: x + a = b

thus x + a = b by A4, A10; :: thesis: verum

x = y

proof

for a, x, y being Element of L st x + a = y + a holds
let a, x, y be Element of L; :: thesis: ( a + x = a + y implies x = y )

consider z being Element of L such that

A12: z + a = 0. L by A1, A2, A3, ALGSTR_1:3;

assume a + x = a + y ; :: thesis: x = y

then (z + a) + x = z + (a + y) by A3

.= (z + a) + y by A3 ;

hence x = (0. L) + y by A6, A12

.= y by A6 ;

:: thesis: verum

end;consider z being Element of L such that

A12: z + a = 0. L by A1, A2, A3, ALGSTR_1:3;

assume a + x = a + y ; :: thesis: x = y

then (z + a) + x = z + (a + y) by A3

.= (z + a) + y by A3 ;

hence x = (0. L) + y by A6, A12

.= y by A6 ;

:: thesis: verum

x = y

proof

hence
L is leftQuasi-Field
by A1, A3, A4, A5, A6, A7, 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 2, VECTSP_1:def 6; :: thesis: verum
let a, x, y be Element of L; :: thesis: ( x + a = y + a implies x = y )

assume x + a = y + a ; :: thesis: x = y

then a + x = y + a by A4

.= a + y by A4 ;

hence x = y by A11; :: thesis: verum

end;assume x + a = y + a ; :: thesis: x = y

then a + x = y + a by A4

.= a + y by A4 ;

hence x = y by A11; :: thesis: verum