let x be set ; :: according to VALUED_2:def 3 :: thesis: ( x in E_PFuncs X implies x is ext-real-valued Function )
thus ( x in E_PFuncs X implies x is ext-real-valued Function ) by Def10; :: thesis: verum