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

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