theorem Th81: :: POLNOT_1:81

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 holds
( Polish-WFF-head ((Polish-unOp (L,E,t)) . F) = t & Polish-WFF-args ((Polish-unOp (L,E,t)) . F) = <*F*> )