let L be non empty doubleLoopStr ; :: thesis: for a, b being Element of L st 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, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds

b * a = 1. L

let a, b be Element of L; :: thesis: ( 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, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L implies b * a = 1. L )

assume that

A1: 0. L <> 1. L and

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

A3: for a being Element of L st a <> 0. L holds

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

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

A5: for a being Element of L holds a * (0. L) = 0. L ; :: thesis: ( not a * b = 1. L or b * a = 1. L )

thus ( a * b = 1. L implies b * a = 1. L ) :: thesis: verum

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

b * a = 1. L

let a, b be Element of L; :: thesis: ( 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, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L implies b * a = 1. L )

assume that

A1: 0. L <> 1. L and

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

A3: for a being Element of L st a <> 0. L holds

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

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

A5: for a being Element of L holds a * (0. L) = 0. L ; :: thesis: ( not a * b = 1. L or b * a = 1. L )

thus ( a * b = 1. L implies b * a = 1. L ) :: thesis: verum