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:
then reconsider i = i as Element of NAT ;
A5: i in Seg n by ;
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 f . (y /. i) <> +infty ; :: thesis:
then reconsider w = f . (y /. i) as Element of REAL by ;
F . i = (p . i) * w by ;
hence F . i <> -infty ; :: thesis: verum
end;
suppose ( p . i <> 0. & f . (y /. i) = +infty ) ; :: thesis:
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