:: 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₁,b₂) where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() V50() complex ext-real non negative Element of NAT : b₁ <= b₂ } is set
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)))