let z be set ; :: thesis: for X, Y being non empty set
for x being Element of X
for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z
let X, Y be non empty set ; :: thesis: for x being Element of X
for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z
let x be Element of X; :: thesis: for y being Element of Y holds ([:X,Y:] --> z) . (x,y) = z
let y be Element of Y; :: thesis: ([:X,Y:] --> z) . (x,y) = z
[x,y] in [:X,Y:] by ZFMISC_1:87;
hence ([:X,Y:] --> z) . (x,y) = z by Th13; :: thesis: verum