for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
( ( c in (Co_Gen A) . 1 implies (Rlor (F,A)) . c = (FinS (F,D)) . 1 ) & ( for n being Nat st 1 <= n & n < len (Co_Gen A) & c in ((Co_Gen A) . (n + 1)) \ ((Co_Gen A) . n) holds
(Rlor (F,A)) . c = (FinS (F,D)) . (n + 1) ) )