set B0 = {<*1*>};
thus for x, y being real-valued FinSequence st x in {<*1*>} & y in {<*1*>} & x <> y holds
|(x,y)| = 0 :: according to EUCLID_7:def 3,EUCLID_7:def 5 :: thesis: {<*1*>} is R-normal

proof

let x, y be real-valued FinSequence; :: thesis: ( x in {<*1*>} & y in {<*1*>} & x <> y implies |(x,y)| = 0 )
assume that
A1: x in {<*1*>} and
A2: y in {<*1*>} ; :: thesis: ( not x <> y or |(x,y)| = 0 )
x = <*1*> by A1, TARSKI:def 1;
hence ( not x <> y or |(x,y)| = 0 ) by A2, TARSKI:def 1; :: thesis: verum

end;

let x be real-valued FinSequence; :: according to EUCLID_7:def 4 :: thesis: ( x in {<*1*>} implies |.x.| = 1 )
assume x in {<*1*>} ; :: thesis: |.x.| = 1
then x = <*1*> by TARSKI:def 1;
then sqr x = <*(1 ^2)*> by RVSUM_1:55;
hence |.x.| = 1 by RVSUM_1:73, SQUARE_1:18; :: thesis: verum