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 ) & ( for a being Element of L holds (0. L) * a = 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 ) & ( for a being Element of L holds (0. L) * a = 0. L ) implies (1. L) * a = a * (1. L) )
assume A1: ( 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 ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) ; :: thesis: (1. L) * a = a * (1. L)
A2: ( a <> 0. L implies (1. L) * a = a * (1. L) )

proof

assume a <> 0. L ; :: thesis: (1. L) * a = a * (1. L)
then consider x being Element of L such that
A3: a * x = 1. L by A1;
thus (1. L) * a = a * (x * a) by A1, A3
.= a * (1. L) by A1, A3, Lm8 ; :: thesis: verum

end;

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

proof

assume A4: a = 0. L ; :: thesis: (1. L) * a = a * (1. L)
hence (1. L) * a = 0. L by A1
.= a * (1. L) by A1, A4 ;
:: thesis: verum

end;

hence (1. L) * a = a * (1. L) by A2; :: thesis: verum