dom (Polish-arity V) = T by FUNCT_2:def 1;
hence Polish-ext-domain ((Polish-arity V),Q) is T -extending Polish-language ; :: thesis: verum