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