REAL is non empty non trivial non finite V60() V61() V62() V66() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V60() V61() V62() V63() V64() V65() V66() Element of K32(REAL)
K32(REAL) is non trivial non finite set
COMPLEX is non empty non trivial non finite V60() V66() set
RAT is non empty non trivial non finite V60() V61() V62() V63() V66() set
INT is non empty non trivial non finite V60() V61() V62() V63() V64() V66() set
K33(COMPLEX,COMPLEX) is non trivial Relation-like non finite complex-valued set
K32(K33(COMPLEX,COMPLEX)) is non trivial non finite set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is non trivial Relation-like non finite complex-valued set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is non trivial non finite set
K33(REAL,REAL) is non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
K32(K33(REAL,REAL)) is non trivial non finite set
K33(K33(REAL,REAL),REAL) is non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
K32(K33(K33(REAL,REAL),REAL)) is non trivial non finite set
K33(RAT,RAT) is non trivial Relation-like RAT -valued non finite complex-valued ext-real-valued real-valued set
K32(K33(RAT,RAT)) is non trivial non finite set
K33(K33(RAT,RAT),RAT) is non trivial Relation-like RAT -valued non finite complex-valued ext-real-valued real-valued set
K32(K33(K33(RAT,RAT),RAT)) is non trivial non finite set
K33(INT,INT) is non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
K32(K33(INT,INT)) is non trivial non finite set
K33(K33(INT,INT),INT) is non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
K32(K33(K33(INT,INT),INT)) is non trivial non finite set
K33(NAT,NAT) is non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
K33(K33(NAT,NAT),NAT) is non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33(K33(NAT,NAT),NAT)) is non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V60() V61() V62() V63() V64() V65() V66() set
K32(NAT) is non trivial non finite set
K32(NAT) is non trivial non finite set
K195(NAT) is V35() set
K363() is set
K32(K363()) is set
K32(K32(K363())) is set
K371() is Element of K32(K32(K363()))
Real>=0 is set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
3 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
_GraphSelectors is non empty V60() V61() V62() V63() V64() V65() Element of K32(NAT)
VertexSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
EdgeSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
SourceSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
TargetSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
4 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
card {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set
7 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
5 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
6 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
9 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
8 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() V31() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of NAT
Real>=0 is V60() V61() V62() Element of K32(REAL)
{ b1 where b1 is V21() real ext-real Element of REAL : 0 <= b1 } is set
<*> REAL is empty Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() FinSequence of REAL
Sum (<*> REAL) is V21() real ext-real Element of REAL
K168() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like total V18(K33(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K32(K33(K33(REAL,REAL),REAL))
K221(REAL,(<*> REAL),K168()) is V21() real ext-real Element of REAL
G is set
v is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
K32(v) is finite V40() set
x is Relation-like NAT -defined G -valued Function-like finite FinSubsequence-like Element of K32(v)
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
val is set
rng (Seq x) is finite set
dom (Seq x) is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Gn is set
(Seq x) . Gn is set
dom v is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
ENext is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
rng v is finite Element of K32(G)
K32(G) is set
x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
v . x is set
10 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
G is set
<*G*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
v is set
<*v*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*G*> ^ <*v*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
x is set
<*x*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(<*G*> ^ <*v*>) ^ <*x*> is non empty Relation-like NAT -defined Function-like finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
val is set
<*val*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*> is non empty Relation-like NAT -defined Function-like finite ((1 + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((1 + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
Gn is set
<*Gn*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*> is non empty Relation-like NAT -defined Function-like finite (((1 + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((1 + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
ENext is set
<*ENext*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*> is non empty Relation-like NAT -defined Function-like finite ((((1 + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((((1 + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
x is set
<*x*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*> is non empty Relation-like NAT -defined Function-like finite (((((1 + 1) + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((((1 + 1) + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
n is set
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*> is non empty Relation-like NAT -defined Function-like finite ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
y is set
<*y*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*> is non empty Relation-like NAT -defined Function-like finite (((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
x is set
<*x*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) ^ <*x*> is non empty Relation-like NAT -defined Function-like finite ((((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
c11 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len c11 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
c11 . 1 is set
c11 . 2 is set
c11 . 3 is set
c11 . 4 is set
c11 . 5 is set
c11 . 6 is set
c11 . 7 is set
c11 . 8 is set
c11 . 9 is set
c11 . 10 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 1 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 2 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 5 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 6 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 7 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 8 is set
len ((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom ((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) is non empty finite (((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Seg 9 is non empty finite 9 -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 9 is set
len <*x*> is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(len ((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>)) + (len <*x*>) is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
9 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 3 is set
((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>) . 4 is set
(len ((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>)) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
c11 . ((len ((((((((<*G*> ^ <*v*>) ^ <*x*>) ^ <*val*>) ^ <*Gn*>) ^ <*ENext*>) ^ <*x*>) ^ <*n*>) ^ <*y*>)) + 1) is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K32(G) is finite V40() set
dom G is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Sum G is V21() real ext-real Element of REAL
K221(REAL,G,K168()) is V21() real ext-real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(G)
(REAL,G,v) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (REAL,G,v) is V21() real ext-real Element of REAL
K221(REAL,(REAL,G,v),K168()) is V21() real ext-real Element of REAL
len (REAL,G,v) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
val is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K32(val) is finite V40() set
dom val is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Gn is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(val)
(REAL,val,Gn) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (REAL,val,Gn) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
x + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
ENext is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
x is V21() real ext-real Element of REAL
<*x*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V54() decreasing non-decreasing non-increasing FinSequence of REAL
ENext ^ <*x*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
card Gn is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom Gn is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
n is set
y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
Seg y is finite y -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
c11 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
val . c11 is V21() real ext-real Element of REAL
len ENext is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
len <*x*> is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(len ENext) + (len <*x*>) is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(len ENext) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
Sgm (dom Gn) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
dom (REAL,val,Gn) is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
card (dom Gn) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
len (Sgm (dom Gn)) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(Sgm (dom Gn)) . (len (Sgm (dom Gn))) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(Sgm (dom Gn)) . (len (REAL,val,Gn)) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom (Sgm (dom Gn)) is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
rng (Sgm (dom Gn)) is finite V60() V61() V62() V63() V64() V65() Element of K32(REAL)
G3 is set
(Sgm (dom Gn)) . G3 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
G3 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
G3 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(REAL,val,Gn) . (len (REAL,val,Gn)) is V21() real ext-real Element of REAL
(Sgm (dom Gn)) * Gn is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
Gn . ((Sgm (dom Gn)) . (len (REAL,val,Gn))) is V21() real ext-real Element of REAL
[c11,x] is set
Sum (REAL,val,Gn) is V21() real ext-real Element of REAL
K221(REAL,(REAL,val,Gn),K168()) is V21() real ext-real Element of REAL
Sum ENext is V21() real ext-real Element of REAL
K221(REAL,ENext,K168()) is V21() real ext-real Element of REAL
(val . c11) + (Sum ENext) is V21() real ext-real set
len val is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
VL9 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
c11 + VL9 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
c11 - 1 is V21() real V30() ext-real set
VL9 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
Seg VL9 is finite VL9 -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Gn | (Seg VL9) is Relation-like NAT -defined Seg VL9 -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
G3 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len G3 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
G3 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len G3 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
G3 ^ G3 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
VL9 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
fsA is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len fsA is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
fsB is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len fsB is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
fsA ^ fsB is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom G3 is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
G3 . c11 is V21() real ext-real Element of REAL
fssq is set
G3 is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(val)
i is set
x1 is set
[i,x1] is set
x2 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom fsA is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
val . x2 is V21() real ext-real Element of REAL
x2 + 0 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
G3 . x2 is V21() real ext-real Element of REAL
fsA . x2 is V21() real ext-real Element of REAL
K32(fsA) is finite V40() set
i is set
[c11,(val . c11)] is set
{[c11,(val . c11)]} is non empty trivial Relation-like Function-like constant finite 1 -element set
Gn . c11 is V21() real ext-real Element of REAL
[c11,(Gn . c11)] is set
i is set
fssq is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(fsA)
x1 is set
x2 is set
[x1,x2] is set
z is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
[z,x2] is set
Gn \ {[c11,(val . c11)]} is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(val)
x1 is set
x2 is set
[x1,x2] is set
z is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
z + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
(z + 1) - 1 is V21() real V30() ext-real set
i is set
Gn . i is V21() real ext-real Element of REAL
[i,(Gn . i)] is set
x1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
{c11} is non empty trivial finite V40() 1 -element V60() V61() V62() V63() V64() V65() set
dom fssq is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
(dom fssq) \/ {c11} is non empty finite V60() V61() V62() V63() V64() V65() set
fssq . i is V21() real ext-real Element of REAL
[i,(fssq . i)] is set
i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
x1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
fssq . i is V21() real ext-real Element of REAL
[i,(fssq . i)] is Element of K33(NAT,REAL)
K33(NAT,REAL) is non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
card fssq is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
card {[c11,(val . c11)]} is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
(card Gn) - (card {[c11,(val . c11)]}) is V21() real V30() ext-real set
(x + 1) - 1 is V21() real V30() ext-real set
(REAL,fsA,fssq) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (REAL,fsA,fssq) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
(Sgm (dom Gn)) . i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
Sgm (dom fssq) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom fssq)) . i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom ENext is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
ENext . i is V21() real ext-real Element of REAL
(REAL,val,Gn) . i is V21() real ext-real Element of REAL
len (Sgm (dom fssq)) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
card (dom fssq) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
z is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
Seg z is finite z -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
dom (Sgm (dom fssq)) is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
rng (Sgm (dom fssq)) is finite V60() V61() V62() V63() V64() V65() Element of K32(REAL)
z is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
Seg z is finite z -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
fssq . ((Sgm (dom fssq)) . i) is V21() real ext-real Element of REAL
[((Sgm (dom fssq)) . i),(fssq . ((Sgm (dom fssq)) . i))] is Element of K33(NAT,REAL)
Gn . ((Sgm (dom fssq)) . i) is V21() real ext-real Element of REAL
Gn . ((Sgm (dom Gn)) . i) is V21() real ext-real Element of REAL
(Sgm (dom fssq)) * fssq is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
dom (REAL,fsA,fssq) is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
(REAL,fsA,fssq) . i is V21() real ext-real Element of REAL
z is set
Seg (len val) is finite len val -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Sgm {c11} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom fssq)) ^ (Sgm {c11}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
z is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
Seg z is finite z -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
fsA . i is V21() real ext-real Element of REAL
G3 . i is V21() real ext-real Element of REAL
val . i is V21() real ext-real Element of REAL
Sum fsA is V21() real ext-real Element of REAL
K221(REAL,fsA,K168()) is V21() real ext-real Element of REAL
(Sum (REAL,val,Gn)) + (Sum ENext) is V21() real ext-real set
((val . c11) + (Sum ENext)) + (Sum fsA) is V21() real ext-real set
(val . c11) + (Sum fsA) is V21() real ext-real set
((val . c11) + (Sum fsA)) + (Sum ENext) is V21() real ext-real set
(Sum fsA) + (val . c11) is V21() real ext-real set
i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
dom G3 is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
c11 + i is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
val . (c11 + i) is V21() real ext-real Element of REAL
G3 . i is V21() real ext-real Element of REAL
Sum G3 is V21() real ext-real Element of REAL
K221(REAL,G3,K168()) is V21() real ext-real Element of REAL
dom fsB is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
fsB . 1 is V21() real ext-real Element of REAL
<*(val . c11)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V54() decreasing non-decreasing non-increasing FinSequence of REAL
Sum val is V21() real ext-real Element of REAL
K221(REAL,val,K168()) is V21() real ext-real Element of REAL
Sum G3 is V21() real ext-real Element of REAL
K221(REAL,G3,K168()) is V21() real ext-real Element of REAL
(Sum G3) + (Sum G3) is V21() real ext-real set
Sum <*(val . c11)*> is V21() real ext-real Element of REAL
K221(REAL,<*(val . c11)*>,K168()) is V21() real ext-real Element of REAL
(Sum fsA) + (Sum <*(val . c11)*>) is V21() real ext-real set
((Sum fsA) + (Sum <*(val . c11)*>)) + (Sum G3) is V21() real ext-real set
((Sum fsA) + (val . c11)) + (Sum G3) is V21() real ext-real set
((Sum fsA) + (val . c11)) + 0 is V21() real ext-real set
val is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K32(val) is finite V40() set
x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom val is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Gn is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(val)
(REAL,val,Gn) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (REAL,val,Gn) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
x + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
Sum (REAL,val,Gn) is V21() real ext-real Element of REAL
K221(REAL,(REAL,val,Gn),K168()) is V21() real ext-real Element of REAL
Sum val is V21() real ext-real Element of REAL
K221(REAL,val,K168()) is V21() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K32(x) is finite V40() set
dom x is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
val is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(x)
(REAL,x,val) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (REAL,x,val) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
Gn is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set
x . Gn is V21() real ext-real Element of REAL
Sum (REAL,x,val) is V21() real ext-real Element of REAL
K221(REAL,(REAL,x,val),K168()) is V21() real ext-real Element of REAL
Sum x is V21() real ext-real Element of REAL
K221(REAL,x,K168()) is V21() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K32(x) is finite V40() set
dom x is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
val is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K32(x)
(REAL,x,val) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (REAL,x,val) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
Sum (REAL,x,val) is V21() real ext-real Element of REAL
K221(REAL,(REAL,x,val),K168()) is V21() real ext-real Element of REAL
Sum x is V21() real ext-real Element of REAL
K221(REAL,x,K168()) is V21() real ext-real Element of REAL
() is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
() is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
() is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
{1} is non empty trivial finite V40() 1 -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
K33({},{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33({},{1})) is finite V40() set
the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1})) is empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))
the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set is empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set
K33({},REAL) is Relation-like complex-valued ext-real-valued real-valued set
K32(K33({},REAL)) is set
the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL)) is empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL))
K33({1},REAL) is non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
K32(K33({1},REAL)) is non trivial non finite set
the Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL)) is Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL))
<*{1}*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*{}*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*{1}*> ^ <*{}*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
<* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*> is non empty Relation-like NAT -defined Function-like finite (1 + 1) + 1 -element FinSequence-like FinSubsequence-like set
(1 + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
((<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*> is non empty Relation-like NAT -defined Function-like finite ((1 + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((1 + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
<* the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set *> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(((<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set *> is non empty Relation-like NAT -defined Function-like finite (((1 + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((1 + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
<* the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
((((<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set *>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL))*> is non empty Relation-like NAT -defined Function-like finite ((((1 + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
((((1 + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
<* the Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL))*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(((((<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set *>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL))*>) ^ <* the Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL))*> is non empty Relation-like NAT -defined Function-like finite (((((1 + 1) + 1) + 1) + 1) + 1) + 1 -element FinSequence-like FinSubsequence-like set
(((((1 + 1) + 1) + 1) + 1) + 1) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real positive non negative V60() V61() V62() V63() V64() V65() Element of NAT
dom the Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL)) is finite V40() V60() V61() V62() V63() V64() V65() Element of K32({1})
K32({1}) is finite V40() set
len ((((((<*{1}*> ^ <*{}*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},{1}))*>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional total V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() set *>) ^ <* the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL))*>) ^ <* the Relation-like {1} -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K32(K33({1},REAL))*>) is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative V60() V61() V62() V63() V64() V65() Element of NAT
n is Relation-like NAT -defined Function-like finite set
dom n is finite V60() V61() V62() V63() V64() V65() Element of K32(NAT)
Seg 7 is non empty finite 7 -element V60() V61() V62() V63() V64() V65() Element of K32(NAT)
n . () is set
n . () is set
the_Vertices_of n is set
n . VertexSelector is set
the_Edges_of n is set
n . EdgeSelector is set
the_Source_of n is set
n . SourceSelector is set
the_Target_of n is set
n . TargetSelector is set
n . () is set
dom the empty Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like one-to-one constant functional total V18( {} , REAL ) V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(K33({},REAL)) is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative complex-valued ext-real-valued real-valued natural-valued V60() V61() V62() V63() V64() V65() V66() Function-yielding V125() Element of K32(NAT)
G is Relation-like NAT -defined Function-like finite [Graph-like] () set
G . () is set
the_Edges_of G is set
G . EdgeSelector is set
G is Relation-like NAT -defined Function-like finite [Graph-like] () set
G . () is set
the_Edges_of G is set
G . EdgeSelector is set
v is Relation-like Function-like set
dom v is set
G is Relation-like NAT -defined Function-like finite [Graph-like] () set
G . () is set
the_Vertices_of G is non empty set
G . VertexSelector is set
v is Relation-like Function-like set
dom v is set
G is Relation-like NAT -defined Function-like finite [Graph-like] () set
(G) is Relation-like Function-like set
G . () is set
dom (G) is set
the_Edges_of G is set
G . EdgeSelector is set
v is Relation-like Function-like set
dom v is set
G is Relation-like NAT -defined Function-like finite [Graph-like] () set
(G) is Relation-like Function-like set
G . () is set
dom (G) is set
the_Vertices_of G is non empty set
G . VertexSelector is set
v is Relation-like Function-like set
dom v is set
G is Relation-like NAT -defined Function-like finite [Graph-like] set
v is set
G .set ((),v) is Relation-like NAT -defined Function-like finite set
() .--> v is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element V60() V61() V62() V63() V64() V65() set
{()} --> v is non empty Relation-like {()} -defined {v} -valued Function-like constant total V18({()},{v}) finite Element of K32(K33({()},{v}))
{v} is non empty trivial finite 1 -element set
K33({()},{v}) is Relation-like finite set
K32(K33({()},{v})) is finite V40() set
G +* (() .--> v) is Relation-like Function-like finite set
G .set ((),v) is Relation-like NAT -defined Function-like finite set
() .--> v is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element V60() V61() V62() V63() V64() V65() set
{()} --> v is non empty Relation-like {()} -defined {v} -valued Function-like constant total V18({()},{v}) finite Element of K32(K33({()},{v}))
K33({()},{v}) is Relation-like finite set
K32(K33({()},{v})) is finite V40() set
G +* (() .--> v) is Relation-like Function-like finite set
G .set ((),v) is Relation-like NAT -defined Function-like finite set
() .--> v is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} is non empty trivial finite V40() 1 -element V60() V61() V62() V63() V64() V65() set
{()} --> v is non empty Relation-like {()} -defined {v} -valued Function-like constant total V18({()},{v}) finite Element of K32(K33({()},{v}))
K33({()},{v}) is Relation-like finite set
K32(K33({()},{v})) is finite V40() set
G +* (() .--> v) is Relation-like Function-like finite set
v is Relation-like NAT -defined Function-like finite [Graph-like] set
x is set
v .set ((),x) is Relation-like NAT -defined Function-like finite [Graph-like] set
() .--> x is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} --> x is non empty Relation-like {()} -defined {x} -valued Function-like constant total V18({()},{x}) finite Element of K32(K33({()},{x}))
{x} is non empty trivial finite 1 -element set
K33({()},{x}) is Relation-like finite set
K32(K33({()},{x})) is finite V40() set
v +* (() .--> x) is Relation-like Function-like finite set
v .set ((),x) is Relation-like NAT -defined Function-like finite [Graph-like] set
() .--> x is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} --> x is non empty Relation-like {()} -defined {x} -valued Function-like constant total V18({()},{x}) finite Element of K32(K33({()},{x}))
K33({()},{x}) is Relation-like finite set
K32(K33({()},{x})) is finite V40() set
v +* (() .--> x) is Relation-like Function-like finite set
v .set ((),x) is Relation-like NAT -defined Function-like finite [Graph-like] set
() .--> x is Relation-like NAT -defined {()} -defined Function-like one-to-one finite set
{()} --> x is non empty Relation-like {()} -defined {x} -valued Function-like constant total V18({()},{x}) finite Element of K32(K33({()},{x