set T = S -termsOfMaxDepth ;
let t be string of S; :: thesis: ( t is m + (0 * n) -termal implies t is m + n -termal )
assume t is m + (0 * n) -termal ; :: thesis: t is m + n -termal
then ( t in (S -termsOfMaxDepth) . m & (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n) ) by Lm5;
hence t is m + n -termal ; :: thesis: verum