F .: f,g in Funcs Z,X by FUNCT_2:11;
hence F .: f,g is Element of Funcs Z,X ; :: thesis: verum