for m, n being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) by Lm5;