let A be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) :: thesis: ( ( for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) ) implies e is_a_unity_wrt o )

( o . (e,a) = a & o . (a,e) = a ) ; :: thesis: 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 ) ) ; :: according to BINOP_1:def 5,BINOP_1:def 6,BINOP_1:def 7 :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ) ) :: thesis: ( ( for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) ) implies e is_a_unity_wrt o )

proof

assume
for a being Element of A holds
assume
( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o )
; :: according to BINOP_1:def 7 :: thesis: for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a )

hence for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) ; :: thesis: verum

end;( o . (e,a) = a & o . (a,e) = a )

hence for a being Element of A holds

( o . (e,a) = a & o . (a,e) = a ) ; :: thesis: verum

( o . (e,a) = a & o . (a,e) = a ) ; :: thesis: 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 ) ) ; :: according to BINOP_1:def 5,BINOP_1:def 6,BINOP_1:def 7 :: thesis: verum