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 (Rland 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 (Rland F,A),C = Sum F,D
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies Sum (Rland F,B),C = Sum F,D )
assume ( F is total & card C = card D ) ; :: thesis: Sum (Rland F,B),C = Sum F,D
then FinS (Rland F,B),C = FinS F,D by Th18;
hence Sum (Rland F,B),C = Sum (FinS F,D) by RFUNCT_3:def 15
.= Sum F,D by RFUNCT_3:def 15 ;
:: thesis: verum