theorem :: POLNOT_2:12

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