let X, Y, Z be non empty set ; :: thesis: 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]
let F be Function of X,Y; :: thesis: for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let x be Element of X; :: thesis: for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let z be Element of Z; :: thesis: [:F,(id Z):] . (x,z) = [(F . x),z]
thus [:F,(id Z):] . (x,z) = [(F . x),((id Z) . z)] by FUNCT_3:75
.= [(F . x),z] ; :: thesis: verum