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