:: POLYNOM6 semantic presentation

REAL is set

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

K48(REAL) is set

COMPLEX 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

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

K48(NAT) is non trivial non finite set

K48(NAT) is non trivial non finite set

K259() is set

1 is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive Element of NAT

{} is set

the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() V32() finite V41() cardinal {} -element FinSequence-membered ext-real set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V31() V32() finite V41() cardinal {} -element FinSequence-membered ext-real set

{{},1} is finite set

K454() is set

K48(K454()) is set

K455() is Element of K48(K454())

2 is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive Element of NAT

K49(NAT,REAL) is set

K48(K49(NAT,REAL)) is set

1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

K671() is Relation-like NAT -defined Function-like total set

3 is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real positive Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

Bags {} is functional non empty Element of K48((Bags {}))

Bags {} is non empty set

K48((Bags {})) 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)

o1 is epsilon-transitive epsilon-connected ordinal set

o2 is epsilon-transitive epsilon-connected ordinal set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

L is set

o1 \/ L is set

P2 is set

P1 is epsilon-transitive epsilon-connected ordinal set

o1 +^ P1 is epsilon-transitive epsilon-connected ordinal set

P1 is epsilon-transitive epsilon-connected ordinal set

P1 -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

o1 is epsilon-transitive epsilon-connected ordinal set

o2 is epsilon-transitive epsilon-connected ordinal non empty set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

o2 +^ o1 is epsilon-transitive epsilon-connected ordinal set

o1 is epsilon-transitive epsilon-connected ordinal set

o2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

P2 is epsilon-transitive epsilon-connected ordinal set

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

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

dom L is set

dom o2 is set

P1 is epsilon-transitive epsilon-connected ordinal set

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal 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

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

K48((o1 +^ o2)) is set

P2 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

P1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P1 is epsilon-transitive epsilon-connected ordinal set

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

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

1P1 -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

P1 is epsilon-transitive epsilon-connected ordinal non empty set

support P2 is finite set

{ H

{ (o1 +^ b

f is set

f is epsilon-transitive epsilon-connected ordinal set

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

f -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

f -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

f is Relation-like o1 +^ o2 -defined Function-like total set

support f is set

support L is finite set

(support L) \/ { H

f is set

f . f is set

dom f is set

y is set

s is epsilon-transitive epsilon-connected ordinal Element of P1

o1 +^ s is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

o1 +^ s is epsilon-transitive epsilon-connected ordinal set

o1 \/ { (o1 +^ b

y is epsilon-transitive epsilon-connected ordinal set

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

y -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

y is epsilon-transitive epsilon-connected ordinal Element of P1

o1 +^ y is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

o1 +^ y is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

kk is epsilon-transitive epsilon-connected ordinal set

L . kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

kk -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

f is set

dom f is set

f . f is set

y is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

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

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

y is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

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

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

y is epsilon-transitive epsilon-connected ordinal set

f is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

y is epsilon-transitive epsilon-connected ordinal set

f . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

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

y -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

s is epsilon-transitive epsilon-connected ordinal set

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

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

s is epsilon-transitive epsilon-connected ordinal set

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

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

P1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

dom P1 is set

1P2 is set

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

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

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

(o1 +^ o2) \/ o1 is set

f is epsilon-transitive epsilon-connected ordinal set

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

f is epsilon-transitive epsilon-connected ordinal set

f -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

f is epsilon-transitive epsilon-connected ordinal set

dom 1P1 is set

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 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

(o1,o2,L,P2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal 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

P1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

1P1 is set

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 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

(o1,o2,L,P2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal 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

1P2 is epsilon-transitive epsilon-connected ordinal set

1P2 -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

K48((o1 +^ o2)) is set

P1 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

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

EmptyBag o1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

EmptyBag (o1 +^ o2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

EmptyBag o2 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

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 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

(o1,o2,L,P2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

dom L is set

P1 is set

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

1P1 is epsilon-transitive epsilon-connected ordinal set

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

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

o1 --> 0 is Relation-like o1 -defined NAT -valued RAT -valued Function-like constant total V28(o1, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K48(K49(o1,NAT))

K49(o1,NAT) is set

K48(K49(o1,NAT)) is set

dom P2 is set

P1 is set

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

1P1 is epsilon-transitive epsilon-connected ordinal set

o1 +^ 1P1 is epsilon-transitive epsilon-connected ordinal 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

o2 --> 0 is Relation-like o2 -defined NAT -valued RAT -valued Function-like constant total V28(o2, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K48(K49(o2,NAT))

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

1P1 is epsilon-transitive epsilon-connected ordinal set

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

K48((o1 +^ o2)) is set

1P1 -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

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

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

(o1 +^ o2) --> 0 is Relation-like o1 +^ o2 -defined NAT -valued RAT -valued Function-like constant total V28(o1 +^ o2, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K48(K49((o1 +^ o2),NAT))

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal 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

L is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

P1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 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

(o1,o2,P1,P2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

L | o1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

support (L | o1) is set

support L is finite set

P1 is set

(L | o1) . P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real 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

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

dom L is set

dom (L | o1) is set

P2 is epsilon-transitive epsilon-connected ordinal non empty set

o1 +^ P2 is epsilon-transitive epsilon-connected ordinal non empty set

P1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

{ (b

{ H

f is set

f is epsilon-transitive epsilon-connected ordinal Element of o1 +^ P2

f -^ o1 is epsilon-transitive epsilon-connected ordinal set

f is set

f is epsilon-transitive epsilon-connected ordinal Element of o2

o1 +^ f is epsilon-transitive epsilon-connected ordinal set

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

y is epsilon-transitive epsilon-connected ordinal Element of o2

o1 +^ y is epsilon-transitive epsilon-connected ordinal set

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

f is Relation-like o2 -defined Function-like total set

support f is set

f is set

f . f is set

dom f is set

y is epsilon-transitive epsilon-connected ordinal Element of P2

o1 +^ y is epsilon-transitive epsilon-connected ordinal set

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

s is epsilon-transitive epsilon-connected ordinal Element of o1 +^ P2

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

f is set

dom f is set

f . f is set

y is epsilon-transitive epsilon-connected ordinal Element of o2

o1 +^ y is epsilon-transitive epsilon-connected ordinal set

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

f 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

(o1,o2,P1,f) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

y is set

dom P1 is set

s is epsilon-transitive epsilon-connected ordinal set

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

P1 . s 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

L . y 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

s is epsilon-transitive epsilon-connected ordinal set

s -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

L . y 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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P1 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

(o1,o2,L,P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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 Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2

(o1,o2,P2,1P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P2 is set

f is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

1P2 is set

f is epsilon-transitive epsilon-connected ordinal set

o1 +^ f is epsilon-transitive epsilon-connected ordinal set

(o1 +^ f) -^ o1 is epsilon-transitive epsilon-connected ordinal 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

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

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

Bags o1 is non empty set

K48((Bags o1)) is set

o2 is non empty right_complementable Abelian add-associative right_zeroed associative right-distributive left-distributive distributive doubleLoopStr

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

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

decomp 1P2 is Relation-like NAT -defined 2 -tuples_on (Bags o1) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags o1)

2 -tuples_on (Bags o1) is functional non empty FinSequence-membered FinSequenceSet of Bags o1

len (decomp 1P2) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT

f is Relation-like NAT -defined the carrier of o2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of o2

Sum f is Element of the carrier of o2

len f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

dom f is finite Element of K48(NAT)

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

f is Relation-like NAT -defined the carrier of o2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of o2

Sum f is Element of the carrier of o2

len f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

dom f is finite Element of K48(NAT)

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

y is Relation-like NAT -defined the carrier of o2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of o2

Sum y is Element of the carrier of o2

len y is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

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

kk is Relation-like NAT -defined the carrier of o2 -valued Function-like finite len f -element FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on the carrier of o2

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

s is Relation-like NAT -defined the carrier of o2 -valued Function-like finite len f -element FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on the carrier of o2

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

s + kk is Relation-like NAT -defined the carrier of o2 -valued Function-like finite len f -element FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on the carrier of o2

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

g is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set

(decomp 1P2) /. g is Relation-like NAT -defined Bags o1 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)

f /. g is Element of the carrier of o2

g is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

g is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

<*g,g*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set

(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

g9 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

b is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

<*g9,b*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support 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

b1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

b2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

<*b1,b2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set

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

len (s + kk) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

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

o1 is epsilon-transitive epsilon-connected ordinal set

o2 is non empty non degenerated non trivial right_complementable Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

Polynom-Ring (o1,o2) is non empty right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive right_unital well-unital left_unital doubleLoopStr

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

EmptyBag o1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

o1 is epsilon-transitive epsilon-connected ordinal non empty set

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

Bags o1 is non empty set

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal non empty set

L is non empty non degenerated non trivial right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

Polynom-Ring (o2,L) is non empty right_complementable strict add-associative right_zeroed doubleLoopStr

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

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal non empty 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,a

( b

Support P2 is functional Element of K48((Bags o1))

K48((Bags o1)) is set

{ H

1P1 is set

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

{ (o1,o2,1P2,b

( b

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

{ H

y is set

s 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

(o1,o2,1P2,s) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

1P1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

f 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

(o1,o2,1P2,f) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ 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 { H

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

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

y 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

(o1,o2,f,y) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

{ (o1,o2,f,b

( b

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

kk is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

g 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

(o1,o2,kk,g) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

y is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

{ (o1,o2,y,b

( b

s 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

(o1,o2,y,s) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

g is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

g 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

(o1,o2,g,g) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

y is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

s 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

(o1,o2,y,s) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

kk . s is Element of the carrier of L

g is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

g 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

(o1,o2,g,g) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

1P2 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

f 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

(o1,o2,f,f) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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

s is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

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

kk 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

(o1,o2,s,kk) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

g . kk is Element of the carrier of L

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P1 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

1P1 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

(o1,o2,L,P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

f is set

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

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

f . f is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

y is epsilon-transitive epsilon-connected ordinal set

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

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

y is epsilon-transitive epsilon-connected ordinal set

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

y -^ o1 is epsilon-transitive epsilon-connected ordinal set

P1 . (y -^ o1) 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

1P1 . (y -^ o1) 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 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

L is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P1 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

(o1,o2,P2,P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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 Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

f 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

(o1,o2,1P2,f) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

s is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

kk is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

g is set

s . g is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

kk . g is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

g is epsilon-transitive epsilon-connected ordinal set

o1 +^ g is epsilon-transitive epsilon-connected ordinal 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 +^ g) -^ o1 is epsilon-transitive epsilon-connected ordinal 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

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

y is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

g is set

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

y . 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

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

g is epsilon-transitive epsilon-connected ordinal set

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

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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal set

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

P1 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

(o1,o2,L,P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

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 Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2

(o1,o2,P2,1P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

1P2 is epsilon-transitive epsilon-connected ordinal 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

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

f is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

y is epsilon-transitive epsilon-connected ordinal set

f . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set

f . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real 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

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

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

P2 . 1P2 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

1P2 -^ o1 is epsilon-transitive epsilon-connected ordinal set

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

f is epsilon-transitive epsilon-connected ordinal set

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

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

o1 +^ f 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

(o1 +^ f) -^ o1 is epsilon-transitive epsilon-connected ordinal 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

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

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

y is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

1P1 . (1P2 -^ o1) 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

1P2 is epsilon-transitive epsilon-connected ordinal set

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

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

f is epsilon-transitive epsilon-connected ordinal 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

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

P2 . 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

1P2 is epsilon-transitive epsilon-connected ordinal set

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

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

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

f is epsilon-transitive epsilon-connected ordinal 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

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

f -^ o1 is epsilon-transitive epsilon-connected ordinal 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

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

1P1 . (f -^ o1) 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,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

o1 is epsilon-transitive epsilon-connected ordinal set

Bags o1 is non empty set

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

K48((Bags o1)) is set

o2 is epsilon-transitive epsilon-connected ordinal set

Bags o2 is non empty set

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

K48((Bags o2)) is set

o1 +^ o2 is epsilon-transitive epsilon-connected ordinal 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)

L is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

divisors L is Relation-like NAT -defined Bags o1 -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags o1

dom (divisors L) is finite Element of K48(NAT)

P2 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

divisors P2 is Relation-like NAT -defined Bags o2 -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags o2

len (divisors P2) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT

(o1,o2,L,P2) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags (o1 +^ o2)

divisors (o1,o2,L,P2) is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like one-to-one non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags (o1 +^ o2)

P1 is Relation-like NAT -defined (Bags (o1 +^ o2)) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (Bags (o1 +^ o2)) *

dom P1 is finite Element of K48(NAT)

FlattenSeq P1 is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support Element of (Bags (o1 +^ o2)) *

Del (P1,1) is Relation-like NAT -defined (Bags (o1 +^ o2)) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (Bags (o1 +^ o2)) *

P1 /. 1 is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support Element of (Bags (o1 +^ o2)) *

(divisors L) /. 1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

f is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags (o1 +^ o2)

1P2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1

len f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT

dom f is finite Element of K48(NAT)

len (divisors L) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT

len P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT