:: GRAPH_4 semantic presentation

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

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

{ b

( b

(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

{ b

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

{ b

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

{ b

{ b

x is set

y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT

{ b

y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT

{ b

y is ext-real non negative V24() V25() V26() V30() V31() finite cardinal V80() Element of NAT

{ b

{ b

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