set V = Polish-expression-set (T,A);
set n = A . t;
set f = Polish-operation (T,A,(A . t),t);
A1:
dom (Polish-operation (T,A,(A . t),t)) = (Polish-expression-set (T,A)) ^^ (A . t)
by FUNCT_2:def 1;
for a being object st a in (Polish-expression-set (T,A)) ^^ (A . t) holds
(Polish-operation (T,A,(A . t),t)) . a in Polish-expression-set (T,A)
by TH39;
hence
Polish-operation (T,A,(A . t),t) is Function of ((Polish-WFF-set (T,A)) ^^ (A . t)),(Polish-WFF-set (T,A))
by A1, FUNCT_2:3; verum