A1: (1_. L) . 0 = 1. L by POLYNOM3:30;
(0_. L) . 0 = 0. L by FUNCOP_1:7;
hence not 1_. L is zero by A1; :: thesis: verum