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