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