theorem :: POLNOT_2:7

for B being Polish-arity-function
for J being Polish-ext-set of B
for F being Formula of J st Polish-ext-head F in dom B holds
Polish-ext-head F = (dom B) -head F by Th10;