theorem :: NDIFF_8:31

for E, F being RealNormSpace
for s1, s2 being Point of [:E,F:] st s1 `2 = s2 `2 holds
reproj1 s1 = reproj1 s2