Def (L U M)(l) == L(l) M(l)

Thm* Alph:Type, M,N:LangOver(Alph). (M U N) LangOver(Alph)