let D be set ; :: thesis: for D1 being Subset of D
for p being FinSequence of D1 holds p is FinSequence of D
let D1 be Subset of D; :: thesis: for p being FinSequence of D1 holds p is FinSequence of D
let p be FinSequence of D1; :: thesis: p is FinSequence of D
rng p c= D1 by FINSEQ_1:def 4;
hence rng p c= D by XBOOLE_1:1; :: according to FINSEQ_1:def 4 :: thesis: verum