theorem :: EQREL_1:58

for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]