rng
f
c=
D
by
RELAT_1:def 19
;
then
f
is
FinSequence
of
D
by
FINSEQ_1:def 4
;
hence
f
/^
n
is
D
-valued
;
:: thesis:
verum