theorem :: REARRAN1:27

for r being Real
for C, D being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
( FinS (((Rlor (F,A)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,A)) - r),C) = Sum ((F - r),D) )