theorem :: FUNCT_4:50

for X, Y, Z being set
for f being Function of [:X,Y:],Z holds ~ f is Function of [:Y,X:],Z ;