theorem Th32: :: NDIFF_4:32

for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1) st J = proj (1,1) holds
J is_continuous_in x0