theorem Th35: :: REARRAN1:36

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
( len (FinS ((Rlor (F,A)),C)) = card C & 1 <= len (FinS ((Rlor (F,A)),C)) )