rng <*f*> c= D *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng <*f*> or y in D * )
assume y in rng <*f*> ; :: thesis: y in D *
then y in {f} by FINSEQ_1:39;
then y = f by TARSKI:def 1;
hence y in D * by FINSEQ_1:def 11; :: thesis: verum

end;

hence <*f*> is FinSequence of D * by FINSEQ_1:def 4; :: thesis: verum