let X, Y, Z be non empty set ; :: thesis: for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let F be Function of X,Y; :: thesis: for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let A be Subset of X; :: thesis: for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let B be Subset of Z; :: thesis: [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
thus [:F,(id Z):] .: [:A,B:] = [:(F .: A),((id Z) .: B):] by FUNCT_3:72
.= [:(F .: A),B:] by FUNCT_1:92 ; :: thesis: verum