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 that
A1: dom (F | (X \/ Y)) is finite and
A2: dom (F | X) misses dom (F | Y) ; :: thesis: Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
A3: dom (F | (X \/ Y)) = (dom F) /\ (X \/ Y) by RELAT_1:61
.= ((dom F) /\ X) \/ ((dom F) /\ Y) by XBOOLE_1:23
.= (dom (F | X)) \/ ((dom F) /\ Y) by RELAT_1:61
.= (dom (F | X)) \/ (dom (F | Y)) by RELAT_1:61 ;
then dom (F | X) is finite by A1, FINSET_1:1, XBOOLE_1:7;
then A4: FinS (F,X) = FinS (F,(dom (F | X))) by Th63;
dom (F | Y) is finite by A1, A3, FINSET_1:1, XBOOLE_1:7;
then A5: FinS (F,Y) = FinS (F,(dom (F | Y))) by Th63;
A6: dom (F | (dom (F | (X \/ Y)))) = (dom F) /\ (dom (F | (X \/ Y))) by RELAT_1:61
.= (dom F) /\ ((dom F) /\ (X \/ Y)) by RELAT_1:61
.= ((dom F) /\ (dom F)) /\ (X \/ Y) by XBOOLE_1:16
.= dom (F | (X \/ Y)) by RELAT_1:61 ;
FinS (F,(X \/ Y)) = FinS (F,(dom (F | (X \/ Y)))) by A1, Th63;
hence Sum (F,(X \/ Y)) = Sum ((FinS (F,X)) ^ (FinS (F,Y))) by A1, A2, A3, A4, A5, A6, Th76, RFINSEQ:9
.= (Sum (F,X)) + (Sum (F,Y)) by RVSUM_1:75 ;
:: thesis: verum