let X be non empty set ; :: thesis: for x, y being object st X --> x = X --> y holds
x = y
let x, y be object ; :: thesis: ( X --> x = X --> y implies x = y )
assume A1: X --> x = X --> y ; :: thesis: x = y
( rng (X --> x) = {x} & rng (X --> y) = {y} ) by FUNCOP_1:8;
hence x = y by A1, ZFMISC_1:3; :: thesis: verum