set U = Polish-ext-domain Q;
Q = Polish-WFF-set ((Polish-ext-domain Q),(Polish-ext-arity Q)) by Def23;
then Q is Polish-ext-domain Q -headed by POLNOT_1:65;
then F is Polish-ext-domain Q -headed ;
hence (Polish-ext-domain Q) -head F is Element of Polish-ext-domain Q by POLNOT_1:def 22; :: thesis: verum