let S be Polish-language; :: thesis: for m, n being Nat holds S ^^ (m + n) is S ^^ m -headed
let m, n be Nat; :: thesis: S ^^ (m + n) is S ^^ m -headed
S ^^ (m + n) = (S ^^ m) ^ (S ^^ n) by Th10;
hence S ^^ (m + n) is S ^^ m -headed ; :: thesis: verum