theorem Th11: :: AOFA_000:11

for f, g being Function
for a, A being set st rng f c= dom f & a in dom f & g * f = g & a in A holds
((A,g) iter f) . a = ((A,g) iter f) . (f . a)