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