let c1, c2 be Element of L; ( ( for a being Element of L holds c1 *' a = c1 ) & ( for a being Element of L holds c2 *' a = c2 ) implies c1 = c2 )
assume that
A1:
for a being Element of L holds c1 *' a = c1
and
A2:
for a being Element of L holds c2 *' a = c2
; c1 = c2
thus c1 =
c2 *' c1
by A1
.=
c2
by A2
; verum