let D be non empty set ; :: thesis: for d being Element of D
for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds
(F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = d
let d be Element of D; :: thesis: for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds
(F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = d
let F be BinOp of D; :: thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp implies (F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = d )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp ; :: thesis: (F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = d
set u = the_inverseOp_wrt F;
set e = the_unity_wrt F;
thus (F * (id D),(the_inverseOp_wrt F)) . d,(the_unity_wrt F) = F . d,((the_inverseOp_wrt F) . (the_unity_wrt F)) by Th87
.= F . d,(the_unity_wrt F) by A1, A2, A3, Th65
.= d by A2, SETWISEO:23 ; :: thesis: verum