take f = the constant PartFunc of REAL,(REAL n); :: thesis: f is continuous
thus f is continuous ; :: thesis: verum