theorem :: FUNCOP_1:70

for z being object
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 by Th7, ZFMISC_1:87;