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