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
{ 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
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) \/ { 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
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 +^ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of P1 : verum } is set
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
{ (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 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,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
{ H1(b1) where b1 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 : b1 in Support P2 } is set
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,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
{ H2(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 : b1 in Support f } is set
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 { H1(b1) where b1 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 : b1 in Support P2 } 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
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,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))
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,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
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
P1 . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*(P1 . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial Function-yielding V36() finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
<*(P1 . 1)*> ^ (Del (P1,1)) is Relation-like NAT -defined Function-like non empty Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
f 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)) *
<*f*> is Relation-like NAT -defined (Bags (o1 +^ o2)) * -valued Function-like constant non empty trivial Function-yielding V36() finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support V259() M54( Bags (o1 +^ o2),1, len f)
len f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
FlattenSeq <*f*> 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)) *
1P1 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)) *
FlattenSeq 1P1 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)) *
(FlattenSeq <*f*>) ^ (FlattenSeq 1P1) 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)) *
f ^ (FlattenSeq 1P1) 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)) *
dom (FlattenSeq P1) is finite Element of K48(NAT)
BagOrder (o1 +^ o2) is Relation-like Bags (o1 +^ o2) -defined Bags (o1 +^ o2) -valued total V65() V68() V72() being_linear-order Element of K48(K49((Bags (o1 +^ o2)),(Bags (o1 +^ o2))))
K49((Bags (o1 +^ o2)),(Bags (o1 +^ o2))) is set
K48(K49((Bags (o1 +^ o2)),(Bags (o1 +^ o2)))) is set
s is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(FlattenSeq P1) /. 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)
(FlattenSeq P1) /. 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)
[((FlattenSeq P1) /. s),((FlattenSeq P1) /. kk)] is set
{((FlattenSeq P1) /. s),((FlattenSeq P1) /. kk)} is functional finite set
{((FlattenSeq P1) /. s)} is functional non empty trivial finite 1 -element set
{{((FlattenSeq P1) /. s),((FlattenSeq P1) /. kk)},{((FlattenSeq P1) /. s)}} is finite V41() set
(FlattenSeq P1) . s is Relation-like Function-like set
g is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . g) is finite Element of K48(NAT)
g -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (g -' 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)) *
Card (P1 | (g -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (g -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (g -' 1)))) + g is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . g) . g is set
P1 /. g 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) /. 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
g9 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)
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
len g9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom g9 is finite Element of K48(NAT)
(divisors P2) /. 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
g9 /. 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)
b 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,b) 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)
Seg (len g9) is finite len g9 -element Element of K48(NAT)
dom (divisors P2) is finite Element of K48(NAT)
(FlattenSeq P1) . kk is Relation-like Function-like set
b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
b2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . b1) is finite Element of K48(NAT)
b1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (b1 -' 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)) *
Card (P1 | (b1 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (b1 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (b1 -' 1)))) + b2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . b1) . b2 is set
P1 /. b1 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) /. b1 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 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)
Q1 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 b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom b is finite Element of K48(NAT)
(divisors L) . b1 is Relation-like Function-like set
b /. b2 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 P2) /. b2 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
b 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,Q1,b) 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)
Seg (len b) is finite len b -element Element of K48(NAT)
(divisors P2) . b2 is Relation-like Function-like set
b19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
b29 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . b19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . b19) is finite Element of K48(NAT)
b19 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (b19 -' 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)) *
Card (P1 | (b19 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (b19 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (b19 -' 1)))) + b29 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . b19) . b29 is set
P1 /. b19 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) /. b19 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
c1 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)
Q1 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 c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom c1 is finite Element of K48(NAT)
(divisors L) . b19 is Relation-like Function-like set
c1 /. b29 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 P2) /. b29 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
c2 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,Q1,c2) 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)
Seg (len c1) is finite len c1 -element Element of K48(NAT)
(divisors P2) . b29 is Relation-like Function-like set
b1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b2 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
Q1 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)
b 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
b19 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,b,b19) 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 L) . g is Relation-like Function-like set
(divisors P2) . g is Relation-like Function-like set
b 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)
b29 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
Q1 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,b29,Q1) 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)
c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
c2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . c1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . c1) is finite Element of K48(NAT)
c1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (c1 -' 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)) *
Card (P1 | (c1 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (c1 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (c1 -' 1)))) + c2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . c1) . c2 is set
P1 /. c1 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) /. c1 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
rFFb2 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)
Q19 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 rFFb2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom rFFb2 is finite Element of K48(NAT)
(divisors P2) /. c2 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
rFFb2 /. c2 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)
rFFb2 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,Q19,rFFb2) 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)
Seg (len rFFb2) is finite len rFFb2 -element Element of K48(NAT)
(divisors L) . c1 is Relation-like Function-like set
(divisors P2) . c2 is Relation-like Function-like set
c1 - 1 is V31() V32() ext-real set
P1 | c1 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)) *
Card (P1 | c1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Card P1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
(Card P1) | c1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
(Card P1) | (g -' 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
F 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)) *
<*F*> is Relation-like NAT -defined (Bags (o1 +^ o2)) * -valued Function-like constant non empty trivial Function-yielding V36() finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support V259() M54( Bags (o1 +^ o2),1, len F)
len F is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
c1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(c1 -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real positive Element of NAT
s 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 | (c1 -' 1)) ^ s 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)) *
Card s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
(Card (P1 | (c1 -' 1))) ^ (Card s) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
card F is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
<*(card F)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite-support Element of 1 -tuples_on NAT
(Card (P1 | (c1 -' 1))) ^ <*(card F)*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | c1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
card (P1 . c1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (c1 -' 1)))) + (card (P1 . c1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
K48((Bags o1)) is set
BagOrder o1 is Relation-like Bags o1 -defined Bags o1 -valued total V65() V68() V72() being_linear-order Element of K48(K49((Bags o1),(Bags o1)))
K49((Bags o1),(Bags o1)) is set
K48(K49((Bags o1),(Bags o1))) is set
F is functional non empty finite Element of K48((Bags o1))
SgmX ((BagOrder o1),F) 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
field (BagOrder o1) is set
K48((Bags o2)) is set
BagOrder o2 is Relation-like Bags o2 -defined Bags o2 -valued total V65() V68() V72() being_linear-order Element of K48(K49((Bags o2),(Bags o2)))
K49((Bags o2),(Bags o2)) is set
K48(K49((Bags o2),(Bags o2))) is set
s is functional non empty finite Element of K48((Bags o2))
SgmX ((BagOrder o2),s) 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
field (BagOrder o2) is set
[((divisors L) /. g),((divisors L) /. c1)] is set
{((divisors L) /. g),((divisors L) /. c1)} is functional finite set
{((divisors L) /. g)} is functional non empty trivial finite 1 -element set
{{((divisors L) /. g),((divisors L) /. c1)},{((divisors L) /. g)}} is finite V41() set
[((divisors P2) /. g),((divisors P2) /. c2)] is set
{((divisors P2) /. g),((divisors P2) /. c2)} is functional finite set
{((divisors P2) /. g)} is functional non empty trivial finite 1 -element set
{{((divisors P2) /. g),((divisors P2) /. c2)},{((divisors P2) /. g)}} is finite V41() set
K48((Bags (o1 +^ o2))) is set
rng (FlattenSeq P1) is finite set
s is functional non empty finite Element of K48((Bags (o1 +^ o2)))
K48((Bags o2)) is set
BagOrder o2 is Relation-like Bags o2 -defined Bags o2 -valued total V65() V68() V72() being_linear-order Element of K48(K49((Bags o2),(Bags o2)))
K49((Bags o2),(Bags o2)) is set
K48(K49((Bags o2),(Bags o2))) is set
kk is functional non empty finite Element of K48((Bags o2))
SgmX ((BagOrder o2),kk) 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
field (BagOrder o2) is set
rng (SgmX ((BagOrder o2),kk)) is finite set
g is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
K48((Bags o1)) is set
BagOrder o1 is Relation-like Bags o1 -defined Bags o1 -valued total V65() V68() V72() being_linear-order Element of K48(K49((Bags o1),(Bags o1)))
K49((Bags o1),(Bags o1)) is set
K48(K49((Bags o1),(Bags o1))) is set
g is functional non empty finite Element of K48((Bags o1))
SgmX ((BagOrder o1),g) 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
field (BagOrder o1) is set
rng (SgmX ((BagOrder o1),g)) is finite set
g is set
(FlattenSeq P1) . g is Relation-like Function-like set
g9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . g9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . g9) is finite Element of K48(NAT)
g9 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (g9 -' 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)) *
Card (P1 | (g9 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (g9 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (g9 -' 1)))) + b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . g9) . b is set
P1 /. g9 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) /. g9 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
b2 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)
b1 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 b2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom b2 is finite Element of K48(NAT)
(divisors L) . g9 is Relation-like Function-like set
Q1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(divisors P2) /. b 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
b2 /. b 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)
b 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,b1,b) 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)
Seg (len b2) is finite len b2 -element Element of K48(NAT)
dom (divisors P2) is finite Element of K48(NAT)
(divisors P2) . b is Relation-like Function-like set
b is Relation-like o2 -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 Element of Bags o1
g9 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,g9) 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)
b is set
(divisors L) . b is Relation-like Function-like set
b1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 /. b1 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) /. b1 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
Q1 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)
b2 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 Q1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom Q1 is finite Element of K48(NAT)
rng (divisors P2) is finite set
dom (divisors P2) is finite Element of K48(NAT)
b is set
(divisors P2) . b is Relation-like Function-like set
Seg (len (divisors P2)) is non empty finite len (divisors P2) -element Element of K48(NAT)
P1 . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (P1 . b1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
Seg (len (P1 . b1)) is finite len (P1 . b1) -element Element of K48(NAT)
dom (P1 . b1) is finite Element of K48(NAT)
b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(divisors P2) /. b 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
Q1 /. b 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)
b19 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,b2,b19) 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)
b1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (b1 -' 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)) *
Card (P1 | (b1 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (b1 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (b1 -' 1)))) + b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . b1) . b is set
(FlattenSeq P1) . ((Sum (Card (P1 | (b1 -' 1)))) + b) is Relation-like Function-like set
field (BagOrder (o1 +^ o2)) is set
SgmX ((BagOrder (o1 +^ o2)),s) 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)
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
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 o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1
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 -' L 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 o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o2
1P2 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
1P2 -' 1P1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(o1,o2,P2,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)
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,L,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)
(o1,o2,P2,1P2) -' (o1,o2,L,1P1) is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(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)
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)
(o1 +^ o2) \ o1 is Element of K48((o1 +^ o2))
K48((o1 +^ o2)) is 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
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
f . (y -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,P2,1P2) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(o1,o2,L,1P1) . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
((o1,o2,P2,1P2) . y) -' ((o1,o2,L,1P1) . y) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P2 . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(P2 . y) -' ((o1,o2,L,1P1) . y) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
L . y is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(P2 . y) -' (L . y) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
1P2 . (y -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(1P2 . (y -^ o1)) -' ((o1,o2,L,1P1) . y) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
1P1 . (y -^ o1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() V34() finite cardinal ext-real set
(1P2 . (y -^ o1)) -' (1P1 . (y -^ o1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
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
2 -tuples_on (Bags o1) is functional non empty FinSequence-membered FinSequenceSet 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
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
2 -tuples_on (Bags (o1 +^ o2)) is functional non empty FinSequence-membered FinSequenceSet of Bags (o1 +^ o2)
(2 -tuples_on (Bags (o1 +^ o2))) * is functional non empty FinSequence-membered FinSequenceSet of 2 -tuples_on (Bags (o1 +^ o2))
2 -tuples_on (Bags o2) is functional non empty FinSequence-membered FinSequenceSet 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
decomp L 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)
dom (decomp 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
decomp P2 is Relation-like NAT -defined 2 -tuples_on (Bags o2) -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 o2)
len (decomp 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)
decomp (o1,o2,L,P2) is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -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 +^ o2))
P1 is Relation-like NAT -defined (2 -tuples_on (Bags (o1 +^ o2))) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) *
dom P1 is finite Element of K48(NAT)
FlattenSeq P1 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
len P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
Seg (len P1) is finite len P1 -element Element of K48(NAT)
(Bags (o1 +^ o2)) * is functional non empty FinSequence-membered FinSequenceSet of Bags (o1 +^ o2)
1P1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . 1P1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . 1P1) is finite Element of K48(NAT)
len (P1 . 1P1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
Seg (len (P1 . 1P1)) is finite len (P1 . 1P1) -element Element of K48(NAT)
rng P1 is finite set
f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . 1P1) . f is set
1P2 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
1P2 /. f is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
f is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
f . 1 is Relation-like Function-like set
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 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,kk*> is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
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)
1P2 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)
dom 1P2 is finite Element of K48(NAT)
f 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)) *
dom f is finite set
dom f is finite Element of K48(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(P1 . 1P1) . f is set
f . f is Relation-like Function-like set
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 is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
y . 1 is Relation-like Function-like set
1P1 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 1P1 is finite Element of K48(NAT)
Card 1P1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
dom (Card 1P1) is finite Element of K48(NAT)
Card P1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
dom (Card P1) is finite Element of K48(NAT)
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)
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
1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
1P1 /. 1P2 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) /. 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
dom (decomp P2) is finite Element of K48(NAT)
dom (divisors P2) is finite Element of K48(NAT)
P1 /. 1P2 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
(decomp L) /. 1P2 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)
s is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
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 o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags o1
<*f,y*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len s is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom s is finite Element of K48(NAT)
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)
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)
dom (1P1 /. 1P2) is finite Element of K48(NAT)
P1 . 1P2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . 1P2) is finite Element of K48(NAT)
len (P1 . 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(divisors P2) /. 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
f /. 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)
(P1 . 1P2) . kk is set
(1P1 /. 1P2) . kk is Relation-like Function-like set
g is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
g . 1 is Relation-like Function-like set
(decomp P2) /. kk is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
s /. kk is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
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
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
<*g,g*> is Relation-like NAT -defined Bags o2 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
(o1,o2,f,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)
(o1,o2,y,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)
<*(o1,o2,f,g),(o1,o2,y,g)*> is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
f . kk is Relation-like Function-like set
dom (decomp P2) is finite Element of K48(NAT)
dom (divisors P2) is finite Element of K48(NAT)
1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(Card 1P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(Card P1) . 1P2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
1P1 . 1P2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
card (1P1 . 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
1P1 /. 1P2 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) /. 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
P1 /. 1P2 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
(decomp L) /. 1P2 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)
card (1P1 /. 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . 1P2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
card (P1 . 1P2) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
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)
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
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)
kk is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
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
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
<*y,s*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom kk is finite Element of K48(NAT)
len (Card 1P1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
len (Card P1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
f is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
len f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
FlattenSeq 1P1 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)) *
len (FlattenSeq 1P1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
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)
dom f is finite Element of K48(NAT)
1P2 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
divisors 1P2 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)
f is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(divisors 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)
f /. f is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
y is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
1P2 -' y is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*y,(1P2 -' y)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
f . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
s is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
P1 . s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (P1 . s) is finite Element of K48(NAT)
s -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
P1 | (s -' 1) is Relation-like NAT -defined (2 -tuples_on (Bags (o1 +^ o2))) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) *
Card (P1 | (s -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (P1 | (s -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (P1 | (s -' 1)))) + kk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(P1 . s) . kk is set
1P1 /. s 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) /. 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
g 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)
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
len g is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom g is finite Element of K48(NAT)
P1 /. s is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
(decomp L) /. s 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)
b is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
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
g9 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,g9*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom b is finite Element of K48(NAT)
L -' g is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*g,(L -' g)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
(decomp P2) /. kk is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
b /. kk is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
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
b2 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
<*b1,b2*> is Relation-like NAT -defined Bags o2 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
(o1,o2,g,b1) 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,g9,b2) 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,g,b1),(o1,o2,g9,b2)*> is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
P2 -' b1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
dom (FlattenSeq 1P1) is finite Element of K48(NAT)
(FlattenSeq 1P1) . f is Relation-like Function-like set
b is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
b19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
1P1 . b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (1P1 . b) is finite Element of K48(NAT)
b -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
1P1 | (b -' 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)) *
Card (1P1 | (b -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (1P1 | (b -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (1P1 | (b -' 1)))) + b19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(1P1 . b) . b19 is set
(Card P1) | (s -' 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
(Card 1P1) | (b -' 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
(divisors P2) /. 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
g /. 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)
b29 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,b29) 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)
<*b1,(P2 -' b1)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
1P1 . s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(1P1 . s) . kk is set
g . kk is Relation-like Function-like set
b 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
Q1 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,b,Q1) 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,g9,Q1) 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)
b . kk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (divisors 1P2) is finite Element of K48(NAT)
o1 is epsilon-transitive epsilon-connected ordinal non empty set
o2 is epsilon-transitive epsilon-connected ordinal non empty set
o1 +^ o2 is epsilon-transitive epsilon-connected ordinal non empty set
L 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 (o2,L) is non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
Polynom-Ring (o1,(Polynom-Ring (o2,L))) is non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
Polynom-Ring ((o1 +^ o2),L) is non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
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 non trivial 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
1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) is non empty non trivial set
K502((Polynom-Ring (o1,(Polynom-Ring (o2,L))))) is V115( Polynom-Ring (o1,(Polynom-Ring (o2,L)))) Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
the OneF of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
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
1_ (Polynom-Ring ((o1 +^ o2),L)) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
the carrier of (Polynom-Ring ((o1 +^ o2),L)) is non empty non trivial set
K502((Polynom-Ring ((o1 +^ o2),L))) is V115( Polynom-Ring ((o1 +^ o2),L)) Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
the OneF of (Polynom-Ring ((o1 +^ o2),L)) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
f is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f 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,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))
y is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
s 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,L,s) 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))
K49( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L))) is set
K48(K49( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L)))) is set
f is Relation-like the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) -defined the carrier of (Polynom-Ring ((o1 +^ o2),L)) -valued Function-like V28( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L))) Element of K48(K49( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L))))
f is Relation-like the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))) -defined the carrier of (Polynom-Ring ((o1 +^ o2),L)) -valued Function-like V28( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L))) Element of K48(K49( the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L)))), the carrier of (Polynom-Ring ((o1 +^ o2),L))))
y is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
s is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
y + s is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . (y + s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
f . y is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
f . s is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
(f . y) + (f . s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
kk is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
g is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
y + s is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . (y + s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
g9 is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
b is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
b1 is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
b 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))
b2 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))
Q1 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))
b is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b . b is Element of the carrier of L
b2 . b is Element of the carrier of L
Q1 . b is Element of the carrier of L
(b2 . b) + (Q1 . b) is Element of the carrier of L
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
g 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))))
b19 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,L,g) 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))
(o1,o2,L,g) . b19 is Element of the carrier of L
c1 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))
b29 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 . b29 is Element of the carrier of (Polynom-Ring (o2,L))
Q1 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,b29,Q1) 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)
c1 . Q1 is Element of the carrier of L
g 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,L,g) 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))
(o1,o2,L,g) . b19 is Element of the carrier of L
rFFb2 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))
c2 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 . c2 is Element of the carrier of (Polynom-Ring (o2,L))
Q19 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,c2,Q19) 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)
rFFb2 . Q19 is Element of the carrier of L
g + g 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,L,(g + g)) 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))
(o1,o2,L,(g + g)) . b19 is Element of the carrier of L
s 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))
rFFb2 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 + g) . rFFb2 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,rFFb2,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 . F is Element of the carrier of L
rFFb2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(g + g) . rFFb2 is Element of the carrier of (Polynom-Ring (o2,L))
g . rFFb2 is Element of the carrier of (Polynom-Ring (o2,L))
g . rFFb2 is Element of the carrier of (Polynom-Ring (o2,L))
(g . rFFb2) + (g . rFFb2) is Element of the carrier of (Polynom-Ring (o2,L))
c1 + rFFb2 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 . Q1 is Element of the carrier of L
rFFb2 . Q1 is Element of the carrier of L
(c1 . Q1) + (rFFb2 . Q1) is Element of the carrier of L
((o1,o2,L,g) . b19) + (Q1 . b) is Element of the carrier of L
b2 + Q1 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 . y) + (f . s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
y is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
s is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
kk is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
g is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . y is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
f . s is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
g9 is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
b is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
y * s is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . (y * s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
g 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))))
g 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))))
g *' g 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))))
f . (g *' g) is set
Q1 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))
2 -tuples_on (Bags (o1 +^ o2)) is functional non empty FinSequence-membered FinSequenceSet of Bags (o1 +^ o2)
b1 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))
b2 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))
b is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
Q1 . b is Element of the carrier of L
decomp b is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -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 +^ o2))
len (decomp b) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT
Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set
b19 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)
b29 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
Q1 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,b29,Q1) 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)
c1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(g *' g) . c1 is Element of the carrier of (Polynom-Ring (o2,L))
decomp c1 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 c1) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT
c2 is Relation-like NAT -defined the carrier of (Polynom-Ring (o2,L)) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of (Polynom-Ring (o2,L))
Sum c2 is Element of the carrier of (Polynom-Ring (o2,L))
len c2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom c2 is finite Element of K48(NAT)
Q19 is set
c2 . Q19 is set
rng c2 is finite set
Q19 is Relation-like Function-like Function-yielding V36() set
rFFb2 is Relation-like Function-like set
dom rFFb2 is set
F is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
Seg F is finite F -element Element of K48(NAT)
rFFb2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng rFFb2 is finite set
F is set
rng Q19 is set
dom rFFb2 is finite Element of K48(NAT)
s is set
rFFb2 . s is set
Q19 . s is Relation-like Function-like set
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
rng (Q19 . s) is set
dom (Q19 . s) is set
(Q19 . s) . Q1 is set
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
decomp Q1 is Relation-like NAT -defined 2 -tuples_on (Bags o2) -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 o2)
2 -tuples_on (Bags o2) is functional non empty FinSequence-membered FinSequenceSet of Bags o2
len (decomp Q1) is epsilon-transitive epsilon-connected ordinal natural non empty V31() V32() finite cardinal ext-real Element of NAT
Seg (len c2) is finite len c2 -element Element of K48(NAT)
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
F is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(decomp c1) /. F 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)
dom (decomp c1) is finite Element of K48(NAT)
s is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
rFFb2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*s,rFFb2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
s + rFFb2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . s is Element of the carrier of (Polynom-Ring (o2,L))
g . rFFb2 is Element of the carrier of (Polynom-Ring (o2,L))
Sr is Element of the carrier of (Polynom-Ring (o2,L))
gg is Element of the carrier of (Polynom-Ring (o2,L))
ff 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 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))
Seg (len (decomp Q1)) is non empty finite len (decomp Q1) -element Element of K48(NAT)
c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(decomp Q1) /. c1 is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
dom (decomp Q1) is finite Element of K48(NAT)
c2 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
Q1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*c2,Q1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
c2 + Q1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
ff . c2 is Element of the carrier of L
G . Q1 is Element of the carrier of L
(ff . c2) * (G . Q1) is Element of the carrier of L
k is Element of the carrier of L
c1 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
dom c1 is finite Element of K48(NAT)
c2 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
len c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
Q1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(decomp Q1) /. Q1 is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
c1 /. Q1 is Element of the carrier of L
F is Relation-like NAT -defined the carrier of L * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of L *
dom F is finite Element of K48(NAT)
FlattenSeq F is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
s is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
Sum s is Element of the carrier of L
len s is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom s is finite Element of K48(NAT)
Sum F is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
len (Sum F) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
b is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . b is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
(o1,o2,L,(g *' g)) 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))
rFFb2 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
dom rFFb2 is finite Element of K48(NAT)
dom (Sum F) is finite Element of K48(NAT)
Sr is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
rFFb2 . Sr is set
(Sum F) . Sr is set
(decomp c1) /. Sr 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)
c2 /. Sr is Element of the carrier of (Polynom-Ring (o2,L))
gg is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
ff is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*gg,ff*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
g . gg is Element of the carrier of (Polynom-Ring (o2,L))
g . ff is Element of the carrier of (Polynom-Ring (o2,L))
(g . gg) * (g . ff) is Element of the carrier of (Polynom-Ring (o2,L))
F /. Sr is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
Q1 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 set
g . G is Element of the carrier of (Polynom-Ring (o2,L))
k 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))
c1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . c1 is Element of the carrier of (Polynom-Ring (o2,L))
c2 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*G,c1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
len c2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom c2 is finite Element of K48(NAT)
Q1 *' k 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))
(Q1 *' k) . Q1 is Element of the carrier of L
i is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum i is Element of the carrier of L
len i is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom i is finite Element of K48(NAT)
Seg (len i) is finite len i -element Element of K48(NAT)
j is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
i /. j is Element of the carrier of L
i . j is set
(decomp Q1) /. j is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
c2 /. j is Element of the carrier of L
i9 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
j9 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*i9,j9*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
Q1 . i9 is Element of the carrier of L
k . j9 is Element of the carrier of L
(Q1 . i9) * (k . j9) is Element of the carrier of L
c1 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
c2 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*c1,c2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
Q1 . c1 is Element of the carrier of L
k . c2 is Element of the carrier of L
(Q1 . c1) * (k . c2) is Element of the carrier of L
c2 . j is set
Q19 . Sr is Relation-like Function-like set
(Q19 . Sr) . Q1 is set
(Sum F) /. Sr is Element of the carrier of L
K49(NAT, the carrier of (Polynom-Ring (o2,L))) is non trivial non finite set
K48(K49(NAT, the carrier of (Polynom-Ring (o2,L)))) is non trivial non finite set
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))
gg is Relation-like NAT -defined the carrier of (Polynom-Ring (o2,L)) -valued Function-like V28( NAT , the carrier of (Polynom-Ring (o2,L))) Element of K48(K49(NAT, the carrier of (Polynom-Ring (o2,L))))
gg . (len c2) is Element of the carrier of (Polynom-Ring (o2,L))
gg . 0 is Element of the carrier of (Polynom-Ring (o2,L))
ff is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
gg . ff 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 . Q1 is Element of the carrier of L
c1 is Element of the carrier of L
c2 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))
c2 . Q1 is Element of the carrier of L
K49(NAT, the carrier of L) is non trivial non finite set
K48(K49(NAT, the carrier of L)) is non trivial non finite set
ff is Relation-like NAT -defined the carrier of L -valued Function-like V28( NAT , the carrier of L) Element of K48(K49(NAT, the carrier of L))
(2 -tuples_on (Bags (o1 +^ o2))) * is functional non empty FinSequence-membered FinSequenceSet of 2 -tuples_on (Bags (o1 +^ o2))
G is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(decomp c1) /. 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)
dom (decomp c1) is finite Element of K48(NAT)
c1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
c2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*c1,c2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
c1 + c2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
Q1 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
k 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
Seg (len (decomp Q1)) is non empty finite len (decomp Q1) -element Element of K48(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(decomp Q1) /. i is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
dom (decomp Q1) is finite Element of K48(NAT)
j is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
i9 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*j,i9*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
j + i9 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
j9 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,Q1,j9) 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)
c1 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,k,c1) 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,Q1,j9),(o1,o2,k,c1)*> is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
c2 is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
<*j9,c1*> is Relation-like NAT -defined Bags o2 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
i is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
dom i is finite Element of K48(NAT)
j is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
<*Q1,k*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len i is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
i9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(decomp Q1) /. i9 is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
i /. i9 is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
G is Relation-like NAT -defined (2 -tuples_on (Bags (o1 +^ o2))) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) *
dom G is finite Element of K48(NAT)
c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
G /. c1 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
(decomp c1) /. c1 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)
Card F is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
dom (Card F) is finite Element of K48(NAT)
Card G is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(Card F) . c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
(Card G) . c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real set
F . c1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
card (F . c1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
F /. c1 is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
(decomp c1) /. c1 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)
G /. c1 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
card (F /. c1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
G . c1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
card (G . c1) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
i 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))
c2 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . c2 is Element of the carrier of (Polynom-Ring (o2,L))
j 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))
Q1 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . Q1 is Element of the carrier of (Polynom-Ring (o2,L))
k is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*c2,Q1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
len k is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom k is finite Element of K48(NAT)
c1 is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
i9 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
j9 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
<*i9,j9*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len c1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom c1 is finite Element of K48(NAT)
(o1,o2,L,(g *' g)) . b19 is Element of the carrier of L
Q1 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))
c1 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 *' g) . c1 is Element of the carrier of (Polynom-Ring (o2,L))
c2 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,c1,c2) 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)
Q1 . c2 is Element of the carrier of L
decomp c1 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)
dom (decomp c1) is finite Element of K48(NAT)
FlattenSeq G is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
len rFFb2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
k + 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
rFFb2 . (k + 1) is set
ff . (k + 1) is Element of the carrier of L
ff . k is Element of the carrier of L
i is Element of the carrier of L
(ff . k) + i is Element of the carrier of L
c2 /. (k + 1) is Element of the carrier of (Polynom-Ring (o2,L))
gg . k is Element of the carrier of (Polynom-Ring (o2,L))
gg . (k + 1) is Element of the carrier of (Polynom-Ring (o2,L))
j 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))
i9 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))
j9 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))
c1 is Element of the carrier of (Polynom-Ring (o2,L))
c2 is Element of the carrier of (Polynom-Ring (o2,L))
cc1 is Element of the carrier of (Polynom-Ring (o2,L))
c2 . (k + 1) is set
cb2 is Element of the carrier of (Polynom-Ring (o2,L))
cb1 is Element of the carrier of (Polynom-Ring (o2,L))
cc2 is Element of the carrier of (Polynom-Ring (o2,L))
cb1 + cc2 is Element of the carrier of (Polynom-Ring (o2,L))
j . Q1 is Element of the carrier of L
j9 . Q1 is Element of the carrier of L
i9 + j 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))
(i9 + j) . Q1 is Element of the carrier of L
i9 . Q1 is Element of the carrier of L
(i9 . Q1) + (j . Q1) is Element of the carrier of 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))
ff . 0 is Element of the carrier of L
(0_ (o2,L)) . Q1 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
Sr 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))
Sr . Q1 is Element of the carrier of L
ff . (len rFFb2) is Element of the carrier of L
Sum rFFb2 is Element of the carrier of L
dom (Card G) is finite Element of K48(NAT)
len (Card F) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
len (Card G) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(decomp b) /. k is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
s /. k is Element of the carrier of L
(FlattenSeq F) . k is set
i is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
F . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (F . i) is finite Element of K48(NAT)
i -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
F | (i -' 1) is Relation-like NAT -defined the carrier of L * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of the carrier of L *
Card (F | (i -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (F | (i -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (F | (i -' 1)))) + j is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(F . i) . j is set
dom (decomp b) is finite Element of K48(NAT)
(decomp b) . k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
j9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
G . i9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (G . i9) is finite Element of K48(NAT)
i9 -' 1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real non negative Element of NAT
G | (i9 -' 1) is Relation-like NAT -defined (2 -tuples_on (Bags (o1 +^ o2))) * -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) *
Card (G | (i9 -' 1)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum (Card (G | (i9 -' 1))) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum (Card (G | (i9 -' 1)))) + j9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(G . i9) . j9 is set
(Card F) | (i -' 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum ((Card F) | (i -' 1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum ((Card F) | (i -' 1))) + j is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Card G) | (i9 -' 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V49() complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of NAT
Sum ((Card G) | (i9 -' 1)) is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
(Sum ((Card G) | (i9 -' 1))) + j9 is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
c1 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
c2 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*c1,c2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
c1 + c2 is Relation-like o1 +^ o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
cc1 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,L,g) 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))
(o1,o2,L,g) . cc1 is Element of the carrier of L
Q1 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))
cb1 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 . cb1 is Element of the carrier of (Polynom-Ring (o2,L))
cb2 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,cb1,cb2) 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)
Q1 . cb2 is Element of the carrier of L
F /. i is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
(decomp c1) /. i 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)
pa19 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))
a19 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . a19 is Element of the carrier of (Polynom-Ring (o2,L))
qb19 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))
b19 is Relation-like o1 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
g . b19 is Element of the carrier of (Polynom-Ring (o2,L))
Fk is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*a19,b19*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
len Fk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom Fk is finite Element of K48(NAT)
G /. i is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Element of (2 -tuples_on (Bags (o1 +^ o2))) *
Gk is Relation-like NAT -defined 2 -tuples_on (Bags (o1 +^ o2)) -valued Function-like Function-yielding V36() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on (Bags (o1 +^ o2))
ga19 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
gb19 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
<*ga19,gb19*> is Relation-like NAT -defined Bags o1 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o1)
len Gk is epsilon-transitive epsilon-connected ordinal natural V31() V32() finite cardinal ext-real Element of NAT
dom Gk is finite Element of K48(NAT)
G . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp Q1) /. j is Relation-like NAT -defined Bags o2 -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
Gk /. j is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
ga199 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
gb199 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
<*ga199,gb199*> is Relation-like NAT -defined Bags o2 -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags o2)
(o1,o2,ga19,ga199) 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,gb19,gb199) 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,ga19,ga199),(o1,o2,gb19,gb199)*> is Relation-like NAT -defined Bags (o1 +^ o2) -valued Function-like non empty Function-yielding V36() finite 2 -element FinSequence-like FinSubsequence-like finite-support Element of 2 -tuples_on (Bags (o1 +^ o2))
(G . i) . j is set
Fk /. j is Element of the carrier of L
a199 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
b199 is Relation-like o2 -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
<*a199,b199*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
pa19 . a199 is Element of the carrier of L
qb19 . b199 is Element of the carrier of L
(pa19 . a199) * (qb19 . b199) is Element of the carrier of L
b1 . c1 is Element of the carrier of L
b2 . c2 is Element of the carrier of L
(b1 . c1) * (b2 . c2) is Element of the carrier of L
cc2 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,L,g) 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))
(o1,o2,L,g) . cc2 is Element of the carrier of L
Q1 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))
cb1 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 . cb1 is Element of the carrier of (Polynom-Ring (o2,L))
cb2 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,cb1,cb2) 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)
Q1 . cb2 is Element of the carrier of L
s . k is set
b1 *' b2 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 . y) * (f . s) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
1P1 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,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 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))
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)
(o1,o2,L,1P1) . y is Element of the carrier of L
1P2 . y is Element of the carrier of L
1_ ((o1 +^ o2),L) 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))
(1_ ((o1 +^ o2),L)) . y is Element of the carrier of L
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
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
1P1 . 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
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)
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
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
1_ (o1,(Polynom-Ring (o2,L))) 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))))
(1_ (o1,(Polynom-Ring (o2,L)))) . s is Element of the carrier of (Polynom-Ring (o2,L))
1_ (Polynom-Ring (o2,L)) is Element of the carrier of (Polynom-Ring (o2,L))
K502((Polynom-Ring (o2,L))) is V115( Polynom-Ring (o2,L)) Element of the carrier of (Polynom-Ring (o2,L))
the OneF of (Polynom-Ring (o2,L)) is Element of the carrier of (Polynom-Ring (o2,L))
1_ (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))
(1_ (o2,L)) . kk is Element of the carrier of L
1_ L is Element of the carrier of L
K502(L) is V115(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
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)
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
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
1_ (o1,(Polynom-Ring (o2,L))) 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))))
(1_ (o1,(Polynom-Ring (o2,L)))) . s is Element of the carrier of (Polynom-Ring (o2,L))
1_ (Polynom-Ring (o2,L)) is Element of the carrier of (Polynom-Ring (o2,L))
K502((Polynom-Ring (o2,L))) is V115( Polynom-Ring (o2,L)) Element of the carrier of (Polynom-Ring (o2,L))
the OneF of (Polynom-Ring (o2,L)) is Element of the carrier of (Polynom-Ring (o2,L))
1_ (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))
0. L is V115(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
1_ (o1,(Polynom-Ring (o2,L))) 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))))
(1_ (o1,(Polynom-Ring (o2,L)))) . s is Element of the carrier of (Polynom-Ring (o2,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))
0. L is V115(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
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)
f . (1_ (Polynom-Ring (o1,(Polynom-Ring (o2,L))))) is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
y is set
dom f is set
s is set
f . y is set
f . s is set
g is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
kk is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
f . g is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
g 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,L,g) 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 . kk is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
g 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,L,g) 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))
Bags o2 is functional non empty Element of K48((Bags o2))
Bags o2 is non empty set
K48((Bags o2)) is set
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
b1 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 . b1 is Element of the carrier of (Polynom-Ring (o2,L))
g . b1 is Element of the carrier of (Polynom-Ring (o2,L))
b 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,b1,b) 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)
b 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))
b . (o1,o2,b1,b) is Element of the carrier of L
Q1 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))
b19 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 . b19 is Element of the carrier of (Polynom-Ring (o2,L))
b29 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,b19,b29) 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)
Q1 . b29 is Element of the carrier of L
g9 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))
g9 . (o1,o2,b1,b) is Element of the carrier of L
Q19 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))
c1 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 . c1 is Element of the carrier of (Polynom-Ring (o2,L))
c2 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,c1,c2) 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)
Q19 . c2 is Element of the carrier of L
b2 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))
b2 . b is Element of the carrier of L
Q1 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))
Q1 . b is Element of the carrier of L
K795( the carrier of (Polynom-Ring ((o1 +^ o2),L)),f) is Element of K48( the carrier of (Polynom-Ring ((o1 +^ o2),L)))
K48( the carrier of (Polynom-Ring ((o1 +^ o2),L))) is set
rng f is set
Bags o2 is non empty set
Bags o2 is functional non empty Element of K48((Bags o2))
K48((Bags o2)) is set
y is set
s 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))
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 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)
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
K49((Bags (o1 +^ o2)),(Bags o1)) is set
K48(K49((Bags (o1 +^ o2)),(Bags o1))) is set
kk is Relation-like Bags (o1 +^ o2) -defined Bags o1 -valued Function-like V28( Bags (o1 +^ o2), Bags o1) Function-yielding V36() Element of K48(K49((Bags (o1 +^ o2)),(Bags o1)))
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 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)
s . (o1,o2,g,g) is Element of the carrier of L
g9 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 . g9 is Element of the carrier of L
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
g is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) Element of K48(K49((Bags o2), the carrier of L))
b 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)
b1 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
b2 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,b1,b2) 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)
Q1 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
K49((Bags (o1 +^ o2)),(Bags o2)) is set
K48(K49((Bags (o1 +^ o2)),(Bags o2))) is set
b is Relation-like Bags (o1 +^ o2) -defined Bags o2 -valued Function-like V28( Bags (o1 +^ o2), Bags o2) Function-yielding V36() Element of K48(K49((Bags (o1 +^ o2)),(Bags o2)))
g9 is Relation-like Bags o2 -defined the carrier of L -valued Function-like V28( Bags o2, the carrier of L) Element of K48(K49((Bags o2), the carrier of L))
Support g9 is functional Element of K48((Bags o2))
K48((Bags o2)) is set
Support s is functional finite Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set
b .: (Support s) is finite set
b1 is set
b2 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,b2) 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)
g9 . b1 is set
0. L is V115(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
s . (o1,o2,g,b2) is Element of the carrier of L
dom b is set
b . (o1,o2,g,b2) 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
b 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 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,b,b) 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)
b1 is Element of the carrier of (Polynom-Ring (o2,L))
b2 is Relation-like Function-like set
Q1 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,Q1) 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)
b2 . Q1 is set
b 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 . b is Element of the carrier of L
g 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))) Element of K48(K49((Bags o1), the carrier of (Polynom-Ring (o2,L))))
g 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))) Element of K48(K49((Bags o1), the carrier of (Polynom-Ring (o2,L))))
Support g is functional Element of K48((Bags o1))
K48((Bags o1)) is set
Support s is functional finite Element of K48((Bags (o1 +^ o2)))
K48((Bags (o1 +^ o2))) is set
kk .: (Support s) is finite set
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 Element of Bags o1
g . g9 is Element of the carrier of (Polynom-Ring (o2,L))
b is Relation-like Function-like set
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
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))
b1 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 b1 is functional finite Element of K48((Bags o2))
K48((Bags o2)) is set
b2 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,g9,b2) 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)
b1 . b2 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
s . (o1,o2,g9,b2) is Element of the carrier of L
dom kk is set
kk . (o1,o2,g9,b2) 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 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 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,b,b) 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 is Element of the carrier of (Polynom-Ring (o1,(Polynom-Ring (o2,L))))
K49((Bags o2), the carrier of L) is set
K48(K49((Bags o2), the carrier of L)) is set
g9 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))))
b 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,L,g9) 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))
(o1,o2,L,g9) . b is Element of the carrier of L
Q1 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))
b1 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
g9 . b1 is Element of the carrier of (Polynom-Ring (o2,L))
b2 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,b1,b2) 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)
Q1 . b2 is Element of the carrier of L
s . b is Element of the carrier of L
b is Relation-like Function-like set
f . g is Element of the carrier of (Polynom-Ring ((o1 +^ o2),L))
dom f is set