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 A1: ( F is total & 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 )
then A2: Rlor F,B, FinS F,D are_fiberwise_equipotent by Th24;
A3: ( dom (Rlor F,B) = C & dom F = D ) by A1, Th21, PARTFUN1:def 4;
then ( (Rlor F,B) | C = Rlor F,B & F | D = F ) by RELAT_1:97;
then FinS F,D,F are_fiberwise_equipotent by A3, RFUNCT_3:def 14;
then Rlor F,B,F are_fiberwise_equipotent by A2, CLASSES1:84;
then A4: (Rlor F,B) - r,F - r are_fiberwise_equipotent by RFUNCT_3:54;
A5: ( dom ((Rlor F,B) - r) = dom (Rlor F,B) & dom (F - r) = dom F ) by VALUED_1:3;
then A6: ( ((Rlor F,B) - r) | C = (Rlor F,B) - r & (F - r) | D = F - r ) by RELAT_1:97;
then FinS ((Rlor F,B) - r),C,(Rlor F,B) - r are_fiberwise_equipotent by A5, RFUNCT_3:def 14;
then FinS ((Rlor F,B) - r),C,F - r are_fiberwise_equipotent by A4, CLASSES1:84;
hence FinS ((Rlor F,B) - r),C = FinS (F - r),D by A5, A6, RFUNCT_3:def 14; :: 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 15
.= Sum (F - r),D by RFUNCT_3:def 15 ;
:: thesis: verum