L:LangOver(Alph). (L
0) = 
lang_zero_power
n) == if n=
0
else ((Ln-1)
L) fi (recursive)
Thm* L:LangOver(Alph). (L0) = lang_zero_power
Thm* L,L':LangOver(Alph), n,n':
.
L = L' 
n = n' (Ln) = (L'n')
lang_power_functionality