set O = T;
set a = HC p,T;

now

assume HC p,T = 0. L ; :: thesis: contradiction
then not HT p,T in Support p by POLYNOM1:def 9;
then Support p = {} by Def6;
then p = 0_ n,L by POLYNOM7:1;
hence contradiction by POLYNOM7:def 2; :: thesis: verum

end;

hence not HC p,T is zero by STRUCT_0:def 12; :: thesis: verum