:: GRAPH_3 semantic presentation

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

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

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

{{},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

bool V is set

v1 is FinSequence-like Element of E

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

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

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

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

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

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

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

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

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

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

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

rng V is finite set

rng E is finite set

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 . 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

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

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

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

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

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

(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

(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

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

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 . (len P9) is set
P9 . 1 is set
n . 1 is set
p9 . (len p9) is set

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

G is non empty V68() MultiGraphStruct
the carrier' of G is set

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

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

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

E is Element of the carrier of G
v1 is Element 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
() + 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:]

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

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

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 . 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

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:]

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

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

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 . 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

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:]

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 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:]

dom V 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
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:]

rng V is finite set

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

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

i is Element 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

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

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

i is Element 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

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

m is Element 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

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

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

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

m is Element of the carrier of G

p1 . 1 is