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

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