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 Th79, RFINSEQ:22
.= (Sum F,X) + (Sum F,Y) by RVSUM_1:105 ;
:: thesis: verum