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