theorem Th15: :: EUCLID_7:16

for f being real-valued FinSequence st |.f.| = 1 holds
{f} is R-normal by TARSKI:def 1;