set O = T;

now :: thesis: ( ( HC (p,T) <> 0. L & HM (p,T) is non-zero ) or ( HC (p,T) = 0. L & HM (p,T) is non-zero ) )

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 1; :: 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 1; :: thesis: verum

end;

end;

end;

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