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 2;
then F | D = F by RELAT_1:68;
then A4: FinS (F,D),F are_fiberwise_equipotent by A3, RFUNCT_3:def 13;
Rland (F,B), FinS (F,D) are_fiberwise_equipotent by A1, A2, Th17;
then Rland (F,B),F are_fiberwise_equipotent by A4, CLASSES1:76;
then (Rland (F,B)) - r,F - r are_fiberwise_equipotent by RFUNCT_3:51;
hence A5: max- ((Rland (F,B)) - r), max- (F - r) are_fiberwise_equipotent by RFUNCT_3:42; :: 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:68;
then FinS ((max- ((Rland (F,B)) - r)),C), max- ((Rland (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;
then A7: FinS ((max- ((Rland (F,B)) - r)),C), max- (F - r) are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (max- (F - r)) = dom (F - r) by RFUNCT_3:def 11;
then (max- (F - r)) | D = max- (F - r) by RELAT_1:68;
hence FinS ((max- ((Rland (F,B)) - r)),C) = FinS ((max- (F - r)),D) by A8, A7, RFUNCT_3:def 13; :: 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 14
.= Sum ((max- (F - r)),D) by RFUNCT_3:def 14 ;
:: thesis: verum