set T = dom B;
reconsider A = B as Polish-arity-function of dom B by Th1;
take Polish-WFF-set ((dom B),A) ; :: thesis: ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & Polish-WFF-set ((dom B),A) = Polish-WFF-set (T,A) )
thus ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & Polish-WFF-set ((dom B),A) = Polish-WFF-set (T,A) ) ; :: thesis: verum