let L be non empty doubleLoopStr ; :: thesis: ( L is doublesidedQuasi-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) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
thus ( L is doublesidedQuasi-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) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ) by ALGSTR_1:7, ALGSTR_1:34, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, STRUCT_0:def 8, VECTSP_1:def 16, VECTSP_1:def 18; :: 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) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) implies L is doublesidedQuasi-Field )
assume A1: ( ( 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) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ; :: thesis: L is doublesidedQuasi-Field

now

thus A2: for a being Element of L holds (0. L) + a = a :: thesis: ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) )

proof

let a be Element of L; :: thesis: (0. L) + a = a
thus (0. L) + a = a + (0. L) by A1
.= a by A1 ; :: thesis: verum

end;

thus for a, b being Element of L ex x being Element of L st a + x = b :: thesis: ( ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) )

proof

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
A3: a + y = 0. L by A1;
take x = y + b; :: thesis: a + x = b
thus a + x = (0. L) + b by A1, A3
.= b by A2 ; :: thesis: verum

end;

thus for a, b being Element of L ex x being Element of L st x + a = b :: thesis: ( ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) )

proof

let a, b be Element of L; :: thesis: ex x being Element of L st x + a = b
consider y being Element of L such that
A4: y + a = 0. L by A1, ALGSTR_1:3;
take x = b + y; :: thesis: x + a = b
thus x + a = b + (0. L) by A1, A4
.= b by A1 ; :: thesis: verum

end;

thus for a, x, y being Element of L st a + x = a + y holds
x = y :: thesis: 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; :: thesis: ( a + x = a + y implies x = y )
consider z being Element of L such that
A5: z + a = 0. L by A1, ALGSTR_1:3;
assume a + x = a + y ; :: thesis: x = y
then (z + a) + x = z + (a + y) by A1
.= (z + a) + y by A1 ;
hence x = (0. L) + y by A2, A5
.= y by A2 ;
:: thesis: verum

end;

thus for a, x, y being Element of L st x + a = y + a holds
x = y :: thesis: verum

proof

let a, x, y be Element of L; :: thesis: ( x + a = y + a implies x = y )
consider z being Element of L such that
A6: a + z = 0. L by A1;
assume x + a = y + a ; :: thesis: x = y
then x + (a + z) = (y + a) + z by A1
.= y + (a + z) by A1 ;
hence x = y + (0. L) by A1, A6
.= y by A1 ;
:: thesis: verum

end;

end;

hence L is doublesidedQuasi-Field by A1, ALGSTR_1:7, ALGSTR_1:34, ALGSTR_1:def 5, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, STRUCT_0:def 8, VECTSP_1:def 16, VECTSP_1:def 18; :: thesis: verum