let L be non empty multLoopStr ; :: thesis: for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of 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) ) holds
(1. L) * a = a * (1. L)
let a be Element of L; :: thesis: ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of 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) ) implies (1. L) * a = a * (1. L) )
assume A1: ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of 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) ) ) ; :: thesis: (1. L) * a = a * (1. L)
then consider x being Element of L such that
A2: a * x = 1. L ;
thus (1. L) * a = a * (x * a) by A1, A2
.= a * (1. L) by A1, A2, Lm16 ; :: thesis: verum