:: deftheorem defines is_an_inverseOp_wrt FINSEQOP:def 1 :
for D being non empty set
for u being UnOp of D
for F being BinOp of D holds
( u is_an_inverseOp_wrt F iff for d being Element of D holds
( F . (d,(u . d)) = the_unity_wrt F & F . ((u . d),d) = the_unity_wrt F ) );