theorem Th7: :: BALLOT_1:7

for f, g being Function st f is one-to-one holds
for x being object st x in dom f holds
Coim ((f * g),(f . x)) = Coim (g,x)