let L be non empty doubleLoopStr ; :: thesis: ( L is _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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )

thus ( L is _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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def 12; :: 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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) implies L is _Field )

assume that

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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) ) and

A2: for a being Element of L holds a * (0. L) = 0. L and

A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) and

A4: for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) and

A5: for a, b being Element of L holds a * b = b * a ; :: thesis: L is _Field

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

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )

thus ( L is _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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def 12; :: 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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) implies L is _Field )

assume that

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 st a <> 0. L holds

ex x being Element of L st a * x = 1. L ) ) and

A2: for a being Element of L holds a * (0. L) = 0. L and

A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) and

A4: for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) and

A5: for a, b being Element of L holds a * b = b * a ; :: thesis: L is _Field

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

proof

for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a)
let a be Element of L; :: thesis: (0. L) * a = 0. L

thus (0. L) * a = a * (0. L) by A5

.= 0. L by A2 ; :: thesis: verum

end;thus (0. L) * a = a * (0. L) by A5

.= 0. L by A2 ; :: thesis: verum

proof

hence
L is _Field
by A1, A2, A3, A4, A5, A6, Th11, GROUP_1:def 12; :: thesis: verum
let a, b, c be Element of L; :: thesis: (b + c) * a = (b * a) + (c * a)

thus (b + c) * a = a * (b + c) by A5

.= (a * b) + (a * c) by A4

.= (b * a) + (a * c) by A5

.= (b * a) + (c * a) by A5 ; :: thesis: verum

end;thus (b + c) * a = a * (b + c) by A5

.= (a * b) + (a * c) by A4

.= (b * a) + (a * c) by A5

.= (b * a) + (c * a) by A5 ; :: thesis: verum