theorem :: VECTSP11:21

for i being Nat
for S being 1-sorted
for F being Function of S,S
for s1, s2 being Element of S
for n, m being Nat st (F |^ m) . s1 = s2 & (F |^ n) . s2 = s2 holds
(F |^ (m + (i * n))) . s1 = s2