theorem Th7: :: REARRAN1:7

for n being Nat
for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}