let L be non empty doubleLoopStr ; :: thesis: for a 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 ) holds

(1. L) * a = a * (1. L)

let a 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 ) implies (1. L) * a = 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: (1. L) * a = a * (1. L)

A6: ( a <> 0. L implies (1. L) * a = a * (1. L) )

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 ) holds

(1. L) * a = a * (1. L)

let a 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 ) implies (1. L) * a = 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: (1. L) * a = a * (1. L)

A6: ( a <> 0. L implies (1. L) * a = a * (1. L) )

proof

( a = 0. L implies (1. L) * a = a * (1. L) )
assume
a <> 0. L
; :: thesis: (1. L) * a = a * (1. L)

then consider x being Element of L such that

A7: a * x = 1. L by A3;

thus (1. L) * a = a * (x * a) by A4, A7

.= a * (1. L) by A1, A2, A3, A4, A5, A7, Lm6 ; :: thesis: verum

end;then consider x being Element of L such that

A7: a * x = 1. L by A3;

thus (1. L) * a = a * (x * a) by A4, A7

.= a * (1. L) by A1, A2, A3, A4, A5, A7, Lm6 ; :: thesis: verum

proof

hence
(1. L) * a = a * (1. L)
by A6; :: thesis: verum
assume A8:
a = 0. L
; :: thesis: (1. L) * a = a * (1. L)

hence (1. L) * a = 0. L by A5

.= a * (1. L) by A2, A8 ;

:: thesis: verum

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

.= a * (1. L) by A2, A8 ;

:: thesis: verum