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) = the_unity_wrt F holds
( d1 = . d2 & . d1 = d2 )

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) = the_unity_wrt F holds
( d1 = . d2 & . d1 = d2 )

let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F implies ( d1 = . d2 & . d1 = d2 ) )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F . (d1,d2) = the_unity_wrt F ; :: thesis: ( d1 = . d2 & . d1 = d2 )
set e = the_unity_wrt F;
set d3 = . d2;
F . ((F . (d1,d2)),( . d2)) = . d2 by ;
then F . (d1,(F . (d2,( . d2)))) = . d2 by A2;
then F . (d1,()) = . d2 by A1, A2, A3, Th59;
hence d1 = . d2 by ; :: thesis: . d1 = d2
set d3 = . d1;
F . (( . d1),(F . (d1,d2))) = . d1 by ;
then F . ((F . (( . d1),d1)),d2) = . d1 by A2;
then F . ((),d2) = . d1 by A1, A2, A3, Th59;
hence (the_inverseOp_wrt F) . d1 = d2 by ; :: thesis: verum