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