theorem Th1: :: POLNOT_2:1
for T being Polish-language
for B being Polish-arity-function holds
( B is Polish-arity-function of T iff T = dom B )