set p = f | (Seg i);

now

let j be Nat; :: thesis: ( j in dom (f | (Seg i)) implies (f | (Seg i)) . j in INT )
assume A1: j in dom (f | (Seg i)) ; :: thesis: (f | (Seg i)) . j in INT
then j in dom f by RELAT_1:57;
then A2: f . j in NAT by FINSEQ_2:11;
(f | (Seg i)) . j = f . j by A1, FUNCT_1:47;
hence (f | (Seg i)) . j in INT by A2, NUMBERS:17; :: thesis: verum

end;

hence Prefix (f,i) is FinSequence of INT by FINSEQ_2:12; :: thesis: verum