let F be FinSequence of ExtREAL ; :: thesis:
let k be Nat; :: thesis:

hereby :: thesis:

assume A1: F is V251() ; :: thesis:

assume -infty in rng (F | k) ; :: thesis:
then consider i being Element of NAT such that
A2: ( i in dom (F | k) & -infty = (F | k) . i ) by PARTFUN1:3;
dom (F | k) c= dom F by RELAT_1:60;
then ( i in dom F & (F | k) . i = F . i ) by A2, FUNCT_1:47;
then -infty in rng F by A2, FUNCT_1:3;
hence contradiction by A1, MESFUNC5:def 3; :: thesis:

end;

hence F | k is V251() by MESFUNC5:def 3; :: thesis:

end;

assume A3: F is V252() ; :: thesis:

assume +infty in rng (F | k) ; :: thesis:
then consider i being Element of NAT such that
A4: ( i in dom (F | k) & +infty = (F | k) . i ) by PARTFUN1:3;
dom (F | k) c= dom F by RELAT_1:60;
then ( i in dom F & (F | k) . i = F . i ) by A4, FUNCT_1:47;
then +infty in rng F by A4, FUNCT_1:3;
hence contradiction by A3, MESFUNC5:def 4; :: thesis:

end;

hence F | k is V252() by MESFUNC5:def 4; :: thesis: