let C, D be 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
( 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; 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; ( 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 )
; ( 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 Th18, Th23;
( Rland (F,B), FinS (F,D) are_fiberwise_equipotent & FinS ((Rland (F,B)),C) = FinS (F,D) )
by A1, Th16, Th17;
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, Th24, Th25, CLASSES1:76; verum