theorem Th79: :: POLNOT_1:79

for L being non trivial Polish-language
for E being Polish-arity-function of L
for t being Element of L
for F being Polish-WFF of L,E holds
( Polish-WFF-head F = t iff ex u being Element of (Polish-WFF-set (L,E)) ^^ (E . t) st F = (Polish-operation (L,E,t)) . u )