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:29

.= [:(F " {y}),((id Z) " {z}):] by FUNCT_3:73

.= [:(F " {y}),{z}:] by FUNCT_2:94 ; :: thesis: verum

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:29

.= [:(F " {y}),((id Z) " {z}):] by FUNCT_3:73

.= [:(F " {y}),{z}:] by FUNCT_2:94 ; :: thesis: verum