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 & dom (F | X) misses dom (F | 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 & dom (F | X) misses dom (F | Y) holds
Sum F,(X \/ Y) = (Sum F,X) + (Sum F,Y)
let X, Y be set ; :: thesis: ( dom (F | (X \/ Y)) is finite & dom (F | X) misses dom (F | Y) implies Sum F,(X \/ Y) = (Sum F,X) + (Sum F,Y) )
assume A1: ( dom (F | (X \/ Y)) is finite & dom (F | X) misses dom (F | Y) ) ; :: thesis: Sum F,(X \/ Y) = (Sum F,X) + (Sum F,Y)
A2: dom (F | (X \/ Y)) = (dom F) /\ (X \/ Y) by RELAT_1:90
.= ((dom F) /\ X) \/ ((dom F) /\ Y) by XBOOLE_1:23
.= (dom (F | X)) \/ ((dom F) /\ Y) by RELAT_1:90
.= (dom (F | X)) \/ (dom (F | Y)) by RELAT_1:90 ;
then ( dom (F | X) is finite & dom (F | Y) is finite ) by A1, FINSET_1:13, XBOOLE_1:7;
then A3: ( FinS F,(X \/ Y) = FinS F,(dom (F | (X \/ Y))) & FinS F,X = FinS F,(dom (F | X)) & FinS F,Y = FinS F,(dom (F | Y)) ) by A1, Th66;
dom (F | (dom (F | (X \/ Y)))) = (dom F) /\ (dom (F | (X \/ Y))) by RELAT_1:90
.= (dom F) /\ ((dom F) /\ (X \/ Y)) by RELAT_1:90
.= ((dom F) /\ (dom F)) /\ (X \/ Y) by XBOOLE_1:16
.= dom (F | (X \/ Y)) by RELAT_1:90 ;
hence Sum F,(X \/ Y) = Sum ((FinS F,X) ^ (FinS F,Y)) by A1, A2, A3, Th79, RFINSEQ:22
.= (Sum F,X) + (Sum F,Y) by RVSUM_1:105 ;
:: thesis: verum