theorem :: POLNOT_1:80

for L being non trivial Polish-language
for E being Polish-arity-function of L
for t being Element of L st E . t = 1 holds
for F being Polish-WFF of L,E st Polish-WFF-head F = t holds
ex G being Polish-WFF of L,E st F = (Polish-unOp (L,E,t)) . G