set g = f | (Seg n);
A1: dom f = NAT by FUNCT_2:def 1;
dom (f | (Seg n)) = Seg n by A1, RELAT_1:62;
then A2: f | (Seg n) is FinSequence by FINSEQ_1:def 2;
rng (f | (Seg n)) c= REAL ;
hence f | (Seg n) is FinSequence of REAL by A2, FINSEQ_1:def 4; :: thesis: verum