let a be Element of (REAL-US n); :: thesis: a is real-valued
reconsider a = a as Element of REAL n by REAL_NS1:def 6;
a is FinSequence of REAL ;
hence a is real-valued ; :: thesis: verum