let A be set ; :: thesis: for o being BinOp of A
for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds
e1 = e2
let o be BinOp of A; :: thesis: for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds
e1 = e2
let e1, e2 be Element of A; :: thesis: ( e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2 )
assume that
A1: e1 is_a_left_unity_wrt o and
A2: e2 is_a_right_unity_wrt o ; :: thesis: e1 = e2
thus e1 = o . (e1,e2) by A2, Def6
.= e2 by A1, Def5 ; :: thesis: verum