let D be set ; :: thesis: for D' being FinSequence-DOMAIN of D holds D' c= D *
let D' be FinSequence-DOMAIN of D; :: thesis: D' c= D *
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in D' or a in D * )
assume a in D' ; :: thesis: a in D *
then a is FinSequence of D by Def3;
hence a in D * by FINSEQ_1:def 11; :: thesis: verum