deffunc H1( set ) -> Element of F1() = F2($1);
A1:
for f being set st f in F1() holds
H1(f) in F1()
;
ex o being Function of F1(),F1() st
for f being set st f in F1() holds
o . f = H1(f)
from FUNCT_2:sch 2(A1);
hence
ex o being UnOp of F1() st
for f being set st f in F1() holds
o . f = F2(f)
; verum