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