let X be set ; :: thesis: ( X is empty implies X is R-normal )
assume A1: X is empty ; :: thesis: X is R-normal
let f be real-valued FinSequence; :: according to EUCLID_7:def 4 :: thesis: ( f in X implies |.f.| = 1 )
thus ( f in X implies |.f.| = 1 ) by A1; :: thesis: verum