let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL
for n being non zero 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 = (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 zero 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 = (p . i) * (f . (y /. i)) ) ) holds
not -infty in rng F
let n be non zero 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 = (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 = (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 = (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 = (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 = (p . i) * (f . (y /. i)) ) ; :: thesis: not -infty in rng F
for i being object st i in dom F holds
F . i <> -infty

proof

let i be object ; :: 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 = (p . i) * (f . (y /. i)) by A3, A5;

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

suppose 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 Element of REAL by A2, XXREAL_0:14;
F . i = (p . i) * w by A7, EXTREAL1:1;
hence F . i <> -infty ; :: thesis: verum

end;

suppose ( 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 3; :: thesis: verum