L:LangOver(Alph). (
L) = L lang_sing_prod
M)(l) == 
i:{0...||l||}. L(l[0..i
]) & M(l[i..||l||])
Thm* L:LangOver(Alph). (L) = L lang_sing_prod
Thm* L:LangOver(Alph). (L) = L lang_prod_sing
Thm* L,L',M,M':LangOver(Alph). L = L' 
M = M' (LM) = (L'M')
lang_prod_functionality