support (n (#) b) c= support b by Th7;
hence n (#) b is finite-support by PRE_POLY:def 8; :: thesis: verum