consider f being Function;
take {f} ; :: thesis: ( not {f} is empty & {f} is functional )
thus not {f} is empty ; :: 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