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