theorem Th24: :: MAZURULM:24

for E, F being RealNormSpace
for f being Function of E,F st f is isometric holds
f is_continuous_on dom f