REAL is V72() V73() V74() V78() V292() V293() V295() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V290() V292() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V290() V292() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is V72() V78() set
RAT is V72() V73() V74() V75() V78() set
INT is V72() V73() V74() V75() V76() V78() set
[:REAL,REAL:] is Relation-like V62() V63() V64() set
bool [:REAL,REAL:] is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() ordinal natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V62() V63() V64() V65() V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V292() V293() V294() V295() set
1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
{{},1} is non empty finite V34() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
K377() is set
bool K377() is non empty set
K378() is Element of bool K377()
2 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:NAT,NAT:] is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like V62() V63() V64() set
bool [:NAT,REAL:] is non empty set
K239(1,NAT) is M10( NAT )
[:COMPLEX,COMPLEX:] is Relation-like V62() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V62() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like V62() V63() V64() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like RAT -valued V62() V63() V64() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V62() V63() V64() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued V62() V63() V64() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V62() V63() V64() set
bool [:[:INT,INT:],INT:] is non empty set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K859() is set
K637() is Relation-like NAT -defined Function-like total set
3 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Seg 1 is non empty trivial finite 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
{1} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
Seg 2 is non empty finite 2 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
{1,2} is non empty finite V34() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty Function-yielding V22() ordinal natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V49() V62() V63() V64() V65() V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V292() V293() V294() V295() Element of NAT
Bags {} is functional non empty Element of bool (Bags {})
Bags {} is non empty set
bool (Bags {}) is non empty set
{{}} is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng R is finite set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng X is finite set
(rng R) \/ (rng X) is finite set
R ^ X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
f0 is Relation-like Function-like set
dom f0 is set
R * f0 is Relation-like NAT -defined Function-like finite finite-support set
X * f0 is Relation-like NAT -defined Function-like finite finite-support set
(R ^ X) * f0 is Relation-like NAT -defined Function-like finite finite-support set
rng (R ^ X) is finite set
dom (X * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom X is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
cR is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len cR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
S ^ cR is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom ((R ^ X) * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom (R ^ X) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom (R * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
tcR is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom tcR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
(S ^ cR) . tcPR is set
S . tcPR is set
R . tcPR is set
f0 . (R . tcPR) is set
(R ^ X) . tcPR is set
f0 . ((R ^ X) . tcPR) is set
tcR . tcPR is set
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
0X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
(len R) + 0X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is set
(R ^ X) . tcPR is set
f0 . ((R ^ X) . tcPR) is set
X . 0X is set
f0 . (X . 0X) is set
cR . 0X is set
(S ^ cR) . tcPR is set
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
len (R ^ X) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(len S) + (len cR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len (S ^ cR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
<*{},{}*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
<*<*{},{}*>*> is Relation-like NAT -defined Function-like constant non empty trivial Function-yielding V22() finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
R is Relation-like non-empty empty-yielding 0 -defined RAT -valued Function-like one-to-one constant functional empty total Function-yielding V22() ordinal natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V62() V63() V64() V65() V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V292() V293() V294() V295() set
decomp R is Relation-like NAT -defined K239(2,(Bags 0)) -valued Function-like one-to-one non empty Function-yielding V22() finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of K239(2,(Bags 0))
Bags 0 is functional non empty Element of bool (Bags 0)
Bags 0 is non empty set
bool (Bags 0) is non empty set
K239(2,(Bags 0)) is M10( Bags 0)
EmptyBag {} is Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional empty total Function-yielding V22() ordinal natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V62() V63() V64() V65() V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V292() V293() V294() V295() Element of Bags {}
{} --> 0 is Relation-like non-empty empty-yielding {} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant functional empty total quasi_total Function-yielding V22() ordinal T-Sequence-like natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V62() V63() V64() V65() V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V292() V293() V294() V295() Element of bool [:{},NAT:]
[:{},NAT:] is Relation-like RAT -valued INT -valued V62() V63() V64() V65() set
bool [:{},NAT:] is non empty set
{0} is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:{},{0}:] is Relation-like RAT -valued INT -valued finite V62() V63() V64() V65() set
divisors R is Relation-like NAT -defined Bags 0 -valued Function-like one-to-one non empty Function-yielding V22() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags 0
<*{}*> is Relation-like NAT -defined Function-like constant non empty trivial Function-yielding V22() finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support set
len (divisors R) is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
dom (divisors R) is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
dom (decomp R) is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
(decomp R) . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(decomp R) /. 1 is Relation-like NAT -defined Bags 0 -valued Function-like Function-yielding V22() finite FinSequence-like FinSubsequence-like finite-support Element of K239(2,(Bags 0))
len (decomp R) is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
f0 is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
f0 | R is Relation-like R -defined X -defined RAT -valued Function-like finite V62() V63() V64() V65() finite-support set
tcR is set
{ b1 where b1 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT : not R <= b1 } is set
cR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
{ b1 where b1 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT : not X <= b1 } is set
X is set
R is set
f0 is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
f0 | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
tcR is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
tcR | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
cR is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
S is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
dom cR is Element of bool R
bool R is non empty set
dom S is Element of bool R
tcPR is set
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is set
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is set
X is set
R is set
f0 is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
f0 | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
tcR is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
tcR | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
f0 -' tcR is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(f0 -' tcR) | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
f0 + tcR is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(f0 + tcR) | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set
cR is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
S is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
cR -' S is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
cR + S is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
dom f0 is Element of bool X
bool X is non empty set
dom (f0 | R) is Element of bool R
bool R is non empty set
X /\ R is set
dom tcR is Element of bool X
dom (tcR | R) is Element of bool R
dom (f0 + tcR) is Element of bool X
dom ((f0 + tcR) | R) is Element of bool R
tcPR is set
((f0 + tcR) | R) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 + tcR) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 . tcPR) + (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) + (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) + (S . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR + S) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (f0 -' tcR) is Element of bool X
dom ((f0 -' tcR) | R) is Element of bool R
tcPR is set
((f0 -' tcR) | R) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 -' tcR) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 . tcPR) -' (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) -' (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) -' (S . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR -' S) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (cR -' S) is Element of bool R
dom (cR + S) is Element of bool R
R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set
f0 is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
R .--> X is Relation-like {R} -defined RAT -valued INT -valued Function-like one-to-one finite V62() V63() V64() V65() finite-support set
{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
{R} --> X is Relation-like {R} -defined RAT -valued INT -valued {X} -valued Function-like constant non empty total quasi_total finite V62() V63() V64() V65() finite-support Element of bool [:{R},{X}:]
{X} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:{R},{X}:] is Relation-like RAT -valued INT -valued non empty finite V62() V63() V64() V65() set
bool [:{R},{X}:] is non empty finite V34() set
f0 +* (R .--> X) is Relation-like RAT -valued Function-like V62() V63() V64() V65() set
dom f0 is finite Element of bool R
bool R is non empty finite V34() set
dom (f0 +* (R .--> X)) is set
dom (R .--> X) is trivial finite V34() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool {R}
bool {R} is non empty finite V34() set
(dom f0) \/ (dom (R .--> X)) is finite set
(dom f0) \/ {R} is non empty finite set
R \/ {R} is non empty finite set
succ R is set
cR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
cR | R is Relation-like R -defined R + 1 -defined RAT -valued Function-like finite V62() V63() V64() V65() finite-support set
cR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (cR | R) is finite Element of bool R
(R + 1) /\ R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() set
(succ R) /\ R is finite set
(R \/ {R}) /\ R is finite set
S is set
(cR | R) . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R .--> X) . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
tcR | R is Relation-like R -defined R + 1 -defined RAT -valued Function-like finite V62() V63() V64() V65() finite-support set
tcR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
cR | R is Relation-like R -defined R + 1 -defined RAT -valued Function-like finite V62() V63() V64() V65() finite-support set
cR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom tcR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
S is set
succ R is set
{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
R \/ {R} is non empty finite set
tcR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R + 1) /\ R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() set
dom f0 is finite Element of bool R
bool R is non empty finite V34() set
tcR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom cR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
EmptyBag (R + 1) is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
(R,0,(EmptyBag R)) is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set
X is set
succ R is set
{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
R \/ {R} is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
(EmptyBag (R + 1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(EmptyBag R) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,(EmptyBag R)) | R is Relation-like R -defined R + 1 -defined RAT -valued Function-like finite V62() V63() V64() V65() finite-support set
((R,0,(EmptyBag R)) | R) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,(EmptyBag R)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(EmptyBag (R + 1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,(EmptyBag R)) . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,(EmptyBag R)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (EmptyBag (R + 1)) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
dom (R,0,(EmptyBag R)) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
R is ordinal set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
f0 is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
X is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
divisors X is Relation-like NAT -defined Bags R -valued Function-like one-to-one non empty Function-yielding V22() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags R
rng (divisors X) is functional non empty finite Element of bool (Bags R)
bool (Bags R) is non empty set
BagOrder R is Relation-like Bags R -defined Bags R -valued total quasi_total V53() V56() V60() being_linear-order Element of bool [:(Bags R),(Bags R):]
[:(Bags R),(Bags R):] is Relation-like non empty set
bool [:(Bags R),(Bags R):] is non empty set
tcR is functional non empty finite Element of bool (Bags R)
SgmX ((BagOrder R),tcR) is Relation-like NAT -defined Bags R -valued Function-like one-to-one non empty Function-yielding V22() finite FinSequence-like FinSubsequence-like finite-support FinSequence of Bags R
field (BagOrder R) is set
R is set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
X is Element of R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
R is non empty set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
support (R,X) is finite Element of bool R
bool R is non empty set
{X} is non empty trivial finite 1 -element Element of bool R
f0 is set
((EmptyBag R) +* (X,1)) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(EmptyBag R) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R --> 0 is Relation-like R -defined NAT -valued RAT -valued INT -valued Function-like constant non empty total quasi_total Function-yielding V22() V62() V63() V64() V65() Element of bool [:R,NAT:]
[:R,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:R,NAT:] is non empty non trivial non finite set
{0} is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:R,{0}:] is Relation-like RAT -valued INT -valued non empty V62() V63() V64() V65() set
dom (EmptyBag R) is Element of bool R
(R,X) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(R,X) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R --> 0 is Relation-like R -defined NAT -valued RAT -valued INT -valued Function-like constant non empty total quasi_total Function-yielding V22() V62() V63() V64() V65() Element of bool [:R,NAT:]
[:R,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:R,NAT:] is non empty non trivial non finite set
{0} is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:R,{0}:] is Relation-like RAT -valued INT -valued non empty V62() V63() V64() V65() set
dom (R --> 0) is non empty Element of bool R
bool R is non empty set
(R --> 0) +* (X,1) is Relation-like R -defined NAT -valued RAT -valued Function-like non empty total quasi_total V62() V63() V64() V65() Element of bool [:R,NAT:]
((R --> 0) +* (X,1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 is Element of R
(R,X) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(EmptyBag R) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
f0 is Element of R
(R,f0) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (f0,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(R,f0) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty ordinal set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
f0 is non empty non trivial unital right_unital well-unital left_unital doubleLoopStr
the carrier of f0 is non empty non trivial set
[:R, the carrier of f0:] is Relation-like non empty set
bool [:R, the carrier of f0:] is non empty set
tcR is Relation-like R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:R, the carrier of f0:]
eval ((R,X),tcR) is Element of the carrier of f0
tcR . X is Element of the carrier of f0
support (R,X) is finite Element of bool R
bool R is non empty set
{X} is non empty trivial finite 1 -element Element of bool R
power f0 is Relation-like [: the carrier of f0,NAT:] -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of f0,NAT:], the carrier of f0:]
[: the carrier of f0,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
[:[: the carrier of f0,NAT:], the carrier of f0:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of f0,NAT:], the carrier of f0:] is non empty non trivial non finite set
(R,X) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(power f0) . ((tcR . X),((R,X) . X)) is Element of the carrier of f0
0 + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
(power f0) . ((tcR . X),(0 + 1)) is Element of the carrier of f0
cR is Element of the carrier of f0
(power f0) . (cR,0) is Element of the carrier of f0
((power f0) . (cR,0)) * cR is Element of the carrier of f0
1_ f0 is Element of the carrier of f0
K409(f0) is Element of the carrier of f0
the OneF of f0 is Element of the carrier of f0
(1_ f0) * cR is Element of the carrier of f0
R is set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
f0 is non empty unital multLoopStr_0
the carrier of f0 is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
1_ f0 is Element of the carrier of f0
(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
R is set
X is non empty non trivial unital doubleLoopStr
1_ X is Element of the carrier of X
the carrier of X is non empty non trivial set
0. X is V102(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
f0 is Element of R
(R,f0,X) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
[:(Bags R), the carrier of X:] is Relation-like non empty set
bool [:(Bags R), the carrier of X:] is non empty set
0_ (R,X) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
(R,f0) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (f0,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(0_ (R,X)) +* ((R,f0),(1_ X)) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
(R,f0,X) . (R,f0) is Element of the carrier of X
dom (0_ (R,X)) is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
(Bags R) --> (0. X) is Relation-like Bags R -defined the carrier of X -valued Function-like constant non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
{(0. X)} is non empty trivial finite 1 -element set
[:(Bags R),{(0. X)}:] is Relation-like non empty set
dom ((Bags R) --> (0. X)) is functional non empty Element of bool (Bags R)
tcR is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(R,f0,X) . tcR is Element of the carrier of X
(0_ (R,X)) . tcR is Element of the carrier of X
R is set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
X is Element of R
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
{(R,X)} is functional non empty trivial finite 1 -element Element of bool (Bags R)
bool (Bags R) is non empty set
f0 is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive right_unital well-unital left_unital V275() V276() V277() V278() doubleLoopStr
(R,X,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
the carrier of f0 is non empty non trivial set
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
1_ f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
K409(f0) is V102(f0) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
the OneF of f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
Support (R,X,f0) is functional Element of bool (Bags R)
tcR is set
cR is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(R,X,f0) . cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
(0_ (R,f0)) . cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
0. f0 is V102(f0) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
the ZeroF of f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
(R,X,f0) . tcR is set
R is ordinal set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
f0 is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive right_unital well-unital left_unital V275() V276() V277() V278() doubleLoopStr
X is Element of R
(R,X,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
the carrier of f0 is non empty non trivial set
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total finite-Support Element of bool [:(Bags R), the carrier of f0:]
(R,X) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
EmptyBag R is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags R
(EmptyBag R) +* (X,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
1_ f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
K409(f0) is V102(f0) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
the OneF of f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f0
(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
Support (R,X,f0) is functional Element of bool (Bags R)
bool (Bags R) is non empty set
{(R,X)} is functional non empty trivial finite 1 -element Element of bool (Bags R)
R is non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive right_unital well-unital left_unital V275() V276() V277() V278() doubleLoopStr
the carrier of R is non empty non trivial set
X is non empty set
Bags X is functional non empty Element of bool (Bags X)
Bags X is non empty set
bool (Bags X) is non empty set
f0 is Element of X
(X,f0,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
[:(Bags X), the carrier of R:] is Relation-like non empty set
bool [:(Bags X), the carrier of R:] is non empty set
0_ (X,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
(X,f0) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags X
EmptyBag X is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags X
(EmptyBag X) +* (f0,1) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
1_ R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
K409(R) is V102(R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
the OneF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(0_ (X,R)) +* ((X,f0),(1_ R)) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
tcR is Element of X
(X,tcR,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
(X,tcR) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags X
(EmptyBag X) +* (tcR,1) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(0_ (X,R)) +* ((X,tcR),(1_ R)) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
(X,tcR,R) . (X,f0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
0. R is V102(R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive left-distributive distributive V275() V276() V277() V278() doubleLoopStr
Polynom-Ring R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed V275() V276() V277() V278() doubleLoopStr
the carrier of (Polynom-Ring R) is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
- X is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
- f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
cR is set
f0 - f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
f0 + (- f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
(f0 - f0) . cR is set
S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(f0 . S) - (f0 . S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
0. R is V102(R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
0_. R is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
NAT --> (0. R) is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty total quasi_total T-Sequence-like Element of bool [:NAT, the carrier of R:]
{(0. R)} is non empty trivial finite 1 -element set
[:NAT,{(0. R)}:] is Relation-like non empty non trivial non finite set
(0_. R) . cR is set
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
- tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
dom (0_. R) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
dom (f0 - f0) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
X + cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
tcR + (- tcR) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
0. (Polynom-Ring R) is V102( Polynom-Ring R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
the ZeroF of (Polynom-Ring R) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
- cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed right-distributive left-distributive distributive V275() V276() V277() V278() doubleLoopStr
Polynom-Ring R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed V275() V276() V277() V278() doubleLoopStr
the carrier of (Polynom-Ring R) is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
X - f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
tcR - cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
- cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
tcR + (- cR) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
- f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
X + (- f0) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of (Polynom-Ring R)
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital V275() V276() V277() V278() doubleLoopStr
Polynom-Ring R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed V275() V276() V277() V278() doubleLoopStr
the carrier of (Polynom-Ring R) is non empty set
bool the carrier of (Polynom-Ring R) is non empty set
X is non empty Element of bool the carrier of (Polynom-Ring R)
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
{ b1 where b1 is Element of X : for b2, b3 being Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:] holds
( not b2 = b1 or not b3 in X or len b2 <= len b3 ) } is set
bool X is non empty set
cR is Element of X
S is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
len tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
[:X,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:X,NAT:] is non empty non trivial non finite set
cR is Relation-like X -defined NAT -valued Function-like non empty total quasi_total V62() V63() V64() V65() Element of bool [:X,NAT:]
f0 is non empty Element of bool X
cR .: f0 is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
min (cR .: f0) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() set
cR .: X is V72() V73() V74() V75() V76() V77() V292() Element of bool NAT
dom cR is non empty Element of bool X
S is set
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
0X is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
tcPR is Element of X
S is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len 0X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
0X is set
S is Element of X
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital V275() V276() V277() V278() doubleLoopStr
Polynom-Ring R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable strict add-associative right_zeroed V275() V276() V277() V278() doubleLoopStr
the carrier of (Polynom-Ring R) is non empty set
bool the carrier of (Polynom-Ring R) is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is non empty Element of bool the carrier of (Polynom-Ring R)
(R,X) is non empty Element of bool X
bool X is non empty set
{ b1 where b1 is Element of X : for b2, b3 being Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:] holds
( not b2 = b1 or not b3 in X or len b2 <= len b3 ) } is set
f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
len f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR is Element of X
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital V275() V276() V277() V278() doubleLoopStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
0. R is V102(R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
0_. R is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
NAT --> (0. R) is Relation-like NAT -defined the carrier of R -valued Function-like constant non empty total quasi_total T-Sequence-like Element of bool [:NAT, the carrier of R:]
{(0. R)} is non empty trivial finite 1 -element set
[:NAT,{(0. R)}:] is Relation-like non empty non trivial non finite set
(0_. R) +* (X,f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
cR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
X + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
tcR . cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(NAT --> (0. R)) . cR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
cR . S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
dom (0_. R) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
(NAT --> (0. R)) . S is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
S is set
tcR . S is set
cR . S is set
tcR . S is set
cR . S is set
dom tcR is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
dom cR is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital V275() V276() V277() V278() doubleLoopStr
the carrier of R is non empty set
0. R is V102(R) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
the ZeroF of R is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
X + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
f0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(R,X,f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
len (R,X,f0) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
(R,X,f0) . tcR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(R,X,f0) . tcR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set
(R,X,f0) . tcR is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
(R,X,f0) . X is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R
R is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital V275() V276() V277() V278() doubleLoopStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 + X is ordinal natural finite cardinal V42() V43() V44<