for f, g, h being Function st ( for x being object holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being object st x in dom h holds
h . x = g . (f . x) ) holds
h = g * f