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()