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; :: thesis: verum