let A be set ; :: thesis: for o being BinOp of A
for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds
e1 = e2
let o be BinOp of A; :: thesis: for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds
e1 = e2
let e1, e2 be Element of A; :: thesis: ( e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2 )
assume that
e1 is_a_left_unity_wrt o and
A1: ( e1 is_a_right_unity_wrt o & e2 is_a_left_unity_wrt o ) and
e2 is_a_right_unity_wrt o ; :: according to BINOP_1:def 7 :: thesis: e1 = e2
thus e1 = e2 by A1, Th17; :: thesis: verum