theorem :: POLNOT_2:19

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for G being Formula of M st E . e = 1 holds
Polish-ext-head ((Polish-unOp (K,M,e)) . G) = e