a . i in rng a by FUNCT_1:3;
then a . i in REAL ;
hence a . i is Element of REAL ; :: thesis: verum