let f be FinSequence of D; :: thesis: f is D -valued
thus rng f c= D by Def4; :: according to RELAT_1:def 19 :: thesis: verum