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

now

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

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: ( c * p in I & HM (c * p),T = Monom (1. L),(HT p,T) & c * p <> 0_ n,L )
reconsider pp = p, cc = c | n,L as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
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 27 ;
hence c * p in I by A1, IDEAL_1:def 2; :: thesis: ( HM (c * p),T = Monom (1. L),(HT p,T) & c * p <> 0_ n,L )
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 10
.= (HC p,T) * ((HC p,T) " ) by TERMORD:def 7
.= 1. L by A3, VECTSP_1:def 22 ;
hence HM (c * p),T = Monom (1. L),(HT p,T) by A4, TERMORD:def 8; :: thesis: c * p <> 0_ n,L
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: verum