theorem Th4: :: HILB10_7:4

for n being Nat
for D being non empty set
for M, A being BinOp of D
for d being Element of D st M is having_a_unity & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
( ( n is even implies M "**" (n |-> ((the_inverseOp_wrt A) . d)) = M "**" (n |-> d) ) & ( n is odd implies M "**" (n |-> ((the_inverseOp_wrt A) . d)) = (the_inverseOp_wrt A) . (M "**" (n |-> d)) ) )