for i, j being Nat
for S being 1-sorted
for F being Function of S,S holds F |^ (i + j) = (F |^ j) * (F |^ i)