let X, Y, Z be set ; :: thesis: for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z
let f be PartFunc of [:X,Y:],Z; :: thesis: ~ f is PartFunc of [:Y,X:],Z
A1: dom f c= [:X,Y:] ;
then A2: dom (~ f) c= [:Y,X:] by Th45;
rng f c= Z ;
then rng (~ f) c= Z by A1, Th47;
hence ~ f is PartFunc of [:Y,X:],Z by A2, RELSET_1:4; :: thesis: verum