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
( max- ((Rland F,A) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,A) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,A) - r)),C = Sum (max- (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
( max- ((Rland F,A) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,A) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,A) - r)),C = Sum (max- (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
( max- ((Rland F,A) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,A) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,A) - r)),C = Sum (max- (F - r)),D )
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies ( max- ((Rland F,B) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,B) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,B) - r)),C = Sum (max- (F - r)),D ) )
assume that
A1: F is total and
A2: card C = card D ; :: thesis: ( max- ((Rland F,B) - r), max- (F - r) are_fiberwise_equipotent & FinS (max- ((Rland F,B) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,B) - r)),C = Sum (max- (F - r)),D )
set mp = max- ((Rland F,B) - r);
set mf = max- (F - r);
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 (Rland F,B) - r,F - r are_fiberwise_equipotent by RFUNCT_3:54;
hence A5: max- ((Rland F,B) - r), max- (F - r) are_fiberwise_equipotent by RFUNCT_3:45; :: thesis: ( FinS (max- ((Rland F,B) - r)),C = FinS (max- (F - r)),D & Sum (max- ((Rland F,B) - r)),C = Sum (max- (F - r)),D )
A6: dom (max- ((Rland F,B) - r)) = dom ((Rland F,B) - r) by RFUNCT_3:def 11;
then (max- ((Rland F,B) - r)) | C = max- ((Rland F,B) - r) by RELAT_1:97;
then FinS (max- ((Rland F,B) - r)),C, max- ((Rland F,B) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def 14;
then A7: FinS (max- ((Rland F,B) - r)),C, max- (F - r) are_fiberwise_equipotent by A5, CLASSES1:84;
A8: dom (max- (F - r)) = dom (F - r) by RFUNCT_3:def 11;
then (max- (F - r)) | D = max- (F - r) by RELAT_1:97;
hence FinS (max- ((Rland F,B) - r)),C = FinS (max- (F - r)),D by A8, A7, RFUNCT_3:def 14; :: thesis: Sum (max- ((Rland F,B) - r)),C = Sum (max- (F - r)),D
hence Sum (max- ((Rland F,B) - r)),C = Sum (FinS (max- (F - r)),D) by RFUNCT_3:def 15
.= Sum (max- (F - r)),D by RFUNCT_3:def 15 ;
:: thesis: verum