:: deftheorem Defrep1 defines reproj1 NDIFF_7:def 1 :
for X, Y being RealNormSpace
for x being Element of [:X,Y:]
for b₄ being Function of X,[:X,Y:] holds
( b₄ = reproj1 x iff for r being Element of X holds b₄ . r = [r,(x `2)] );