set f = Polish-operation (T,A,(A . t),t);
u in (Polish-WFF-set (T,A)) ^^ (A . t) ;
then u in dom (Polish-operation (T,A,(A . t),t)) by FUNCT_2:def 1;
then (Polish-operation (T,A,(A . t),t)) . u = t ^ u by Def12;
hence T -head ((Polish-operation (T,A,(A . t),t)) . u) = t ; :: thesis: verum