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

proof

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;

hence 0 <= SumBin (a,f,s) by RVSUM_1:84; :: thesis: verum