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))

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

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

A610:
Sum (F,(f " s)) = SumBin (a,f,s)
by A290;
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;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

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