deg (0_. L) = - 1 by HURWITZ:20;
hence ( 0_. L is zero & 0_. L is constant ) by defconst, defzer; :: thesis: verum