:: deftheorem Def3 defines proj NDIFF_5:def 3 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for b₃ being Function of (product G),(G . i) holds
( b₃ = proj i iff for x being Element of product (carr G) holds b₃ . x = x . i );