let F be FinSequence of ExtREAL ; :: thesis: for k being Nat holds
( ( F is V251() implies F | k is V251() ) & ( F is V252() implies F | k is V252() ) )
let k be Nat; :: thesis: ( ( F is V251() implies F | k is V251() ) & ( F is V252() implies F | k is V252() ) )

hereby :: thesis: ( F is V252() implies F | k is V252() )

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

now :: thesis: not -infty in rng (F | k)

assume -infty in rng (F | k) ; :: thesis: contradiction
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: verum

end;

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

end;

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

now :: thesis: not +infty in rng (F | k)

assume +infty in rng (F | k) ; :: thesis: contradiction
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: verum

end;

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