REAL is set
NAT is non empty V24() V25() V26() non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is set
NAT is non empty V24() V25() V26() non finite cardinal limit_cardinal set
K19(NAT) is non finite set
K19(NAT) is non finite set
COMPLEX is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() set
1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
G is set
sc is non empty V66() MultiGraphStruct
the carrier of sc is non empty set
m is Element of the carrier of sc
n is Element of the carrier of sc
the Source of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
the carrier' of sc is set
K20( the carrier' of sc, the carrier of sc) is Relation-like set
K19(K20( the carrier' of sc, the carrier of sc)) is set
the Source of sc . G is set
the Target of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
the Target of sc . G is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
G is set
sc is non empty V66() MultiGraphStruct
the carrier of sc is non empty set
m is Element of the carrier of sc
n is Element of the carrier of sc
vs is Element of the carrier of sc
v1 is Element of the carrier of sc
the Source of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
the carrier' of sc is set
K20( the carrier' of sc, the carrier of sc) is Relation-like set
K19(K20( the carrier' of sc, the carrier of sc)) is set
the Source of sc . G is set
the Target of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
the Target of sc . G is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in sc & b1 = the Source of G . b2 ) } is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in sc & b1 = the Target of G . b2 ) } is set
G is non empty V66() MultiGraphStruct
(G,{}) is set
the carrier of G is non empty set
the carrier' of G is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in {} & b1 = the Source of G . b2 ) } is set
(G,{}) is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in {} & b1 = the Target of G . b2 ) } is set
the Element of (G,{}) is Element of (G,{})
n is Element of the carrier of G
vs is Element of the carrier' of G
the Source of G . vs is set
the Element of (G,{}) is Element of (G,{})
n is Element of the carrier of G
vs is Element of the carrier' of G
the Target of G . vs is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len m) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. n is Element of the carrier of G
n + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. (n + 1) is Element of the carrier of G
m . n is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
rng sc is set
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
rng m is set
(G,(rng m)) is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in rng m & b1 = the Source of G . b2 ) } is set
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len m) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is set
vs is Element of the carrier of G
v1 is Element of the carrier' of G
the Source of G . v1 is set
v1 is Element of the carrier' of G
the Source of G . v1 is set
dom m is Element of K19(NAT)
v2 is set
m . v2 is set
v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. v19 is Element of the carrier of G
v19 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. (v19 + 1) is Element of the carrier of G
sc . v19 is set
m . v19 is set
dom sc is Element of K19(NAT)
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
rng sc is set
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
rng m is set
(G,(rng m)) is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in rng m & b1 = the Target of G . b2 ) } is set
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len m) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is set
vs is Element of the carrier of G
v1 is Element of the carrier' of G
the Target of G . v1 is set
v1 is Element of the carrier' of G
the Target of G . v1 is set
dom m is Element of K19(NAT)
v2 is set
m . v2 is set
v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. v19 is Element of the carrier of G
sc /. (v19 + 1) is Element of the carrier of G
sc . (v19 + 1) is set
m . v19 is set
dom sc is Element of K19(NAT)
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
rng sc is set
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
rng m is set
(G,(rng m)) is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in rng m & b1 = the Source of G . b2 ) } is set
(G,(rng m)) is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
{ b1 where b1 is Element of the carrier of G : ex b2 being Element of the carrier' of G st
( b2 in rng m & b1 = the Target of G . b2 ) } is set
(G,(rng m)) \/ (G,(rng m)) is set
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len m) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is set
dom sc is Element of K19(NAT)
vs is set
sc . vs is set
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom m is Element of K19(NAT)
m . v1 is set
sc /. v1 is Element of the carrier of G
v1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. (v1 + 1) is Element of the carrier of G
sc . v1 is set
v2 is Element of the carrier' of G
the Source of G . v2 is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom m is Element of K19(NAT)
m . (len m) is set
sc /. (len m) is Element of the carrier of G
sc /. ((len m) + 1) is Element of the carrier of G
sc . ((len m) + 1) is set
v19 is Element of the carrier' of G
the Target of G . v19 is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
sc is Element of the carrier of G
<*sc*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len <*sc*> is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() Element of NAT
(len {}) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<*sc*> /. n is Element of the carrier of G
n + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<*sc*> /. (n + 1) is Element of the carrier of G
{} . n is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
the carrier of G is non empty set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len sc) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
sc . (len sc) is set
the Target of G . (sc . (len sc)) is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
Seg ((len sc) + 1) is non empty finite (len sc) + 1 -element Element of K19(NAT)
m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
sc . m is set
the Source of G . (sc . m) is set
n is set
vs is set
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom m is Element of K19(NAT)
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom m is Element of K19(NAT)
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
rng m is set
n is set
vs is set
m . vs is set
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg (len sc) is finite len sc -element Element of K19(NAT)
dom sc is Element of K19(NAT)
rng sc is set
sc . v1 is set
the Source of G . (sc . v1) is set
Seg (len sc) is finite len sc -element Element of K19(NAT)
dom sc is Element of K19(NAT)
rng sc is set
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. vs is Element of the carrier of G
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. (vs + 1) is Element of the carrier of G
sc . vs is set
m . vs is set
the Source of G . (sc . vs) is set
m . (vs + 1) is set
the Target of G . (sc . vs) is set
m . vs is set
the Source of G . (sc . vs) is set
m . (vs + 1) is set
sc . (vs + 1) is set
the Source of G . (sc . (vs + 1)) is set
the Target of G . (sc . vs) is set
the Element of the carrier of G is Element of the carrier of G
<* the Element of the carrier of G*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len <* the Element of the carrier of G*> is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len sc) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<* the Element of the carrier of G*> /. vs is Element of the carrier of G
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<* the Element of the carrier of G*> /. (vs + 1) is Element of the carrier of G
sc . vs is set
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
sc . vs is set
m . vs is set
sc /. vs is Element of the carrier of G
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. (vs + 1) is Element of the carrier of G
n . vs is set
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
the Source of G . (n . vs) is set
m /. vs is Element of the carrier of G
m /. (vs + 1) is Element of the carrier of G
vs - 1 is ext-real V31() V80() set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. (vs -' 1) is Element of the carrier of G
(vs -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. ((vs -' 1) + 1) is Element of the carrier of G
n . (vs -' 1) is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
the Target of G . (n . (vs -' 1)) is set
m /. (vs -' 1) is Element of the carrier of G
m /. ((vs -' 1) + 1) is Element of the carrier of G
sc /. vs is Element of the carrier of G
G is non empty V66() MultiGraphStruct
the carrier' of G is set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
the carrier of G is non empty set
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg G is finite G -element Element of K19(NAT)
G + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg (G + 1) is non empty finite G + 1 -element Element of K19(NAT)
sc is non empty V66() MultiGraphStruct
the carrier of sc is non empty set
the carrier' of sc is set
m is Relation-like NAT -defined the carrier of sc -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of sc
m | (Seg (G + 1)) is Relation-like NAT -defined Seg (G + 1) -defined NAT -defined the carrier of sc -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of sc))
K20(NAT, the carrier of sc) is Relation-like non finite set
K19(K20(NAT, the carrier of sc)) is non finite set
n is Relation-like NAT -defined the carrier of sc -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of sc
vs is Relation-like NAT -defined the carrier' of sc -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of sc
vs | (Seg G) is Relation-like NAT -defined Seg G -defined NAT -defined the carrier' of sc -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier' of sc))
K20(NAT, the carrier' of sc) is Relation-like set
K19(K20(NAT, the carrier' of sc)) is set
v1 is Relation-like NAT -defined the carrier' of sc -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of sc
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len vs) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 . v2 is set
vs . v2 is set
v2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . v2 is set
m . v2 is set
n . (v2 + 1) is set
m . (v2 + 1) is set
m /. v2 is Element of the carrier of sc
m /. (v2 + 1) is Element of the carrier of sc
n /. v2 is Element of the carrier of sc
n /. (v2 + 1) is Element of the carrier of sc
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. v2 is Element of the carrier of sc
v2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. (v2 + 1) is Element of the carrier of sc
v1 . v2 is set
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is non empty V66() MultiGraphStruct
the carrier' of n is set
vs is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc,m) -cut vs is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
the carrier of n is non empty set
v1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len G) + sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len G) + sc) - sc is ext-real V31() V80() set
m + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(m + 1) - sc is ext-real V31() V80() set
the Source of n is Relation-like Function-like V18( the carrier' of n, the carrier of n) Element of K19(K20( the carrier' of n, the carrier of n))
K20( the carrier' of n, the carrier of n) is Relation-like set
K19(K20( the carrier' of n, the carrier of n)) is set
the Target of n is Relation-like Function-like V18( the carrier' of n, the carrier of n) Element of K19(K20( the carrier' of n, the carrier of n))
v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G . (v19 + 1) is set
the Source of n . (G . (v19 + 1)) is set
G . v19 is set
the Target of n . (G . v19) is set
1 - 1 is ext-real V31() V80() set
sc - 1 is ext-real V31() V80() set
sc -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v29 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v29 + v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 /. fvs1 is Element of the carrier of n
fvs1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 /. (fvs1 + 1) is Element of the carrier of n
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc + fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc + (fc9 + 1) is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs . (fvs1 + 1) is set
vs . fvs1 is set
(sc - 1) + v19 is ext-real V31() V80() set
m - (sc - 1) is ext-real V31() V80() set
(sc - 1) + (m - (sc - 1)) is ext-real V31() V80() set
the Target of n . (vs . fvs1) is set
v19 + sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc + v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(fvs1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 /. ((fvs1 + 1) + 1) is Element of the carrier of n
v2 is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like Chain of n
G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m is non empty V66() MultiGraphStruct
the carrier of m is non empty set
the carrier' of m is set
n is Relation-like NAT -defined the carrier of m -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of m
(G,(sc + 1)) -cut n is Relation-like NAT -defined the carrier of m -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of m
vs is Relation-like NAT -defined the carrier of m -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of m
v1 is Relation-like NAT -defined the carrier' of m -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of m
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(G,sc) -cut v1 is Relation-like NAT -defined the carrier' of m -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of m
v2 is Relation-like NAT -defined the carrier' of m -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of m
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) + G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len vs) + G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs /. v19 is Element of the carrier of m
v19 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs /. (v19 + 1) is Element of the carrier of m
v2 . v19 is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v29 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v29 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G + v29 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. (G + v29) is Element of the carrier of m
(G + v29) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n /. ((G + v29) + 1) is Element of the carrier of m
G + v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((G + v29) + 1) - 1 is ext-real V31() V80() set
((len v2) + G) - 1 is ext-real V31() V80() set
v1 . (G + v29) is set
vs . v19 is set
n . (G + v29) is set
G + (v29 + 1) is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs . (v19 + 1) is set
n . ((G + v29) + 1) is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (len sc) is set
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
m . 1 is set
n is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
vs is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
n ^ vs is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len vs) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc ^' m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (n ^ vs) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
the Source of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
K20( the carrier' of G, the carrier of G) is Relation-like set
K19(K20( the carrier' of G, the carrier of G)) is set
the Target of G is Relation-like Function-like V18( the carrier' of G, the carrier of G) Element of K19(K20( the carrier' of G, the carrier of G))
v29 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v29 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(n ^ vs) . (v29 + 1) is set
the Source of G . ((n ^ vs) . (v29 + 1)) is set
(n ^ vs) . v29 is set
the Target of G . ((n ^ vs) . v29) is set
dom (n ^ vs) is Element of K19(NAT)
dom n is Element of K19(NAT)
n . v29 is set
sc /. v29 is Element of the carrier of G
sc /. (v29 + 1) is Element of the carrier of G
sc . v29 is set
sc . (v29 + 1) is set
(sc ^' m) . v29 is set
(sc ^' m) . (v29 + 1) is set
dom vs is Element of K19(NAT)
fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
c2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs . c2 is set
c2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m /. c2 is Element of the carrier of G
m /. (c2 + 1) is Element of the carrier of G
m . c2 is set
m . (c2 + 1) is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . v29 is set
(sc ^' m) . (len sc) is set
((len n) + 1) + fvs9 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . (((len n) + 1) + fvs9) is set
(len sc) + fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((len sc) + fvs9) is set
(sc ^' m) . (v29 + 1) is set
((len n) + 1) + c2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . (((len n) + 1) + c2) is set
(len sc) + c2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((len sc) + c2) is set
dom n is Element of K19(NAT)
dom vs is Element of K19(NAT)
(sc ^' m) . v29 is set
(sc ^' m) . (v29 + 1) is set
dom n is Element of K19(NAT)
(sc ^' m) . v29 is set
(sc ^' m) . (v29 + 1) is set
dom vs is Element of K19(NAT)
fvs1 is Element of the carrier of G
c2 is Element of the carrier of G
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 is Element of the carrier of G
fvs9 is Element of the carrier of G
fvs1 is Element of the carrier of G
c2 is Element of the carrier of G
n . (v29 + 1) is set
sc /. (v29 + 1) is Element of the carrier of G
(v29 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc /. ((v29 + 1) + 1) is Element of the carrier of G
sc . (v29 + 1) is set
sc . ((v29 + 1) + 1) is set
(sc ^' m) . ((v29 + 1) + 1) is set
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs . fc9 is set
fc9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m /. fc9 is Element of the carrier of G
m /. (fc9 + 1) is Element of the carrier of G
m . fc9 is set
m . (fc9 + 1) is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fc9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . (len sc) is set
((len n) + 1) + fc9 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . (((len n) + 1) + fc9) is set
(len sc) + fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((len sc) + fc9) is set
(v29 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((v29 + 1) + 1) is set
((len n) + 1) + fc9 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . (((len n) + 1) + fc9) is set
(len sc) + fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((len sc) + fc9) is set
(v29 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((v29 + 1) + 1) is set
(v29 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc ^' m) . ((v29 + 1) + 1) is set
vs2 is Element of the carrier of G
fc9 is Element of the carrier of G
fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len n) + fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is Element of the carrier of G
fc9 is Element of the carrier of G
v19 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like Chain of G
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (len sc) is set
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
m . 1 is set
sc ^' m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
vs is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
v1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
vs ^ v1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len vs) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len (sc ^' m) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len (sc ^' m)) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len sc) + (len m) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len vs) + (len v1) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len vs) + (len v1)) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len (vs ^ v1) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len (vs ^ v1)) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
c2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len fvs1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
c2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 /. c2 is Element of the carrier of G
fvs1 . c2 is set
fvs1 /. (c2 + 1) is Element of the carrier of G
fvs1 . (c2 + 1) is set
dom (vs ^ v1) is Element of K19(NAT)
dom vs is Element of K19(NAT)
sc /. c2 is Element of the carrier of G
sc /. (c2 + 1) is Element of the carrier of G
vs . c2 is set
sc . c2 is set
sc . (c2 + 1) is set
(vs ^ v1) . c2 is set
dom v1 is Element of K19(NAT)
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len vs) + vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
(len vs) + vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(vs ^ v1) . c2 is set
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 . fc9 is set
fc9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m /. fc9 is Element of the carrier of G
m . fc9 is set
m /. (fc9 + 1) is Element of the carrier of G
m . (fc9 + 1) is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 . (len sc) is set
((len vs) + 1) + fvs9 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 . (((len vs) + 1) + fvs9) is set
(len sc) + fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 . ((len sc) + fvs9) is set
((len vs) + 1) + fc9 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 . (((len vs) + 1) + fc9) is set
(len sc) + fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs1 . ((len sc) + fc9) is set
dom vs is Element of K19(NAT)
dom v1 is Element of K19(NAT)
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
sc is Element of the carrier of G
<*sc*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len <*sc*> is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() Element of NAT
(len {}) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<*sc*> /. vs is Element of the carrier of G
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
<*sc*> /. (vs + 1) is Element of the carrier of G
{} . vs is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V80() set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
the Relation-like non-empty empty-yielding NAT -defined the carrier' of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered oriented cyclic V80() Chain of G is Relation-like non-empty empty-yielding NAT -defined the carrier' of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered oriented cyclic V80() Chain of G
the carrier of G is non empty set
the Element of the carrier of G is Element of the carrier of G
<* the Element of the carrier of G*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . vs is set
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . v1 is set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
the Relation-like non-empty empty-yielding NAT -defined the carrier' of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered oriented cyclic V80() Chain of G is Relation-like non-empty empty-yielding NAT -defined the carrier' of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V24() V25() V26() V28() V29() V30() V31() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered oriented cyclic V80() Chain of G
the carrier of G is non empty set
the Element of the carrier of G is Element of the carrier of G
<* the Element of the carrier of G*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . v1 is set
v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . v2 is set
vs is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like Chain of G
G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg G is finite G -element Element of K19(NAT)
sc is non empty V66() MultiGraphStruct
the carrier' of sc is set
m is Relation-like NAT -defined the carrier' of sc -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of sc
m | (Seg G) is Relation-like NAT -defined Seg G -defined NAT -defined the carrier' of sc -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier' of sc))
K20(NAT, the carrier' of sc) is Relation-like set
K19(K20(NAT, the carrier' of sc)) is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
the Source of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
the carrier of sc is non empty set
K20( the carrier' of sc, the carrier of sc) is Relation-like set
K19(K20( the carrier' of sc, the carrier of sc)) is set
the Target of sc is Relation-like Function-like V18( the carrier' of sc, the carrier of sc) Element of K19(K20( the carrier' of sc, the carrier of sc))
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(m | (Seg G)) . (vs + 1) is set
the Source of sc . ((m | (Seg G)) . (vs + 1)) is set
(m | (Seg G)) . vs is set
the Target of sc . ((m | (Seg G)) . vs) is set
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . vs is set
m . (vs + 1) is set
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is non empty V66() MultiGraphStruct
the carrier' of sc is set
m is Relation-like NAT -defined the carrier' of sc -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of sc
G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg G is finite G -element Element of K19(NAT)
m | (Seg G) is Relation-like NAT -defined Seg G -defined NAT -defined the carrier' of sc -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier' of sc))
K20(NAT, the carrier' of sc) is Relation-like set
K19(K20(NAT, the carrier' of sc)) is set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
the carrier of G is non empty set
n is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n . vs is set
n . v1 is set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented (G) Chain of G
the carrier of G is non empty set
m is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(sc,m) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ((sc,m) -cut G) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len ((sc,m) -cut G)) + sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((sc,m) -cut G) . (n + 1) is set
sc + n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G . (sc + n) is set
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((sc,m) -cut G) . (n + 1) is set
sc + n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G . (sc + n) is set
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
K19(sc) is set
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . 1 is set
sc . (len sc) is set
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
K19(m) is set
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . n is set
sc . vs is set
(len m) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs - n is ext-real V31() V80() set
n - n is ext-real V31() V80() set
n -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
1 - 1 is ext-real V31() V80() set
n - 1 is ext-real V31() V80() set
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(n - 1) + 1 is ext-real V31() V80() set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(1 + 1) - 1 is ext-real V31() V80() set
((len m) + 1) - 1 is ext-real V31() V80() set
(1,v1) -cut m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(vs,(len m)) -cut m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(1,n) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(vs,((len m) + 1)) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
vs + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((vs + 1),((len m) + 1)) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
vs2 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v19 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v19) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs - 1 is ext-real V31() V80() set
vs -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v19) + vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs - vs is ext-real V31() V80() set
(len m) - vs is ext-real V31() V80() set
(len v19) -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v19) - 1 is ext-real V31() V80() set
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 + (len v19) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((0 + 1),(len fc9)) -cut fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
((0 + 1),1) -cut fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
((1 + 1),(len fc9)) -cut fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(((0 + 1),1) -cut fc9) ^ (((1 + 1),(len fc9)) -cut fc9) is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
((fvs9 + 1),vs) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(((fvs9 + 1),vs) -cut sc) ^ (((vs + 1),((len m) + 1)) -cut sc) is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(1,1) -cut fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
fc9 . (0 + 1) is set
<*(fc9 . (0 + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
vs + 0 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (vs + 0) is set
<*(sc . (vs + 0))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
(vs,vs) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(2,(len fc9)) -cut fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b1 & b1 <= v1 ) or ( vs <= b1 & b1 <= len m ) ) } is set
sc is Relation-like Function-like set
dom sc is set
Seg (len m) is finite len m -element Element of K19(NAT)
p1 is set
domfc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p1 is Relation-like NAT -defined Function-like FinSubsequence-like set
domfc is set
SL is set
domfvs is set
[SL,domfvs] is set
{SL,domfvs} is non empty set
{SL} is non empty V12() 1 -element set
{{SL,domfvs},{SL}} is non empty set
dom p1 is set
p1 . SL is set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom m is Element of K19(NAT)
m . SL is set
domfc is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq domfc is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b1 & b1 <= n ) or ( vs + 1 <= b1 & b1 <= len sc ) ) } is set
domfvs is Relation-like Function-like set
dom domfvs is set
Seg (len sc) is finite len sc -element Element of K19(NAT)
SL is set
p is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
SL is Relation-like NAT -defined Function-like FinSubsequence-like set
p is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
dom SL is set
SL . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom sc is Element of K19(NAT)
sc . k is set
p is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fc9 . 1 is set
vs2 . (len vs2) is set
v2 ^ v19 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
x is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 ^' fc9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y . 1 is set
y . (len y) is set
vs2 ^ (((vs + 1),((len m) + 1)) -cut sc) is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
- (vs - n) is ext-real V31() V80() set
- (- (vs - n)) is ext-real V31() V80() set
((len m) - vs) + 1 is ext-real V31() V80() set
(n - 1) + (((len m) - vs) + 1) is ext-real V31() V80() set
- vs is ext-real non positive V31() V80() set
n + (- vs) is ext-real V31() V80() set
(len m) + (n + (- vs)) is ext-real V31() V80() set
(len x) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
1 + (len v2) is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 . 1 is set
fc9 . (len fc9) is set
sc . ((len m) + 1) is set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= v1 ) } is set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs <= b1 & b1 <= len m ) } is set
x is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= v1 ) } \/ { b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs <= b1 & b1 <= len m ) } is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= v1 ) or ( vs <= b2 & b2 <= len m ) ) } is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= v1 ) or ( vs <= b2 & b2 <= len m ) ) } is set
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= v1 ) or ( vs <= b2 & b2 <= len m ) ) } is set
x is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x is finite set
DL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y is finite set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x \/ y is set
Sgm (x \/ y) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Sgm x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Sgm y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm x) ^ (Sgm y) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
card y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
- 1 is ext-real non positive V31() V80() set
(len v19) + (- 1) is ext-real V31() V80() set
((len v19) + (- 1)) + 1 is ext-real V31() V80() set
len (Sgm y) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg v1 is finite v1 -element Element of K19(NAT)
idseq v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
id (Seg v1) is Relation-like Seg v1 -defined Seg v1 -valued Function-like one-to-one total Element of K19(K20((Seg v1),(Seg v1)))
K20((Seg v1),(Seg v1)) is Relation-like set
K19(K20((Seg v1),(Seg v1))) is set
dom (Sgm x) is Element of K19(NAT)
rng (Sgm x) is set
dom domfc is set
rng (Sgm y) is set
DL is set
DR is set
DL is set
[DR,DL] is set
{DR,DL} is non empty set
{DR} is non empty V12() 1 -element set
{{DR,DL},{DR}} is non empty set
dom v2 is Element of K19(NAT)
v2 . DR is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm x) . DR is set
(Sgm x) * domfc is Relation-like NAT -defined the carrier' of G -valued Function-like set
dom ((Sgm x) * domfc) is set
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm x) * domfc) . DR is set
domfc . DR is set
1 + lp21 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . (1 + lp21) is set
DR is set
DL is set
[DR,DL] is set
{DR,DL} is non empty set
{DR} is non empty V12() 1 -element set
{{DR,DL},{DR}} is non empty set
((Sgm x) * domfc) . DR is set
(Sgm x) . DR is set
domfc . ((Sgm x) . DR) is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm x) . DR is set
v2 . DR is set
m . DR is set
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
DL is set
DR is set
DL is set
[DR,DL] is set
{DR,DL} is non empty set
{DR} is non empty V12() 1 -element set
{{DR,DL},{DR}} is non empty set
dom v19 is Element of K19(NAT)
v19 . DR is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom (Sgm y) is Element of K19(NAT)
fvs9 + DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm y) . DR is set
(Sgm y) * domfc is Relation-like NAT -defined the carrier' of G -valued Function-like set
dom ((Sgm y) * domfc) is set
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm y) * domfc) . DR is set
domfc . (fvs9 + DR) is set
vs + lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . (vs + lp21) is set
DR is set
DL is set
[DR,DL] is set
{DR,DL} is non empty set
{DR} is non empty V12() 1 -element set
{{DR,DL},{DR}} is non empty set
((Sgm y) * domfc) . DR is set
(Sgm y) . DR is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
fvs9 + DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm y) . DR is set
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 . DR is set
(fvs9 + 1) + lp21 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . ((fvs9 + 1) + lp21) is set
domfc . ((Sgm y) . DR) is set
((Sgm x) ^ (Sgm y)) * domfc is Relation-like NAT -defined the carrier' of G -valued Function-like set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs + 1 <= b1 & b1 <= len sc ) } is set
DL is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= n ) } \/ { b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs + 1 <= b1 & b1 <= len sc ) } is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( vs + 1 <= b2 & b2 <= len sc ) ) } is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( vs + 1 <= b2 & b2 <= len sc ) ) } is set
{ b2 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( vs + 1 <= b2 & b2 <= len sc ) ) } is set
DL is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
DL is set
DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
DL is finite set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp22 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
DR is finite set
SR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
DL \/ DR is set
Sgm (DL \/ DR) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Sgm DL is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Sgm DR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm DL) ^ (Sgm DR) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(len fc9) - 1 is ext-real V31() V80() set
(len fc9) -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp21 - 1 is ext-real V31() V80() set
lp22 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(vs + 1) + lp22 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(lp21 - 1) + 1 is ext-real V31() V80() set
vs + ((lp21 - 1) + 1) is ext-real V31() V80() set
(((len m) - vs) + 1) + 1 is ext-real V31() V80() set
((((len m) - vs) + 1) + 1) - 1 is ext-real V31() V80() set
vs + (((((len m) - vs) + 1) + 1) - 1) is ext-real V31() V80() set
card DR is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
lp22 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len m) + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len fc9) + vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len (((vs + 1),((len m) + 1)) -cut sc) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len (((vs + 1),((len m) + 1)) -cut sc)) + (vs + 1) is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len (((vs + 1),((len m) + 1)) -cut sc)) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len (((vs + 1),((len m) + 1)) -cut sc)) + 1) + vs is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len (Sgm DR) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg n is finite n -element Element of K19(NAT)
idseq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total Element of K19(K20((Seg n),(Seg n)))
K20((Seg n),(Seg n)) is Relation-like set
K19(K20((Seg n),(Seg n))) is set
dom (Sgm DL) is Element of K19(NAT)
rng (Sgm DL) is set
dom p is set
rng (Sgm DR) is set
p is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
dom vs2 is Element of K19(NAT)
vs2 . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm DL) . k is set
(Sgm DL) * p is Relation-like NAT -defined the carrier of G -valued Function-like set
dom ((Sgm DL) * p) is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm DL) * p) . x is set
p . k is set
1 + i is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (1 + i) is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
((Sgm DL) * p) . x is set
(Sgm DL) . x is set
p . ((Sgm DL) . x) is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm DL) . k is set
vs2 . k is set
sc . k is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + lp21 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
dom (((vs + 1),((len m) + 1)) -cut sc) is Element of K19(NAT)
(((vs + 1),((len m) + 1)) -cut sc) . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom (Sgm DR) is Element of K19(NAT)
vs + k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm DR) . k is set
(Sgm DR) * p is Relation-like NAT -defined the carrier of G -valued Function-like set
dom ((Sgm DR) * p) is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm DR) * p) . x is set
p . (vs + k) is set
(vs + 1) + i is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . ((vs + 1) + i) is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
((Sgm DR) * p) . x is set
(Sgm DR) . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm DR) . k is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(((vs + 1),((len m) + 1)) -cut sc) . k is set
(vs + 1) + i is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . ((vs + 1) + i) is set
p . ((Sgm DR) . k) is set
((Sgm DL) ^ (Sgm DR)) * p is Relation-like NAT -defined the carrier of G -valued Function-like set
(vs,(len m)) -cut m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(vs,((len m) + 1)) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs <= b1 & b1 <= len m ) } is set
fvs1 is Relation-like Function-like set
dom fvs1 is set
Seg (len m) is finite len m -element Element of K19(NAT)
c2 is set
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
c2 is Relation-like NAT -defined Function-like FinSubsequence-like set
vs2 is set
fc9 is set
fvs9 is set
[fc9,fvs9] is set
{fc9,fvs9} is non empty set
{fc9} is non empty V12() 1 -element set
{{fc9,fvs9},{fc9}} is non empty set
dom c2 is set
c2 . fc9 is set
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom m is Element of K19(NAT)
m . sc is set
vs2 is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq vs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( vs <= b1 & b1 <= len sc ) } is set
fvs9 is Relation-like Function-like set
dom fvs9 is set
Seg (len sc) is finite len sc -element Element of K19(NAT)
sc is set
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is Relation-like NAT -defined Function-like FinSubsequence-like set
fc9 is set
sc is set
p1 is set
[sc,p1] is set
{sc,p1} is non empty set
{sc} is non empty V12() 1 -element set
{{sc,p1},{sc}} is non empty set
dom sc is set
sc . sc is set
domfc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom sc is Element of K19(NAT)
sc . domfc is set
fc9 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq fc9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len p1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p1 . 1 is set
p1 . (len p1) is set
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) + vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs - vs is ext-real V31() V80() set
(len m) - vs is ext-real V31() V80() set
vs - 1 is ext-real V31() V80() set
vs -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) - 1 is ext-real V31() V80() set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc + (len v2) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len m) + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len ((vs,((len m) + 1)) -cut sc) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len ((vs,((len m) + 1)) -cut sc)) + vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((len m) - vs) + 1 is ext-real V31() V80() set
(((len m) - vs) + 1) + 1 is ext-real V31() V80() set
- vs is ext-real non positive V31() V80() set
(- vs) + 1 is ext-real V31() V80() set
(len m) + ((- vs) + 1) is ext-real V31() V80() set
- (vs - 1) is ext-real V31() V80() set
- (- (vs - 1)) is ext-real V31() V80() set
(len sc) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfvs is set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfvs is finite set
card domfvs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
- 1 is ext-real non positive V31() V80() set
(len v2) + (- 1) is ext-real V31() V80() set
((len v2) + (- 1)) + 1 is ext-real V31() V80() set
Sgm domfvs is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Sgm domfvs) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
rng (Sgm domfvs) is set
dom vs2 is set
x is set
y is set
k is set
[y,k] is set
{y,k} is non empty set
{y} is non empty V12() 1 -element set
{{y,k},{y}} is non empty set
dom v2 is Element of K19(NAT)
v2 . y is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom (Sgm domfvs) is Element of K19(NAT)
domfc + i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm domfvs) . i is set
(Sgm domfvs) * vs2 is Relation-like NAT -defined the carrier' of G -valued Function-like set
dom ((Sgm domfvs) * vs2) is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm domfvs) * vs2) . y is set
vs2 . (domfc + i) is set
vs + x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . (vs + x) is set
y is set
k is set
[y,k] is set
{y,k} is non empty set
{y} is non empty V12() 1 -element set
{{y,k},{y}} is non empty set
((Sgm domfvs) * vs2) . y is set
(Sgm domfvs) . y is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc + i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm domfvs) . i is set
x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v2 . i is set
(domfc + 1) + x is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . ((domfc + 1) + x) is set
vs2 . ((Sgm domfvs) . i) is set
x is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len ((vs,((len m) + 1)) -cut sc)) - 1 is ext-real V31() V80() set
(len ((vs,((len m) + 1)) -cut sc)) -' 1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs + y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc + (len ((vs,((len m) + 1)) -cut sc)) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x is finite set
card x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len ((vs,((len m) + 1)) -cut sc)) + (- 1) is ext-real V31() V80() set
((len ((vs,((len m) + 1)) -cut sc)) + (- 1)) + 1 is ext-real V31() V80() set
Sgm x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Sgm x) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
rng (Sgm x) is set
dom fc9 is set
i is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
dom ((vs,((len m) + 1)) -cut sc) is Element of K19(NAT)
((vs,((len m) + 1)) -cut sc) . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom (Sgm x) is Element of K19(NAT)
domfc + k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm x) . k is set
(Sgm x) * fc9 is Relation-like NAT -defined the carrier of G -valued Function-like set
dom ((Sgm x) * fc9) is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm x) * fc9) . x is set
fc9 . (domfc + k) is set
vs + i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (vs + i) is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
((Sgm x) * fc9) . x is set
(Sgm x) . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc + k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm x) . k is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((vs,((len m) + 1)) -cut sc) . k is set
(domfc + 1) + i is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . ((domfc + 1) + i) is set
fc9 . ((Sgm x) . k) is set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(1 + 1) - 1 is ext-real V31() V80() set
((len m) + 1) - 1 is ext-real V31() V80() set
(1,v1) -cut m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(1,n) -cut sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len ((1,n) -cut sc) is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len v2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= v1 ) } is set
fvs1 is Relation-like Function-like set
dom fvs1 is set
Seg (len m) is finite len m -element Element of K19(NAT)
c2 is set
vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
c2 is Relation-like NAT -defined Function-like FinSubsequence-like set
vs2 is set
fc9 is set
fvs9 is set
[fc9,fvs9] is set
{fc9,fvs9} is non empty set
{fc9} is non empty V12() 1 -element set
{{fc9,fvs9},{fc9}} is non empty set
dom c2 is set
c2 . fc9 is set
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom m is Element of K19(NAT)
m . sc is set
vs2 is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq vs2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{ b1 where b1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
fvs9 is Relation-like Function-like set
dom fvs9 is set
Seg (len sc) is finite len sc -element Element of K19(NAT)
sc is set
fc9 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc is Relation-like NAT -defined Function-like FinSubsequence-like set
fc9 is set
sc is set
p1 is set
[sc,p1] is set
{sc,p1} is non empty set
{sc} is non empty V12() 1 -element set
{{sc,p1},{sc}} is non empty set
dom sc is set
sc . sc is set
domfc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom sc is Element of K19(NAT)
sc . domfc is set
fc9 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq fc9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len p1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
p1 . 1 is set
p1 . (len p1) is set
domfc is set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfc is finite set
Seg v1 is finite v1 -element Element of K19(NAT)
Sgm domfc is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
idseq v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
id (Seg v1) is Relation-like Seg v1 -defined Seg v1 -valued Function-like one-to-one total Element of K19(K20((Seg v1),(Seg v1)))
K20((Seg v1),(Seg v1)) is Relation-like set
K19(K20((Seg v1),(Seg v1))) is set
dom (Sgm domfc) is Element of K19(NAT)
domfvs is set
SL is set
p is set
[SL,p] is set
{SL,p} is non empty set
{SL} is non empty V12() 1 -element set
{{SL,p},{SL}} is non empty set
dom v2 is Element of K19(NAT)
v2 . SL is set
x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm domfc) . x is set
(Sgm domfc) * vs2 is Relation-like NAT -defined the carrier' of G -valued Function-like set
dom ((Sgm domfc) * vs2) is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm domfc) * vs2) . SL is set
vs2 . x is set
1 + y is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m . (1 + y) is set
SL is set
p is set
[SL,p] is set
{SL,p} is non empty set
{SL} is non empty V12() 1 -element set
{{SL,p},{SL}} is non empty set
((Sgm domfc) * vs2) . SL is set
(Sgm domfc) . SL is set
vs2 . ((Sgm domfc) . SL) is set
x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom vs2 is set
(Sgm domfc) . x is set
v2 . x is set
m . x is set
y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
y + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfvs is set
SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
domfvs is finite set
Seg n is finite n -element Element of K19(NAT)
Sgm domfvs is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
idseq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total Element of K19(K20((Seg n),(Seg n)))
K20((Seg n),(Seg n)) is Relation-like set
K19(K20((Seg n),(Seg n))) is set
dom (Sgm domfvs) is Element of K19(NAT)
p is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
dom ((1,n) -cut sc) is Element of K19(NAT)
((1,n) -cut sc) . x is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(Sgm domfvs) . k is set
(Sgm domfvs) * fc9 is Relation-like NAT -defined the carrier of G -valued Function-like set
dom ((Sgm domfvs) * fc9) is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
((Sgm domfvs) * fc9) . x is set
fc9 . k is set
1 + i is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (1 + i) is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty V12() 1 -element set
{{x,y},{x}} is non empty set
((Sgm domfvs) * fc9) . x is set
(Sgm domfvs) . x is set
fc9 . ((Sgm domfvs) . x) is set
k is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom fc9 is set
(Sgm domfvs) . k is set
((1,n) -cut sc) . k is set
sc . k is set
i is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
i + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G is non empty V66() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
sc is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
K19(sc) is set
sc . 1 is set
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . (len sc) is set
m is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
K19(m) is set
n is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
vs is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
len m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
vs is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
vs is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v2 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v2 . 1 is set
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v2 . (len v2) is set
len v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() set
vs is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
v1 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v19 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v19 . 1 is set
len v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 . (len v19) is set
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
v1 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v19 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v19 . 1 is set
len v19 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v19 . (len v19) is set
len v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
K19(v2) is set
K19(v19) is set
c2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len c2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len vs2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs2 . 1 is set
vs2 . (len vs2) is set
v29 is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(v2)
Seq v29 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fvs1 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(v19)
Seq fvs1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom vs is set
Sgm (dom vs) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom v29 is set
(Sgm (dom vs)) | (dom v29) is Relation-like NAT -defined dom v29 -defined NAT -defined NAT -valued Function-like FinSubsequence-like Element of K19(K20(NAT,NAT))
K20(NAT,NAT) is Relation-like non finite set
K19(K20(NAT,NAT)) is non finite set
rng ((Sgm (dom vs)) | (dom v29)) is set
vs | (rng ((Sgm (dom vs)) | (dom v29))) is Relation-like NAT -defined rng ((Sgm (dom vs)) | (dom v29)) -defined NAT -defined the carrier' of G -valued Function-like FinSubsequence-like set
fc9 is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq fc9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom v1 is set
Sgm (dom v1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom fvs1 is set
(Sgm (dom v1)) | (dom fvs1) is Relation-like NAT -defined dom fvs1 -defined NAT -defined NAT -valued Function-like FinSubsequence-like Element of K19(K20(NAT,NAT))
rng ((Sgm (dom v1)) | (dom fvs1)) is set
v1 | (rng ((Sgm (dom v1)) | (dom fvs1))) is Relation-like NAT -defined rng ((Sgm (dom v1)) | (dom fvs1)) -defined NAT -defined the carrier of G -valued Function-like FinSubsequence-like set
fvs9 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq fvs9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
fc9 is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq fc9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
sc is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq sc is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
domfc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
p1 is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
SL is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
SL . 1 is set
len SL is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
SL . (len SL) is set
domfvs is Relation-like NAT -defined the carrier' of G -valued Function-like FinSubsequence-like Element of K19(m)
Seq domfvs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
SL is Relation-like NAT -defined the carrier of G -valued Function-like FinSubsequence-like Element of K19(sc)
Seq SL is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
x . 1 is set
len x is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
x . (len x) is set
len p is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg sc is finite sc -element Element of K19(NAT)
G | (Seg sc) is Relation-like NAT -defined Seg sc -defined NAT -defined Function-like FinSubsequence-like set
m is non empty V66() MultiGraphStruct
the carrier' of m is set
v1 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
v2 is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
dom vs is Element of K19(NAT)
vs . v2 is set
G . v2 is set
vs . v1 is set
G . v1 is set
dom G is Element of K19(NAT)
len G is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
Seg (len G) is finite len G -element Element of K19(NAT)
Seg (len vs) is finite len vs -element Element of K19(NAT)
n is Relation-like NAT -defined the carrier' of m -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of m
G is non empty V66() MultiGraphStruct
the carrier' of G is set
sc is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of G
len sc is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
sc . m is set
sc . n is set
the carrier of G is non empty set
vs is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len vs is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
(len sc) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
n + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
m + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT
vs /. m is Element of the carrier of G
vs /. (m + 1) is Element of the carrier of G
vs /. n is Element of the carrier of G
vs /. (n + 1) is Element of the carrier of G
vs . m is set
vs . (m + 1) is set
vs . n is set
vs . (n + 1) is set
sc is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is non empty V66() MultiGraphStruct
the carrier' of G is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is non empty V66() MultiGraphStruct
the carrier' of m is set
v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
vs is non empty V66() MultiGraphStruct
the carrier' of vs is set