theorem Th3: :: ABCMIZ_1:3

for f being Function
for x, y being object st f = [x,y] holds
x = y