let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set
for r being Real
for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
let F be PartFunc of D,REAL; :: thesis: for X being set
for r being Real
for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
let X be set ; :: thesis: for r being Real
for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
let r be Real; :: thesis: for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
set fx = FinS (F,X);
let Y be finite set ; :: thesis: ( Y = dom (F | X) implies Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y)) )
reconsider rr = r as Element of REAL by XREAL_0:def 1;
set dr = (card Y) |-> rr;
assume A1: Y = dom (F | X) ; :: thesis: Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
then len (FinS (F,X)) = card Y by Th67;
then reconsider xf = FinS (F,X), rd = (card Y) |-> rr as Element of (card Y) -tuples_on REAL by FINSEQ_2:92;
FinS ((F - r),X) = (FinS (F,X)) - ((card Y) |-> rr) by A1, Th73;
hence Sum ((F - r),X) = (Sum xf) - (Sum rd) by RVSUM_1:90
.= (Sum (F,X)) - (r * (card Y)) by RVSUM_1:80 ;
:: thesis: verum