let X be set ; :: thesis: ( X is ext-real-functions-membered implies X is functional )

assume A2: X is ext-real-functions-membered ; :: thesis: X is functional

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in X or x is set )

thus ( not x in X or x is set ) by A2; :: thesis: verum

assume A2: X is ext-real-functions-membered ; :: thesis: X is functional

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in X or x is set )

thus ( not x in X or x is set ) by A2; :: thesis: verum