let c1, c2 be Element of L; :: thesis: ( ( 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 ; :: thesis: c1 = c2
thus c1 = c2 *' c1 by A1
.= c2 by A2 ; :: thesis: verum