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

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