theorem Th16: :: EUCLID_7:17

for B0 being set
for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds
B0 \/ {x0} is R-normal