theorem Th9: :: REARRAN1:9

for D being non empty finite set
for a being terms've_same_card_as_number length_equal_card_of_set FinSequence of bool D ex d being Element of D st a . 1 = {d}