:: deftheorem defines having_an_inverseOp FINSEQOP:def 2 :
for D being non empty set
for F being BinOp of D holds
( F is having_an_inverseOp iff ex u being UnOp of D st u is_an_inverseOp_wrt F );