let D be non empty set ; :: thesis: for D9 being Subset of D
for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
let D9 be Subset of D; :: thesis: for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
let S be FinSequenceSet of D9; :: thesis: S is FinSequenceSet of D
S is FinSequenceSet of D

proof

let a be object ; :: 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 D9 by Def3;
rng p c= D9 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 FinSequenceSet of D ; :: thesis: verum