let X, Y, Z be 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]
let F be 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 x be Element of X; for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let z be Element of Z; [: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]
; verum