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