let D be non empty set ; :: thesis: for F, G being PartFunc of D,REAL
for X being set st dom (F | X) is finite & dom (F | X) = dom (G | X) holds
Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))
let F, G be PartFunc of D,REAL; :: thesis: for X being set st dom (F | X) is finite & dom (F | X) = dom (G | X) holds
Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))
let X be set ; :: thesis: ( dom (F | X) is finite & dom (F | X) = dom (G | X) implies Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X)) )
assume A1: ( dom (F | X) is finite & dom (F | X) = dom (G | X) ) ; :: thesis: Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))
dom (((- 1) (#) G) | X) = (dom ((- 1) (#) G)) /\ X by RELAT_1:61
.= (dom G) /\ X by VALUED_1:def 5
.= dom (G | X) by RELAT_1:61 ;
hence Sum ((F - G),X) = (Sum (F,X)) + (Sum (((- 1) (#) G),X)) by A1, Th78
.= (Sum (F,X)) + ((- 1) * (Sum (G,X))) by A1, Th77
.= (Sum (F,X)) - (Sum (G,X)) ;
:: thesis: verum