theorem :: REARRAN1:29

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
( max+ ((Rland (F,A)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rland (F,A)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rland (F,A)) - r)),C) = Sum ((max+ (F - r)),D) )