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

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