theorem :: FCONT_1:43

for X being set
for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being Real st x0 in X holds
f . x0 = x0 ^2 ) holds
f | X is continuous