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