let x be set ; :: according to GRCAT_1:def 25 :: 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:121; :: thesis: verum