theorem :: POLNOT_2:20

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (K,M,e)) . (G,H)