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} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & a = the_unity_wrt o & the_unity_wrt (o .:^2 ) = {a} ) by A1, Th53, 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)} ) ; :: thesis: verum