let D be non empty set ; :: thesis: for D' being non empty Subset of D
for S being FinSequence-DOMAIN of D' holds S is FinSequence-DOMAIN of D
let D' be non empty Subset of D; :: thesis: for S being FinSequence-DOMAIN of D' holds S is FinSequence-DOMAIN of D
let S be FinSequence-DOMAIN of D'; :: thesis: S is FinSequence-DOMAIN of D
S is FinSequenceSet of D

proof

let a be set ; :: according to FINSEQ_2:def 3 :: thesis: ( a in S implies a is FinSequence of D )
assume a in S ; :: thesis: a is FinSequence of D
then reconsider p = a as FinSequence of D' by Def3;
( rng p c= D' & D' c= D ) by FINSEQ_1:def 4;
then rng p c= D by XBOOLE_1:1;
hence a is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

end;

hence S is FinSequence-DOMAIN of D ; :: thesis: verum