for L being non trivial Polish-language
for E being Polish-arity-function of L
for t being Element of L
for a being object st a in dom (Polish-operation (L,E,t)) holds
ex p being FinSequence st
( p = (Polish-operation (L,E,t)) . a & L -head p = t )