let a be non empty positive FinSequence of REAL ; :: thesis: for f being FinSequence of NAT

for s being set holds 0 <= SumBin (a,f,s)

let f be FinSequence of NAT ; :: thesis: for s being set holds 0 <= SumBin (a,f,s)

let s be set ; :: thesis: 0 <= SumBin (a,f,s)

reconsider seqaxs = Seq (a,(f " s)) as real-valued FinSequence ;

for i being Nat st i in dom seqaxs holds

0 <= seqaxs . i

for s being set holds 0 <= SumBin (a,f,s)

let f be FinSequence of NAT ; :: thesis: for s being set holds 0 <= SumBin (a,f,s)

let s be set ; :: thesis: 0 <= SumBin (a,f,s)

reconsider seqaxs = Seq (a,(f " s)) as real-valued FinSequence ;

for i being Nat st i in dom seqaxs holds

0 <= seqaxs . i

proof

hence
0 <= SumBin (a,f,s)
by RVSUM_1:84; :: thesis: verum
let i be Nat; :: thesis: ( i in dom seqaxs implies 0 <= seqaxs . i )

assume i in dom seqaxs ; :: thesis: 0 <= seqaxs . i

then L300: seqaxs . i in rng seqaxs by FUNCT_1:3;

L400: rng seqaxs = rng (Seq (a | (f " s)))

.= rng (a | (f " s)) by FINSEQ_1:101 ;

rng (a | (f " s)) c= rng a by RELAT_1:70;

hence 0 <= seqaxs . i by L300, L400, PARTFUN3:def 1; :: thesis: verum

end;assume i in dom seqaxs ; :: thesis: 0 <= seqaxs . i

then L300: seqaxs . i in rng seqaxs by FUNCT_1:3;

L400: rng seqaxs = rng (Seq (a | (f " s)))

.= rng (a | (f " s)) by FINSEQ_1:101 ;

rng (a | (f " s)) c= rng a by RELAT_1:70;

hence 0 <= seqaxs . i by L300, L400, PARTFUN3:def 1; :: thesis: verum