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: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 by A1, FINSET_1:13, XBOOLE_1:7;
then A4: FinS F,X = FinS F,(dom (F | X)) by Th66;
dom (F | Y) is finite by A1, A3, FINSET_1:13, XBOOLE_1:7;
then A5: FinS F,Y = FinS F,(dom (F | Y)) by Th66;
A6: 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 ;
FinS F,(X \/ Y) = FinS F,(dom (F | (X \/ Y))) by A1, Th66;
hence Sum F,(X \/ Y) = Sum ((FinS F,X) ^ (FinS F,Y)) by A1, A2, A3, A4, A5, A6, Th79, RFINSEQ:22
.= (Sum F,X) + (Sum F,Y) by RVSUM_1:105 ;
:: thesis: verum