dom f = (Polish-WFF-set (T,A)) ^^ (A . t) by FUNCT_2:def 1;
hence f . u is Polish-WFF of T,A by FUNCT_2:5; :: thesis: verum