theorem Th48: :: FUNCT_4:48

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