for A being set
for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A))