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