A: support b1 <> {} by bbag;
set o = the Element of support b1;
D: b1 . the Element of support b1 <> 0 by A, PRE_POLY:def 7;
set b = b1 + b2;
(b1 + b2) . the Element of support b1 = (b1 . the Element of support b1) + (b2 . the Element of support b1) by PRE_POLY:def 5;
hence not b1 + b2 is zero by D; :: thesis: verum