set p = a .--> b;
A1: ( dom (a .--> b) = {a} & rng (a .--> b) = {b} ) by FUNCOP_1:14, FUNCOP_1:19;
thus a .--> b is PartFunc of X,Y by A1, RELSET_1:17; :: thesis: verum