theorem LM8: :: DUALSP04:22

for X being RealUnitarySpace
for u being linear-Functional of X
for v being linear-Functional of (RUSp2RNSp X) st u = v holds
PreNorms u = PreNorms v