let x be set ; :: according to GRCAT_1:def 20 :: thesis: ( x in Funcs ( the carrier of G, the carrier of H) implies x is Function of G,H )
assume x in Funcs ( the carrier of G, the carrier of H) ; :: thesis: x is Function of G,H
hence x is Function of G,H by FUNCT_2:66; :: thesis: verum