len <%p,q%> = {0,1} by AFINSQ_1:38, CARD_1:50;
hence <%p,q%> is total by PARTFUN1:def 2; :: thesis: verum