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 ( 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 ( Rland F,B, FinS F,D are_fiberwise_equipotent & FinS (Rland F,B),C = FinS F,D & Sum (Rland F,B),C = Sum F,D & Rlor F,B, FinS F,D are_fiberwise_equipotent & FinS (Rlor F,B),C = FinS F,D & Sum (Rlor F,B),C = Sum F,D ) by Th17, Th18, Th19, Th24, Th25, Th26;
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 CLASSES1:84; :: thesis: verum