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
( Rlor (F,A), Rland (F,A) are_fiberwise_equipotent & FinS ((Rlor (F,A)),C) = FinS ((Rland (F,A)),C) & Sum ((Rlor (F,A)),C) = Sum ((Rland (F,A)),C) )
let F be PartFunc of D,REAL; :: thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
( Rlor (F,A), Rland (F,A) are_fiberwise_equipotent & FinS ((Rlor (F,A)),C) = FinS ((Rland (F,A)),C) & Sum ((Rlor (F,A)),C) = Sum ((Rland (F,A)),C) )
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) ) )
assume A1: ( F is total & card C = card D ) ; :: thesis: ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) )
then A2: ( Sum ((Rland (F,B)),C) = Sum (F,D) & Rlor (F,B), FinS (F,D) are_fiberwise_equipotent ) by Th19, Th24;
( Rland (F,B), FinS (F,D) are_fiberwise_equipotent & FinS ((Rland (F,B)),C) = FinS (F,D) ) by A1, Th17, Th18;
hence ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) ) by A1, A2, Th25, Th26, CLASSES1:76; :: thesis: verum