let f be real-valued FinSequence; :: thesis: ( |.f.| = 1 implies {f} is R-normal )
assume A1: |.f.| = 1 ; :: thesis: {f} is R-normal
let x be real-valued FinSequence; :: according to EUCLID_7:def 4 :: thesis: ( x in {f} implies |.x.| = 1 )
assume x in {f} ; :: thesis: |.x.| = 1
hence |.x.| = 1 by A1, TARSKI:def 1; :: thesis: verum