for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D
for n, m being Nat st n in dom a & m in dom a & n <> m holds
a . n <> a . m