let p be FinSequence of x; :: thesis: p is FinSequence of D
rng p c= x by FINSEQ_1:def 4;
hence rng p c= D by XBOOLE_1:1; :: according to FINSEQ_1:def 4 :: thesis: verum