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