let a be non empty FinSequence of REAL ; 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 ; for s being set st s misses rng f holds
SumBin (a,f,s) = 0
let s be set ; ( s misses rng f implies SumBin (a,f,s) = 0 )
assume L033:
s misses rng f
; 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; verum