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 A1: ( F is total & 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 )
then A2: Rlor F,B, FinS F,D are_fiberwise_equipotent by Th24;
A3: ( C is finite & 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;
set mp = max- ((Rlor F,B) - r);
set mf = max- (F - r);
A5: ( dom (max- ((Rlor F,B) - r)) = dom ((Rlor F,B) - r) & dom (max- (F - r)) = dom (F - r) ) by RFUNCT_3:def 11;
thus A6: max- ((Rlor F,B) - r), max- (F - r) are_fiberwise_equipotent by A4, RFUNCT_3:45; :: 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 )
A7: ( (max- ((Rlor F,B) - r)) | C = max- ((Rlor F,B) - r) & (max- (F - r)) | D = max- (F - r) ) by A5, RELAT_1:97;
then FinS (max- ((Rlor F,B) - r)),C, max- ((Rlor F,B) - r) are_fiberwise_equipotent by A5, RFUNCT_3:def 14;
then FinS (max- ((Rlor F,B) - r)),C, max- (F - r) are_fiberwise_equipotent by A6, CLASSES1:84;
hence FinS (max- ((Rlor F,B) - r)),C = FinS (max- (F - r)),D by A5, 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