theorem
for
C,
D 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
(
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) )