theorem :: FUNCT_3:72

for A, B being set
for f, g being Function holds [:f,g:] .: [:B,A:] = [:(f .: B),(g .: A):]