let A be set ; for o being BinOp of A
for e being Element of A holds
( e is_a_unity_wrt o iff for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
let o be BinOp of A; for e being Element of A holds
( e is_a_unity_wrt o iff for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
let e be Element of A; ( e is_a_unity_wrt o iff for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
thus
( e is_a_unity_wrt o implies for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
( ( for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) ) implies e is_a_unity_wrt o )
assume
for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a )
; e is_a_unity_wrt o
hence
( ( for a being Element of A holds o . (e,a) = a ) & ( for a being Element of A holds o . (a,e) = a ) )
; BINOP_1:def 5,BINOP_1:def 6,BINOP_1:def 7 verum