theorem :: GRFUNC_1:4

for x, z being object
for f, g being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )