let a be Element of (REAL-L n); :: according to MONOID_0:def 2 :: thesis: a is set
reconsider a = a as Element of REAL n ;
a is FinSequence of REAL ;
hence a is set ; :: thesis: verum