let r be Real; :: thesis: for D, C being 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
( FinS (((Rlor (F,A)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,A)) - r),C) = Sum ((F - r),D) )
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
( FinS (((Rlor (F,A)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,A)) - r),C) = Sum ((F - r),D) )
let F be PartFunc of D,REAL; :: thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
( FinS (((Rlor (F,A)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,A)) - r),C) = Sum ((F - r),D) )
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies ( FinS (((Rlor (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),D) ) )
assume that
A1: F is total and
A2: card C = card D ; :: thesis: ( FinS (((Rlor (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),D) )
A3: dom F = D by A1, PARTFUN1:def 2;
then F | D = F by RELAT_1:68;
then A4: FinS (F,D),F are_fiberwise_equipotent by A3, RFUNCT_3:def 13;
Rlor (F,B), FinS (F,D) are_fiberwise_equipotent by A1, A2, Th24;
then Rlor (F,B),F are_fiberwise_equipotent by A4, CLASSES1:76;
then A5: (Rlor (F,B)) - r,F - r are_fiberwise_equipotent by RFUNCT_3:51;
A6: dom ((Rlor (F,B)) - r) = dom (Rlor (F,B)) by VALUED_1:3;
then ((Rlor (F,B)) - r) | C = (Rlor (F,B)) - r by RELAT_1:68;
then FinS (((Rlor (F,B)) - r),C),(Rlor (F,B)) - r are_fiberwise_equipotent by A6, RFUNCT_3:def 13;
then A7: FinS (((Rlor (F,B)) - r),C),F - r are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (F - r) = dom F by VALUED_1:3;
then (F - r) | D = F - r by RELAT_1:68;
hence FinS (((Rlor (F,B)) - r),C) = FinS ((F - r),D) by A8, A7, RFUNCT_3:def 13; :: thesis: Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),D)
hence Sum (((Rlor (F,B)) - r),C) = Sum (FinS ((F - r),D)) by RFUNCT_3:def 14
.= Sum ((F - r),D) by RFUNCT_3:def 14 ;
:: thesis: verum