let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT st dom f = dom a holds

SumBin (a,f,(rng f)) = Sum a

let f be FinSequence of NAT ; :: thesis: ( dom f = dom a implies SumBin (a,f,(rng f)) = Sum a )

assume L00: dom f = dom a ; :: thesis: SumBin (a,f,(rng f)) = Sum a

L200: f " (rng f) = dom f by RELAT_1:134;

Seq (a,(f " (rng f))) = Seq (a | (dom a)) by L200, L00

.= a by FINSEQ_3:116 ;

hence SumBin (a,f,(rng f)) = Sum a ; :: thesis: verum

SumBin (a,f,(rng f)) = Sum a

let f be FinSequence of NAT ; :: thesis: ( dom f = dom a implies SumBin (a,f,(rng f)) = Sum a )

assume L00: dom f = dom a ; :: thesis: SumBin (a,f,(rng f)) = Sum a

L200: f " (rng f) = dom f by RELAT_1:134;

Seq (a,(f " (rng f))) = Seq (a | (dom a)) by L200, L00

.= a by FINSEQ_3:116 ;

hence SumBin (a,f,(rng f)) = Sum a ; :: thesis: verum