let X, Y, Z be non empty set ; 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; 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; for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let B be Subset of Z; [: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
; verum