let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL
for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let f be Function of the carrier of X,ExtREAL ; :: thesis: for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let n be non empty Element of NAT ; :: thesis: for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let p be FinSequence of REAL ; :: thesis: for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let F be FinSequence of ExtREAL ; :: thesis: for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let y be FinSequence of the carrier of X; :: thesis: ( len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies not -infty in rng F )
assume that
A1: len F = n and
A2: for x being VECTOR of X holds f . x <> -infty and
A3: for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; :: thesis: not -infty in rng F
for i being set st i in dom F holds
F . i <> -infty

proof

let i be set ; :: thesis: ( i in dom F implies F . i <> -infty )
assume A4: i in dom F ; :: thesis: F . i <> -infty
then reconsider i = i as Element of NAT ;
A5: i in Seg n by A1, A4, FINSEQ_1:def 3;
then A6: p . i >= 0 by A3;
A7: F . i = (R_EAL (p . i)) * (f . (y /. i)) by A3, A5;

per cases ( R_EAL (p . i) = 0. or f . (y /. i) <> +infty or ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ) ;

suppose R_EAL (p . i) = 0. ; :: thesis: F . i <> -infty

hence F . i <> -infty by A7; :: thesis: verum

end;

suppose f . (y /. i) <> +infty ; :: thesis: F . i <> -infty

then reconsider w = f . (y /. i) as Real by A2, XXREAL_0:14;
F . i = (p . i) * w by A7, EXTREAL1:13;
hence F . i <> -infty ; :: thesis: verum

end;

suppose ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ; :: thesis: F . i <> -infty

hence F . i <> -infty by A6, A7; :: thesis: verum

end;

end;

end;

hence not -infty in rng F by FUNCT_1:def 5; :: thesis: verum