:: GRAPH_5 semantic presentation

REAL is non empty V19() non finite V99() V100() V101() V105() set
NAT is ordinal V19() non finite cardinal limit_cardinal V99() V100() V101() V102() V103() V104() V105() Element of K27(REAL)
K27(REAL) is V19() non finite set
omega is ordinal V19() non finite cardinal limit_cardinal V99() V100() V101() V102() V103() V104() V105() set
K27(omega) is V19() non finite set
K27(NAT) is V19() non finite set
INT is non empty V19() non finite V99() V100() V101() V102() V103() V105() set
K141(NAT) is V42() set
COMPLEX is non empty V19() non finite V99() V105() set
RAT is non empty V19() non finite V99() V100() V101() V102() V105() set
K28(COMPLEX,COMPLEX) is Relation-like V19() non finite V88() set
K27(K28(COMPLEX,COMPLEX)) is V19() non finite set
K28(K28(COMPLEX,COMPLEX),COMPLEX) is Relation-like V19() non finite V88() set
K27(K28(K28(COMPLEX,COMPLEX),COMPLEX)) is V19() non finite set
K28(REAL,REAL) is Relation-like V19() non finite V88() V89() V90() set
K27(K28(REAL,REAL)) is V19() non finite set
K28(K28(REAL,REAL),REAL) is Relation-like V19() non finite V88() V89() V90() set
K27(K28(K28(REAL,REAL),REAL)) is V19() non finite set
K28(RAT,RAT) is Relation-like RAT -valued V19() non finite V88() V89() V90() set
K27(K28(RAT,RAT)) is V19() non finite set
K28(K28(RAT,RAT),RAT) is Relation-like RAT -valued V19() non finite V88() V89() V90() set
K27(K28(K28(RAT,RAT),RAT)) is V19() non finite set
K28(INT,INT) is Relation-like RAT -valued INT -valued V19() non finite V88() V89() V90() set
K27(K28(INT,INT)) is V19() non finite set
K28(K28(INT,INT),INT) is Relation-like RAT -valued INT -valued V19() non finite V88() V89() V90() set
K27(K28(K28(INT,INT),INT)) is V19() non finite set
K28(NAT,NAT) is Relation-like RAT -valued INT -valued V88() V89() V90() V91() set
K28(K28(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V88() V89() V90() V91() set
K27(K28(K28(NAT,NAT),NAT)) is set
K263() is set
1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
K446() is set
K27(K446()) is set
K27(K27(K446())) is set
DEDEKIND_CUTS is non empty Element of K27(K27(K446()))
REAL+ is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V43() real ext-real non positive non negative V88() V89() V90() V91() V99() V100() V101() V102() V103() V104() V105() set
2 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
3 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
Seg 1 is non empty V19() finite 1 -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V43() real V45() V46() ext-real non positive non negative V88() V89() V90() V91() V99() V100() V101() V102() V103() V104() V105() Element of NAT
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued ordinal natural Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V43() real ext-real non positive non negative V88() V89() V90() V91() V99() V100() V101() V102() V103() V104() V105() FinSequence of REAL
Sum (<*> REAL) is V43() real ext-real Element of REAL
K193() is Relation-like Function-like V36(K28(REAL,REAL), REAL ) V88() V89() V90() Element of K27(K28(K28(REAL,REAL),REAL))
K142(REAL,(<*> REAL),K193()) is V43() real ext-real Element of REAL
{ b₁ where b₁ is V43() real ext-real Element of REAL : 0 <= b₁ } is set
e is set
V is Relation-like Function-like set
rng V is set
dom V is set
V . e is set
W is Relation-like Function-like set
rng W is set
dom W is set
F₂() is set
F₁() is set
e is set
V is Element of F₂()
F₃(V) is set
e is Relation-like Function-like set
dom e is set
e is Relation-like Function-like set
dom e is set
V is Element of F₂()
e . V is set
F₃(V) is set
W is Element of F₂()
F₃(W) is set
V is Element of F₂()
e . V is set
F₃(V) is set
e is finite set
e * is functional non empty FinSequence-membered FinSequenceSet of e
V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b₁ & len b₁ <= V ) } is set
W is set
Seg V is finite V -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
G is Relation-like Function-like set
dom G is set
Union G is set
P is set
Q is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e *
len Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom Q is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
R is ordinal natural finite cardinal V43() real ext-real non negative set
Seg R is finite R -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b₁ where b₁ is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : len b₁ = R } is set
R -tuples_on e is finite with_common_domain product-like FinSequenceSet of e
G . R is set
P is set
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
G . Q is set
Q -tuples_on e is finite with_common_domain product-like FinSequenceSet of e
G . P is set
e is finite set
e * is functional non empty FinSequence-membered FinSequenceSet of e
V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : len b₁ <= V } is set
W is set
{ b₁ where b₁ is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b₁ & len b₁ <= V ) } is set
{{}} is functional non empty V19() finite V28() 1 -element V99() V100() V101() V102() V103() V104() set
{{}} \/ { b₁ where b₁ is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b₁ & len b₁ <= V ) } is non empty set
P is set
Q is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e *
len Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
e is finite set
card e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
K27(e) is finite V28() set
V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
W is set
{W} is non empty V19() finite 1 -element set
e \ {W} is finite Element of K27(e)
P is Element of e
{P} is non empty V19() finite 1 -element set
G is finite Element of K27(e)
G \/ {P} is non empty finite set
card G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
(card G) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
e is finite set
card e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
K27(e) is finite V28() set
W is finite Element of K27(e)
V is Element of e
{V} is non empty V19() finite 1 -element set
W \/ {V} is non empty finite set
card W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
F₁() is non empty finite set
K27(F₁()) is finite V28() set
card F₁() is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of omega
(card F₁()) -' 1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
((card F₁()) -' 1) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(card F₁()) - 1 is V43() real ext-real set
((card F₁()) - 1) + 1 is V43() real ext-real set
e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e + 1) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
V is finite Element of K27(F₁())
card V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
K27(V) is finite V28() set
G is finite Element of K27(V)
W is Element of V
{W} is non empty V19() finite 1 -element set
G \/ {W} is non empty finite set
card G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
Q is finite Element of K27(F₁())
R is Element of F₁()
F₂(R) is V43() real ext-real set
P is Element of F₁()
F₂(P) is V43() real ext-real set
v1 is Element of F₁()
v2 is Element of F₁()
F₂(v2) is V43() real ext-real set
F₂(v1) is V43() real ext-real set
{v1} is non empty V19() finite 1 -element set
F₂(v1) is V43() real ext-real set
F₂(v2) is V43() real ext-real set
{v1} is non empty V19() finite 1 -element set
F₂(v1) is V43() real ext-real set
F₂(v1) is V43() real ext-real set
P is Element of F₁()
F₂(P) is V43() real ext-real set
v1 is Element of F₁()
v2 is Element of F₁()
F₂(v1) is V43() real ext-real set
F₂(v2) is V43() real ext-real set
{P} is non empty V19() finite 1 -element set
F₂(v1) is V43() real ext-real set
F₂(v2) is V43() real ext-real set
{P} is non empty V19() finite 1 -element set
F₂(v1) is V43() real ext-real set
F₂(v1) is V43() real ext-real set
P is Element of F₁()
F₂(P) is V43() real ext-real set
V is finite Element of K27(F₁())
card V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
e is finite Element of K27(F₁())
card e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
V is Element of e
{V} is non empty V19() finite 1 -element set
W is Element of F₁()
F₂(W) is V43() real ext-real set
G is Element of F₁()
F₂(G) is V43() real ext-real set
e is Element of F₁()
F₂(e) is V43() real ext-real set
V is Element of F₁()
F₂(V) is V43() real ext-real set
e is set
e * is functional non empty FinSequence-membered FinSequenceSet of e
K27((e *)) is set
V is functional non empty FinSequence-membered Element of K27((e *))
W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of V
G is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e *
e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . e is set
W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V ^ W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(V ^ W) . e is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . e is set
W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W ^ V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len W) + e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(W ^ V) . ((len W) + e) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
e is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V is set
dom e is finite set
W is set
e . V is set
e . W is set
dom e is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e . V is set
W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e . W is set
dom e is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
e is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
rng e is finite set
card (rng e) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e . V is set
e . W is set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
the Source of V is Relation-like Function-like V36( the carrier' of V, the carrier of V) Element of K27(K28( the carrier' of V, the carrier of V))
the carrier of V is non empty set
K28( the carrier' of V, the carrier of V) is Relation-like set
K27(K28( the carrier' of V, the carrier of V)) is set
W . e is set
the Source of V . (W . e) is set
the Target of V is Relation-like Function-like V36( the carrier' of V, the carrier of V) Element of K27(K28( the carrier' of V, the carrier of V))
the Target of V . (W . e) is set
e is set
<*e*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V ^ <*e*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng (V ^ <*e*>) is non empty finite set
rng V is finite set
W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng W is finite set
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V ^ <*e*>) . ((len V) + 1) is set
len (V ^ <*e*>) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom (V ^ <*e*>) is non empty finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
Q is set
W . Q is set
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 is ordinal natural finite cardinal V43() real ext-real non negative set
R + v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 ^ Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pe is ordinal natural finite cardinal V43() real ext-real non negative set
1 + pe is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V9 is set
<*V9*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
pe ^ <*V9*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
dom v3 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v3 . R is set
pe ^ <*e*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(pe ^ <*e*>) ^ Eg is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
pe ^ Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (pe ^ Eg) is finite set
len pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len pe) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s is set
FT is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
FS is set
V . FS is set
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V ^ <*e*>) . x is set
rng (pe ^ <*e*>) is non empty finite set
rng Eg is finite set
(rng (pe ^ <*e*>)) \/ (rng Eg) is non empty finite set
rng pe is finite set
rng <*e*> is non empty V19() finite 1 -element set
(rng pe) \/ (rng <*e*>) is non empty finite set
((rng pe) \/ (rng <*e*>)) \/ (rng Eg) is non empty finite set
(rng pe) \/ (rng Eg) is finite set
((rng pe) \/ (rng Eg)) \/ (rng <*e*>) is non empty finite set
(rng (pe ^ Eg)) \/ (rng <*e*>) is non empty finite set
{e} is non empty V19() finite 1 -element set
(rng (pe ^ Eg)) \/ {e} is non empty finite set
e is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
e ^ V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
the carrier of W is non empty set
len (e ^ V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len (e ^ V)) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + (len V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + ((len V) + 1) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 ^ v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len v1) + Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len v1) + (len v3) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom v3 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v3 . Eg is set
R . ((len v1) + Eg) is set
Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . ((len e) + Eg) is set
((len e) + Eg) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . (((len e) + Eg) + 1) is set
(e ^ V) . ((len e) + Eg) is set
V9 is Element of the carrier of W
s is Element of the carrier of W
FT is Element of the carrier of W
v3 . Eg is set
Eg + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 . (Eg + 1) is set
(len v1) + (Eg + 1) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . ((len v1) + (Eg + 1)) is set
FS is Element of the carrier of W
V . Eg is set
(len e) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
((len e) + 1) + (len V) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 ^ Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . V9 is set
dom pe is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
pe . V9 is set
V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . V9 is set
V9 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
R . (V9 + 1) is set
(e ^ V) . V9 is set
s is Element of the carrier of W
FT is Element of the carrier of W
FS is Element of the carrier of W
pe . V9 is set
x is Element of the carrier of W
pe . (V9 + 1) is set
e . V9 is set
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom e is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
e . pe is set
pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
V . pe is set
pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
e ^ V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
len (e ^ V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + (len V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . (P + 1) is set
(len e) + (P + 1) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e ^ V) . ((len e) + (P + 1)) is set
((len e) + P) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e ^ V) . (((len e) + P) + 1) is set
the Source of W is Relation-like Function-like V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
the carrier of W is non empty set
K28( the carrier' of W, the carrier of W) is Relation-like set
K27(K28( the carrier' of W, the carrier of W)) is set
the Source of W . ((e ^ V) . (((len e) + P) + 1)) is set
the Target of W is Relation-like Function-like V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
(e ^ V) . ((len e) + P) is set
the Target of W . ((e ^ V) . ((len e) + P)) is set
the Source of W . (V . (P + 1)) is set
V . P is set
the Target of W . (V . P) is set
P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
e . (P + 1) is set
(e ^ V) . (P + 1) is set
the Source of W . ((e ^ V) . (P + 1)) is set
(e ^ V) . P is set
the Target of W . ((e ^ V) . P) is set
the Source of W . (e . (P + 1)) is set
e . P is set
the Target of W . (e . P) is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the carrier of e is non empty set
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . (len V) is set
the Target of e . (V . (len V)) is set
W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
W . 1 is set
the Source of e . (W . 1) is set
V ^ W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
G is Relation-like NAT -defined the carrier of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len W) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
G /. 1 is Element of the carrier of e
1 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
G /. (1 + 1) is Element of the carrier of e
G . 1 is set
P is Relation-like NAT -defined the carrier of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
P /. (len V) is Element of the carrier of e
P /. ((len V) + 1) is Element of the carrier of e
P /. (len P) is Element of the carrier of e
P . (len P) is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty set
the Element of the carrier of e is Element of the carrier of e
<* the Element of the carrier of e*> is Relation-like NAT -defined the carrier of e -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of e
G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len <* the Element of the carrier of e*> is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
<* the Element of the carrier of e*> . G is set
<* the Element of the carrier of e*> . P is set
e is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
e ^ V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
the carrier of W is non empty set
P is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len (e ^ V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len (e ^ V)) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
len e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + (len V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
((len e) + 1) + (len V) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
Q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Q ^ R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + ((len V) + 1) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 ^ v2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 . Eg is set
v3 . pe is set
P . Eg is set
P . pe is set
(len v3) + 0 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len e) + pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
((len e) + pe) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
pe + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom Eg is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
Eg /. (pe + 1) is Element of the carrier of W
Eg . (pe + 1) is set
(len v1) + (pe + 1) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . ((len v1) + (pe + 1)) is set
P /. (((len e) + pe) + 1) is Element of the carrier of W
pe + 0 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg /. pe is Element of the carrier of W
Eg . pe is set
P . ((len e) + pe) is set
P /. ((len e) + pe) is Element of the carrier of W
(e ^ V) . ((len e) + pe) is set
V . pe is set
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe + 0 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom v3 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v3 /. pe is Element of the carrier of W
v3 . pe is set
P . pe is set
P /. pe is Element of the carrier of W
v3 /. (pe + 1) is Element of the carrier of W
v3 . (pe + 1) is set
P . (pe + 1) is set
P /. (pe + 1) is Element of the carrier of W
(e ^ V) . pe is set
e . pe is set
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Eg . pe is set
Eg . V9 is set
(len v1) + pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . ((len v1) + pe) is set
(len v1) + V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . ((len v1) + V9) is set
0 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
e is non empty V73() MultiGraphStruct
the carrier' of e is set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the carrier of e is non empty set
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
V . 1 is set
the Source of e . (V . 1) is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the Target of e . (V . 1) is set
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
V . Q is set
Q is Element of the carrier of e
R is Element of the carrier of e
<*Q,R*> is Relation-like NAT -defined the carrier of e -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len <*Q,R*> is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 is Element of the carrier of e
<*Q,R*> . v2 is set
Eg is Element of the carrier of e
v2 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*Q,R*> . (v2 + 1) is set
V . v2 is set
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*Q,R*> . v2 is set
<*Q,R*> . v3 is set
1 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v3 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*Q,R*> . v2 is set
<*Q,R*> . v2 is set
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . (v2 + 1) is set
the Source of e . (V . (v2 + 1)) is set
V . v2 is set
the Target of e . (V . v2) is set
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*Q,R*> /. 1 is Element of the carrier of e
<*Q,R*> /. (1 + 1) is Element of the carrier of e
<*Q,R*> /. v2 is Element of the carrier of e
v2 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*Q,R*> /. (v2 + 1) is Element of the carrier of e
V . v2 is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the carrier of e is non empty set
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . (len V) is set
the Target of e . (V . (len V)) is set
V . 1 is set
the Source of e . (V . 1) is set
W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
len W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W . 1 is set
the Source of e . (W . 1) is set
the Target of e . (W . 1) is set
V ^ W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s is Relation-like NAT -defined the carrier of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V9 is Element of the carrier of e
<*V9*> is Relation-like NAT -defined the carrier of e -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of e
s ^ <*V9*> is Relation-like NAT -defined the carrier of e -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. x is Element of the carrier of e
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. (x + 1) is Element of the carrier of e
V . x is set
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len (V ^ W) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe is Element of the carrier of e
s /. (len V) is Element of the carrier of e
s /. ((len V) + 1) is Element of the carrier of e
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s1 is Element of the carrier of e
s . x is set
(s ^ <*V9*>) . x is set
s2 is Element of the carrier of e
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(s ^ <*V9*>) . (x + 1) is set
(V ^ W) . x is set
s /. x is Element of the carrier of e
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. (x + 1) is Element of the carrier of e
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
k is Element of the carrier of e
s . x is set
(s ^ <*V9*>) . x is set
s1 is Element of the carrier of e
s . (x + 1) is set
(s ^ <*V9*>) . (x + 1) is set
V . x is set
(V ^ W) . x is set
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom (V ^ W) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
(V ^ W) . x is set
rng (V ^ W) is finite set
rng V is finite set
rng W is finite set
(rng V) \/ (rng W) is finite set
len (s ^ <*V9*>) is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len s) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len (V ^ W)) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. (len V) is Element of the carrier of e
s /. ((len V) + 1) is Element of the carrier of e
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(s ^ <*V9*>) . x is set
(s ^ <*V9*>) . k is set
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s . x is set
s . k is set
s /. 1 is Element of the carrier of e
1 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. (1 + 1) is Element of the carrier of e
s1 is ordinal natural finite cardinal V43() real ext-real non negative set
s1 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s /. s2 is Element of the carrier of e
s /. (s2 + 1) is Element of the carrier of e
V . s2 is set
the Target of e . (V . s2) is set
s . (s2 + 1) is set
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . (x + 1) is set
the Source of e . (V . (x + 1)) is set
V . x is set
the Target of e . (V . x) is set
(V ^ W) . x is set
(V ^ W) . (x + 1) is set
the Source of e . ((V ^ W) . (x + 1)) is set
the Target of e . ((V ^ W) . x) is set
(V ^ W) . x is set
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V ^ W) . (x + 1) is set
the Source of e . ((V ^ W) . (x + 1)) is set
the Target of e . ((V ^ W) . x) is set
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(s ^ <*V9*>) . x is set
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s . x is set
(s ^ <*V9*>) . x is set
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom (s ^ <*V9*>) is non empty finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
s /. (x + 1) is Element of the carrier of e
s . (x + 1) is set
(s ^ <*V9*>) . (x + 1) is set
(s ^ <*V9*>) /. (x + 1) is Element of the carrier of e
s /. x is Element of the carrier of e
V . x is set
s . x is set
(s ^ <*V9*>) . x is set
(s ^ <*V9*>) /. x is Element of the carrier of e
(V ^ W) . x is set
x + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(s ^ <*V9*>) . (x + 1) is set
(s ^ <*V9*>) /. (x + 1) is Element of the carrier of e
pe is Element of the carrier of e
s . x is set
(s ^ <*V9*>) . x is set
(s ^ <*V9*>) /. x is Element of the carrier of e
(V ^ W) . x is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
the carrier of e is non empty set
G is Relation-like NAT -defined the carrier of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
G /. Q is Element of the carrier of e
Q + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
G /. (Q + 1) is Element of the carrier of e
V . Q is set
V . P is set
G /. P is Element of the carrier of e
P + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
G /. (P + 1) is Element of the carrier of e
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
the Source of e . (V . Q) is set
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
G . P is set
G . Q is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the carrier of e is non empty set
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
V is Element of the carrier' of e
the Source of e . V is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the Target of e . V is set
{( the Source of e . V),( the Target of e . V)} is non empty finite set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b₁ where b₁ is Element of the carrier of e : ex b₂ being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b₂ in dom V & b₁ in (e,(V /. b₂)) ) } is set
K27( the carrier of e) is set
G is set
P is Element of the carrier of e
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V /. Q is Element of the carrier' of e
(e,(V /. Q)) is set
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
the Source of e . (V /. Q) is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the Target of e . (V /. Q) is set
{( the Source of e . (V /. Q)),( the Target of e . (V /. Q))} is non empty finite set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the Source of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
the carrier of e is non empty set
K28( the carrier' of e, the carrier of e) is Relation-like set
K27(K28( the carrier' of e, the carrier of e)) is set
the Target of e is Relation-like Function-like V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, the carrier of e))
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
len V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e,V) is Element of K27( the carrier of e)
K27( the carrier of e) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b₁ where b₁ is Element of the carrier of e : ex b₂ being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b₂ in dom V & b₁ in (e,(V /. b₂)) ) } is set
W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
V ^ W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
len W is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e,W) is Element of K27( the carrier of e)
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b₁ where b₁ is Element of the carrier of e : ex b₂ being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b₂ in dom W & b₁ in (e,(W /. b₂)) ) } is set
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
G . 1 is set
the Source of e . (G . 1) is set
len G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
G . (len G) is set
the Target of e . (G . (len G)) is set
R is Relation-like NAT -defined the carrier of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of e
len R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len G) + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len V) + (len W) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
R /. 1 is Element of the carrier of e
1 + 1 is ordinal natural non empty finite cardinal V43() real V45() V46() ext-real positive non negative V99() V100() V101() V102() V103() V104() Element of NAT
R /. (1 + 1) is Element of the carrier of e
R . 1 is set
R /. (len G) is Element of the carrier of e
R /. ((len G) + 1) is Element of the carrier of e
R . (len R) is set
v1 is Element of the carrier of e
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v2 is Element of the carrier' of e
(e,(W /. v2)) is set
the Source of e . (W /. v2) is set
the Target of e . (W /. v2) is set
{( the Source of e . (W /. v2)),( the Target of e . (W /. v2))} is non empty finite set
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v2 is Element of the carrier' of e
(e,(W /. v2)) is set
the Source of <