:: deftheorem defines length_equal_card_of_set REARRAN1:def 3 :
for X being set
for IT being FinSequence of X holds
( IT is length_equal_card_of_set iff ex B being finite set st
( B = union X & len IT = card B ) );