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+ ((Rlor (F,A)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,A)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (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+ ((Rlor (F,A)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,A)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (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+ ((Rlor (F,A)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,A)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (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+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) ) )
assume that
A1: F is total and
A2: card C = card D ; :: thesis: ( max+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
set mp = max+ ((Rlor (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;
Rlor (F,B), FinS (F,D) are_fiberwise_equipotent by A1, A2, Th24;
then Rlor (F,B),F are_fiberwise_equipotent by A4, CLASSES1:84;
then (Rlor (F,B)) - r,F - r are_fiberwise_equipotent by RFUNCT_3:54;
hence A5: max+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent by RFUNCT_3:44; :: thesis: ( FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
A6: dom (max+ ((Rlor (F,B)) - r)) = dom ((Rlor (F,B)) - r) by RFUNCT_3:def 10;
then (max+ ((Rlor (F,B)) - r)) | C = max+ ((Rlor (F,B)) - r) by RELAT_1:97;
then FinS ((max+ ((Rlor (F,B)) - r)),C), max+ ((Rlor (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def 14;
then A7: FinS ((max+ ((Rlor (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 10;
then (max+ (F - r)) | D = max+ (F - r) by RELAT_1:97;
hence FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) by A8, A7, RFUNCT_3:def 14; :: thesis: Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D)
hence Sum ((max+ ((Rlor (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