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

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