:: deftheorem defines Co_Gen REARRAN1:def 4 :
for D being non empty finite set
for A, b₃ being RearrangmentGen of D holds
( b₃ = Co_Gen A iff for m being Nat st 1 <= m & m <= (len b₃) - 1 holds
b₃ . m = D \ (A . ((len A) - m)) );