let X, Y be non empty set ; :: thesis: for x being Element of X
for y being Element of Y holds
( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
let x be Element of X; :: thesis: for y being Element of Y holds
( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
let y be Element of Y; :: thesis: ( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
[x,y] in [:X,Y:] by ZFMISC_1:87;
hence ( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) ) by Def4; :: thesis: verum