let a be Element of (REAL-L n); :: thesis: a is real-valued
reconsider a = a as Element of REAL n ;
a is FinSequence of REAL ;
hence a is real-valued ; :: thesis: verum