:: POLYNOM6 semantic presentation

REAL is set

K48(REAL) is set

RAT is set
INT is set
K49(COMPLEX,COMPLEX) is set
K48(K49(COMPLEX,COMPLEX)) is set
K49(K49(COMPLEX,COMPLEX),COMPLEX) is set
K48(K49(K49(COMPLEX,COMPLEX),COMPLEX)) is set
K49(REAL,REAL) is set
K48(K49(REAL,REAL)) is set
K49(K49(REAL,REAL),REAL) is set
K48(K49(K49(REAL,REAL),REAL)) is set
K49(RAT,RAT) is set
K48(K49(RAT,RAT)) is set
K49(K49(RAT,RAT),RAT) is set
K48(K49(K49(RAT,RAT),RAT)) is set
K49(INT,INT) is set
K48(K49(INT,INT)) is set
K49(K49(INT,INT),INT) is set
K48(K49(K49(INT,INT),INT)) is set
K49(NAT,NAT) is non trivial non finite set
K49(K49(NAT,NAT),NAT) is non trivial non finite set
K48(K49(K49(NAT,NAT),NAT)) is non trivial non finite set

K48(NAT) is non trivial non finite set
K48(NAT) is non trivial non finite set
K259() is set

{} is set

{{},1} is finite set
K454() is set
K48(K454()) is set
K455() is Element of K48(K454())

K49(NAT,REAL) is set
K48(K49(NAT,REAL)) is set

Bags {} is functional non empty Element of K48(())
Bags {} is non empty set
K48(()) is set
is non empty trivial finite 1 -element set
L is non empty doubleLoopStr
id L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V28( the carrier of L, the carrier of L) unity-preserving multiplicative additive RingHomomorphism Element of K48(K49( the carrier of L, the carrier of L))
the carrier of L is non empty set
K49( the carrier of L, the carrier of L) is set
K48(K49( the carrier of L, the carrier of L)) is set
id the carrier of L is Relation-like the carrier of L -defined the carrier of L -valued Function-like one-to-one non empty total Element of K48(K49( the carrier of L, the carrier of L))
K795( the carrier of L,(id L)) is Element of K48( the carrier of L)
K48( the carrier of L) is set
rng (id L) is set
[#] L is non empty non proper Element of K48( the carrier of L)

L is set
o1 \/ L is set
P2 is set

dom L is set
dom o2 is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

support P2 is finite set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of P1 : b1 in support P2 } is set
{ (o1 +^ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of P1 : verum } is set
f is set

support f is set

() \/ { H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of P1 : b1 in support P2 } is set
f is set
f . f is set
dom f is set
y is set

o1 \/ { (o1 +^ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of P1 : verum } is set

f is set
dom f is set
f . f is set

dom P1 is set
1P2 is set

((o1 +^ o2) \ o1) \/ o1 is set
(o1 +^ o2) \/ o1 is set

dom 1P1 is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

1P1 is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set
1P1 is set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

dom L is set
P1 is set

(o1,o2,L,P2) . 1P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

K49(o1,NAT) is set
K48(K49(o1,NAT)) is set
dom P2 is set
P1 is set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set
(o1,o2,L,P2) . (o1 +^ 1P1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1 +^ 1P1) -^ o1 is epsilon-transitive epsilon-connected ordinal set
P2 . ((o1 +^ 1P1) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

K49(o2,NAT) is set
K48(K49(o2,NAT)) is set
dom (o1,o2,L,P2) is set
P1 is set
(o1,o2,L,P2) . P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

(o1,o2,L,P2) . 1P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

K49((o1 +^ o2),NAT) is set
K48(K49((o1 +^ o2),NAT)) is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set
Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

support (L | o1) is set

P1 is set

dom (L | o1) is set
[P1,((L | o1) . P1)] is set
{P1,((L | o1) . P1)} is finite set
{P1} is non empty trivial finite 1 -element set
{{P1,((L | o1) . P1)},{P1}} is finite V41() set

dom L is set
dom (L | o1) is set

{ (b1 -^ o1) where b1 is epsilon-transitive epsilon-connected ordinal Element of o1 +^ P2 : ( o1 c= b1 & b1 in support L ) } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of o1 +^ P2 : b1 in support L } is set
f is set

f is set

support f is set
f is set
f . f is set
dom f is set

f is set
dom f is set
f . f is set

y is set
dom P1 is set

(o1,o2,P1,f) . s is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,P1,f) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

L . (o1 +^ (s -^ o1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,P1,f) . s is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,P1,f) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

1P2 is set

(o1,o2,L,P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

1P2 is set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set
(o1,o2,L,P1) . (o1 +^ f) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
P1 . ((o1 +^ f) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

Bags o1 is functional non empty Element of K48((Bags o1))
Bags o1 is non empty set
K48((Bags o1)) is set

the carrier of o2 is non empty set
K49((Bags o1), the carrier of o2) is set
K48(K49((Bags o1), the carrier of o2)) is set
L is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
P2 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
L + P2 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
(L + P2) *' P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
L *' P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
P2 *' P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))
(L *' P1) + (P2 *' P1) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) Element of K48(K49((Bags o1), the carrier of o2))

((L + P2) *' P1) . 1P2 is Element of the carrier of o2

Sum f is Element of the carrier of o2

dom f is finite Element of K48(NAT)
(P2 *' P1) . 1P2 is Element of the carrier of o2

Sum f is Element of the carrier of o2

dom f is finite Element of K48(NAT)
(L *' P1) . 1P2 is Element of the carrier of o2

Sum y is Element of the carrier of o2

dom y is finite Element of K48(NAT)
(len f) -tuples_on the carrier of o2 is functional non empty FinSequence-membered FinSequenceSet of the carrier of o2

dom kk is finite len f -element Element of K48(NAT)

dom (s + kk) is finite len f -element Element of K48(NAT)

f /. g is Element of the carrier of o2

(L + P2) . g is Element of the carrier of o2
P1 . g is Element of the carrier of o2
((L + P2) . g) * (P1 . g) is Element of the carrier of o2
s /. g is Element of the carrier of o2
s . g is set
kk /. g is Element of the carrier of o2
kk . g is set

P2 . g9 is Element of the carrier of o2
P1 . b is Element of the carrier of o2
(P2 . g9) * (P1 . b) is Element of the carrier of o2

L . b1 is Element of the carrier of o2
P1 . b2 is Element of the carrier of o2
(L . b1) * (P1 . b2) is Element of the carrier of o2
f . g is set
L . g is Element of the carrier of o2
P2 . g is Element of the carrier of o2
(L . g) + (P2 . g) is Element of the carrier of o2
((L . g) + (P2 . g)) * (P1 . g) is Element of the carrier of o2
(L . g) * (P1 . g) is Element of the carrier of o2
(P2 . g) * (P1 . g) is Element of the carrier of o2
((L . g) * (P1 . g)) + ((P2 . g) * (P1 . g)) is Element of the carrier of o2
(s + kk) . g is set

Sum s is Element of the carrier of o2
Sum kk is Element of the carrier of o2
(Sum s) + (Sum kk) is Element of the carrier of o2
((L *' P1) + (P2 *' P1)) . 1P2 is Element of the carrier of o2

1_ (Polynom-Ring (o1,o2)) is Element of the carrier of (Polynom-Ring (o1,o2))
the carrier of (Polynom-Ring (o1,o2)) is non empty set
K502((Polynom-Ring (o1,o2))) is Element of the carrier of (Polynom-Ring (o1,o2))
the OneF of (Polynom-Ring (o1,o2)) is Element of the carrier of (Polynom-Ring (o1,o2))
0. (Polynom-Ring (o1,o2)) is V115( Polynom-Ring (o1,o2)) Element of the carrier of (Polynom-Ring (o1,o2))
the ZeroF of (Polynom-Ring (o1,o2)) is Element of the carrier of (Polynom-Ring (o1,o2))
1_ (o1,o2) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
Bags o1 is functional non empty Element of K48((Bags o1))
Bags o1 is non empty set
K48((Bags o1)) is set
the carrier of o2 is non empty non trivial set
K49((Bags o1), the carrier of o2) is set
K48(K49((Bags o1), the carrier of o2)) is set
0_ (o1,o2) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))

(0_ (o1,o2)) . (EmptyBag o1) is Element of the carrier of o2
0. o2 is V115(o2) Element of the carrier of o2
the ZeroF of o2 is Element of the carrier of o2
1_ o2 is Element of the carrier of o2
K502(o2) is V115(o2) Element of the carrier of o2
the OneF of o2 is Element of the carrier of o2
the carrier of (Polynom-Ring (o1,o2)) is non empty set
L is Element of the carrier of (Polynom-Ring (o1,o2))
P2 is Element of the carrier of (Polynom-Ring (o1,o2))
P1 is Element of the carrier of (Polynom-Ring (o1,o2))
P2 + P1 is Element of the carrier of (Polynom-Ring (o1,o2))
L * (P2 + P1) is Element of the carrier of (Polynom-Ring (o1,o2))
L * P2 is Element of the carrier of (Polynom-Ring (o1,o2))
L * P1 is Element of the carrier of (Polynom-Ring (o1,o2))
(L * P2) + (L * P1) is Element of the carrier of (Polynom-Ring (o1,o2))
(P2 + P1) * L is Element of the carrier of (Polynom-Ring (o1,o2))
P2 * L is Element of the carrier of (Polynom-Ring (o1,o2))
P1 * L is Element of the carrier of (Polynom-Ring (o1,o2))
(P2 * L) + (P1 * L) is Element of the carrier of (Polynom-Ring (o1,o2))
Bags o1 is functional non empty Element of K48((Bags o1))
Bags o1 is non empty set
K48((Bags o1)) is set
the carrier of o2 is non empty non trivial set
K49((Bags o1), the carrier of o2) is set
K48(K49((Bags o1), the carrier of o2)) is set
1P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
1P2 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
1P1 *' 1P2 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
f is Element of the carrier of (Polynom-Ring (o1,o2))
y is Element of the carrier of (Polynom-Ring (o1,o2))
f * y is Element of the carrier of (Polynom-Ring (o1,o2))
f is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
1P1 *' f is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
s is Element of the carrier of (Polynom-Ring (o1,o2))
f * s is Element of the carrier of (Polynom-Ring (o1,o2))
y + s is Element of the carrier of (Polynom-Ring (o1,o2))
1P2 + f is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
P2 + P1 is Element of the carrier of (Polynom-Ring (o1,o2))
L * (P2 + P1) is Element of the carrier of (Polynom-Ring (o1,o2))
1P1 *' (1P2 + f) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
(1P1 *' 1P2) + (1P1 *' f) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
(L * P2) + (L * P1) is Element of the carrier of (Polynom-Ring (o1,o2))
1P2 *' 1P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
y * f is Element of the carrier of (Polynom-Ring (o1,o2))
f *' 1P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
s * f is Element of the carrier of (Polynom-Ring (o1,o2))
(P2 + P1) * L is Element of the carrier of (Polynom-Ring (o1,o2))
(1P2 + f) *' 1P1 is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
(1P2 *' 1P1) + (f *' 1P1) is Relation-like Bags o1 -defined the carrier of o2 -valued Function-like V28( Bags o1, the carrier of o2) V250( Bags o1,o2) Element of K48(K49((Bags o1), the carrier of o2))
(P2 * L) + (P1 * L) is Element of the carrier of (Polynom-Ring (o1,o2))

Bags o1 is functional non empty Element of K48((Bags o1))
Bags o1 is non empty set
K48((Bags o1)) is set

the carrier of (Polynom-Ring (o2,L)) is non empty set
K49((Bags o1), the carrier of (Polynom-Ring (o2,L))) is set
K48(K49((Bags o1), the carrier of (Polynom-Ring (o2,L)))) is set

Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
Bags (o1 +^ o2) is non empty set
K48((Bags (o1 +^ o2))) is set
the carrier of L is non empty non trivial set
K49((Bags (o1 +^ o2)), the carrier of L) is set
K48(K49((Bags (o1 +^ o2)), the carrier of L)) is set
Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
P2 is Relation-like Bags o1 -defined the carrier of (Polynom-Ring (o2,L)) -valued Function-like V28( Bags o1, the carrier of (Polynom-Ring (o2,L))) V250( Bags o1, Polynom-Ring (o2,L)) Element of K48(K49((Bags o1), the carrier of (Polynom-Ring (o2,L))))
{ (o1,o2,a1,b1) where b1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2 : ex b2 being Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L)) st
( b2 = P2 . a1 & b1 in Support b2 )
}
is set

Support P2 is functional Element of K48((Bags o1))
K48((Bags o1)) is set
{ } is set
1P1 is set

P2 . 1P2 is Element of the carrier of (Polynom-Ring (o2,L))
{ (o1,o2,1P2,b1) where b1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2 : ex b2 being Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L)) st
( b2 = P2 . 1P2 & b1 in Support b2 )
}
is set

f is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
Support f is functional finite Element of K48((Bags o2))
K48((Bags o2)) is set
{ } is set
y is set

kk is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
Support kk is functional finite Element of K48((Bags o2))

P2 . 1P2 is Element of the carrier of (Polynom-Ring (o2,L))
f is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
f . f is Element of the carrier of L
1P1 is Relation-like Bags (o1 +^ o2) -defined the carrier of L -valued Function-like V28( Bags (o1 +^ o2), the carrier of L) Element of K48(K49((Bags (o1 +^ o2)), the carrier of L))
1P2 is Relation-like Bags (o1 +^ o2) -defined the carrier of L -valued Function-like V28( Bags (o1 +^ o2), the carrier of L) Element of K48(K49((Bags (o1 +^ o2)), the carrier of L))
Support 1P2 is functional Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set
union { } is set
f is set
1P2 . f is set
0. L is V115(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L

P2 . f is Element of the carrier of (Polynom-Ring (o2,L))
{ (o1,o2,f,b1) where b1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2 : ex b2 being Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L)) st
( b2 = P2 . f & b1 in Support b2 )
}
is set

s is set
1P2 . (o1,o2,f,y) is Element of the carrier of L
g is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))

P2 . kk is Element of the carrier of (Polynom-Ring (o2,L))

g . g is Element of the carrier of L
0. (Polynom-Ring (o2,L)) is V115( Polynom-Ring (o2,L)) Element of the carrier of (Polynom-Ring (o2,L))
the ZeroF of (Polynom-Ring (o2,L)) is Element of the carrier of (Polynom-Ring (o2,L))
0_ (o2,L) is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
Support g is functional finite Element of K48((Bags o2))
K48((Bags o2)) is set
f is set
f is set

P2 . y is Element of the carrier of (Polynom-Ring (o2,L))
{ (o1,o2,y,b1) where b1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2 : ex b2 being Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L)) st
( b2 = P2 . y & b1 in Support b2 )
}
is set

kk is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
Support kk is functional finite Element of K48((Bags o2))
K48((Bags o2)) is set
kk is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
Support kk is functional finite Element of K48((Bags o2))
K48((Bags o2)) is set
kk . s is Element of the carrier of L
0. L is V115(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
1P2 . (o1,o2,y,s) is Element of the carrier of L
g is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))

P2 . g is Element of the carrier of (Polynom-Ring (o2,L))

g . g is Element of the carrier of L
g . s is Element of the carrier of L
f is Relation-like Bags (o1 +^ o2) -defined the carrier of L -valued Function-like V28( Bags (o1 +^ o2), the carrier of L) V250( Bags (o1 +^ o2),L) Element of K48(K49((Bags (o1 +^ o2)), the carrier of L))

f . f is Element of the carrier of L
kk is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))

P2 . y is Element of the carrier of (Polynom-Ring (o2,L))

kk . s is Element of the carrier of L

P2 . g is Element of the carrier of (Polynom-Ring (o2,L))
g is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))
g . g is Element of the carrier of L
P1 is Relation-like Bags (o1 +^ o2) -defined the carrier of L -valued Function-like V28( Bags (o1 +^ o2), the carrier of L) V250( Bags (o1 +^ o2),L) Element of K48(K49((Bags (o1 +^ o2)), the carrier of L))
1P1 is Relation-like Bags (o1 +^ o2) -defined the carrier of L -valued Function-like V28( Bags (o1 +^ o2), the carrier of L) V250( Bags (o1 +^ o2),L) Element of K48(K49((Bags (o1 +^ o2)), the carrier of L))

P1 . 1P2 is Element of the carrier of L
1P1 . 1P2 is Element of the carrier of L
y is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))

P2 . f is Element of the carrier of (Polynom-Ring (o2,L))

y . f is Element of the carrier of L
g is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) V250( Bags o2,L) Element of K48(K49((Bags o2), the carrier of L))

P2 . s is Element of the carrier of (Polynom-Ring (o2,L))

g . kk is Element of the carrier of L

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

f is set

(o1,o2,L,P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,L,P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

(o1,o2,L,P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,P2,1P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,L,P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

g is set

(o1,o2,1P2,f) . (o1 +^ g) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,P1) . (o1 +^ g) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set
P1 . ((o1 +^ g) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

g is set

(o1,o2,1P2,f) . g is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,P1) . g is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,1P2,f) . g is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is non empty set
Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set

(o1,o2,P2,1P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,L,P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
dom (o1,o2,P2,1P1) is set

(o1,o2,L,P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

o1 +^ (1P2 -^ o1) is epsilon-transitive epsilon-connected ordinal set

(o1,o2,P2,1P1) . (o1 +^ f) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

1P1 . ((o1 +^ f) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,L,P1) . (o1 +^ f) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
P1 . ((o1 +^ f) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
f is set

(o1,o2,L,P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,P2,1P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

(o1,o2,L,P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,L,P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1,o2,L,P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P1) . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

(o1 +^ 1P2) -^ o1 is epsilon-transitive epsilon-connected ordinal set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set

(o1 +^ 1P2) -^ o1 is epsilon-transitive epsilon-connected ordinal set
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is set
(o1,o2,P2,1P1) . (o1 +^ 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
1P1 . ((o1 +^ 1P2) -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,L,P1) . (o1 +^ 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

Bags o1 is non empty set
Bags o1 is functional non empty Element of K48((Bags o1))
K48((Bags o1)) is set

Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set

Bags (o1 +^ o2) is functional non empty Element of K48((Bags (o1 +^ o2)))
Bags (o1 +^ o2) is non empty set
K48((Bags (o1 +^ o2))) is set
(Bags (o1 +^ o2)) * is functional non empty FinSequence-membered FinSequenceSet of Bags (o1 +^ o2)

dom () is finite Element of K48(NAT)

dom P1 is finite Element of K48(NAT)

dom f is finite Element of K48(NAT)