:: deftheorem Def2a defines is_inner_wrt GROUP_22:def 2 :
for G being Group
for a being Element of G
for f being Function holds
( a is_inner_wrt f iff for x being Element of G holds f . x = x |^ a );