theorem Th27: :: ENS_1:28

for V being non empty set
for f, g being Morphism of (Ens V) st dom g = cod f holds
g (*) f = (@ g) * (@ f)