theorem :: REARRAN1:38

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 D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r