set T = dom B;
reconsider A = B as Polish-arity-function of dom B by Th1;
take Polish-WFF-set ((dom B),A) ; :: thesis: ( Polish-WFF-set ((dom B),A) is B -closed & Polish-WFF-set ((dom B),A) is B -compatible )
thus ( Polish-WFF-set ((dom B),A) is B -closed & Polish-WFF-set ((dom B),A) is B -compatible ) ; :: thesis: verum