for A being set
for K being Element of Normal_forms_on A holds FinJoin (K,(Atom A)) = FinUnion (K,(singleton (DISJOINT_PAIRS A)))