:: GROEB_1 semantic presentation

REAL is set

K10(REAL) is non empty set

K10(omega) is non empty non trivial non finite set
K10(NAT) is non empty non trivial non finite set
K227() is set

RAT is set
is non empty trivial functional finite V28() 1 -element set

K205() is non empty functional FinSequence-membered M10()
K11(K205(),) is non empty Relation-like set
K10(K11(K205(),)) is non empty set
PFuncs (K205(),) is set
K11(NAT,NAT) is non empty non trivial Relation-like non finite set
K10(K11(NAT,NAT)) is non empty non trivial non finite set

INT is set

K10(K11(NAT,REAL)) is non empty set

Seg 1 is non empty trivial finite 1 -element Element of K10(NAT)
{1} is non empty trivial finite V28() 1 -element set
Seg 2 is non empty finite 2 -element Element of K10(NAT)
{1,2} is non empty finite V28() set

{ K545(NAT,NAT,b1,b2) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT : b1 <= b2 } is set

RelStr(# NAT,NATOrd #) is non empty strict RelStr

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set

the carrier of T is non empty non trivial set
K11((Bags n), the carrier of T) is non empty Relation-like set
K10(K11((Bags n), the carrier of T)) is non empty set
L is non empty Relation-like Function-like total V46( Bags n, the carrier of T) V271( Bags n,T) Element of K10(K11((Bags n), the carrier of T))

the carrier of (Polynom-Ring (n,T)) is non empty set
K10( the carrier of (Polynom-Ring (n,T))) is non empty set
I is set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

(I . GH) / (HC (G,T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

GH *' G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((I . GH) / (HC (G,T))) * (GH *' G) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I - (((I . GH) / (HC (G,T))) * (GH *' G)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Monom (((I . GH) / (HC (G,T))),GH) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(Monom (((I . GH) / (HC (G,T))),GH)) *' G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support H is functional finite Element of K10((Bags n))
K10((Bags n)) is non empty set

Support I is functional finite Element of K10((Bags n))

0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

(I . GH) / (HC (GH,T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

g *' GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((I . GH) / (HC (GH,T))) * (g *' GH) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I - (((I . GH) / (HC (GH,T))) * (g *' GH)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Monom (((I . GH) / (HC (GH,T))),g) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

(I . GH) * ((HC (GH,T)) ") is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
coefficient (Monom (((I . GH) / (HC (GH,T))),g)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
HC ((Monom (((I . GH) / (HC (GH,T))),g)),T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L
b9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
b9 *' GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
HT ((b9 *' GH),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

(HT (b9,T)) + (HT (GH,T)) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

(term b9) + (HT (GH,T)) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set
(Monom (((I . GH) / (HC (GH,T))),g)) *' GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

the carrier of n is non empty set
K10( the carrier of n) is non empty set
T is Element of K10( the carrier of n)
T -Ideal is non empty add-closed left-ideal right-ideal Element of K10( the carrier of n)

K205( the carrier of n) is non empty functional FinSequence-membered M10( the carrier of n)
H is set
dom <*L*> is non empty trivial finite 1 -element Element of K10(NAT)

<*L*> . 1 is set

((1. n) * L) * (1. n) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n
G is non empty Element of K10( the carrier of n)

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set

the carrier of (Polynom-Ring (n,L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I - G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

- G is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

(- G) + G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

the ZeroF of (Polynom-Ring (n,L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))

I + (- G) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set

the carrier of (Polynom-Ring (n,L)) is non empty set
K10( the carrier of (Polynom-Ring (n,L))) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
H is Element of K10( the carrier of (Polynom-Ring (n,L)))
GH is Element of K10( the carrier of (Polynom-Ring (n,L)))
GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))

the carrier of (Polynom-Ring (n,L)) is non empty set
K10( the carrier of (Polynom-Ring (n,L))) is non empty set
NonZero (Polynom-Ring (n,L)) is Element of K10( the carrier of (Polynom-Ring (n,L)))
[#] (Polynom-Ring (n,L)) is non empty non proper Element of K10( the carrier of (Polynom-Ring (n,L)))

the ZeroF of (Polynom-Ring (n,L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))
{(0. (Polynom-Ring (n,L)))} is non empty trivial finite 1 -element set
([#] (Polynom-Ring (n,L))) \ {(0. (Polynom-Ring (n,L)))} is Element of K10( the carrier of (Polynom-Ring (n,L)))
I is Element of K10( the carrier of (Polynom-Ring (n,L)))
G is Element of K10( the carrier of (Polynom-Ring (n,L)))
PolyRedRel (I,T) is Relation-like Element of K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))
K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))) is Relation-like set
K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)))) is non empty set
PolyRedRel (G,T) is Relation-like Element of K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))
H is set
GH is set
GH is set
[GH,GH] is V21() set
the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(n,L,(0_ (n,L))) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
g is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set

the carrier of T is non empty set
K11((Bags n), the carrier of T) is non empty Relation-like set
K10(K11((Bags n), the carrier of T)) is non empty set
L is non empty Relation-like Function-like total V46( Bags n, the carrier of T) V271( Bags n,T) Element of K10(K11((Bags n), the carrier of T))
- L is non empty Relation-like Function-like total total V46( Bags n, the carrier of T) V46( Bags n, the carrier of T) V271( Bags n,T) Element of K10(K11((Bags n), the carrier of T))
Support (- L) is functional Element of K10((Bags n))
K10((Bags n)) is non empty set
Support L is functional Element of K10((Bags n))
I is set

I is set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- I is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

the carrier of (Polynom-Ring (n,L)) is non empty set

- (0_ (n,L)) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- (0_ (n,L))) + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

the ZeroF of (Polynom-Ring (n,L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))

H + (0. (Polynom-Ring (n,L))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))
(- I) + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support I is functional finite Element of K10((Bags n))
K10((Bags n)) is non empty set
Support (- I) is functional finite Element of K10((Bags n))
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I - G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
HT ((I - G),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

max ((HT (I,T)),(HT (G,T)),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set
- G is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
I + (- G) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
HT ((I + (- G)),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

max ((HT (I,T)),(HT ((- G),T)),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support G is functional finite Element of K10((Bags n))
K10((Bags n)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support I is functional finite Element of K10((Bags n))

RelStr(# (Bags n),T #) is non empty strict total reflexive transitive antisymmetric V251() RelStr
GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support GH is functional finite Element of K10((Bags n))
g is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support g is functional finite Element of K10((Bags n))

Red (GH,T) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Red (g,T) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Support (Red (GH,T)) is functional finite Element of K10((Bags n))
{(HT (GH,T))} is non empty trivial functional finite 1 -element set
(Support GH) \ {(HT (GH,T))} is functional finite Element of K10((Bags n))
Support (Red (g,T)) is functional finite Element of K10((Bags n))
{(HT (g,T))} is non empty trivial functional finite 1 -element set
() \ {(HT (g,T))} is functional finite Element of K10((Bags n))
h is set
h is set
Support (GH,T) is Element of K458( the carrier of RelStr(# (Bags n),T #))
the carrier of RelStr(# (Bags n),T #) is non empty set
K458( the carrier of RelStr(# (Bags n),T #)) is V235() set
Support (g,T) is Element of K458( the carrier of RelStr(# (Bags n),T #))
Support ((Red (GH,T)),T) is Element of K458( the carrier of RelStr(# (Bags n),T #))
PosetMax (Support (GH,T)) is Element of the carrier of RelStr(# (Bags n),T #)
PosetMax (Support (g,T)) is Element of the carrier of RelStr(# (Bags n),T #)
Support ((Red (g,T)),T) is Element of K458( the carrier of RelStr(# (Bags n),T #))
{(PosetMax (Support (g,T)))} is non empty trivial finite 1 -element set
(Support (g,T)) \ {(PosetMax (Support (g,T)))} is Element of K10((Support (g,T)))
K10((Support (g,T))) is non empty set
(Support (Red (GH,T))) \/ {(HT (GH,T))} is non empty finite set
(Support GH) \/ {(HT (GH,T))} is non empty finite set

(card (Support (Red (GH,T)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real positive non negative Element of NAT
[(Support (Red (GH,T))),(Support (Red (g,T)))] is V21() set
FinOrd RelStr(# (Bags n),T #) is Relation-like total V46(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))) reflexive antisymmetric transitive Element of K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))))
K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))) is Relation-like set
K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #)))) is non empty set
[(Support ((Red (GH,T)),T)),(Support ((Red (g,T)),T))] is V21() set
FinOrd-Approx RelStr(# (Bags n),T #) is non empty Relation-like Function-like total V46( NAT ,K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))))) Element of K10(K11(NAT,K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))))))
K11(NAT,K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #))))) is non empty non trivial Relation-like non finite set
K10(K11(NAT,K10(K11(K458( the carrier of RelStr(# (Bags n),T #)),K458( the carrier of RelStr(# (Bags n),T #)))))) is non empty non trivial non finite set
rng (FinOrd-Approx RelStr(# (Bags n),T #)) is non empty set
union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) is set
{(PosetMax (Support (GH,T)))} is non empty trivial finite 1 -element set
(Support (GH,T)) \ {(PosetMax (Support (GH,T)))} is Element of K10((Support (GH,T)))
K10((Support (GH,T))) is non empty set
[(Support (GH,T)),(Support (g,T))] is V21() set
[(Support GH),()] is V21() set

GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support GH is functional finite Element of K10((Bags n))
GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support GH is functional finite Element of K10((Bags n))

H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support H is functional finite Element of K10((Bags n))
GH is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
Support GH is functional finite Element of K10((Bags n))

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
G is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

Support I is functional finite Element of K10((Bags n))
K10((Bags n)) is non empty set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(n,L,I) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))

the carrier of (Polynom-Ring (n,L)) is non empty set
K10( the carrier of (Polynom-Ring (n,L))) is non empty set
PolyRedRel ((n,L,I),T) is Relation-like co-well_founded weakly-normalizing strongly-normalizing irreflexive Element of K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))
NonZero (Polynom-Ring (n,L)) is Element of K10( the carrier of (Polynom-Ring (n,L)))
[#] (Polynom-Ring (n,L)) is non empty non proper Element of K10( the carrier of (Polynom-Ring (n,L)))

the ZeroF of (Polynom-Ring (n,L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))
{(0. (Polynom-Ring (n,L)))} is non empty trivial finite 1 -element set
([#] (Polynom-Ring (n,L))) \ {(0. (Polynom-Ring (n,L)))} is Element of K10( the carrier of (Polynom-Ring (n,L)))
K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))) is Relation-like set
K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)))) is non empty set
0_ (n,L) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like Constant V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
H is set
GH is set
[H,GH] is V21() set
GH is set
[H,GH] is V21() set
g is set
g is set
[g,g] is V21() set
(n,L,(0_ (n,L))) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
h is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
b9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
GH is set
GH is set
[GH,GH] is V21() set
g is set
[GH,g] is V21() set
g is set
b9 is set
[g,b9] is V21() set
(n,L,(0_ (n,L))) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
h is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(n,L,H) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
f is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
f is set
f is set
[f,f] is V21() set
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h - (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (h9 *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (- (h9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h + (- (h9 *' H))) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- (h9 *' H)) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + ((- (h9 *' H)) + (h9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) - (g9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (g9 *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) + (- (g9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- g9 is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- g9) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) + ((- g9) *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 + (- g9) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 + (- g9)) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 - g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 - g9) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is set
b9 is set
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h - (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (h9 *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (- (h9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h + (- (h9 *' H))) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- (h9 *' H)) + (h9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + ((- (h9 *' H)) + (h9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) - (g9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (g9 *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) + (- (g9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- g9 is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- g9) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 *' H) + ((- g9) *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 + (- g9) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 + (- g9)) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 - g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 - g9) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is set
b9 is set
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 - g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- g9 is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 + (- g9) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h9 + (- g9)) + g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- g9) + g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 + ((- g9) + g9) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
b9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
b9 *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h - (b9 *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q is non empty Relation-like Function-like total V46( Bags n, the carrier of L) monomial-like V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h - (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- b9 is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- b9) + q is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- b9) + b9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q + ((- b9) + b9) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + b9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (q *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (- (q *' H)) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (h - (q *' H)) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h - (b9 *' H)) + (- (h - (q *' H))) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (- (q *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (h + (- (q *' H))) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h - (b9 *' H)) + (- (h + (- (q *' H)))) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- h is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- h) + (- (- (q *' H))) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h - (b9 *' H)) + ((- h) + (- (- (q *' H)))) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- (b9 *' H) is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (- (b9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h + (- (b9 *' H))) + ((- h) + (- (- (q *' H)))) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h + (- (b9 *' H))) + (- h) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((h + (- (b9 *' H))) + (- h)) + (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h + (- h) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(h + (- h)) + (- (b9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((h + (- h)) + (- (b9 *' H))) + (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + (- (b9 *' H)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((0_ (n,L)) + (- (b9 *' H))) + (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- (b9 *' H)) + (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- b9) *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
((- b9) *' H) + (q *' H) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
q *' H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
r is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
p is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
r - p is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
- p is non empty Relation-like Function-like total total V46( Bags n, the carrier of L) V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
r + (- p) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(r + (- p)) + p is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(0_ (n,L)) + p is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(- p) + p is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
r + ((- p) + p) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
r + (0_ (n,L)) is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
g9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) non-zero V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
h9 is set
b9 is set
h9 is set
g9 is set
h9 is set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of (Polynom-Ring (n,L)) is non empty set
K10( the carrier of (Polynom-Ring (n,L))) is non empty set
the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
I is Element of K10( the carrier of (Polynom-Ring (n,L)))
I -Ideal is non empty add-closed left-ideal right-ideal Element of K10( the carrier of (Polynom-Ring (n,L)))
PolyRedRel (I,T) is Relation-like co-well_founded weakly-normalizing strongly-normalizing irreflexive Element of K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))
NonZero (Polynom-Ring (n,L)) is Element of K10( the carrier of (Polynom-Ring (n,L)))
[#] (Polynom-Ring (n,L)) is non empty non proper Element of K10( the carrier of (Polynom-Ring (n,L)))

the ZeroF of (Polynom-Ring (n,L)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,L))
{(0. (Polynom-Ring (n,L)))} is non empty trivial finite 1 -element set
([#] (Polynom-Ring (n,L))) \ {(0. (Polynom-Ring (n,L)))} is Element of K10( the carrier of (Polynom-Ring (n,L)))
K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))) is Relation-like set
K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)))) is non empty set
H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(n,L,H) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
(n,L,H) -Ideal is non empty add-closed left-ideal right-ideal finitely_generated Element of K10( the carrier of (Polynom-Ring (n,L)))
H is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
(n,L,H) is non empty trivial functional finite 1 -element Element of K10( the carrier of (Polynom-Ring (n,L)))
(n,L,H) -Ideal is non empty add-closed left-ideal right-ideal finitely_generated Element of K10( the carrier of (Polynom-Ring (n,L)))
PolyRedRel ((n,L,H),T) is Relation-like co-well_founded weakly-normalizing strongly-normalizing irreflexive Element of K10(K11((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))
g is set
g is set
[g,g] is V21() set
b9 is set
[g,b9] is V21() set
h is set
h is set
[h,h] is V21() set
f is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))
f is set
g9 is set
[f,g9] is V21() set
h9 is non empty Relation-like Function-like total V46( Bags n, the carrier of L) V271( Bags n,L) Element of K10(K11((Bags n), the carrier of L))

q is set
r is set

Bags n is non empty functional Element of K10((Bags n))
Bags n is non empty set
K10((Bags n)) is non empty set
K11((Bags n),(Bags n)) is non empty Relation-like set
K10(K11((Bags n),(Bags n))) is non empty set

the carrier of (Polynom-Ring (n,L)) is non empty set
K10( the carrier of (Polynom-Ring (n,L))) is non empty set
the carrier of L is non empty non trivial set
K11((Bags n), the carrier of L) is non empty Relation-like set
K10(K11((Bags n), the carrier of L)) is non empty set
T is Relation-like total V46( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K10(K11((Bags n),(Bags n)))
I is Element of K10( the carrier of (Polynom-Ring (n,L)))