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