:: GROEB_3 semantic presentation

REAL is set

K15(REAL) is non empty set

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

RAT is set
INT is set

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

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

n is 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

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,G] is V24() set
{L,G} is non empty functional finite 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

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

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 + 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,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

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,G] is V24() set
{L,G} is non empty functional finite 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
[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) -' 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) -' 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

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

[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,G] is V24() set
{L,G} is non empty functional finite 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) -' 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

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

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

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

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

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

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

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

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

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

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

g1 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

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

K16((Bags n),(Bags n)) is non empty Relation-like set
K15(K16((Bags n),(Bags n))) 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))
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

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

K16((),(Support (G *' L))) is Relation-like finite set
K15(K16((),(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 (G *' L))))

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

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

g2 .: () 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

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

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

(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

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

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

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

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

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

h . rp2 is set

dom h is non empty Element of K15(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

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

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

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

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

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

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

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

((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) + ((- L) . g2) 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))

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

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

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

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

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

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

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))
() \ G is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ G) --> (0. T) is Relation-like () \ G -defined the carrier of T -valued Function-like V48(() \ G) V49(() \ G, the carrier of T) Element of K15(K16((() \ G), the carrier of T))
K16((() \ G), the carrier of T) is Relation-like set
K15(K16((() \ G), the carrier of T)) is non empty set
L +* ((() \ G) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set
h is set

dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
(L +* ((() \ G) --> (0. T))) . h is set
((() \ G) --> (0. T)) . h is set
(L +* ((() \ G) --> (0. T))) . h is set
dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set

(L +* ((() \ G) --> (0. T))) . h is set
L . h is Element of the carrier of T
(L +* ((() \ G) --> (0. T))) . h is set

dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
(L +* ((() \ G) --> (0. T))) . h is set

dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
(L +* ((() \ G) --> (0. T))) . h is set
h is set
dom L is non empty functional Element of K15((Bags n))
dom (L +* ((() \ G) --> (0. T))) is non empty set
(Bags n) \/ (() \ 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))
() \ G is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ G) --> (0. T) is Relation-like () \ G -defined the carrier of T -valued Function-like V48(() \ G) V49(() \ G, the carrier of T) Element of K15(K16((() \ G), the carrier of T))
K16((() \ G), the carrier of T) is Relation-like set
K15(K16((() \ G), the carrier of T)) is non empty set
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

(L +* ((() \ G) --> (0. T))) . h is set
dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
L . h is Element of the carrier of T
dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
L . h is Element of the carrier of T
dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
L . h is Element of the carrier of T

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))
() \ G is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ G) --> (0. T) is Relation-like () \ G -defined the carrier of T -valued Function-like V48(() \ G) V49(() \ G, the carrier of T) Element of K15(K16((() \ G), the carrier of T))
K16((() \ G), the carrier of T) is Relation-like set
K15(K16((() \ G), the carrier of T)) is non empty set
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))
() \ G is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ G) --> (0. T) is Relation-like () \ G -defined the carrier of T -valued Function-like V48(() \ G) V49(() \ G, the carrier of T) Element of K15(K16((() \ G), the carrier of T))
K16((() \ G), the carrier of T) is Relation-like set
K15(K16((() \ G), the carrier of T)) is non empty set
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))
() /\ G is set
h is set

dom ((() \ G) --> (0. T)) is Element of K15((() \ G))
K15((() \ G)) is non empty set
(L +* ((() \ G) --> (0. T))) . h is set
((() \ G) --> (0. T)) . h is set
L . h is Element of the carrier of T
h is set

(L +* ((() \ G) --> (0. T))) . h is set
L . h is Element of the carrier of T

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

(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))
() \ G is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ G) --> (0. T) is Relation-like () \ G -defined the carrier of T -valued Function-like V48(() \ G) V49(() \ G, the carrier of T) Element of K15(K16((() \ G), the carrier of T))
K16((() \ G), the carrier of T) is Relation-like set
K15(K16((() \ G), the carrier of T)) is non empty set
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
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,()) 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))
() \ () is set
0. T is zero Element of the carrier of T
the ZeroF of T is Element of the carrier of T
(() \ ()) --> (0. T) is Relation-like () \ () -defined the carrier of T -valued Function-like V48(() \ ()) V49(() \ (), the carrier of T) 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
(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))
() \ ({} (Bags n)) is set
(() \ ({} (Bags n))) --> (0. T) is 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))
K16((() \ ({} (Bags n))), the carrier of T) is Relation-like set
K15(K16((() \ ({} (Bags n))), the carrier of T)) is non empty set
L +* ((() \ ({} (Bags n))) --> (0. T)) is non empty Relation-like the carrier of T -valued Function-like set

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

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

() --> (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((), the carrier of T))
K16((), the carrier of T) is Relation-like set
K15(K16((), the carrier of T)) is non empty set
dom (() --> (0. T)) is functional Element of K15(())
K15(()) is non empty set
g2 is set
dom (n,T,L,({} (Bags n))) is non empty functional Element of K15((Bags n))

(n,T,L,({} (Bags n))) . h is Element of the carrier of T
(() --> (0. T)) . h is set
(0_ (n,T)) . h is Element of the carrier of T

(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

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

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

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

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

g2 + 1 is ext-real positive non neg