:: deftheorem defines Rland REARRAN1:def 5 :
for D, C being non empty finite set
for A being RearrangmentGen of C
for F being PartFunc of D,REAL holds Rland (F,A) = Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));