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 A1: ( F is total & 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 )
then A2: Rland F,B, FinS F,D are_fiberwise_equipotent by Th17;
A3: ( dom (Rland F,B) = C & dom F = D ) by A1, Th13, PARTFUN1:def 4;
then ( (Rland F,B) | C = Rland F,B & F | D = F ) by RELAT_1:97;
then FinS F,D,F are_fiberwise_equipotent by A3, RFUNCT_3:def 14;
then Rland F,B,F are_fiberwise_equipotent by A2, CLASSES1:84;
then A4: (Rland F,B) - r,F - r are_fiberwise_equipotent by RFUNCT_3:54;
set mp = max+ ((Rland F,B) - r);
set mf = max+ (F - r);
A5: ( dom (max+ ((Rland F,B) - r)) = dom ((Rland F,B) - r) & dom (max+ (F - r)) = dom (F - r) ) by RFUNCT_3:def 10;
thus A6: max+ ((Rland F,B) - r), max+ (F - r) are_fiberwise_equipotent by A4, RFUNCT_3:44; :: 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 )
A7: ( (max+ ((Rland F,B) - r)) | C = max+ ((Rland F,B) - r) & (max+ (F - r)) | D = max+ (F - r) ) by A5, RELAT_1:97;
then FinS (max+ ((Rland F,B) - r)),C, max+ ((Rland F,B) - r) are_fiberwise_equipotent by A5, RFUNCT_3:def 14;
then FinS (max+ ((Rland F,B) - r)),C, max+ (F - r) are_fiberwise_equipotent by A6, CLASSES1:84;
hence FinS (max+ ((Rland F,B) - r)),C = FinS (max+ (F - r)),D by A5, 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