assume not support (0 * b) is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in support (0 * b) ;
(0 * b) . x <> 0 by A1, PRE_POLY:def 7;
then 0 * (b . x) <> 0 by Def2;
hence contradiction ; :: thesis: verum