theorem Th14: :: MAZURULM:14

for E, F being RealNormSpace
for f being Function of E,F st f is bijective & f is midpoints-preserving holds
f /" is midpoints-preserving