let X be RealLinearSpace; :: thesis:
let f be Function of the carrier of X, ExtREAL ; :: thesis:
let n be non empty Element of NAT ; :: thesis:
let p be FinSequence of REAL ; :: thesis:
let F be FinSequence of ExtREAL ; :: thesis:
let y be FinSequence of the carrier of X; :: thesis:
assume that
A1: ( len p = n & len F = n & len y = 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:
for i being set st i in dom F holds
F . i <> -infty

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

per cases ;

suppose R_EAL (p . i) = 0. ; :: thesis:

hence F . i <> -infty by A5, EXTREAL1:def 1; :: thesis:

end;

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

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

end;

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

then 0. < R_EAL (p . i) by A5, MEASURE6:def 1;
hence F . i <> -infty by A5, A6, EXTREAL1:def 1; :: thesis:

end;

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