theorem Th83: :: POLNOT_1:83

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, G being Polish-WFF of L,E holds
( Polish-WFF-head ((Polish-binOp (L,E,t)) . (F,G)) = t & Polish-WFF-args ((Polish-binOp (L,E,t)) . (F,G)) = <*F,G*> )