let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) implies HT ((P -Ideal),T) c= multiples (HT (P,T)) )

assume A1: for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ; :: thesis: HT ((P -Ideal),T) c= multiples (HT (P,T))

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in HT ((P -Ideal),T) or u in multiples (HT (P,T)) )

assume A2: u in HT ((P -Ideal),T) ; :: thesis: u in multiples (HT (P,T))

then reconsider u9 = u as Element of Bags n ;

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides u9 ) by A1, A2;

hence u in multiples (HT (P,T)) ; :: thesis: verum

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) holds

HT ((P -Ideal),T) c= multiples (HT (P,T))

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ) implies HT ((P -Ideal),T) c= multiples (HT (P,T)) )

assume A1: for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ; :: thesis: HT ((P -Ideal),T) c= multiples (HT (P,T))

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in HT ((P -Ideal),T) or u in multiples (HT (P,T)) )

assume A2: u in HT ((P -Ideal),T) ; :: thesis: u in multiples (HT (P,T))

then reconsider u9 = u as Element of Bags n ;

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides u9 ) by A1, A2;

hence u in multiples (HT (P,T)) ; :: thesis: verum