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