let C, D 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 Th24;
hence Sum ((Rlor (F,B)),C) = Sum (FinS (F,D)) by RFUNCT_3:def 14
.= Sum (F,D) by RFUNCT_3:def 14 ;
:: thesis: verum