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