dom (0 ,1 --> p,q) = {0 ,1} by FUNCT_4:65;
hence 0 ,1 --> p,q is ManySortedSet of {0 ,1} by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum