theorem REP2: :: NDIFF_8:32

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