let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT
for s, t being set st s misses t holds
SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t))
let f be FinSequence of NAT ; :: thesis: for s, t being set st s misses t holds
SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t))
let s, t be set ; :: thesis: ( s misses t implies SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t)) )
assume L08: s misses t ; :: thesis: SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t))
set U = f " s;
set V = f " t;
reconsider F = a as PartFunc of NAT,REAL ;
A200: dom (F | ((f " s) \/ (f " t))) is finite ;
A290: for W being set holds Sum (F,W) = Sum (Seq (a,W))

proof

let W be set ; :: thesis: Sum (F,W) = Sum (Seq (a,W))
dom (F | (W /\ W)) is finite ;
then A310: a | W, FinS (F,W) are_fiberwise_equipotent by RFUNCT_3:def 13;
reconsider fssu = a | W as Subset of a by RELAT_1:59;
A320: Seq fssu,fssu are_fiberwise_equipotent by DBLSEQ_2:51;
thus Sum (F,W) = Sum (FinS (F,W)) by RFUNCT_3:def 14
.= Sum (Seq (a,W)) by A310, A320, CLASSES1:76, RFINSEQ:9 ; :: thesis: verum

end;

A610: Sum (F,(f " s)) = SumBin (a,f,s) by A290;
A620: Sum (F,(f " t)) = SumBin (a,f,t) by A290;
Sum (F,((f " s) \/ (f " t))) = Sum (Seq (a,((f " s) \/ (f " t)))) by A290
.= SumBin (a,f,(s \/ t)) by RELAT_1:140 ;
hence SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t)) by A200, L08, FUNCT_1:71, RFUNCT_3:83, A610, A620; :: thesis: verum