theorem Th33: :: LOPBAN14:32

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>