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