:: deftheorem Def8 defines * GROUP_1A:def 7 :
for G being addGroup
for i being Integer
for h being Element of G holds
( ( 0 <= i implies i * h = (mult G) . (|.i.|,h) ) & ( not 0 <= i implies i * h = - ((mult G) . (|.i.|,h)) ) );