REAL is V100() V101() V102() V106() V109() V110() V112() set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal V100() V101() V102() V103() V104() V105() V106() V107() V109() Element of bool REAL
bool REAL is set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal V100() V101() V102() V103() V104() V105() V106() V107() V109() set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is V100() V106() set
RAT is V100() V101() V102() V103() V106() set
INT is V100() V101() V102() V103() V104() V106() set
{} is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set
the Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set
2 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
3 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
0 is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() V123() Element of NAT
dom {} is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set
rng {} is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set
card {} is Relation-like non-empty empty-yielding V6() V7() V8() V10() V11() V12() functional empty finite finite-yielding V32() cardinal {} -element FinSequence-like FinSequence-membered V39() integer ext-real non positive non negative V100() V101() V102() V103() V104() V105() V106() V109() V110() V111() V112() V122() set
{{},1} is non empty finite V32() V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() set
Seg 1 is non empty trivial finite 1 -element V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() Element of bool NAT
G is set
V is functional non empty FinSequence-membered FinSequenceSet of G
bool V is set
E is functional non empty FinSequence-membered Element of bool V
v1 is FinSequence-like Element of E
G is V39() integer even ext-real V122() set
V is V39() integer even ext-real V122() set
G - V is V39() integer ext-real V122() set
E is V39() integer ext-real V122() set
2 * E is V39() integer even ext-real V122() set
v1 is V39() integer ext-real V122() set
2 * v1 is V39() integer even ext-real V122() set
v1 - E is V39() integer ext-real V122() set
2 * (v1 - E) is V39() integer even ext-real V122() set
G is V39() integer ext-real V122() set
V is V39() integer ext-real V122() set
G - V is V39() integer ext-real V122() set
E is V39() integer ext-real V122() set
v1 is V39() integer ext-real V122() set
E - v1 is V39() integer ext-real V122() set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len G is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(V,E) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ((V,E) -cut G) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len ((V,E) -cut G)) + V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
((V,E) -cut G) . (v1 + 1) is set
V + v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G . (V + v1) is set
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
((V,E) -cut G) . (v1 + 1) is set
V + v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G . (V + v1) is set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom G is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(V,E) -cut G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom ((V,E) -cut G) is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
((V,E) -cut G) . v1 is set
V + v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len ((V,E) -cut G) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len G is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
G9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G9 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
V + G9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G . E9 is set
E9 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(len ((V,E) -cut G)) + V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
V + (len ((V,E) -cut G)) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len G is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len G is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len V) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V . E is set
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V . v1 is set
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is set
<*V*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
E is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v2 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . v1 is set
E . v2 is set
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(E,v1) -cut V is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len v2 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v2 . G9 is set
v2 . E9 is set
dom v2 is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
E + E9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
P9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V . P9 is set
P9 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E + G9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
n is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V . n is set
n + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G is non empty V68() MultiGraphStruct
the carrier' of G is set
the carrier of G is non empty set
V is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
rng V is finite set
E is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
rng E is finite set
V ^ E is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
v1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 . (len v1) is set
v2 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v2 . 1 is set
n is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
P9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len P9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
P9 . n is set
P9 . p9 is set
dom P9 is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
V . n is set
V . p9 is set
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
dom E is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V . n is set
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . p is set
vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
dom E is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
dom E is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + p1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
(len V) + vs9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . p is set
E . vs9 is set
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
dom E is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G is non empty V68() MultiGraphStruct
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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 non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<* the Element of the carrier of G*> . 1 is set
len <* the Element of the carrier of G*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
<* the Element of the carrier of G*> . (len <* the Element of the carrier of G*>) is set
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
V + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like cyclic Chain of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
((V + 1),(len E)) -cut E is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(1,V) -cut E is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(((V + 1),(len E)) -cut E) ^ ((1,V) -cut E) is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
len ((1,V) -cut E) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len ((1,V) -cut E)) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
len (((V + 1),(len E)) -cut E) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len (((V + 1),(len E)) -cut E)) + (V + 1) is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(len E) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
the carrier of G is non empty set
P9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(1,(V + 1)) -cut P9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len P9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
((V + 1),(len P9)) -cut P9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(len E) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
p9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
E9 is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
(len P9) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
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 V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len n) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(V + 1) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
G9 is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
len p9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len p9) + (V + 1) is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
1 + (V + 1) is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
p9 ^' n 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 n)) -cut n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p9 ^ ((2,(len n)) -cut n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E9 ^ G9 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
P9 . (len P9) is set
P9 . 1 is set
n . 1 is set
p9 . (len p9) is set
p is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
G9 ^ E9 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
rng G9 is finite set
rng E9 is finite set
n . (len n) is set
P9 . (V + 1) is set
p9 . 1 is set
p . 1 is set
len p is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p . (len p) is set
vs is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Chain of G
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
rng V is finite set
E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
((E + 1),(len V)) -cut V is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(1,E) -cut V is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(((E + 1),(len V)) -cut V) ^ ((1,E) -cut V) is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
len ((((E + 1),(len V)) -cut V) ^ ((1,E) -cut V)) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
rng ((((E + 1),(len V)) -cut V) ^ ((1,E) -cut V)) is finite set
((((E + 1),(len V)) -cut V) ^ ((1,E) -cut V)) . 1 is set
V . (E + 1) is set
(len V) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
((1,E) -cut V) ^ (((E + 1),(len V)) -cut V) is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
len ((1,E) -cut V) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
len (((E + 1),(len V)) -cut V) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len ((1,E) -cut V)) + (len (((E + 1),(len V)) -cut V)) is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
rng ((1,E) -cut V) is finite set
rng (((E + 1),(len V)) -cut V) is finite set
(rng ((1,E) -cut V)) \/ (rng (((E + 1),(len V)) -cut V)) is finite set
(len (((E + 1),(len V)) -cut V)) + (E + 1) is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
1 + (E + 1) is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
dom (((E + 1),(len V)) -cut V) is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(((E + 1),(len V)) -cut V) . (0 + 1) is set
(E + 1) + 0 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
V . ((E + 1) + 0) is set
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E is Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like cyclic Chain of G
dom E is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
E . V is set
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
rng E is finite set
E . 1 is set
1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
v1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(V,(len E)) -cut E is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(1,v1) -cut E is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
((V,(len E)) -cut E) ^ ((1,v1) -cut E) 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 one-to-one finite FinSequence-like FinSubsequence-like cyclic Chain of G
v2 . 1 is set
len v2 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
rng v2 is finite set
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
the carrier' of G is set
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is set
the Source of G . V is set
the Target of G . V is set
<*V*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
E is Element of the carrier of G
v1 is Element of the carrier of G
<*v1,E*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
<*v1,E*> /. (1 + 1) is Element of the carrier of G
len <*V*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
len <*v1,E*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(len <*V*>) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
<*v1,E*> /. E9 is Element of the carrier of G
E9 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
<*v1,E*> /. (E9 + 1) is Element of the carrier of G
<*V*> . E9 is set
<*V*> . 1 is set
<*v1,E*> /. 1 is Element of the carrier of G
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . (len E) is set
E . 1 is set
v1 is set
the Source of G . v1 is set
<*v1*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
V ^ <*v1*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
the Target of G . v1 is set
<*( the Source of G . v1),( the Target of G . v1)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
E ^' <*( the Source of G . v1),( the Target of G . v1)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*( the Source of G . v1),( the Target of G . v1)*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(2,(len <*( the Source of G . v1),( the Target of G . v1)*>)) -cut <*( the Source of G . v1),( the Target of G . v1)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^ ((2,(len <*( the Source of G . v1),( the Target of G . v1)*>)) -cut <*( the Source of G . v1),( the Target of G . v1)*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G9 is Element of the carrier of G
E9 is Element of the carrier of G
<*G9,E9*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
P9 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 Function-like finite FinSequence-like FinSubsequence-like Chain of G
P9 . 1 is set
V ^ v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^' P9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len P9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(2,(len P9)) -cut P9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^ ((2,(len P9)) -cut P9) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
p9 . 1 is set
len p9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p9 . (len p9) is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len V) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
P9 . (len P9) is set
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . (len E) is set
E . 1 is set
v1 is set
the Target of G . v1 is set
<*v1*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
V ^ <*v1*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
the Source of G . v1 is set
<*( the Target of G . v1),( the Source of G . v1)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
E ^' <*( the Target of G . v1),( the Source of G . v1)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*( the Target of G . v1),( the Source of G . v1)*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(2,(len <*( the Target of G . v1),( the Source of G . v1)*>)) -cut <*( the Target of G . v1),( the Source of G . v1)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^ ((2,(len <*( the Target of G . v1),( the Source of G . v1)*>)) -cut <*( the Target of G . v1),( the Source of G . v1)*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E9 is Element of the carrier of G
G9 is Element of the carrier of G
<*E9,G9*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
P9 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 Function-like finite FinSequence-like FinSubsequence-like Chain of G
P9 . 1 is set
V ^ v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^' P9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len P9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(2,(len P9)) -cut P9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
E ^ ((2,(len P9)) -cut P9) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p9 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
p9 . 1 is set
len p9 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p9 . (len p9) is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len V) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
P9 . (len P9) is set
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
the carrier' of G is set
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len E is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
(len V) + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V122() set
v1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E . v1 is set
V . v1 is set
the Target of G . (V . v1) is set
E . (v1 + 1) is set
the Source of G . (V . v1) is set
v2 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . v2 is set
E /. v2 is Element of the carrier of G
v2 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E . (v2 + 1) is set
E /. (v2 + 1) is Element of the carrier of G
V . v2 is set
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
the carrier' of G is set
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
dom V is finite V100() V101() V102() V103() V104() V105() V109() V110() V111() Element of bool NAT
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
v1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
E . v1 is set
V . v1 is set
the Target of G . (V . v1) is set
v1 + 1 is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
E . (v1 + 1) is set
the Source of G . (V . v1) is set
len V is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
the carrier' of G is set
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
rng V is finite set
E is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
rng E is finite set
v1 is set
the Target of G . v1 is set
the Source of G . v1 is set
v2 is Element of the carrier' of G
G9 is Element of the carrier of G
G -VSet (rng V) 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 V & ( b1 = the Source of G . b2 or b1 = the Target of G . b2 ) ) } is set
E9 is Element of the carrier of G
G is non empty V68() MultiGraphStruct
V is set
G -VSet V is set
the carrier of G is non empty set
the carrier' of G is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: 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 V & ( b1 = the Source of G . b2 or b1 = the Target of G . b2 ) ) } is set
bool the carrier of G is set
{ b1 where b1 is Element of the carrier of G : S1[b1] } is set
G is non empty V68() MultiGraphStruct
(G,{}) is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is set
the carrier' of G is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: 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 Source of G . b2 or b1 = the Target of G . b2 ) ) } is set
V is set
E is Element of the carrier of G
v1 is Element of the carrier' of G
the Source of G . v1 is set
the Target of G . v1 is set
G is non empty V68() MultiGraphStruct
the carrier' of G is set
V is set
E is set
(G,E) is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: 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 E & ( b1 = the Source of G . b2 or b1 = the Target of G . b2 ) ) } is set
the Source of G . V is set
v1 is Element of the carrier of G
G is non empty V68() MultiGraphStruct
the carrier of G is non empty set
the carrier' of G is set
the Source of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is set
the Target of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like V25( the carrier' of G, the carrier of G) Element of bool [: the carrier' of G, the carrier of G:]
G9 is Element of the carrier of G
E9 is Element of the carrier of G
v2 is non empty set
{ b1 where b1 is Element of v2 : ( b1 = G9 or ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G ex b3 being Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G st
( not b2 is empty & b3 is_vertex_seq_of b2 & b3 . 1 = G9 & b3 . (len b3) = b1 ) ) } is set
v2 \ { b1 where b1 is Element of v2 : ( b1 = G9 or ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G ex b3 being Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G st
( not b2 is empty & b3 is_vertex_seq_of b2 & b3 . 1 = G9 & b3 . (len b3) = b1 ) ) } is Element of bool v2
bool v2 is set
p9 is non empty set
p is Element of the carrier of G
vs9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
p1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
p1 . 1 is set
len p1 is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
p1 . (len p1) is set
{ b1 where b1 is Element of v2 : S1[b1] } is set
vs9 is set
dom the Source of G is set
the carrier' of G \ vs9 is Element of bool the carrier' of G
bool the carrier' of G is set
the Source of G | ( the carrier' of G \ vs9) is Relation-like the carrier' of G -defined the carrier' of G \ vs9 -defined the carrier' of G -defined the carrier of G -valued Function-like Element of bool [: the carrier' of G, the carrier of G:]
dom ( the Source of G | ( the carrier' of G \ vs9)) is set
(dom the Source of G) /\ ( the carrier' of G \ vs9) is Element of bool the carrier' of G
rng the Source of G is set
rng ( the Source of G | ( the carrier' of G \ vs9)) is set
p is non empty set
vs is set
vs is set
( the Source of G | ( the carrier' of G \ vs9)) . vs is set
p is Element of the carrier' of G
( the Source of G | ( the carrier' of G \ vs9)) . p is set
the Source of G . p is set
the Target of G . p is set
m is Element of the carrier of G
<*p*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
i is Element of the carrier of G
<*G9,i*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
t is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len t is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
t . 1 is set
t . (len t) is set
ep is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
ep is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
t is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
t . 1 is set
len t is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
t . (len t) is set
ep is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
t is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
t . 1 is set
len t is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
t . (len t) is set
<*p*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
ep ^ <*p*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*( the Source of G . p),( the Target of G . p)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
t ^' <*( the Source of G . p),( the Target of G . p)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*( the Source of G . p),( the Target of G . p)*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(2,(len <*( the Source of G . p),( the Target of G . p)*>)) -cut <*( the Source of G . p),( the Target of G . p)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t ^ ((2,(len <*( the Source of G . p),( the Target of G . p)*>)) -cut <*( the Source of G . p),( the Target of G . p)*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
i is Element of the carrier of G
ts is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
ts . 1 is set
len ts is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
ts . (len ts) is set
ep is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
t is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
t . 1 is set
len t is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
t . (len t) is set
the Target of G . p is set
[:( the carrier' of G \ vs9),p:] is Relation-like set
bool [:( the carrier' of G \ vs9),p:] is set
dom the Target of G is set
the Target of G | ( the carrier' of G \ vs9) is Relation-like the carrier' of G -defined the carrier' of G \ vs9 -defined the carrier' of G -defined the carrier of G -valued Function-like Element of bool [: the carrier' of G, the carrier of G:]
dom ( the Target of G | ( the carrier' of G \ vs9)) is set
(dom the Target of G) /\ ( the carrier' of G \ vs9) is Element of bool the carrier' of G
rng the Target of G is set
rng ( the Target of G | ( the carrier' of G \ vs9)) is set
vs is set
p is set
( the Target of G | ( the carrier' of G \ vs9)) . p is set
i is Element of the carrier' of G
( the Target of G | ( the carrier' of G \ vs9)) . i is set
the Target of G . i is set
the Source of G . i is set
ep is Element of the carrier of G
<*i*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
m is Element of the carrier of G
<*G9,m*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
s is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len s is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
s . 1 is set
s . (len s) is set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
s is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
s . 1 is set
len s is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
s . (len s) is set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
s is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
s . 1 is set
len s is V6() V7() V8() V12() finite cardinal V39() integer ext-real non negative V100() V101() V102() V103() V104() V105() V109() V110() V111() V122() V123() Element of NAT
s . (len s) is set
<*i*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
t ^ <*i*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*( the Target of G . i),( the Source of G . i)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
s ^' <*( the Target of G . i),( the Source of G . i)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*( the Target of G . i),( the Source of G . i)*> is V6() V7() V8() V12() non empty finite cardinal V39() integer ext-real positive non negative V100() V101() V102() V103() V104() V105() V107() V108() V109() V110() V111() V122() V123() Element of NAT
(2,(len <*( the Target of G . i),( the Source of G . i)*>)) -cut <*( the Target of G . i),( the Source of G . i)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s ^ ((2,(len <*( the Target of G . i),( the Source of G . i)*>)) -cut <*( the Target of G . i),( the Source of G . i)*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ts is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of G
m is Element of the carrier of G
p1 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
p1 . 1 is