let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
let F be PartFunc of D,REAL; :: thesis: for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
let X, Y be set ; :: thesis: ( dom (F | (X \/ Y)) is finite & X misses Y implies Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y)) )
assume ( dom (F | (X \/ Y)) is finite & X misses Y ) ; :: thesis: Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
hence Sum (F,(X \/ Y)) = Sum ((FinS (F,X)) ^ (FinS (F,Y))) by Th76, RFINSEQ:9
.= (Sum (F,X)) + (Sum (F,Y)) by RVSUM_1:75 ;
:: thesis: verum