consider f being non-empty Function of 0 ,REAL ;
take f ; :: thesis: ( f is non-empty & f is real-valued )
thus ( f is non-empty & f is real-valued ) ; :: thesis: verum