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

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