consider f being V8() PartFunc of REAL ,REAL ;
take f ; :: thesis: f is continuous
thus f is continuous ; :: thesis: verum