for T being Polish-language
for A being Polish-arity-function of T
for D being non empty set
for f being Polish-recursion-function of A,D
for K1, K2 being Function of (Polish-WFF-set (T,A)),D st K1 is f -recursive & K2 is f -recursive holds
K1 = K2