for f being Function-yielding Function
for i, A being set st ( for g being Function st g in f .: A holds
i in dom g ) holds
pi ((f .: A),i) c= ((commute f) . i) .: A