let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis:
assume that
A1: p in I and
A2: p <> 0_ (n,L) ; :: thesis:
set c = (HC (p,T)) " ;
A3: HC (p,T) <> 0. L by A2, TERMORD:17;

now :: thesis:

assume (HC (p,T)) " = 0. L ; :: thesis:
then 0. L = ((HC (p,T)) ") * (HC (p,T))
.= 1. L by A3, VECTSP_1:def 10 ;
hence contradiction ; :: thesis:

end;

then reconsider c = (HC (p,T)) " as non zero Element of L by STRUCT_0:def 12;
set q = c * p;
take c * p ; :: thesis:
reconsider pp = p, cc = c | (n,L) as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider pp = pp, cc = cc as Element of (Polynom-Ring (n,L)) ;
c * p = (c | (n,L)) *' p by POLYNOM7:27
.= cc * pp by POLYNOM1:def 11 ;
hence c * p in I by A1, IDEAL_1:def 2; :: thesis:
A4: HT ((c * p),T) = HT (p,T) by POLYRED:21;
then HC ((c * p),T) = (c * p) . (HT (p,T)) by TERMORD:def 7
.= c * (p . (HT (p,T))) by POLYNOM7:def 9
.= (HC (p,T)) * ((HC (p,T)) ") by TERMORD:def 7
.= 1. L by A3, VECTSP_1:def 10 ;
hence HM ((c * p),T) = Monom ((1. L),(HT (p,T))) by A4, TERMORD:def 8; :: thesis:
then 1. L = coefficient (HM ((c * p),T)) by POLYNOM7:9
.= HC ((c * p),T) by TERMORD:22 ;
then HC ((c * p),T) <> 0. L ;
hence c * p <> 0_ (n,L) by TERMORD:17; :: thesis: