let q be FinSubsequence; :: thesis: q is finite
ex n being Nat st dom q c= Seg n by Def12;
hence q is finite by FINSET_1:10; :: thesis: verum