let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT
for s being set st s misses rng f holds
SumBin (a,f,s) = 0
let f be FinSequence of NAT ; :: thesis: for s being set st s misses rng f holds
SumBin (a,f,s) = 0
let s be set ; :: thesis: ( s misses rng f implies SumBin (a,f,s) = 0 )
assume L033: s misses rng f ; :: thesis: SumBin (a,f,s) = 0
reconsider emptyrealseq = <*> REAL as FinSequence of REAL ;
Seq (a,{}) = Seq (a | {})
.= emptyrealseq ;
hence SumBin (a,f,s) = 0 by L033, RELAT_1:138, RVSUM_1:72; :: thesis: verum