let A be set ; :: thesis: ( A is empty implies A is functional )
assume A1: A is empty ; :: thesis: A is functional
let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( x in A implies x is Function )
thus ( x in A implies x is Function ) by A1; :: thesis: verum