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