set p = a .--> b;
( dom (a .--> b) = {a} & rng (a .--> b) = {b} ) by FUNCOP_1:8;
then ( dom (a .--> b) c= X & rng (a .--> b) c= Y ) ;
hence a .--> b is PartFunc of X,Y by RELSET_1:4; :: thesis: verum