theorem :: REARRAN1:39

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 D = card C holds
( Rland (F,A),F are_fiberwise_equipotent & Rlor (F,A),F are_fiberwise_equipotent & rng (Rland (F,A)) = rng F & rng (Rlor (F,A)) = rng F )