let a be Element of (RealVectSpace (Seg n)); :: according to MONOID_0:def 2 :: thesis: a is set
a is Element of REAL n by FINSEQ_2:93;
hence a is set ; :: thesis: verum