set O = T;

now

per cases ( HC p,T <> 0. L or HC p,T = 0. L ) ;

case HC p,T <> 0. L ; :: thesis: HM p,T is non-zero

then HT p,T in Support (HM p,T) by Lm9;
then HM p,T <> 0_ n,L by POLYNOM7:1;
hence HM p,T is non-zero by POLYNOM7:def 2; :: thesis: verum

end;

case HC p,T = 0. L ; :: thesis: HM p,T is non-zero

then p = 0_ n,L by Lm7;
hence HM p,T is non-zero by POLYNOM7:def 2; :: thesis: verum

end;

end;

end;

hence HM p,T is non-zero ; :: thesis: verum