let D be non empty set ; :: thesis: for o being BinOp of D st o is having_a_unity holds
( o .:^2 is having_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2) = {(the_unity_wrt o)} )
let o be BinOp of D; :: thesis: ( o is having_a_unity implies ( o .:^2 is having_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2) = {(the_unity_wrt o)} ) )
given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def 2 :: thesis: ( o .:^2 is having_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2) = {(the_unity_wrt o)} )
a = the_unity_wrt o by A1, BINOP_1:def 8;
hence ( o .:^2 is having_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2) = {(the_unity_wrt o)} ) by A1, Th52; :: thesis: verum