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:84; :: thesis: verum