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