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:32;
hence f | (Seg i) is FinSequence of D by Th28; :: thesis: verum