let a be Element of (RealVectSpace A); :: thesis: a is real-valued
( a is Function of A,REAL or a is empty ) by FUNCT_2:66;
hence a is real-valued ; :: thesis: verum