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)) )
set dr = (card Y) |-> r;
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 Th70;
then reconsider xf = FinS F,X, rd = (card Y) |-> r as Element of (card Y) -tuples_on REAL by FINSEQ_2:110;
FinS (F - r),X = (FinS F,X) - ((card Y) |-> r) by A1, Th76;
hence Sum (F - r),X = (Sum xf) - (Sum rd) by RVSUM_1:120
.= (Sum F,X) - (r * (card Y)) by RVSUM_1:110 ;
:: thesis: verum