let f be Function; :: thesis: {f} is functional
let g be set ; :: according to FRAENKEL:def 1 :: thesis: ( g in {f} implies g is Function )
thus ( g in {f} implies g is Function ) by TARSKI:def 1; :: thesis: verum