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