theorem :: POLNOT_1:82

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