support (b |^ n) = support b by Def6;
hence support (b |^ n) is finite ; :: according to POLYNOM1:def 8 :: thesis: verum