:: GROEB_1 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K10(REAL)

K10(REAL) is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

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

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

K227() is set

{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V49() V50() Function-yielding V141() irreflexive complex ext-real non negative V211() V212() V213() V214() FinSequence-yielding finite-support set

RAT is set

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

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real positive non negative Element of NAT

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

COMPLEX is set

INT is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real positive non negative Element of NAT

K11(NAT,REAL) is Relation-like set

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

3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real positive non negative Element of NAT

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

0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V49() V50() Function-yielding V141() irreflexive complex ext-real non negative V211() V212() V213() V214() FinSequence-yielding finite-support Element of NAT

NATOrd is Relation-like Element of K10(K11(NAT,NAT))

{ K545(NAT,NAT,b

OrderedNAT is non empty transitive antisymmetric quasi_ordered Dickson V251() RelStr

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

n is epsilon-transitive epsilon-connected ordinal 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

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

{L} is non empty trivial functional finite 1 -element set

Polynom-Ring (n,T) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

n is epsilon-transitive epsilon-connected ordinal 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)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

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

HT (G,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

I . GH is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

HC (G,T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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 is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

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

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))

n is epsilon-transitive epsilon-connected ordinal 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 admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

HT (I,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

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

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

I . GH is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

0. L is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

the ZeroF of L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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))

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 (GH,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HC (GH,T) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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 is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

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

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))

(HC (GH,T)) " is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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) 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 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))

n is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)

L is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

<*L*> is non empty trivial Relation-like NAT -defined the carrier of n -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support M11( the carrier of n,K205( 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*> /. H is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

<*L*> . 1 is set

1. n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

the OneF of n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

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

((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)

H is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support LinearCombination of G

Sum H is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

n is epsilon-transitive epsilon-connected ordinal 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

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

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

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

H - GH is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,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))

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

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

g + GH is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring (n,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))

0. (Polynom-Ring (n,L)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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))

- GH 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))

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

n is epsilon-transitive epsilon-connected ordinal 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)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

H is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

n is epsilon-transitive epsilon-connected ordinal 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)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

n is epsilon-transitive epsilon-connected ordinal 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)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)))

0. (Polynom-Ring (n,L)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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))

n is epsilon-transitive epsilon-connected ordinal 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

T is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

G is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

L . G is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(- L) . G is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (0. T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (- (0. T)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . G) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

I is set

G is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

(- L) . G is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

L . G is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

- (L . G) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

n is epsilon-transitive epsilon-connected ordinal 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)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

HT ((- I),T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HT (I,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of 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))

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

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

- (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))

0. (Polynom-Ring (n,L)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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))

H 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. (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_ (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))

n is epsilon-transitive epsilon-connected ordinal 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 admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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

HT (I,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HT (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

HT ((- 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

n is epsilon-transitive epsilon-connected ordinal 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 admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

H is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT

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))

card (Support GH) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of omega

H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real positive non negative Element of NAT

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))

HT (GH,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of 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))

HT (g,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

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

(Support g) \ {(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))) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of omega

(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),(Support g)] is V21() set

HT (g,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HT (g,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HT (g,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of 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))

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))

card (Support GH) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of omega

card (Support G) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of omega

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))

card (Support H) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of omega

H is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal 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 admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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))

HT (G,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

HT (I,T) is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support Element of Bags n

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

K10((Bags n)) is non empty set

H is Relation-like n -defined RAT -valued Function-like total V211() V212() V213() V214() finite-support set

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT

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 V261() admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)))

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)))

0. (Polynom-Ring (n,L)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT

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 V261() admissible Element of K10(K11((Bags n),(Bags n)))

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V130() left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)))

0. (Polynom-Ring (n,L)) is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of 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))

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

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

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

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

GH is Relation-like co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property confluent with_Church-Rosser_property locally-confluent complete irreflexive set

q is set

r is set

n is epsilon-transitive epsilon-connected ordinal 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

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring (n,L) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

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)))