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

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