theorem :: POLNOT_2:10

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for G being Formula of M st C . e = 1 holds
Polish-ext-head ((Polish-unOp (C,M,e)) . G) = e