theorem Th8: :: LOPBAN14:7

for X being RealLinearSpace
for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPRLSP X