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 ((Rland F,A) - r),C = FinS (F - r),D & Sum ((Rland 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 ((Rland F,A) - r),C = FinS (F - r),D & Sum ((Rland 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 ((Rland F,A) - r),C = FinS (F - r),D & Sum ((Rland F,A) - r),C = Sum (F - r),D )
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies ( FinS ((Rland F,B) - r),C = FinS (F - r),D & Sum ((Rland F,B) - r),C = Sum (F - r),D ) )
assume that
A1: F is total and
A2: card C = card D ; :: thesis: ( FinS ((Rland F,B) - r),C = FinS (F - r),D & Sum ((Rland F,B) - r),C = Sum (F - r),D )
A3: dom F = D by A1, PARTFUN1:def 4;
then F | D = F by RELAT_1:97;
then A4: FinS F,D,F are_fiberwise_equipotent by A3, RFUNCT_3:def 14;
Rland F,B, FinS F,D are_fiberwise_equipotent by A1, A2, Th17;
then Rland F,B,F are_fiberwise_equipotent by A4, CLASSES1:84;
then A5: (Rland F,B) - r,F - r are_fiberwise_equipotent by RFUNCT_3:54;
A6: dom ((Rland F,B) - r) = dom (Rland F,B) by VALUED_1:3;
then ((Rland F,B) - r) | C = (Rland F,B) - r by RELAT_1:97;
then FinS ((Rland F,B) - r),C,(Rland F,B) - r are_fiberwise_equipotent by A6, RFUNCT_3:def 14;
then A7: FinS ((Rland F,B) - r),C,F - r are_fiberwise_equipotent by A5, CLASSES1:84;
A8: dom (F - r) = dom F by VALUED_1:3;
then (F - r) | D = F - r by RELAT_1:97;
hence FinS ((Rland F,B) - r),C = FinS (F - r),D by A8, A7, RFUNCT_3:def 14; :: thesis: Sum ((Rland F,B) - r),C = Sum (F - r),D
hence Sum ((Rland 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