let D be non empty set ; :: thesis: for d1, d2 being Element of D
for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . d1,d2 = d2 or F . d2,d1 = d2 ) holds
d1 = the_unity_wrt F
let d1, d2 be Element of D; :: thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . d1,d2 = d2 or F . d2,d1 = d2 ) holds
d1 = the_unity_wrt F
let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . d1,d2 = d2 or F . d2,d1 = d2 ) implies d1 = the_unity_wrt F )
assume A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) ; :: thesis: ( ( not F . d1,d2 = d2 & not F . d2,d1 = d2 ) or d1 = the_unity_wrt F )
set e = the_unity_wrt F;
assume ( F . d1,d2 = d2 or F . d2,d1 = d2 ) ; :: thesis: d1 = the_unity_wrt F
then ( F . d1,d2 = F . (the_unity_wrt F),d2 or F . d2,d1 = F . d2,(the_unity_wrt F) ) by A1, SETWISEO:23;
hence d1 = the_unity_wrt F by A1, Th68; :: thesis: verum