theorem Th65: :: POLNOT_1:70

for T being Polish-language
for A being Polish-arity-function of T
for t being Element of T
for u being FinSequence st u in (Polish-WFF-set (T,A)) ^^ (A . t) holds
T -tail ((Polish-operation (T,A,t)) . u) = u