F [;] a,f in Funcs Z,X by FUNCT_2:11;
hence F [;] a,f is Element of Funcs Z,X ; :: thesis: verum