theorem Th23: :: REARRAN1:24

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), FinS (F,D) are_fiberwise_equipotent