for S being 1-sorted
for F being Function of S,S holds F |^ 1 = F