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 that

A1: F is having_a_unity and

A2: ( 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:15;

hence d1 = the_unity_wrt F by A1, A2, Th64; :: thesis: verum

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 that

A1: F is having_a_unity and

A2: ( 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:15;

hence d1 = the_unity_wrt F by A1, A2, Th64; :: thesis: verum