:: deftheorem Def8 defines Inv LMOD_XX1:def 8 :
for M being AbGroup
for f, b₃ being Element of set_End M holds
( b₃ = Inv f iff for x being Element of M holds b₃ . x = f . (- x) );