theorem :: POLNOT_2:21

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 G, H being Formula of M st E . e = 2 holds
Polish-ext-head ((Polish-binOp (K,M,e)) . (G,H)) = e