theorem :: FCONT_1:40

for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in dom f holds
f . x0 = x0 ) holds
f is continuous