let E, F be RealNormSpace; :: thesis: for s1, s2 being Point of [:E,F:] st s1 `1 = s2 `1 holds
reproj2 s1 = reproj2 s2
let s1, s2 be Point of [:E,F:]; :: thesis: ( s1 `1 = s2 `1 implies reproj2 s1 = reproj2 s2 )
assume A1: s1 `1 = s2 `1 ; :: thesis: reproj2 s1 = reproj2 s2
now :: thesis: for r being Element of F holds (reproj2 s1) . r = (reproj2 s2) . r
let r be Element of F; :: thesis: (reproj2 s1) . r = (reproj2 s2) . r
thus (reproj2 s1) . r = [(s2 `1),r] by A1, NDIFF_7:def 2
.= (reproj2 s2) . r by NDIFF_7:def 2 ; :: thesis: verum
end;
hence reproj2 s1 = reproj2 s2 by FUNCT_2:63; :: thesis: verum