(a,a) Subnomial n = (n + 1) |-> (a |^ n) by CONST1;
hence (a,a) Subnomial n is constant ; :: thesis: verum