theorem :: REARRAN1:37

for n being Nat
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 & n in dom A holds
(FinS ((Rlor (F,A)),C)) | n = FinS ((Rlor (F,A)),((Co_Gen A) . n))