let i be Nat; :: thesis: for D being non empty set
for f being Function of NAT ,D holds f | (Seg i) is FinSequence of D
let D be non empty set ; :: thesis: for f being Function of NAT ,D holds f | (Seg i) is FinSequence of D
let f be Function of NAT ,D; :: thesis: f | (Seg i) is FinSequence of D
f | (Seg i) is Function of (Seg i),D by FUNCT_2:38;
hence f | (Seg i) is FinSequence of D by Th28; :: thesis: verum