theorem Th72: :: FUNCOP_1:72

for x, y being object holds (x .--> y) . x = y