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) + b1) where b1 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n : b1 in Support L } is 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))
Support G is functional finite Element of K15((Bags n))
{(term G)} is non empty trivial functional finite 1 -element set
{ (b1 + b2) where b1, b2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n : ( b1 in Support G & b2 in Support L ) } is 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
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
{ (b1 + b2) where b1, b2 is Relation-like n -defined RAT -valued Function-like V48(n) V240() V241() V242() V243() finite-support Element of Bags n : ( b1 in Support G & b2 in Support L ) } 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
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