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