let p be FinSequence; :: thesis: p is FinSubsequence
dom p = Seg (len p) by Def3;
hence p is FinSubsequence by Def12; :: thesis: verum