let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( x in {f,g} implies x is Function )
thus ( x in {f,g} implies x is Function ) by TARSKI:def 2; :: thesis: verum