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 A2: j in dom (f | (Seg i)) ; :: thesis: (f | (Seg i)) . j in INT
then j in dom f by RELAT_1:86;
then A3: f . j in NAT by FINSEQ_2:13;
(f | (Seg i)) . j = f . j by A2, FUNCT_1:70;
hence (f | (Seg i)) . j in INT by A3, NUMBERS:17; :: thesis: verum

end;

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