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:90
.= (dom G) /\ X by VALUED_1:def 5
.= dom (G | X) by RELAT_1:90 ;
hence Sum (F - G),X = (Sum F,X) + (Sum ((- 1) (#) G),X) by A1, Th81
.= (Sum F,X) + ((- 1) * (Sum G,X)) by A1, Th80
.= (Sum F,X) - (Sum G,X) ;
:: thesis: verum