:: deftheorem Def11 defines E_Funcs VALUED_2:def 11 :
for D, b₂ being set holds
( b₂ = E_Funcs D iff for f being object holds
( f in b₂ iff f is Function of D,ExtREAL ) );