Added lemmas about Maps.
Added Lemma Disjoint_sa_mul.