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