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