theorem Th32: :: LOPBAN14:31

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 i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>