:: GROEB_3 semantic presentation

REAL is set

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

K15(REAL) is non empty set

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

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

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

COMPLEX is set

RAT is set

INT is set

{} is ext-real non positive non negative empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding set

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

K16(NAT,NAT) is non empty non trivial Relation-like non finite set

K15(K16(NAT,NAT)) is non empty non trivial non finite set

K16(NAT,REAL) is Relation-like set

K15(K16(NAT,REAL)) is non empty set

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

0 is ext-real non positive non negative empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding Element of NAT

card {} is ext-real non positive non negative empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding set

n is set

T is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

T + L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(T + L) / L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L + ((T + L) / L) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(L + ((T + L) / L)) -' L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K15(K16((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[L,G] is V24() set

{L,G} is non empty functional finite set

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

{{L,G},{L}} is non empty finite V31() set

[(L + g1),(G + g1)] is V24() set

{(L + g1),(G + g1)} is non empty functional finite set

{(L + g1)} is non empty trivial functional finite 1 -element set

{{(L + g1),(G + g1)},{(L + g1)}} is non empty finite V31() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric transitive Element of K15(K16((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K15(K16((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(L + g1) -' g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[L,G] is V24() set

{L,G} is non empty functional finite set

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

{{L,G},{L}} is non empty finite V31() set

[(L + g1),(G + g1)] is V24() set

{(L + g1),(G + g1)} is non empty functional finite set

{(L + g1)} is non empty trivial functional finite 1 -element set

{{(L + g1),(G + g1)},{(L + g1)}} is non empty finite V31() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K15(K16((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G + g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[L,G] is V24() set

{L,G} is non empty functional finite set

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

{{L,G},{L}} is non empty finite V31() set

G + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[(L + g1),(G + g1)] is V24() set

{(L + g1),(G + g1)} is non empty functional finite set

{(L + g1)} is non empty trivial functional finite 1 -element set

{{(L + g1),(G + g1)},{(L + g1)}} is non empty finite V31() set

[g1,g2] is V24() set

{g1,g2} is non empty functional finite set

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

{{g1,g2},{g1}} is non empty finite V31() set

[(G + g1),(G + g2)] is V24() set

{(G + g1),(G + g2)} is non empty functional finite set

{(G + g1)} is non empty trivial functional finite 1 -element set

{{(G + g1),(G + g2)},{(G + g1)}} is non empty finite V31() set

L + g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(L + g2) -' g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(G + g2) -' g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g2 + G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(g2 + G) -' G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 + G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(g1 + G) -' G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric transitive admissible Element of K15(K16((Bags n),(Bags n)))

L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

L + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G + g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[g1,g2] is V24() set

{g1,g2} is non empty functional finite set

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

{{g1,g2},{g1}} is non empty finite V31() set

G + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

[(G + g1),(G + g2)] is V24() set

{(G + g1),(G + g2)} is non empty functional finite set

{(G + g1)} is non empty trivial functional finite 1 -element set

{{(G + g1),(G + g2)},{(G + g1)}} is non empty finite V31() set

[L,G] is V24() set

{L,G} is non empty functional finite set

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

{{L,G},{L}} is non empty finite V31() set

[(L + g1),(G + g1)] is V24() set

{(L + g1),(G + g1)} is non empty functional finite set

{(L + g1)} is non empty trivial functional finite 1 -element set

{{(L + g1),(G + g1)},{(L + g1)}} is non empty finite V31() set

g2 + G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(g2 + G) -' G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 + G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(g1 + G) -' G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

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

the carrier of T is non empty non trivial set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

L *' G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

term (L *' G) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

term L is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

term G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term L) + (term G) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n))) is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))

HC (G, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))) is non zero 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

HC (L, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))) is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

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

g2 is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

h is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

g2 * h is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

Monom (g2,(term L)) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Element of K15(K16((Bags n), the carrier of T))

Monom (h,(term G)) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Element of K15(K16((Bags n), the carrier of T))

h is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

Monom (h,((term L) + (term G))) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Element of K15(K16((Bags n), the carrier of T))

term (Monom (h,((term L) + (term G)))) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

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

the carrier of T is non empty non trivial set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support L is functional finite Element of K15((Bags n))

K15((Bags n)) is non empty set

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

term G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G *' L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support (G *' L) is functional finite Element of K15((Bags n))

g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + g1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(G *' L) . ((term G) + g1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

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

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

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

Support G is functional finite Element of K15((Bags n))

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

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

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

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

the carrier of T is non empty non trivial set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support L is functional finite Element of K15((Bags n))

K15((Bags n)) is non empty set

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

G *' L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support (G *' L) is functional finite Element of K15((Bags n))

term G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

{ ((term G) + b

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

Support G is functional finite Element of K15((Bags n))

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

{ (b

g1 is set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

h + h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g1 is set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(term G) + g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

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

the carrier of T is non empty non trivial set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support L is functional finite Element of K15((Bags n))

K15((Bags n)) is non empty set

card (Support L) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of omega

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero monomial-like Element of K15(K16((Bags n), the carrier of T))

G *' L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support (G *' L) is functional finite Element of K15((Bags n))

card (Support (G *' L)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of omega

term G is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n))) is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n)))

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

Support G is functional finite Element of K15((Bags n))

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

g2 is set

In (g2,(Bags n)) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(In (g2,(Bags n))) @ is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + ((In (g2,(Bags n))) @) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

In (h,(Bags n)) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(In (h,(Bags n))) @ is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

K16((Support L),(Support (G *' L))) is Relation-like finite set

K15(K16((Support L),(Support (G *' L)))) is non empty finite V31() set

g2 is Relation-like Support L -defined Support (G *' L) -valued Function-like finite V49( Support L, Support (G *' L)) finite-support Element of K15(K16((Support L),(Support (G *' L))))

HT (G, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n)))) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

h is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero Element of K15(K16((Bags n), the carrier of T))

HT (h, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n)))) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(HT (G, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n))))) + (HT (h, the Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive admissible Element of K15(K16((Bags n),(Bags n))))) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

G *' h is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support non-zero Element of K15(K16((Bags n), the carrier of T))

Support (G *' h) is functional finite Element of K15((Bags n))

dom g2 is functional finite Element of K15((Support L))

K15((Support L)) is non empty finite V31() set

{ (b

h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

rp2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

m is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

rp2 + m is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

In (m,(Bags n)) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(In (m,(Bags n))) @ is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + m is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g2 . m is Relation-like Function-like set

g2 .: (Support L) is functional finite Element of K15((Support (G *' L)))

K15((Support (G *' L))) is non empty finite V31() set

h is set

h is set

g2 . h is Relation-like Function-like set

g2 . h is Relation-like Function-like set

m is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

In (m,(Bags n)) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(In (m,(Bags n))) @ is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

rp2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

In (rp2,(Bags n)) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(In (rp2,(Bags n))) @ is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(term G) + rp2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

g2 . m is Relation-like Function-like set

(term G) + m is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

m + (term G) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(m + (term G)) -' (term G) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

h is set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((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 V105() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty non trivial set

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

K15(K16((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

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

G is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

g1 is set

g2 is Element of K15( the carrier of (Polynom-Ring (n,L)))

PolyRedRel (g2,T) is Relation-like NonZero (Polynom-Ring (n,L)) -defined the carrier of (Polynom-Ring (n,L)) -valued Element of K15(K16((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))))

NonZero (Polynom-Ring (n,L)) is Element of K15( the carrier of (Polynom-Ring (n,L)))

[#] (Polynom-Ring (n,L)) is non empty non proper Element of K15( 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 K15( the carrier of (Polynom-Ring (n,L)))

K16((NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L))) is Relation-like set

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

h is non empty Relation-like Function-like FinSequence-like RedSequence of PolyRedRel (g2,T)

h . 1 is set

len h is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

h . (len h) is set

(len h) - 1 is ext-real V52() V53() complex set

rp2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

h . rp2 is set

rp2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

dom h is non empty Element of K15(NAT)

0 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

[(h . rp2),g1] is V24() set

{(h . rp2),g1} is non empty finite set

{(h . rp2)} is non empty trivial finite 1 -element set

{{(h . rp2),g1},{(h . rp2)}} is non empty finite V31() set

m is set

m9 is set

[m,m9] is V24() set

{m,m9} is non empty finite set

{m} is non empty trivial finite 1 -element set

{{m,m9},{m}} is non empty finite V31() set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))

L is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of L is non empty non trivial set

0_ (n,L) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of L))

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

K15(K16((Bags n), the carrier of L)) is non empty set

Red ((0_ (n,L)),T) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

HM ((0_ (n,L)),T) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support monomial-like Element of K15(K16((Bags n), the carrier of L))

HC ((HM ((0_ (n,L)),T)),T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

HC ((0_ (n,L)),T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of L

HT ((0_ (n,L)),T) is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(0_ (n,L)) . (HT ((0_ (n,L)),T)) 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)) - (0_ (n,L)) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable V105() 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 T is non empty non trivial set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

L - G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G + (L - G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

- G is non empty Relation-like Bags n -defined Bags n -defined the carrier of T -valued Function-like V48( Bags n) V48( Bags n) V49( Bags n, the carrier of T) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

L + (- G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G + (L + (- G)) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G + (- G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

(G + (- G)) + L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

(0_ (n,T)) + L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((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 addLoopStr

the carrier of T is non empty set

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

- (0_ (n,T)) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

g1 is set

dom (- (0_ (n,T))) is non empty functional Element of K15((Bags n))

K15((Bags n)) is non empty set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

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

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

- ((0_ (n,T)) . g2) 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

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

(- (0_ (n,T))) . g1 is set

(0_ (n,T)) . g1 is set

dom (0_ (n,T)) is non empty functional Element of K15((Bags n))

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((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 addLoopStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

(0_ (n,T)) - L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

- L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

g1 is set

dom ((0_ (n,T)) - L) is non empty functional Element of K15((Bags n))

K15((Bags n)) is non empty set

g2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

((0_ (n,T)) - L) . g2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

(0_ (n,T)) + (- L) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

((0_ (n,T)) + (- L)) . g2 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of T

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

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

((0_ (n,T)) . g2) + ((- L) . g2) 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

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

((0_ (n,T)) - L) . g1 is set

(- L) . g1 is set

dom (- L) is non empty functional Element of K15((Bags n))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))

L is non empty non trivial 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 L is non empty non trivial set

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

K15(K16((Bags n), the carrier of L)) is non empty set

G is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

Red (G,T) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

G - (Red (G,T)) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

HM (G,T) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support monomial-like Element of K15(K16((Bags n), the carrier of L))

(HM (G,T)) + (Red (G,T)) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

((HM (G,T)) + (Red (G,T))) - (Red (G,T)) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

- (Red (G,T)) is non empty Relation-like Bags n -defined Bags n -defined the carrier of L -valued Function-like V48( Bags n) V48( Bags n) V49( Bags n, the carrier of L) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

((HM (G,T)) + (Red (G,T))) + (- (Red (G,T))) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

(Red (G,T)) + (- (Red (G,T))) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

(HM (G,T)) + ((Red (G,T)) + (- (Red (G,T)))) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

0_ (n,L) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of L))

(HM (G,T)) + (0_ (n,L)) is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((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 addLoopStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

K15((Bags n)) is non empty set

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

T is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable V105() 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

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

{L,G} is non empty functional finite 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

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

g1 is set

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

K15((Bags n)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

G is functional Element of K15((Bags n))

(Support L) \ G is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ G) --> (0. T) is Relation-like (Support L) \ G -defined the carrier of T -valued Function-like V48((Support L) \ G) V49((Support L) \ G, the carrier of T) Element of K15(K16(((Support L) \ G), the carrier of T))

K16(((Support L) \ G), the carrier of T) is Relation-like set

K15(K16(((Support L) \ G), the carrier of T)) is non empty set

L +* (((Support L) \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

(L +* (((Support L) \ G) --> (0. T))) . h is set

(((Support L) \ G) --> (0. T)) . h is set

(L +* (((Support L) \ G) --> (0. T))) . h is set

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(L +* (((Support L) \ G) --> (0. T))) . h is set

L . h is Element of the carrier of T

(L +* (((Support L) \ G) --> (0. T))) . h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

(L +* (((Support L) \ G) --> (0. T))) . h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

(L +* (((Support L) \ G) --> (0. T))) . h is set

h is set

dom L is non empty functional Element of K15((Bags n))

dom (L +* (((Support L) \ G) --> (0. T))) is non empty set

(Bags n) \/ ((Support L) \ G) is non empty set

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

G is functional Element of K15((Bags n))

(n,T,L,G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

(Support L) \ G is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ G) --> (0. T) is Relation-like (Support L) \ G -defined the carrier of T -valued Function-like V48((Support L) \ G) V49((Support L) \ G, the carrier of T) Element of K15(K16(((Support L) \ G), the carrier of T))

K16(((Support L) \ G), the carrier of T) is Relation-like set

K15(K16(((Support L) \ G), the carrier of T)) is non empty set

L +* (((Support L) \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

Support (n,T,L,G) is functional Element of K15((Bags n))

h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(L +* (((Support L) \ G) --> (0. T))) . h is set

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

L . h is Element of the carrier of T

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

L . h is Element of the carrier of T

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

L . h is Element of the carrier of T

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

K15((Bags n)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support Element of K15(K16((Bags n), the carrier of T))

G is functional Element of K15((Bags n))

(n,T,L,G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

(Support L) \ G is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ G) --> (0. T) is Relation-like (Support L) \ G -defined the carrier of T -valued Function-like V48((Support L) \ G) V49((Support L) \ G, the carrier of T) Element of K15(K16(((Support L) \ G), the carrier of T))

K16(((Support L) \ G), the carrier of T) is Relation-like set

K15(K16(((Support L) \ G), the carrier of T)) is non empty set

L +* (((Support L) \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

Support (n,T,L,G) is functional Element of K15((Bags n))

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

G is functional Element of K15((Bags n))

(n,T,L,G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

(Support L) \ G is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ G) --> (0. T) is Relation-like (Support L) \ G -defined the carrier of T -valued Function-like V48((Support L) \ G) V49((Support L) \ G, the carrier of T) Element of K15(K16(((Support L) \ G), the carrier of T))

K16(((Support L) \ G), the carrier of T) is Relation-like set

K15(K16(((Support L) \ G), the carrier of T)) is non empty set

L +* (((Support L) \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

Support (n,T,L,G) is functional Element of K15((Bags n))

(Support L) /\ G is set

h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

dom (((Support L) \ G) --> (0. T)) is Element of K15(((Support L) \ G))

K15(((Support L) \ G)) is non empty set

(L +* (((Support L) \ G) --> (0. T))) . h is set

(((Support L) \ G) --> (0. T)) . h is set

L . h is Element of the carrier of T

h is set

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(L +* (((Support L) \ G) --> (0. T))) . h is set

L . h is Element of the carrier of T

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(n,T,L,G) . h is Element of the carrier of T

L . h is Element of the carrier of T

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support set

(n,T,L,G) . h is Element of the carrier of T

L . h is Element of the carrier of T

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

K15((Bags n)) is non empty set

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

G is functional Element of K15((Bags n))

(n,T,L,G) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

(Support L) \ G is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ G) --> (0. T) is Relation-like (Support L) \ G -defined the carrier of T -valued Function-like V48((Support L) \ G) V49((Support L) \ G, the carrier of T) Element of K15(K16(((Support L) \ G), the carrier of T))

K16(((Support L) \ G), the carrier of T) is Relation-like set

K15(K16(((Support L) \ G), the carrier of T)) is non empty set

L +* (((Support L) \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

Support (n,T,L,G) is functional Element of K15((Bags n))

n is set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

{} (Bags n) is ext-real non positive non negative empty proper Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding Element of K15((Bags n))

K15((Bags n)) is non empty set

T is non empty ZeroStr

the carrier of T is non empty set

K16((Bags n), the carrier of T) is non empty Relation-like set

K15(K16((Bags n), the carrier of T)) is non empty set

0_ (n,T) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) finite-Support monomial-like Constant Element of K15(K16((Bags n), the carrier of T))

L is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

Support L is functional Element of K15((Bags n))

(n,T,L,(Support L)) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

(Support L) \ (Support L) is set

0. T is zero Element of the carrier of T

the ZeroF of T is Element of the carrier of T

((Support L) \ (Support L)) --> (0. T) is Relation-like (Support L) \ (Support L) -defined the carrier of T -valued Function-like V48((Support L) \ (Support L)) V49((Support L) \ (Support L), the carrier of T) Element of K15(K16(((Support L) \ (Support L)), the carrier of T))

K16(((Support L) \ (Support L)), the carrier of T) is Relation-like set

K15(K16(((Support L) \ (Support L)), the carrier of T)) is non empty set

L +* (((Support L) \ (Support L)) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

(n,T,L,({} (Bags n))) is non empty Relation-like Bags n -defined the carrier of T -valued Function-like V48( Bags n) V49( Bags n, the carrier of T) Element of K15(K16((Bags n), the carrier of T))

(Support L) \ ({} (Bags n)) is set

((Support L) \ ({} (Bags n))) --> (0. T) is Relation-like (Support L) \ ({} (Bags n)) -defined the carrier of T -valued Function-like V48((Support L) \ ({} (Bags n))) V49((Support L) \ ({} (Bags n)), the carrier of T) Element of K15(K16(((Support L) \ ({} (Bags n))), the carrier of T))

K16(((Support L) \ ({} (Bags n))), the carrier of T) is Relation-like set

K15(K16(((Support L) \ ({} (Bags n))), the carrier of T)) is non empty set

L +* (((Support L) \ ({} (Bags n))) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

{} --> (0. T) is ext-real non positive non negative empty Relation-like non-empty empty-yielding {} -defined the carrier of T -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V48( {} ) V49( {} , the carrier of T) V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding Element of K15(K16({}, the carrier of T))

K16({}, the carrier of T) is Relation-like set

K15(K16({}, the carrier of T)) is non empty set

L +* ({} --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

dom ({} --> (0. T)) is ext-real non positive non negative empty non proper Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V31() cardinal {} -element co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V52() V53() irreflexive complex V240() V241() V242() V243() FinSequence-yielding finite-support Function-yielding Element of K15({})

K15({}) is non empty finite V31() set

L +* {} is non empty Relation-like Function-like set

(Support L) --> (0. T) is Relation-like Support L -defined the carrier of T -valued Function-like V48( Support L) V49( Support L, the carrier of T) Element of K15(K16((Support L), the carrier of T))

K16((Support L), the carrier of T) is Relation-like set

K15(K16((Support L), the carrier of T)) is non empty set

dom ((Support L) --> (0. T)) is functional Element of K15((Support L))

K15((Support L)) is non empty set

g2 is set

dom (n,T,L,({} (Bags n))) is non empty functional Element of K15((Bags n))

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(n,T,L,({} (Bags n))) . h is Element of the carrier of T

((Support L) --> (0. T)) . h is set

(0_ (n,T)) . h is Element of the carrier of T

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(n,T,L,({} (Bags n))) . h is Element of the carrier of T

L . h is Element of the carrier of T

(0_ (n,T)) . h is Element of the carrier of T

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(n,T,L,({} (Bags n))) . h is Element of the carrier of T

(0_ (n,T)) . h is Element of the carrier of T

h is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n

(n,T,L,({} (Bags n))) . h is Element of the carrier of T

(0_ (n,T)) . h is Element of the carrier of T

(n,T,L,({} (Bags n))) . g2 is set

(0_ (n,T)) . g2 is set

dom (0_ (n,T)) is non empty functional Element of K15((Bags n))

n is epsilon-transitive epsilon-connected ordinal set

Bags n is non empty functional Element of K15((Bags n))

Bags n is non empty set

K15((Bags n)) is non empty set

K16((Bags n),(Bags n)) is non empty Relation-like set

K15(K16((Bags n),(Bags n))) is non empty set

L 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 addLoopStr

the carrier of L is non empty set

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

K15(K16((Bags n), the carrier of L)) is non empty set

g1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

G is non empty Relation-like Bags n -defined the carrier of L -valued Function-like V48( Bags n) V49( Bags n, the carrier of L) finite-Support Element of K15(K16((Bags n), the carrier of L))

Support G is functional finite Element of K15((Bags n))

K15((Bags n)) is non empty set

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

T is Relation-like Bags n -defined Bags n -valued V48( Bags n) V49( Bags n, Bags n) reflexive antisymmetric connected transitive Element of K15(K16((Bags n),(Bags n)))

g2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V52() V53() complex Element of NAT

g2 + 1 is ext-real positive non neg