theorem :: EQREL_1:59

for X, Y, Z being 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:]