set W = Polish-WFF-set (L,E);
consider H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) such that
A1: H is Subst s -recursive by Th75;
take G = H . F; :: thesis: ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st
( H is Subst s -recursive & G = H . F )
take H ; :: thesis: ( H is Subst s -recursive & G = H . F )
thus ( H is Subst s -recursive & G = H . F ) by A1; :: thesis: verum