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 Th81

.= F . (d,(the_unity_wrt F)) by A1, A2, A3, Th61

.= d by A2, SETWISEO:15 ; :: thesis: verum

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 Th81

.= F . (d,(the_unity_wrt F)) by A1, A2, A3, Th61

.= d by A2, SETWISEO:15 ; :: thesis: verum