let i be natural Number ; :: thesis: for D being non empty set
for f being sequence of D holds f | (Seg i) is FinSequence of D
let D be non empty set ; :: thesis: for f being sequence of D holds f | (Seg i) is FinSequence of D
reconsider i = i as Nat by TARSKI:1;
for f being sequence of D holds f | (Seg i) is FinSequence of D by Th23;
hence for f being sequence of D holds f | (Seg i) is FinSequence of D ; :: thesis: verum