let A be set ; :: thesis: for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )
let o be BinOp of A; :: thesis: for e being Element of A st o is commutative holds
( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )
let e be Element of A; :: thesis: ( o is commutative implies ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) )
assume A1: o is commutative ; :: thesis: ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )
then ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) by Th14;
hence ( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o ) by A1, Th15; :: thesis: verum