let D, C be non empty finite set ; :: thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Sum (Rlor F,A),C = Sum F,D
let F be PartFunc of D,REAL ; :: thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Sum (Rlor F,A),C = Sum F,D
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies Sum (Rlor F,B),C = Sum F,D )
assume ( F is total & card C = card D ) ; :: thesis: Sum (Rlor F,B),C = Sum F,D
then FinS (Rlor F,B),C = FinS F,D by Th25;
hence Sum (Rlor F,B),C = Sum (FinS F,D) by RFUNCT_3:def 15
.= Sum F,D by RFUNCT_3:def 15 ;
:: thesis: verum