theorem :: POLNOT_2:11

for B being Polish-arity-function
for C being Extension of B
for e being Element of dom C
for M being Polish-ext-set of C
for F being Formula of M st C . e = 2 & Polish-ext-head F = e holds
ex G, H being Formula of M st F = (Polish-binOp (C,M,e)) . (G,H)