:: CATALAN2 semantic presentation

REAL is non empty non trivial non finite V50() V51() V52() V56() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V50() V51() V52() V53() V54() V55() V56() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
[:NAT,REAL:] is non empty non trivial Relation-like V35() V36() V37() non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V50() V56() set
RAT is non empty non trivial non finite V50() V51() V52() V53() V56() set
INT is non empty non trivial non finite V50() V51() V52() V53() V54() V56() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
{{},1} is non empty finite V49() V50() V51() V52() V53() V54() V55() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V50() V51() V52() V53() V54() V55() V56() cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like V35() non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like V35() non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like V35() V36() V37() non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like V35() V36() V37() non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued V35() V36() V37() non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued V35() V36() V37() non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() V38() non finite nonnegative-yielding set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() V38() non finite nonnegative-yielding set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
Catalan 1 is V11() real ext-real Element of REAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() V31() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
- 1 is V11() real V30() ext-real non positive Element of REAL
card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() set
dom {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() set
addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V22([:REAL,REAL:]) quasi_total V35() V36() V37() V135( REAL ) V140( REAL ) V141( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
24 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
{0,1} is non empty finite V49() V50() V51() V52() V53() V54() V55() Element of bool NAT
|.0.| is V11() real V31() ext-real Element of REAL
sqrt 1 is V11() real ext-real Element of REAL
K38(1) is V11() real V30() ext-real non positive set
addnat is non empty Relation-like [:NAT,NAT:] -defined NAT -valued INT -valued Function-like V22([:NAT,NAT:]) quasi_total V35() V36() V37() V38() nonnegative-yielding V135( NAT ) V140( NAT ) V141( NAT ) Element of bool [:[:NAT,NAT:],NAT:]
SumC is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
SumC ^ R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
SumC is set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
r is T-Sequence-like Relation-like NAT -defined SumC -valued Function-like finite V213() set
r | R is T-Sequence-like Relation-like R -defined NAT -defined SumC -valued rng r -valued Function-like finite V213() set
rng r is finite set
Cat is T-Sequence-like Relation-like NAT -defined Function-like finite V213() set
(r | R) ^ Cat is T-Sequence-like Relation-like NAT -defined Function-like finite V213() set
rng Cat is finite set
rng r is finite Element of bool SumC
bool SumC is non empty set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R | SumC is T-Sequence-like Relation-like SumC -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
Sum (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | SumC)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
len R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R | (len R) is T-Sequence-like Relation-like len R -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum (R | (len R)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | (len R))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
SumC is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
SumC . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
len SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(dom SumC) /\ 1 is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
SumC | 1 is T-Sequence-like Relation-like 1 -defined NAT -defined NAT -valued RAT -valued rng SumC -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng SumC is finite V50() V51() V52() V53() V54() V55() set
(SumC | 1) . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
<%(SumC . 0)%> is non empty trivial T-Sequence-like Relation-like NAT -defined NAT -valued Function-like constant V35() V36() V37() V38() V39() V40() V41() V42() finite nonnegative-yielding 1 -element V213() set
Sum <%(SumC . 0)%> is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
addnat "**" <%(SumC . 0)%> is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
len (SumC | 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC | 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
2 * (SumC . 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
SumC is set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> R is Relation-like SumC -defined RAT -valued INT -valued {R} -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() nonnegative-yielding Element of bool [:SumC,{R}:]
{R} is non empty trivial finite V49() V50() V51() V52() V53() V54() V55() 1 -element set
[:SumC,{R}:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,{R}:] is non empty set
rng (SumC --> R) is trivial finite V49() V50() V51() V52() V53() V54() V55() Element of bool {R}
bool {R} is non empty finite V49() set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
{r} is non empty trivial finite V49() V50() V51() V52() V53() V54() V55() 1 -element set
R --> r is T-Sequence-like Relation-like R -defined NAT -valued RAT -valued INT -valued {r} -valued Function-like constant V22(R) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:R,{r}:]
[:R,{r}:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() finite nonnegative-yielding set
bool [:R,{r}:] is non empty finite V49() set
(R --> r) | SumC is T-Sequence-like Relation-like SumC -defined R -defined NAT -valued RAT -valued INT -valued {r} -valued rng (R --> r) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:R,{r}:]
rng (R --> r) is trivial finite V50() V51() V52() V53() V54() V55() set
SumC --> r is T-Sequence-like Relation-like SumC -defined NAT -valued RAT -valued INT -valued {r} -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:SumC,{r}:]
[:SumC,{r}:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() finite nonnegative-yielding set
bool [:SumC,{r}:] is non empty finite V49() set
SumC /\ R is finite V50() V51() V52() V53() V54() V55() set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> 0 is T-Sequence-like Relation-like SumC -defined NAT -valued RAT -valued INT -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:SumC,NAT:]
[:SumC,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,NAT:] is non empty set
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
rng (SumC --> 0) is trivial finite V50() V51() V52() V53() V54() V55() Element of bool RAT
bool RAT is non empty non trivial non finite set
{0} is non empty trivial functional finite V49() V50() V51() V52() V53() V54() V55() 1 -element Element of bool NAT
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(SumC --> 0) | R is T-Sequence-like Relation-like R -defined SumC -defined NAT -valued RAT -valued INT -valued rng (SumC --> 0) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() set
rng (SumC --> 0) is trivial finite V50() V51() V52() V53() V54() V55() set
Sum ((SumC --> 0) | R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum ((SumC --> 0) | R)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(SumC --> 0) | R is T-Sequence-like Relation-like SumC -defined R -defined SumC -defined NAT -valued RAT -valued INT -valued rng (SumC --> 0) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:SumC,NAT:]
R --> 0 is T-Sequence-like Relation-like R -defined NAT -valued RAT -valued INT -valued Function-like constant V22(R) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:R,NAT:]
[:R,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:R,NAT:] is non empty set
Sum (R --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
0 * R is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() V31() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of NAT
0 --> 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding {} -defined 0 -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant functional V22( {} ) V22( 0 ) quasi_total real V30() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of bool [:0,NAT:]
[:0,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:0,NAT:] is non empty set
1 --> 0 is non empty T-Sequence-like Relation-like 1 -defined NAT -valued RAT -valued INT -valued Function-like constant V22(1) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:1,NAT:]
[:1,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() V38() non finite nonnegative-yielding set
bool [:1,NAT:] is non empty non trivial non finite set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> 0 is T-Sequence-like Relation-like SumC -defined NAT -valued RAT -valued INT -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:SumC,NAT:]
[:SumC,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,NAT:] is non empty set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> 0 is T-Sequence-like Relation-like SumC -defined NAT -valued RAT -valued INT -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:SumC,NAT:]
[:SumC,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,NAT:] is non empty set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R --> 1 is T-Sequence-like Relation-like non-empty R -defined NAT -valued RAT -valued INT -valued Function-like constant V22(R) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:R,NAT:]
[:R,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:R,NAT:] is non empty set
((SumC --> 0),(R --> 1)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (R --> 1) is trivial finite V50() V51() V52() V53() V54() V55() V209() Element of bool RAT
bool RAT is non empty non trivial non finite set
{1} is non empty trivial finite V49() V50() V51() V52() V53() V54() V55() 1 -element Element of bool NAT
rng (SumC --> 0) is trivial finite V50() V51() V52() V53() V54() V55() Element of bool RAT
{0} is non empty trivial functional finite V49() V50() V51() V52() V53() V54() V55() 1 -element Element of bool NAT
(rng (SumC --> 0)) \/ (rng (R --> 1)) is finite V50() V51() V52() V53() V54() V55() Element of bool RAT
rng ((SumC --> 0),(R --> 1)) is finite V50() V51() V52() V53() V54() V55() Element of bool RAT
dom ((SumC --> 0),(R --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
((SumC --> 0),(R --> 1)) | Cat is T-Sequence-like Relation-like Cat -defined NAT -defined NAT -valued RAT -valued rng ((SumC --> 0),(R --> 1)) -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng ((SumC --> 0),(R --> 1)) is finite V50() V51() V52() V53() V54() V55() set
Sum (((SumC --> 0),(R --> 1)) | Cat) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (((SumC --> 0),(R --> 1)) | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
(SumC --> 0) | Cat is T-Sequence-like Relation-like SumC -defined Cat -defined SumC -defined NAT -valued RAT -valued INT -valued rng (SumC --> 0) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:SumC,NAT:]
rng (SumC --> 0) is trivial finite V50() V51() V52() V53() V54() V55() set
Cat --> 0 is T-Sequence-like Relation-like Cat -defined NAT -valued RAT -valued INT -valued Function-like constant V22(Cat) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:Cat,NAT:]
[:Cat,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:Cat,NAT:] is non empty set
Sum (Cat --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
0 * Cat is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() V31() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of NAT
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
Cat - (dom (SumC --> 0)) is V11() real V30() V31() ext-real Element of INT
len ((SumC --> 0),(R --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom ((SumC --> 0),(R --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
len (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
len (R --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (R --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(len (SumC --> 0)) + (len (R --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
Cat - (len (SumC --> 0)) is V11() real V30() V31() ext-real Element of INT
(len (R --> 1)) + (len (SumC --> 0)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((len (R --> 1)) + (len (SumC --> 0))) - (len (SumC --> 0)) is V11() real V30() V31() ext-real Element of INT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(R --> 1) | s is T-Sequence-like Relation-like R -defined s -defined R -defined NAT -valued RAT -valued INT -valued rng (R --> 1) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:R,NAT:]
rng (R --> 1) is trivial finite V50() V51() V52() V53() V54() V55() V209() set
s --> 1 is T-Sequence-like Relation-like non-empty s -defined NAT -valued RAT -valued INT -valued Function-like constant V22(s) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:s,NAT:]
[:s,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:s,NAT:] is non empty set
s + (dom (SumC --> 0)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
c₆ is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
c₆ | s is T-Sequence-like Relation-like s -defined NAT -defined NAT -valued RAT -valued rng c₆ -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng c₆ is finite V50() V51() V52() V53() V54() V55() set
((SumC --> 0),(c₆ | s)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
Sum (s --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
(Sum (SumC --> 0)) + (Sum (s --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
dom (R --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool R
bool R is non empty finite V49() set
Cat - SumC is V11() real V30() V31() ext-real Element of INT
R + SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(R + SumC) - SumC is V11() real V30() V31() ext-real Element of INT
(Cat - SumC) + (Cat - SumC) is V11() real V30() V31() ext-real Element of INT
SumC + (Cat - SumC) is V11() real V30() V31() ext-real Element of INT
SumC * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() V31() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of NAT
s * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R | SumC is T-Sequence-like Relation-like SumC -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
dom (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(R | SumC) | r is T-Sequence-like Relation-like r -defined NAT -defined NAT -valued RAT -valued rng (R | SumC) -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (R | SumC) is finite V50() V51() V52() V53() V54() V55() set
Sum ((R | SumC) | r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum ((R | SumC) | r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
(dom R) /\ SumC is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
R | r is T-Sequence-like Relation-like r -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (R | SumC) is finite V50() V51() V52() V53() V54() V55() Element of bool RAT
bool RAT is non empty non trivial non finite set
rng R is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
SumC is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
(SumC,R) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng SumC is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
rng R is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
(rng SumC) \/ (rng R) is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
rng (SumC,R) is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
dom (SumC,R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(SumC,R) | r is T-Sequence-like Relation-like r -defined NAT -defined NAT -valued RAT -valued rng (SumC,R) -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (SumC,R) is finite V50() V51() V52() V53() V54() V55() set
Sum ((SumC,R) | r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum ((SumC,R) | r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
SumC | r is T-Sequence-like Relation-like r -defined NAT -defined NAT -valued RAT -valued rng SumC -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng SumC is finite V50() V51() V52() V53() V54() V55() set
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
r - (dom SumC) is V11() real V30() V31() ext-real Element of INT
SumC | (dom SumC) is T-Sequence-like Relation-like dom SumC -defined NAT -defined NAT -valued RAT -valued rng SumC -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng SumC is finite V50() V51() V52() V53() V54() V55() set
Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
Cat + (dom SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
R | Cat is T-Sequence-like Relation-like Cat -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
(SumC,(R | Cat)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
Sum (R | Cat) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
(Sum SumC) + (Sum (R | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
len SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC | (len SumC) is T-Sequence-like Relation-like len SumC -defined NAT -defined NAT -valued RAT -valued rng SumC -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum (SumC | (len SumC)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (SumC | (len SumC))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
2 * (Sum (R | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
2 * (Sum SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(2 * (Sum SumC)) + (2 * (Sum (R | Cat))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(dom SumC) + Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
2 * SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(2 * SumC) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R | ((2 * SumC) + 1) is T-Sequence-like Relation-like (2 * SumC) + 1 -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
Sum (R | ((2 * SumC) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | ((2 * SumC) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(Sum (R | ((2 * SumC) + 1))) - SumC is V11() real V30() V31() ext-real Element of INT
2 * ((Sum (R | ((2 * SumC) + 1))) - SumC) is V11() real V30() V31() ext-real Element of INT
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> 1 is T-Sequence-like Relation-like non-empty SumC -defined NAT -valued RAT -valued INT -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:SumC,NAT:]
[:SumC,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,NAT:] is non empty set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
len R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
Sum R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(len R) - (2 * (Sum R)) is V11() real V30() V31() ext-real Element of INT
(R,(SumC --> 1)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (SumC --> 1) is trivial finite V50() V51() V52() V53() V54() V55() V209() Element of bool RAT
bool RAT is non empty non trivial non finite set
{1} is non empty trivial finite V49() V50() V51() V52() V53() V54() V55() 1 -element Element of bool NAT
rng R is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
(rng R) \/ (rng (SumC --> 1)) is finite V50() V51() V52() V53() V54() V55() set
rng (R,(SumC --> 1)) is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
dom (R,(SumC --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(R,(SumC --> 1)) | Cat is T-Sequence-like Relation-like Cat -defined NAT -defined NAT -valued RAT -valued rng (R,(SumC --> 1)) -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng (R,(SumC --> 1)) is finite V50() V51() V52() V53() V54() V55() set
Sum ((R,(SumC --> 1)) | Cat) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum ((R,(SumC --> 1)) | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
R | Cat is T-Sequence-like Relation-like Cat -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
Cat - (dom R) is V11() real V30() V31() ext-real Element of INT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(dom R) + s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s --> 1 is T-Sequence-like Relation-like non-empty s -defined NAT -valued RAT -valued INT -valued Function-like constant V22(s) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:s,NAT:]
[:s,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:s,NAT:] is non empty set
Sum (s --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
s * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(R,(s --> 1)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum (R,(s --> 1)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
(Sum R) + s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool SumC
bool SumC is non empty finite V49() set
len (SumC --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (SumC --> 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
(len R) + SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
s + (dom R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
SumC + (dom R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(SumC --> 1) | s is T-Sequence-like Relation-like SumC -defined s -defined SumC -defined NAT -valued RAT -valued INT -valued rng (SumC --> 1) -valued Function-like constant V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:SumC,NAT:]
rng (SumC --> 1) is trivial finite V50() V51() V52() V53() V54() V55() V209() set
(2 * (Sum R)) + Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
((2 * (Sum R)) + Cat) - (dom R) is V11() real V30() V31() ext-real Element of INT
(((2 * (Sum R)) + Cat) - (dom R)) + s is V11() real V30() V31() ext-real Element of INT
(((2 * (Sum R)) + Cat) - (dom R)) + SumC is V11() real V30() V31() ext-real Element of INT
SumC - SumC is V11() real V30() V31() ext-real Element of INT
((len R) - (2 * (Sum R))) - SumC is V11() real V30() V31() ext-real Element of INT
Cat - (((len R) - (2 * (Sum R))) - SumC) is V11() real V30() V31() ext-real Element of INT
Cat - 0 is V11() real V30() V31() ext-real non negative Element of INT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
SumC --> 1 is T-Sequence-like Relation-like non-empty SumC -defined NAT -valued RAT -valued INT -valued Function-like constant V22(SumC) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:SumC,NAT:]
[:SumC,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:SumC,NAT:] is non empty set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R --> 0 is T-Sequence-like Relation-like R -defined NAT -valued RAT -valued INT -valued Function-like constant V22(R) quasi_total V35() V36() V37() V38() finite nonnegative-yielding Function-yielding V137() V213() Element of bool [:R,NAT:]
[:R,NAT:] is Relation-like RAT -valued INT -valued V35() V36() V37() V38() nonnegative-yielding set
bool [:R,NAT:] is non empty set
r is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
len r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R + (len r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
Sum r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(R + (len r)) - (2 * (Sum r)) is V11() real V30() V31() ext-real Element of INT
((R --> 0),r) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
(((R --> 0),r),(SumC --> 1)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
dom (R --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool R
bool R is non empty finite V49() set
len (R --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (R --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
len ((R --> 0),r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom ((R --> 0),r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
Sum (R --> 0) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
R * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional real V30() V31() ext-real non positive non negative V35() V36() V37() V38() finite finite-yielding V49() V50() V51() V52() V53() V54() V55() V56() nonnegative-yielding cardinal {} -element Function-yielding V137() V213() Element of NAT
Sum ((R --> 0),r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
0 + (Sum r) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R | SumC is T-Sequence-like Relation-like SumC -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
Sum (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | SumC)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
len R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
len (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R | (len R) is T-Sequence-like Relation-like len R -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
dom R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
(dom R) /\ SumC is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
R | SumC is T-Sequence-like Relation-like SumC -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng R is finite V50() V51() V52() V53() V54() V55() set
Sum (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | SumC)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
r is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
((R | SumC),r) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
len (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom (R | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
rng r is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
rng R is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
dom r is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of bool NAT
Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
r | Cat is T-Sequence-like Relation-like Cat -defined NAT -defined NAT -valued RAT -valued rng r -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng r is finite V50() V51() V52() V53() V54() V55() set
Sum (r | Cat) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (r | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(len (R | SumC)) + Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
R | ((len (R | SumC)) + Cat) is T-Sequence-like Relation-like (len (R | SumC)) + Cat -defined NAT -defined NAT -valued RAT -valued rng R -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
((R | SumC),(r | Cat)) is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum (R | ((len (R | SumC)) + Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
(Sum (R | SumC)) + (Sum (r | Cat)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (R | ((len (R | SumC)) + Cat))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
SumC + (2 * (Sum (r | Cat))) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
1 --> 1 is non empty T-Sequence-like Relation-like non-empty 1 -defined NAT -valued RAT -valued INT -valued Function-like constant V22(1) quasi_total V35() V36() V37() V38() finite nonnegative-yielding V213() Element of bool [:1,NAT:]
[:1,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued V35() V36() V37() V38() non finite nonnegative-yielding set
bool [:1,NAT:] is non empty non trivial non finite set
SumC is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
r is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
r | SumC is T-Sequence-like Relation-like SumC -defined NAT -defined NAT -valued RAT -valued rng r -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng r is finite V50() V51() V52() V53() V54() V55() set
Sum (r | SumC) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (r | SumC)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
r | R is T-Sequence-like Relation-like R -defined NAT -defined NAT -valued RAT -valued rng r -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
((r | R),(1 --> 1)) is non empty T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Cat is T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Cat . R is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(Sum (r | SumC)) - 1 is V11() real V30() V31() ext-real Element of INT
rng Cat is finite V50() V51() V52() V53() V54() V55() Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
2 * s is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
(2 * s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
<%0%> is non empty trivial T-Sequence-like Relation-like NAT -defined NAT -valued Function-like constant V35() V36() V37() V38() V39() V40() V41() V42() finite nonnegative-yielding 1 -element V213() set
Sum <%0%> is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
Cat | R is T-Sequence-like Relation-like R -defined NAT -defined NAT -valued RAT -valued rng Cat -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
rng Cat is finite V50() V51() V52() V53() V54() V55() set
Sum (Cat | R) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
2 * (Sum (Cat | R)) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
len Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() V31() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of NAT
dom Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal set
<%(Cat . R)%> is non empty trivial T-Sequence-like Relation-like NAT -defined NAT -valued Function-like constant V35() V36() V37() V38() V39() V40() V41() V42() finite nonnegative-yielding 1 -element V213() set
((Cat | R),<%(Cat . R)%>) is non empty T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() set
Sum Cat is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
(Sum (Cat | R)) + (Sum <%0%>) is epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real non negative finite V50() V51() V52() V53() V54() V55() cardinal Element of COMPLEX
<%(Cat . R)%> is non empty trivial T-Sequence-like Relation-like NAT -defined NAT -valued Function-like constant V35() V36() V37() V38() V39() V40() V41() V42() finite nonnegative-yielding 1 -element V213() set
dom <%(Cat . R)%> is non empty trivial epsilon-transitive epsilon-connected ordinal natural V11() real V30() ext-real positive non negative finite V50() V51() V52() V53() V54() V55() cardinal 1 -element Element of bool NAT
rng <%(Cat . R)%> is non empty trivial finite V50() V51() V52() V53() V54() V55() 1 -element Element of bool NAT
{1} is non empty trivial finite V49() V50()