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