let D be non empty set ; :: thesis: for o being BinOp of D
for a being Element of D st a is_a_unity_wrt o holds
( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
let o be BinOp of D; :: thesis: for a being Element of D st a is_a_unity_wrt o holds
( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
let a be Element of D; :: thesis: ( a is_a_unity_wrt o implies ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) )
assume A1: a is_a_unity_wrt o ; :: thesis: ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
now :: thesis: for x being Subset of D holds
( (o .:^2) . ({a},x) = x & (o .:^2) . (x,{a}) = x )
let x be Subset of D; :: thesis: ( (o .:^2) . ({a},x) = x & (o .:^2) . (x,{a}) = x )
thus (o .:^2) . ({a},x) = o .: [:{a},x:] by Th44
.= D /\ x by A1, Th51
.= x by XBOOLE_1:28 ; :: thesis: (o .:^2) . (x,{a}) = x
thus (o .:^2) . (x,{a}) = o .: [:x,{a}:] by Th44
.= D /\ x by A1, Th51
.= x by XBOOLE_1:28 ; :: thesis: verum
end;
hence A2: {a} is_a_unity_wrt o .:^2 by BINOP_1:3; :: thesis: ( o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
hence ex A being Subset of D st A is_a_unity_wrt o .:^2 ; :: according to SETWISEO:def 2 :: thesis: the_unity_wrt (o .:^2) = {a}
thus the_unity_wrt (o .:^2) = {a} by A2, BINOP_1:def 8; :: thesis: verum