let X, Y, Z be non empty set ; :: thesis: for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let F be Function of X,Y; :: thesis: for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let y be Element of Y; :: thesis: for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let z be Element of Z; :: thesis: [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
thus [:F,(id Z):] " {[y,z]} = [:F,(id Z):] " [:{y},{z}:] by ZFMISC_1:35
.= [:(F " {y}),((id Z) " {z}):] by FUNCT_3:94
.= [:(F " {y}),{z}:] by FUNCT_2:171 ; :: thesis: verum