let E, F be RealNormSpace; :: thesis: for s1, s2 being Point of [:E,F:] st s1 `2 = s2 `2 holds
reproj1 s1 = reproj1 s2
let s1, s2 be Point of [:E,F:]; :: thesis: ( s1 `2 = s2 `2 implies reproj1 s1 = reproj1 s2 )
assume A1: s1 `2 = s2 `2 ; :: thesis: reproj1 s1 = reproj1 s2

now :: thesis: for r being Element of E holds (reproj1 s1) . r = (reproj1 s2) . r

let r be Element of E; :: thesis: (reproj1 s1) . r = (reproj1 s2) . r
thus (reproj1 s1) . r = [r,(s2 `2)] by A1, NDIFF_7:def 1
.= (reproj1 s2) . r by NDIFF_7:def 1 ; :: thesis: verum

end;

hence reproj1 s1 = reproj1 s2 by FUNCT_2:63; :: thesis: verum