:: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def 3 :
for D being non empty set
for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds
for b₃ being UnOp of D holds
( b₃ = the_inverseOp_wrt F iff b₃ is_an_inverseOp_wrt F );