((a,b) Subnomial ((n + 1) - 1)) null n is n + 1 -element ;
hence (a,b) Subnomial n is n + 1 -element ; :: thesis: verum