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

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

hence
not -infty in rng F
by FUNCT_1:def 3; :: thesis: verum
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;

end;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 ) )
;

end;