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
{ b1 where b1 is V43() real ext-real Element of REAL : 0 <= b1 } 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
F2() is set
F1() is set
e is set
V is Element of F2()
F3(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 F2()
e . V is set
F3(V) is set
W is Element of F2()
F3(W) is set
V is Element of F2()
e . V is set
F3(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
{ b1 where b1 is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b1 & len b1 <= 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)
{ b1 where b1 is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : len b1 = 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
{ b1 where b1 is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : len b1 <= V } is set
W is set
{ b1 where b1 is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b1 & len b1 <= V ) } is set
{{}} is functional non empty V19() finite V28() 1 -element V99() V100() V101() V102() V103() V104() set
{{}} \/ { b1 where b1 is Relation-like NAT -defined e -valued Function-like finite FinSequence-like FinSubsequence-like Element of e * : ( 1 <= len b1 & len b1 <= 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
F1() is non empty finite set
K27(F1()) is finite V28() set
card F1() 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 F1()) -' 1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
((card F1()) -' 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 F1()) - 1 is V43() real ext-real set
((card F1()) - 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(F1())
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(F1())
R is Element of F1()
F2(R) is V43() real ext-real set
P is Element of F1()
F2(P) is V43() real ext-real set
v1 is Element of F1()
v2 is Element of F1()
F2(v2) is V43() real ext-real set
F2(v1) is V43() real ext-real set
{v1} is non empty V19() finite 1 -element set
F2(v1) is V43() real ext-real set
F2(v2) is V43() real ext-real set
{v1} is non empty V19() finite 1 -element set
F2(v1) is V43() real ext-real set
F2(v1) is V43() real ext-real set
P is Element of F1()
F2(P) is V43() real ext-real set
v1 is Element of F1()
v2 is Element of F1()
F2(v1) is V43() real ext-real set
F2(v2) is V43() real ext-real set
{P} is non empty V19() finite 1 -element set
F2(v1) is V43() real ext-real set
F2(v2) is V43() real ext-real set
{P} is non empty V19() finite 1 -element set
F2(v1) is V43() real ext-real set
F2(v1) is V43() real ext-real set
P is Element of F1()
F2(P) is V43() real ext-real set
V is finite Element of K27(F1())
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(F1())
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 F1()
F2(W) is V43() real ext-real set
G is Element of F1()
F2(G) is V43() real ext-real set
e is Element of F1()
F2(e) is V43() real ext-real set
V is Element of F1()
F2(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)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom V & b1 in (e,(V /. b2)) ) } 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)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom V & b1 in (e,(V /. b2)) ) } 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)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (e,(W /. b2)) ) } 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 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
(len V) + 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 set
G . ((len V) + v2) is set
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
1 + v2 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 V) + v2) is Element of the carrier of e
((len V) + 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
R /. (((len V) + v2) + 1) is Element of the carrier of e
the Source of e . (G . ((len V) + v2)) is set
R . ((len V) + v2) is set
the Target of e . (G . ((len V) + v2)) is set
R . (((len V) + v2) + 1) is set
the Source of e . (G . ((len V) + v2)) is set
the Target of e . (G . ((len V) + v2)) 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
V /. v2 is Element of the carrier' of e
(e,(V /. v2)) is set
the Source of e . (V /. v2) is set
the Target of e . (V /. v2) is set
{( the Source of e . (V /. v2)),( the Target of e . (V /. 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
V /. v2 is Element of the carrier' of e
(e,(V /. v2)) is set
the Source of e . (V /. v2) is set
the Target of e . (V /. v2) is set
{( the Source of e . (V /. v2)),( the Target of e . (V /. v2))} is non empty finite set
V . v2 is set
G . v2 is set
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
R /. (v2 + 1) is Element of the carrier of e
the Source of e . (G . v2) is set
R . v2 is set
the Target of e . (G . v2) is 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
R . (v2 + 1) is set
the Source of e . (G . v2) is set
the Target of e . (G . v2) is set
e is set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W) is Element of K27( the carrier of V)
the carrier of V is non empty set
K27( the carrier of V) is set
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (V,(W /. b2)) ) } is set
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))
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
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))
Q is ordinal natural finite cardinal V43() real ext-real non negative 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
W /. Q is Element of the carrier' of V
(V,(W /. Q)) is set
the Source of V . (W /. Q) is set
the Target of V . (W /. Q) is set
{( the Source of V . (W /. Q)),( the Target of V . (W /. Q))} is non empty finite set
R is set
W . Q is set
the Source of V . (W . Q) is set
the Target of V . (W . Q) is set
v1 is Element of the carrier of V
Q is set
R is Element of the carrier of V
v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v1 is Element of the carrier' of V
(V,(W /. v1)) is set
the Source of V . (W /. v1) is set
the Target of V . (W /. v1) is set
{( the Source of V . (W /. v1)),( the Target of V . (W /. v1))} is non empty finite set
v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v1 is Element of the carrier' of V
(V,(W /. v1)) is set
the Source of V . (W /. v1) is set
the Target of V . (W /. v1) is set
{( the Source of V . (W /. v1)),( the Target of V . (W /. v1))} is non empty finite set
e is set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W) is Element of K27( the carrier of V)
the carrier of V is non empty set
K27( the carrier of V) is set
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (V,(W /. b2)) ) } is 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
G is ordinal natural finite cardinal V43() real ext-real non negative set
W /. G is Element of the carrier' of V
(V,(W /. G)) is set
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))
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
the Source of V . (W /. G) 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 /. G) is set
{( the Source of V . (W /. G)),( the Target of V . (W /. G))} is non empty finite set
P is ordinal natural finite cardinal V43() real ext-real non negative set
G + P is ordinal natural finite cardinal V43() real ext-real non negative set
R is ordinal natural finite cardinal V43() real ext-real non negative set
1 + 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
v1 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
1 + Q 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 + (1 + Q) 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 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
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
v2 ^ v3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v1 + 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 /. (v1 + 1) is Element of the carrier' of V
(V,(W /. (v1 + 1))) is set
the Source of V . (W /. (v1 + 1)) is set
the Target of V . (W /. (v1 + 1)) is set
{( the Source of V . (W /. (v1 + 1))),( the Target of V . (W /. (v1 + 1)))} is non empty finite set
Eg is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V,Eg) is Element of K27( the carrier of V)
dom Eg is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom Eg & b1 in (V,(Eg /. b2)) ) } is set
pe is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
Eg ^ pe is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
V9 is ordinal natural finite cardinal V43() real ext-real non negative set
Eg /. V9 is Element of the carrier' of V
(V,(Eg /. V9)) is set
the Source of V . (Eg /. V9) is set
the Target of V . (Eg /. V9) is set
{( the Source of V . (Eg /. V9)),( the Target of V . (Eg /. V9))} is non empty finite set
Eg . V9 is set
W . V9 is set
W /. V9 is Element of the carrier' of V
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
rng V is finite set
(e,V) is Element of K27( the carrier of e)
the carrier of e is non empty set
K27( the carrier of e) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom V & b1 in (e,(V /. b2)) ) } 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
rng W is finite set
(e,W) is Element of K27( the carrier of e)
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (e,(W /. b2)) ) } 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
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
V . Q is set
R is set
W . R is set
v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v1 is Element of the carrier' of e
e is set
V is set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
the carrier of W is non empty set
G is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
rng G is finite set
(W,G) is Element of K27( the carrier of W)
K27( the carrier of W) is set
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom G & b1 in (W,(G /. b2)) ) } is set
(W,G) \ e is Element of K27( the carrier of W)
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
rng P is finite set
(W,P) is Element of K27( the carrier of W)
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom P & b1 in (W,(P /. b2)) ) } is set
(W,P) \ e is Element of K27( the carrier of W)
e is set
V is set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
the carrier of W is non empty set
G is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,G) is Element of K27( the carrier of W)
K27( the carrier of W) is set
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom G & b1 in (W,(G /. b2)) ) } is set
(W,G) \ e is Element of K27( the carrier of W)
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
G ^ P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,(G ^ P)) is Element of K27( the carrier of W)
dom (G ^ P) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom (G ^ P) & b1 in (W,((G ^ P) /. b2)) ) } is set
(W,(G ^ P)) \ e is Element of K27( the carrier of W)
(W,P) is Element of K27( the carrier of W)
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom P & b1 in (W,(P /. b2)) ) } is set
(W,P) \ e is Element of K27( the carrier of W)
rng G is finite set
rng (G ^ P) is finite set
rng P is finite set
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 non empty V73() MultiGraphStruct
the carrier' of V is set
the carrier of V is non empty set
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))
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
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))
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)
W . e is set
the Source of V . (W . e) is set
the Target of V . (W . e) is set
(V,W) is Element of K27( the carrier of V)
K27( the carrier of V) is set
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (V,(W /. b2)) ) } is set
G is Element of the carrier of V
W /. e is Element of the carrier' of V
the Source of V . (W /. e) is set
the Target of V . (W /. e) is set
(V,(W /. e)) is set
{( the Source of V . (W /. e)),( the Target of V . (W /. e))} is non empty finite 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 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)
the carrier of e is non empty set
K27( the carrier of e) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom V & b1 in (e,(V /. b2)) ) } is set
V /. 1 is Element of the carrier' of e
(e,(V /. 1)) 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 /. 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
{( the Source of e . (V /. 1)),( the Target of e . (V /. 1))} is non empty finite set
P is set
Q is Element of the carrier of e
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V /. R is Element of the carrier' of e
(e,(V /. R)) is set
the Source of e . (V /. R) is set
the Target of e . (V /. R) is set
{( the Source of e . (V /. R)),( the Target of e . (V /. R))} is non empty finite set
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V /. R is Element of the carrier' of e
(e,(V /. R)) is set
the Source of e . (V /. R) is set
the Target of e . (V /. R) is set
{( the Source of e . (V /. R)),( the Target of e . (V /. R))} is non empty finite set
V . 1 is set
the Source of e . (V . 1) is set
the Target of e . (V . 1) is set
Q is Element of the carrier of e
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
(e,V) is Element of K27( the carrier of e)
the carrier of e is non empty set
K27( the carrier of e) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom V & b1 in (e,(V /. b2)) ) } 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
(e,(V ^ W)) is Element of K27( the carrier of e)
dom (V ^ W) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom (V ^ W) & b1 in (e,((V ^ W) /. b2)) ) } is set
(e,W) is Element of K27( the carrier of e)
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (e,(W /. b2)) ) } is set
rng V is finite set
rng (V ^ W) is finite set
rng W is finite 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
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
V . 1 is set
the Target of e . (V . 1) is set
{( the Target of e . (V . 1))} is non empty V19() finite 1 -element set
W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,W) is Element of K27( the carrier of e)
K27( the carrier of e) is set
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (e,(W /. b2)) ) } is set
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
G ^ 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 G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(e,G) is Element of K27( the carrier of e)
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom G & b1 in (e,(G /. b2)) ) } is set
(e,G) \/ {( the Target of e . (V . 1))} is non empty 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))
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 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
v1 is set
v2 is Element of the carrier of e
v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v3 is Element of the carrier' of e
(e,(W /. v3)) is set
the Source of e . (W /. v3) is set
the Target of e . (W /. v3) is set
{( the Source of e . (W /. v3)),( the Target of e . (W /. v3))} is non empty finite set
v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. v3 is Element of the carrier' of e
(e,(W /. v3)) is set
the Source of e . (W /. v3) is set
the Target of e . (W /. v3) is set
{( the Source of e . (W /. v3)),( the Target of e . (W /. v3))} is non empty finite set
W . v3 is set
G . v3 is set
G /. v3 is Element of the carrier' of e
Eg is Element of the carrier of e
W . v3 is set
the Source of e . (W . v3) is set
W . (len G) is set
the Target of e . (W . (len G)) is set
G . (len G) is set
the Target of e . (G . (len G)) is set
G /. (len G) is Element of the carrier' of e
the Target of e . (G /. (len G)) is set
(e,(G /. (len G))) is set
the Source of e . (G /. (len G)) is set
{( the Source of e . (G /. (len G))),( the Target of e . (G /. (len G)))} is non empty finite set
Eg is Element of the carrier of e
W . v3 is set
the Target of e . (W . v3) is set
Eg is Element of the carrier of e
W . v3 is set
the Source of e . (W . v3) is set
the Target of e . (W . v3) is set
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v2 is Element of the carrier of e
W . (len W) is set
the Target of e . (W . (len W)) is set
W /. (len W) is Element of the carrier' of e
the Target of e . (W /. (len W)) is set
(e,(W /. (len W))) is set
the Source of e . (W /. (len W)) is set
{( the Source of e . (W /. (len W))),( the Target of e . (W /. (len W)))} is non empty finite set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
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))
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 Element of the carrier of e
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
(e,W) is Element of K27( the carrier of e)
K27( the carrier of e) is set
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom W & b1 in (e,(W /. b2)) ) } is 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
Q is Element of the carrier of e
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. R is Element of the carrier' of e
(e,(W /. R)) is set
the Source of e . (W /. R) is set
the Target of e . (W /. R) is set
{( the Source of e . (W /. R)),( the Target of e . (W /. R))} is non empty finite set
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
W /. R is Element of the carrier' of e
(e,(W /. R)) is set
the Source of e . (W /. R) is set
the Target of e . (W /. R) is set
{( the Source of e . (W /. R)),( the Target of e . (W /. R))} is non empty finite set
W . R is set
the Target of e . (W . R) is set
W . R is set
the Source of e . (W . R) is set
v1 is ordinal natural finite cardinal V43() real ext-real non negative set
1 + v1 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
W . v2 is set
the Target of e . (W . v2) is set
W . R is set
the Target of e . (W . R) is set
the Source of e . (W . R) is set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e : (e,b1,V,W) } is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
P is set
Q is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,G) is Element of K27( the carrier of e)
K27( the carrier of e) is set
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of e : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom G & b1 in (e,(G /. b2)) ) } 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
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
G . 1 is set
the Source of e . (G . 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))
G . (len G) is set
the Target of e . (G . (len G)) is set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
Q is non empty V73() MultiGraphStruct
the carrier of Q is non empty set
the carrier' of Q is set
e is set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V is set
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V : (V,b1,W,G) } is set
v2 is Relation-like NAT -defined the carrier' of Q -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of Q
P is set
R is Element of the carrier of Q
v1 is Element of the carrier of Q
(Q,R,v1) is functional FinSequence-membered Element of K27(( the carrier' of Q *))
the carrier' of Q * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of Q
K27(( the carrier' of Q *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of Q -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of Q : (Q,b1,R,v1) } is set
e is set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
the carrier' of V is set
W is Element of the carrier of V
G is Element of the carrier of V
P is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
(V,P) is Element of K27( the carrier of V)
K27( the carrier of V) is set
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom P & b1 in (V,(P /. b2)) ) } is set
{G} is non empty V19() finite 1 -element set
(V,P) \ {G} is Element of K27( the carrier of V)
e is set
V is set
W is non empty V73() MultiGraphStruct
the carrier of W is non empty set
the carrier' of W is set
G is Element of the carrier of W
P is Element of the carrier of W
Q is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,Q) is Element of K27( the carrier of W)
K27( the carrier of W) is set
dom Q is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom Q & b1 in (W,(Q /. b2)) ) } is set
{P} is non empty V19() finite 1 -element set
(W,Q) \ {P} is Element of K27( the carrier of W)
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
V . 1 is 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
W is Element of the carrier of e
G is Element of the carrier of e
P is Element of the carrier of e
Q is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain 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
Q ^ V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
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))
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))
Q . (len Q) is set
the Target of e . (Q . (len Q)) is set
the Source of e . (V . 1) is set
v2 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
len v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len 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
the Target of e . (V . 1) is set
v2 . (len v2) is set
the Target of e . (v2 . (len v2)) is set
Q . 1 is set
the Source of e . (Q . 1) is set
v2 . 1 is set
the Source of e . (v2 . 1) is set
e is set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
the carrier of V is non empty set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of 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
W . 1 is set
G is Element of the carrier of V
P is Element of the carrier of V
{P} is non empty V19() finite 1 -element set
e \/ {P} is non empty set
Q is Element of the carrier of V
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
v1 ^ W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
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))
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
the Target of V . (W . 1) is set
(V,R) is Element of K27( the carrier of V)
K27( the carrier of V) is set
dom R is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom R & b1 in (V,(R /. b2)) ) } is set
{Q} is non empty V19() finite 1 -element set
(V,R) \ {Q} is Element of K27( the carrier of V)
(V,v1) is Element of K27( the carrier of V)
dom v1 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom v1 & b1 in (V,(v1 /. b2)) ) } is set
(V,v1) \/ {Q} is non empty set
((V,v1) \/ {Q}) \ {Q} is Element of K27(((V,v1) \/ {Q}))
K27(((V,v1) \/ {Q})) is set
(V,v1) \ {Q} is Element of K27( the carrier of V)
(V,v1) \ {P} is Element of K27( the carrier of V)
v3 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
P is set
Q is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
G is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W,G) } is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
Q is set
R is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
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 Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
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))
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
rng V is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (V . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (V . (len V)) & rng b1 c= rng V ) } is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
G is set
P is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
P . 1 is set
the Source of e . (P . 1) is set
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . (len P) is set
the Target of e . (P . (len P)) is set
rng P is finite set
e is non empty V73() MultiGraphStruct
the carrier' of e is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
W 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
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
V is Element of the carrier of e
W is Element of the carrier of e
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e : (e,b1,V,W) } is set
G is set
P is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
e is non empty V73() MultiGraphStruct
the carrier' of e is set
(e) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,V) is functional FinSequence-membered Element of K27(( 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))
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))
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
rng V is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (V . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (V . (len V)) & rng b1 c= rng V ) } is set
W 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
rng G is finite set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
(e) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
G is set
P is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,G) is functional FinSequence-membered Element of K27(( 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
G . 1 is set
the Source of e . (G . 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))
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
rng G is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (G . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (G . (len G)) & rng b1 c= rng G ) } is set
P is set
Q is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
Q . 1 is set
the Source of e . (Q . 1) is 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
Q . (len Q) is set
the Target of e . (Q . (len Q)) is set
rng Q is finite set
e is set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
the carrier' of V is set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G,e) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G,e) } is set
P is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
(V,P) is functional FinSequence-membered Element of K27(( the carrier' of V *))
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))
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
P . 1 is set
the Source of V . (P . 1) 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))
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . (len P) is set
the Target of V . (P . (len P)) is set
rng P is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (P . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (P . (len P)) & rng b1 c= rng P ) } is set
Q is set
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
R . 1 is set
the Source of V . (R . 1) is 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
R . (len R) is set
the Target of V . (R . (len R)) is set
rng R is finite set
(V,P) is Element of K27( the carrier of V)
K27( the carrier of V) is set
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom P & b1 in (V,(P /. b2)) ) } is set
{G} is non empty V19() finite 1 -element set
(V,P) \ {G} is Element of K27( the carrier of V)
(V,R) is Element of K27( the carrier of V)
dom R is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom R & b1 in (V,(R /. b2)) ) } is set
(V,R) \ {G} is Element of K27( the carrier of V)
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 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
W is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( 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
W . 1 is set
the Source of e . (W . 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))
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 . (len W) is set
the Target of e . (W . (len W)) is set
rng W is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (W . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (W . (len W)) & rng b1 c= rng W ) } is set
card (rng W) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
card (dom W) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
Seg (len W) is finite len W -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
card (Seg (len W)) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
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
rng G is finite set
card (rng G) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
G is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,G) is functional FinSequence-membered Element of K27(( 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
G . 1 is set
the Source of e . (G . 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))
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
rng G is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (G . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (G . (len G)) & rng b1 c= rng G ) } 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
R + 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 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 the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
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 Element of the carrier of e
v3 is Element of the carrier of e
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
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
Eg ^ pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
V9 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
len V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom V9 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
V9 . 1 is set
the Source of e . (V9 . 1) is set
v1 . 1 is set
V9 . (len V9) is set
the Target of e . (V9 . (len V9)) is set
s is Element of the carrier of e
FT is Element of the carrier of e
(e,V9) is functional FinSequence-membered Element of K27(( the carrier' of e *))
rng V9 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (V9 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (V9 . (len V9)) & rng b1 c= rng V9 ) } is set
FS is set
rng v1 is finite set
rng pe is finite set
dom pe is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
(len 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
v1 . ((len V9) + 1) is set
pe . 1 is set
x is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
x . 1 is set
the Source of e . (x . 1) is set
len x is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x . (len x) is set
the Target of e . (x . (len x)) is set
rng x is finite set
the Source of e . (v1 . ((len V9) + 1)) is set
v1 . (len V9) is set
the Target of e . (v1 . (len V9)) is set
the Source of e . (pe . 1) is set
the Target of e . (pe . 1) is set
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x . k is set
the Target of e . (x . k) is set
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x . k is set
the Target of e . (x . k) is set
s1 is ordinal natural finite cardinal V43() real ext-real non negative set
k + s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 ^ s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s2 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
s2 . 1 is set
the Source of e . (s2 . 1) is set
the Source of e . (v1 . 1) is set
rng s2 is finite set
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 . (len s2) is set
the Target of e . (s2 . (len s2)) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the Target of e . (pe . 1) is set
k is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
x ^ k is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of e
rng (x ^ k) is finite set
rng k is finite set
(rng x) \/ (rng k) is finite set
(rng v1) \/ (rng v1) is finite set
(x ^ k) . 1 is set
the Source of e . ((x ^ k) . 1) is set
the Source of e . (v1 . 1) is set
len (x ^ k) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len 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
(x ^ k) . (len (x ^ k)) is set
the Target of e . ((x ^ k) . (len (x ^ k))) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
k is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
s1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 . (len s1) is set
the Target of e . (s1 . (len s1)) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
the Source of e . (v1 . 1) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the Source of e . (v1 . 1) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the Source of e . (v1 . 1) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
the Target of e . (pe . 1) is set
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x . k is set
the Target of e . (x . k) is set
v1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
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 Element of the carrier of e
v3 is Element of the carrier of e
(e,v1) is functional FinSequence-membered Element of K27(( the carrier' of e *))
v1 . 1 is set
the Source of e . (v1 . 1) is set
v1 . (len v1) is set
the Target of e . (v1 . (len v1)) is set
rng v1 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (v1 . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (v1 . (len v1)) & rng b1 c= rng v1 ) } 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
R is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain 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
(e,R) is functional FinSequence-membered Element of K27(( the carrier' of e *))
R . 1 is set
the Source of e . (R . 1) is set
R . (len R) is set
the Target of e . (R . (len R)) is set
rng R is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (R . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (R . (len R)) & rng b1 c= rng R ) } is set
v1 is Element of the carrier of e
v2 is Element of the carrier of e
v3 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e
(len G) -' 1 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) + 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 set
e is set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
the carrier' of V is set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G,e) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G,e) } is set
P is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
(V,P) is functional FinSequence-membered Element of K27(( the carrier' of V *))
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))
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
P . 1 is set
the Source of V . (P . 1) 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))
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . (len P) is set
the Target of V . (P . (len P)) is set
rng P is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (P . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (P . (len P)) & rng b1 c= rng P ) } is set
(len P) -' 1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
((len P) -' 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
v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 + 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 + 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
v2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len 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 V
Eg is Element of the carrier of V
pe is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,v2) is Element of K27( the carrier of V)
K27( the carrier of V) is set
dom v2 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom v2 & b1 in (V,(v2 /. b2)) ) } is set
{Eg} is non empty V19() finite 1 -element set
(V,v2) \ {Eg} is Element of K27( the carrier of V)
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 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
pe /. (len v2) is Element of the carrier of V
pe /. ((len v2) + 1) is Element of the carrier of V
v2 . (len v2) is set
the Target of V . (v2 . (len v2)) is set
pe . (len pe) is set
v2 . 1 is set
the Source of V . (v2 . 1) is set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
V9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe . V9 is set
pe . s 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
s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe . V9 is set
pe . s is set
FT is ordinal natural finite cardinal V43() real ext-real non negative set
1 + FT 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 ext-real non negative set
s + x 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 Element of the carrier of V
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
pe /. (1 + 1) is Element of the carrier of V
v2 . 1 is set
pe /. s is Element of the carrier of V
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
pe /. (s + 1) is Element of the carrier of V
v2 . s is set
the Source of V . (v2 . s) is set
pe /. V9 is Element of the carrier of V
the Source of V . (v2 . 1) is set
FS 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
1 + k 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
FS + (1 + k) 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
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 ^ s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s2 . 1 is set
s2 . (len s2) is set
the Target of V . (s2 . (len s2)) is set
FS + 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
- 1 is V43() real ext-real non positive set
(FS + 1) + (- 1) is V43() real ext-real set
1 + (- 1) is V43() real ext-real set
s2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
s1 ^ s2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,(s1 ^ s2)) is Element of K27( the carrier of V)
dom (s1 ^ s2) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom (s1 ^ s2) & b1 in (V,((s1 ^ s2) /. b2)) ) } is set
(V,(s1 ^ s2)) \ {Eg} is Element of K27( the carrier of V)
(V,s2) is Element of K27( the carrier of V)
dom s2 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s2 & b1 in (V,(s2 /. b2)) ) } is set
(V,s2) \ {Eg} is Element of K27( the carrier of V)
(V,s2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
s2 . 1 is set
the Source of V . (s2 . 1) is set
s2 . (len s2) is set
the Target of V . (s2 . (len s2)) is set
rng s2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (s2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (s2 . (len s2)) & rng b1 c= rng s2 ) } is set
i is set
vx is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
vx . 1 is set
the Source of V . (vx . 1) is set
len vx is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
vx . (len vx) is set
the Target of V . (vx . (len vx)) is set
rng vx is finite set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
x is ordinal natural finite cardinal V43() real ext-real non negative set
1 + x 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
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 is ordinal natural finite cardinal V43() real ext-real non negative set
k + s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real 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
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 ^ s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s1 . (len s1) is set
v2 . k is set
s1 . 1 is set
v2 . 1 is set
the Source of V . (s1 . 1) is set
rng s1 is finite set
rng v2 is finite set
pe /. k is Element of the carrier of V
k + 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 /. (k + 1) is Element of the carrier of V
the Target of V . (v2 . k) is set
pe /. V9 is Element of the carrier of V
i is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len i is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
i . (len i) is set
the Target of V . (i . (len i)) is set
vx is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
i ^ vx is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,(i ^ vx)) is Element of K27( the carrier of V)
dom (i ^ vx) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom (i ^ vx) & b1 in (V,((i ^ vx) /. b2)) ) } is set
(V,(i ^ vx)) \ {Eg} is Element of K27( the carrier of V)
(V,i) is Element of K27( the carrier of V)
dom i is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom i & b1 in (V,(i /. b2)) ) } is set
(V,i) \ {Eg} is Element of K27( the carrier of V)
(V,i) is functional FinSequence-membered Element of K27(( the carrier' of V *))
i . 1 is set
the Source of V . (i . 1) is set
rng i is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (i . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (i . (len i)) & rng b1 c= rng i ) } is set
q9 is set
j is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
j . 1 is set
the Source of V . (j . 1) is set
len j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
j . (len j) is set
the Target of V . (j . (len j)) is set
rng j is finite set
the Source of V . (v2 . 1) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
q9 is ordinal natural finite cardinal V43() real ext-real non negative set
s + q9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe /. s is Element of the carrier of V
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
pe /. (s + 1) is Element of the carrier of V
v2 . s is set
the Source of V . (v2 . s) is set
i is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len i is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
i . (len i) is set
the Target of V . (i . (len i)) is set
FS is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
1 + j 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
FS + (1 + j) 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
qx is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len qx is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
qx ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len t1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t1 . 1 is set
i ^ t1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
t2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len t2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t2 . (len t2) is set
(len i) + (len t1) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t2 . ((len i) + (len t1)) is set
t1 . (len t1) is set
the Target of V . (t2 . (len t2)) is set
rng t2 is finite set
rng i is finite set
rng t1 is finite set
(rng i) \/ (rng t1) is finite set
(V,t2) is Element of K27( the carrier of V)
dom t2 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of V : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom t2 & b1 in (V,(t2 /. b2)) ) } is set
(V,t2) \ {Eg} is Element of K27( the carrier of V)
k + (1 + j) 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 + j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V9 + j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t2 . 1 is set
the Source of V . (t2 . 1) is set
(V,t2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (t2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (t2 . (len t2)) & rng b1 c= rng t2 ) } is set
t1 is set
t2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
t2 . 1 is set
the Source of V . (t2 . 1) is set
len t2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t2 . (len t2) is set
the Target of V . (t2 . (len t2)) is set
rng t2 is finite set
the Source of V . (v2 . 1) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the Source of V . (v2 . 1) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the Source of V . (v2 . 1) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
v2 . 1 is set
the Source of V . (v2 . 1) is set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
v2 . 1 is set
the Source of V . (v2 . 1) is set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } 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
s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
pe . V9 is set
pe . s is set
v2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len 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 V
Eg is Element of the carrier of V
(V,v2) is functional FinSequence-membered Element of K27(( the carrier' of V *))
v2 . 1 is set
the Source of V . (v2 . 1) is set
v2 . (len v2) is set
the Target of V . (v2 . (len v2)) is set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v2 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v2 . (len v2)) & rng b1 c= rng v2 ) } 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
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V,v1) is functional FinSequence-membered Element of K27(( the carrier' of V *))
v1 . 1 is set
the Source of V . (v1 . 1) is set
v1 . (len v1) is set
the Target of V . (v1 . (len v1)) is set
rng v1 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v1 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
v2 is Element of the carrier of V
v3 is Element of the carrier of V
Eg is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
v1 is set
e is set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
(V) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V is set
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : verum } is set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G,e) is functional FinSequence-membered Element of K27(( the carrier' of V *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G,e) } is set
P is set
Q is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
e is V99() V100() V101() Element of K27(REAL)
V is V99() V100() V101() Element of K27(REAL)
() is non empty V99() V100() V101() Element of K27(REAL)
e is non empty V73() MultiGraphStruct
the carrier' of e is set
W is Relation-like Function-like 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)
G is Relation-like Function-like set
dom G is set
K28( the carrier' of e,REAL) is Relation-like V88() V89() V90() set
K27(K28( the carrier' of e,REAL)) is set
P is ordinal natural finite cardinal V43() real ext-real non negative set
G . P is set
V . P is set
W . (V . P) is 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
Seg (len V) is finite len V -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
P is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . Q is V43() real ext-real Element of REAL
V . Q is set
W . (V . Q) is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
P is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
Q is ordinal natural finite cardinal V43() real ext-real non negative set
G . Q is V43() real ext-real Element of REAL
V . Q is set
W . (V . Q) is set
P . Q is V43() real ext-real Element of REAL
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
W is Relation-like Function-like set
(e,V,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (e,V,W) is V43() real ext-real Element of REAL
K142(REAL,(e,V,W),K193()) is V43() real ext-real Element of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
K28( the carrier' of V,()) is Relation-like V88() V89() V90() set
K27(K28( the carrier' of V,())) is set
K28( the carrier' of V,REAL) is Relation-like V88() V89() V90() set
K27(K28( the carrier' of V,REAL)) is set
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
K28( the carrier' of V,()) is Relation-like V88() V89() V90() set
K27(K28( the carrier' of V,())) 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
G . P is V43() real ext-real Element of REAL
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
W . P is set
e . (W . P) is set
Q is V43() real ext-real Element of REAL
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 Function-like set
W is non empty V73() MultiGraphStruct
the carrier' of W is set
G is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
rng G is finite set
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
(W,G,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(W,G,V) . e is V43() real ext-real Element of REAL
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
rng P is finite set
dom P is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
(W,P,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
G . e is set
R is set
P . R is set
v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(W,P,V) . v1 is V43() real ext-real Element of REAL
V . (G . e) is set
e is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
rng e is finite V99() V100() V101() Element of K27(REAL)
dom e is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
V is ordinal natural finite cardinal V43() real ext-real non negative set
e . V is V43() real ext-real Element of REAL
V is V43() real ext-real Element of REAL
W is set
e . W is V43() real ext-real Element of REAL
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
e is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
V is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
e ^ V is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
rng W is finite V99() V100() V101() Element of K27(REAL)
dom e is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom V is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
rng e is finite V99() V100() V101() Element of K27(REAL)
G is V43() real ext-real Element of REAL
G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
e . G is V43() real ext-real Element of REAL
rng V is finite V99() V100() V101() Element of K27(REAL)
G is V43() real ext-real Element of REAL
G is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
V . G is V43() real ext-real Element of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of 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
rng W is finite set
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
G is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng G is finite set
(V,G,e) is V43() real ext-real Element of REAL
(V,G,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,G,e) is V43() real ext-real Element of REAL
K142(REAL,(V,G,e),K193()) is V43() real ext-real Element of REAL
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
(V,W,e) . 1 is V43() real ext-real Element of REAL
R is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V,G,e) . R is V43() real ext-real Element of REAL
dom (V,G,e) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
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,G,e) 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,e) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
len (V,W,e) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
<*((V,W,e) . 1)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like V88() V89() V90() V92() V93() V94() V95() FinSequence of REAL
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 REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
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 REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
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 REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
pe is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
V9 is V43() real ext-real Element of REAL
<*V9*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like V88() V89() V90() V92() V93() V94() V95() FinSequence of REAL
pe ^ <*V9*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom v3 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v3 . R is V43() real ext-real Element of REAL
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 ordinal natural finite cardinal V43() real ext-real non negative set
(V,G,e) . s is V43() real ext-real Element of REAL
rng (V,G,e) is finite V99() V100() V101() Element of K27(REAL)
s is V43() real ext-real Element of REAL
dom Eg is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s is ordinal natural finite cardinal V43() real ext-real non negative set
Eg . s is V43() real ext-real Element of REAL
Sum Eg is V43() real ext-real Element of REAL
K142(REAL,Eg,K193()) is V43() real ext-real Element of REAL
s is ordinal natural finite cardinal V43() real ext-real non negative set
v3 . s is V43() real ext-real Element of REAL
rng v3 is finite V99() V100() V101() Element of K27(REAL)
s is V43() real ext-real Element of REAL
dom pe is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
s is ordinal natural finite cardinal V43() real ext-real non negative set
pe . s is V43() real ext-real Element of REAL
Sum pe is V43() real ext-real Element of REAL
K142(REAL,pe,K193()) is V43() real ext-real Element of REAL
Sum v3 is V43() real ext-real Element of REAL
K142(REAL,v3,K193()) is V43() real ext-real Element of REAL
Sum <*V9*> is V43() real ext-real Element of REAL
K142(REAL,<*V9*>,K193()) is V43() real ext-real Element of REAL
(Sum pe) + (Sum <*V9*>) is V43() real ext-real set
(Sum pe) + ((V,W,e) . 1) is V43() real ext-real set
0 + ((V,W,e) . 1) is V43() real ext-real set
(Sum v3) + (Sum Eg) is V43() real ext-real set
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
dom (V,W,e) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
P is ordinal natural finite cardinal V43() real ext-real non negative set
(V,W,e) . P is V43() real ext-real Element of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
dom (V,W,e) is 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)
len (V,W,e) 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
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier of V is non empty set
the carrier' of V is set
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G) is functional FinSequence-membered Element of K27(( the carrier' of V *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G) } is set
P is functional non empty finite FinSequence-membered Element of K27(( the carrier' of V *))
Q is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like ( the carrier' of V,P)
(V,Q,e) is V43() real ext-real Element of REAL
(V,Q,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,Q,e) is V43() real ext-real Element of REAL
K142(REAL,(V,Q,e),K193()) is V43() real ext-real Element of REAL
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,v1,e) is V43() real ext-real Element of REAL
(V,v1,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v1,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v1,e),K193()) is V43() real ext-real Element of REAL
v2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like ( the carrier' of V,P)
(V,v2,e) is V43() real ext-real Element of REAL
(V,v2,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v2,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v2,e),K193()) is V43() real ext-real Element of REAL
e is set
V is Relation-like Function-like set
W is non empty V73() MultiGraphStruct
the carrier of W is non empty set
the carrier' of W is set
the carrier' of W * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of W
K27(( the carrier' of W *)) is set
G is Element of the carrier of W
P is Element of the carrier of W
(W,G,P,e) is functional FinSequence-membered Element of K27(( the carrier' of W *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W : (W,b1,G,P,e) } is set
Q is functional non empty finite FinSequence-membered Element of K27(( the carrier' of W *))
R is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like ( the carrier' of W,Q)
(W,R,V) is V43() real ext-real Element of REAL
(W,R,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,R,V) is V43() real ext-real Element of REAL
K142(REAL,(W,R,V),K193()) is V43() real ext-real Element of REAL
v1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W
(W,v1,V) is V43() real ext-real Element of REAL
(W,v1,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v1,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v1,V),K193()) is V43() real ext-real Element of REAL
v2 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,v2,V) is V43() real ext-real Element of REAL
(W,v2,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v2,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v2,V),K193()) is V43() real ext-real Element of REAL
v3 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like ( the carrier' of W,Q)
(W,v3,V) is V43() real ext-real Element of REAL
(W,v3,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v3,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v3,V),K193()) is V43() real ext-real Element of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
G is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
W ^ G is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,(W ^ G),e) is V43() real ext-real Element of REAL
(V,(W ^ G),e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,(W ^ G),e) is V43() real ext-real Element of REAL
K142(REAL,(V,(W ^ G),e),K193()) is V43() real ext-real Element of REAL
(V,G,e) is V43() real ext-real Element of REAL
(V,G,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,G,e) is V43() real ext-real Element of REAL
K142(REAL,(V,G,e),K193()) is V43() real ext-real Element of REAL
(V,W,e) + (V,G,e) is V43() real ext-real set
dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom (V,W,e) is finite V99() V100() V101() V102() V103() V104() Element of K27(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 (V,W,e) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom G is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom (V,G,e) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
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,G,e) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
dom (W ^ G) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
dom (V,(W ^ G),e) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
len (V,(W ^ G),e) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len (W ^ 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,W,e)) + (len (V,G,e)) 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
(len (V,W,e)) + v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V,G,e) . v2 is V43() real ext-real Element of REAL
G . v2 is set
e . (G . v2) is set
(W ^ G) . ((len (V,W,e)) + v2) is set
(V,(W ^ G),e) . ((len (V,W,e)) + v2) is V43() real ext-real Element of REAL
v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(V,W,e) . v2 is V43() real ext-real Element of REAL
W . v2 is set
e . (W . v2) is set
(W ^ G) . v2 is set
(V,(W ^ G),e) . v2 is V43() real ext-real Element of REAL
(V,W,e) ^ (V,G,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng W is finite set
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
G is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng G is finite set
(V,G,e) is V43() real ext-real Element of REAL
(V,G,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,G,e) is V43() real ext-real Element of REAL
K142(REAL,(V,G,e),K193()) is V43() real ext-real Element of REAL
Q is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
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
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng v1 is finite set
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng R is finite 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
v3 is set
<*v3*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
v2 ^ <*v3*> is Relation-like NAT -defined Function-like non empty 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
(len 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
rng v2 is finite set
Eg is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Eg ^ <*v3*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Eg ^ <*v3*>) ^ pe is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
Eg ^ pe is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (Eg ^ pe) is finite set
V9 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,V9,e) is V43() real ext-real Element of REAL
(V,V9,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,V9,e) is V43() real ext-real Element of REAL
K142(REAL,(V,V9,e),K193()) is V43() real ext-real Element of REAL
FS is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
FT is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
FS ^ FT is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,(FS ^ FT),e) is V43() real ext-real Element of REAL
(V,(FS ^ FT),e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,(FS ^ FT),e) is V43() real ext-real Element of REAL
K142(REAL,(V,(FS ^ FT),e),K193()) is V43() real ext-real Element of REAL
(V,v1,e) is V43() real ext-real Element of REAL
(V,v1,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v1,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v1,e),K193()) is V43() real ext-real Element of REAL
s is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,s,e) is V43() real ext-real Element of REAL
(V,s,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,s,e) is V43() real ext-real Element of REAL
K142(REAL,(V,s,e),K193()) is V43() real ext-real Element of REAL
(V,V9,e) + (V,s,e) is V43() real ext-real set
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
FS ^ s is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,(FS ^ s),e) is V43() real ext-real Element of REAL
(V,(FS ^ s),e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,(FS ^ s),e) is V43() real ext-real Element of REAL
K142(REAL,(V,(FS ^ s),e),K193()) is V43() real ext-real Element of REAL
(V,FT,e) is V43() real ext-real Element of REAL
(V,FT,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,FT,e) is V43() real ext-real Element of REAL
K142(REAL,(V,FT,e),K193()) is V43() real ext-real Element of REAL
(V,(FS ^ s),e) + (V,FT,e) is V43() real ext-real set
(V,FS,e) is V43() real ext-real Element of REAL
(V,FS,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,FS,e) is V43() real ext-real Element of REAL
K142(REAL,(V,FS,e),K193()) is V43() real ext-real Element of REAL
(V,FS,e) + (V,s,e) is V43() real ext-real set
((V,FS,e) + (V,s,e)) + (V,FT,e) is V43() real ext-real set
(V,FS,e) + (V,FT,e) is V43() real ext-real set
((V,FS,e) + (V,FT,e)) + (V,s,e) is V43() real ext-real set
(V,(FS ^ FT),e) + (V,s,e) is V43() real ext-real set
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng v1 is finite set
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng R is finite 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
(V,v1,e) is V43() real ext-real Element of REAL
(V,v1,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v1,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v1,e),K193()) is V43() real ext-real Element of REAL
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng R is finite set
Q is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng Q is finite 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
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
(V,Q,e) is V43() real ext-real Element of REAL
(V,Q,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,Q,e) is V43() real ext-real Element of REAL
K142(REAL,(V,Q,e),K193()) is V43() real ext-real Element of REAL
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 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng R is finite set
Q is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
rng Q is finite 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
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
(V,Q,e) is V43() real ext-real Element of REAL
(V,Q,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,Q,e) is V43() real ext-real Element of REAL
K142(REAL,(V,Q,e),K193()) is V43() real ext-real Element of REAL
e is Relation-like Function-like set
V is non empty V73() MultiGraphStruct
the carrier' of V is set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,W,e) is V43() real ext-real Element of REAL
(V,W,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,W,e) is V43() real ext-real Element of REAL
K142(REAL,(V,W,e),K193()) is V43() real ext-real Element of REAL
G is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
(V,G) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
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
G . 1 is set
the Source of V . (G . 1) 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))
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 V . (G . (len G)) is set
rng G is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (G . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (G . (len G)) & rng b1 c= rng G ) } is set
(V,G,e) is V43() real ext-real Element of REAL
(V,G,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,G,e) is V43() real ext-real Element of REAL
K142(REAL,(V,G,e),K193()) is V43() real ext-real Element of REAL
P is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
P . 1 is set
the Source of V . (P . 1) is set
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . (len P) is set
the Target of V . (P . (len P)) is set
rng P is finite set
P is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
P . 1 is set
the Source of V . (P . 1) is set
len P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
P . (len P) is set
the Target of V . (P . (len P)) is set
rng P is finite set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
e is non empty V73() MultiGraphStruct
the carrier of e is non empty set
the carrier' of e is set
e is non empty V73() finite MultiGraphStruct
the carrier' of e is finite set
VerticesCount 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 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
the carrier of e is non empty finite 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) + 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 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R is set
<*R*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set
Q ^ <*R*> is Relation-like NAT -defined Function-like non empty 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
len <*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 Q) + (len <*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 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
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
dom Q is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
G . v1 is set
Q . v1 is set
Q . v2 is set
G . v2 is set
rng Q is finite set
card (rng Q) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
rng G is finite set
P is finite set
card P is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
e is non empty V73() finite MultiGraphStruct
the carrier' of e is finite set
EdgesCount 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 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
rng V is finite set
card (rng V) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of omega
W is 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
e is non empty V73() finite MultiGraphStruct
(e) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is finite set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
EdgesCount e is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of e * : len b1 <= EdgesCount e } is set
P is set
Q is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain 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
e is non empty V73() finite MultiGraphStruct
(e) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is finite set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
e is non empty V73() finite MultiGraphStruct
the carrier' of e is finite set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,V) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
the Source of e is Relation-like Function-like finite 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 finite set
K28( the carrier' of e, the carrier of e) is Relation-like finite set
K27(K28( the carrier' of e, the carrier of e)) is finite V28() set
V . 1 is set
the Source of e . (V . 1) is set
the Target of e is Relation-like Function-like finite V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, 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
V . (len V) is set
the Target of e . (V . (len V)) is set
rng V is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (V . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (V . (len V)) & rng b1 c= rng V ) } is set
(e) is functional finite FinSequence-membered Element of K27(( the carrier' of e *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
e is non empty V73() finite MultiGraphStruct
the carrier of e is non empty finite set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is finite set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
(e) is functional finite FinSequence-membered Element of K27(( the carrier' of e *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : verum } is set
e is set
V is non empty V73() finite MultiGraphStruct
the carrier of V is non empty finite set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G,e) is functional FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V is finite set
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G,e) } is set
(V) is functional finite FinSequence-membered Element of K27(( the carrier' of V *))
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : verum } is set
e is non empty V73() finite MultiGraphStruct
the carrier' of e is finite set
V is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of e
(e,V) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
the Source of e is Relation-like Function-like finite 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 finite set
K28( the carrier' of e, the carrier of e) is Relation-like finite set
K27(K28( the carrier' of e, the carrier of e)) is finite V28() set
V . 1 is set
the Source of e . (V . 1) is set
the Target of e is Relation-like Function-like finite V36( the carrier' of e, the carrier of e) Element of K27(K28( the carrier' of e, 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
V . (len V) is set
the Target of e . (V . (len V)) is set
rng V is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : ( not b1 = {} & the Source of e . (b1 . 1) = the Source of e . (V . 1) & the Target of e . (b1 . (len b1)) = the Target of e . (V . (len V)) & rng b1 c= rng V ) } is set
e is non empty V73() finite MultiGraphStruct
the carrier of e is non empty finite set
V is Element of the carrier of e
W is Element of the carrier of e
(e,V,W) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is finite set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W) } is set
e is non empty V73() finite MultiGraphStruct
the carrier of e is non empty finite set
V is Element of the carrier of e
W is Element of the carrier of e
G is set
(e,V,W,G) is functional FinSequence-membered Element of K27(( the carrier' of e *))
the carrier' of e is finite set
the carrier' of e * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of e
K27(( the carrier' of e *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of e -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of e : (e,b1,V,W,G) } is set
V is non empty V73() finite MultiGraphStruct
the carrier of V is non empty finite set
W is Element of the carrier of V
G is Element of the carrier of V
(V,W,G) is functional finite FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V is finite set
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,W,G) } is set
e is Relation-like Function-like set
W is non empty V73() finite MultiGraphStruct
the carrier of W is non empty finite set
G is Element of the carrier of W
P is Element of the carrier of W
e is set
(W,G,P,e) is functional finite FinSequence-membered Element of K27(( the carrier' of W *))
the carrier' of W is finite set
the carrier' of W * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of W
K27(( the carrier' of W *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W : (W,b1,G,P,e) } is set
V is Relation-like Function-like set
e is Relation-like Function-like set
V is non empty V73() finite MultiGraphStruct
the carrier' of V is finite set
the carrier of V is non empty finite set
W is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
G is Element of the carrier of V
P is Element of the carrier of V
(V,G,P) is functional finite FinSequence-membered Element of K27(( the carrier' of V *))
the carrier' of V * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of V
K27(( the carrier' of V *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : (V,b1,G,P) } is set
Q is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of V
(V,Q,e) is V43() real ext-real Element of REAL
(V,Q,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,Q,e) is V43() real ext-real Element of REAL
K142(REAL,(V,Q,e),K193()) is V43() real ext-real Element of REAL
R is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V
(V,R,e) is V43() real ext-real Element of REAL
(V,R,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,R,e) is V43() real ext-real Element of REAL
K142(REAL,(V,R,e),K193()) is V43() real ext-real Element of REAL
v1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of V
(V,v1) is functional finite FinSequence-membered Element of K27(( the carrier' of V *))
the Source of V is Relation-like Function-like finite V36( the carrier' of V, the carrier of V) Element of K27(K28( the carrier' of V, the carrier of V))
K28( the carrier' of V, the carrier of V) is Relation-like finite set
K27(K28( the carrier' of V, the carrier of V)) is finite V28() set
v1 . 1 is set
the Source of V . (v1 . 1) is set
the Target of V is Relation-like Function-like finite V36( the carrier' of V, the carrier of V) Element of K27(K28( the carrier' of V, the carrier of V))
len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v1 . (len v1) is set
the Target of V . (v1 . (len v1)) is set
rng v1 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of V : ( not b1 = {} & the Source of V . (b1 . 1) = the Source of V . (v1 . 1) & the Target of V . (b1 . (len b1)) = the Target of V . (v1 . (len v1)) & rng b1 c= rng v1 ) } is set
v2 is Relation-like NAT -defined the carrier' of V -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of V *
(V,v2,e) is V43() real ext-real Element of REAL
(V,v2,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v2,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v2,e),K193()) is V43() real ext-real Element of REAL
(V,v1,e) is V43() real ext-real Element of REAL
(V,v1,e) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (V,v1,e) is V43() real ext-real Element of REAL
K142(REAL,(V,v1,e),K193()) is V43() real ext-real Element of REAL
e is set
V is Relation-like Function-like set
W is non empty V73() finite MultiGraphStruct
the carrier' of W is finite set
the carrier of W is non empty finite set
G is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
P is Element of the carrier of W
Q is Element of the carrier of W
(W,P,Q,e) is functional finite FinSequence-membered Element of K27(( the carrier' of W *))
the carrier' of W * is functional non empty FinSequence-membered FinSequenceSet of the carrier' of W
K27(( the carrier' of W *)) is set
{ b1 where b1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W : (W,b1,P,Q,e) } is set
R is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,R,V) is V43() real ext-real Element of REAL
(W,R,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,R,V) is V43() real ext-real Element of REAL
K142(REAL,(W,R,V),K193()) is V43() real ext-real Element of REAL
v1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W
(W,v1,V) is V43() real ext-real Element of REAL
(W,v1,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v1,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v1,V),K193()) is V43() real ext-real Element of REAL
v2 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,v2) is functional finite FinSequence-membered Element of K27(( the carrier' of W *))
the Source of W is Relation-like Function-like finite V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
K28( the carrier' of W, the carrier of W) is Relation-like finite set
K27(K28( the carrier' of W, the carrier of W)) is finite V28() set
v2 . 1 is set
the Source of W . (v2 . 1) is set
the Target of W is Relation-like Function-like finite V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
len v2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
v2 . (len v2) is set
the Target of W . (v2 . (len v2)) is set
rng v2 is finite set
{ b1 where b1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W : ( not b1 = {} & the Source of W . (b1 . 1) = the Source of W . (v2 . 1) & the Target of W . (b1 . (len b1)) = the Target of W . (v2 . (len v2)) & rng b1 c= rng v2 ) } is set
v3 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of W *
(W,v3,V) is V43() real ext-real Element of REAL
(W,v3,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v3,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v3,V),K193()) is V43() real ext-real Element of REAL
(W,v2,V) is V43() real ext-real Element of REAL
(W,v2,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,v2,V) is V43() real ext-real Element of REAL
K142(REAL,(W,v2,V),K193()) is V43() real ext-real Element of REAL
e is set
V is Relation-like Function-like set
W is non empty V73() finite MultiGraphStruct
the carrier' of W is finite set
the carrier of W is non empty finite set
G is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,G,V) is V43() real ext-real Element of REAL
(W,G,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,G,V) is V43() real ext-real Element of REAL
K142(REAL,(W,G,V),K193()) is V43() real ext-real Element of REAL
P is Element of the carrier of W
Q is Element of the carrier of W
R is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,R) is finite Element of K27( the carrier of W)
K27( the carrier of W) is finite V28() set
dom R is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom R & b1 in (W,(R /. b2)) ) } is set
the Target of W is Relation-like Function-like finite V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
K28( the carrier' of W, the carrier of W) is Relation-like finite set
K27(K28( the carrier' of W, the carrier of W)) is finite V28() set
the Source of W is Relation-like Function-like finite V36( the carrier' of W, the carrier of W) Element of K27(K28( the carrier' of W, the carrier of W))
len R 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
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
R /. (v3 + 1) is Element of the carrier' of W
(W,(R /. (v3 + 1))) is set
the Source of W . (R /. (v3 + 1)) is set
the Target of W . (R /. (v3 + 1)) is set
{( the Source of W . (R /. (v3 + 1))),( the Target of W . (R /. (v3 + 1)))} is non empty finite set
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
pe is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
Eg ^ pe is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,Eg) is finite Element of K27( the carrier of W)
dom Eg is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom Eg & b1 in (W,(Eg /. b2)) ) } is 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 Eg) + (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 ext-real non negative set
1 + 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
FS is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
FT is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
x ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R . (v3 + 1) is set
FT . 1 is set
s1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
s1 . 1 is set
s2 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,s2,V) is V43() real ext-real Element of REAL
(W,s2,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,s2,V) is V43() real ext-real Element of REAL
K142(REAL,(W,s2,V),K193()) is V43() real ext-real Element of REAL
s is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
s ^ s1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(s ^ s1) ^ s2 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
(W,R,V) is V43() real ext-real Element of REAL
(W,R,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,R,V) is V43() real ext-real Element of REAL
K142(REAL,(W,R,V),K193()) is V43() real ext-real Element of REAL
(W,(s ^ s1),V) is V43() real ext-real Element of REAL
(W,(s ^ s1),V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,(s ^ s1),V) is V43() real ext-real Element of REAL
K142(REAL,(W,(s ^ s1),V),K193()) is V43() real ext-real Element of REAL
(W,(s ^ s1),V) + (W,s2,V) is V43() real ext-real set
(W,(s ^ s1),V) + 0 is V43() real ext-real set
s2 is set
dom s1 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
R . 1 is set
the Source of W . (R . 1) is set
the Source of W . (s1 . 1) is set
(W,s1) is finite Element of K27( the carrier of W)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s1 & b1 in (W,(s1 /. b2)) ) } is set
i is Element of the carrier of W
{i} is non empty V19() finite 1 -element set
(W,s1) \ {i} is finite Element of K27( the carrier of W)
vx is set
s1 /. 1 is Element of the carrier' of W
(W,(s1 /. 1)) is set
the Source of W . (s1 /. 1) is set
the Target of W . (s1 /. 1) is set
{( the Source of W . (s1 /. 1)),( the Target of W . (s1 /. 1))} is non empty finite set
vx is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W
(W,vx,V) is V43() real ext-real Element of REAL
(W,vx,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,vx,V) is V43() real ext-real Element of REAL
K142(REAL,(W,vx,V),K193()) is V43() real ext-real Element of REAL
(W,s1,V) is V43() real ext-real Element of REAL
(W,s1,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,s1,V) is V43() real ext-real Element of REAL
K142(REAL,(W,s1,V),K193()) is V43() real ext-real Element of REAL
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
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
the Source of W . (R . (v3 + 1)) is set
i is Element of the carrier of W
R . v3 is set
the Target of W . (R . v3) is set
s . v3 is set
(W,s) is finite Element of K27( the carrier of W)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s & b1 in (W,(s /. b2)) ) } is set
vx is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
(W,vx) is finite Element of K27( the carrier of W)
dom vx is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom vx & b1 in (W,(vx /. b2)) ) } is set
{i} is non empty V19() finite 1 -element set
(W,vx) \ {i} is finite Element of K27( the carrier of W)
the Target of W . (s1 . 1) is set
{( the Target of W . (s1 . 1))} is non empty V19() finite 1 -element set
j is set
(W,s) \/ {( the Target of W . (s1 . 1))} is non empty finite set
len vx is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len s) + (len s1) is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
vx . (len vx) is set
vx . 1 is set
s . 1 is set
the Source of W . (vx . 1) is set
q9 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W
(W,q9,V) is V43() real ext-real Element of REAL
(W,q9,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,q9,V) is V43() real ext-real Element of REAL
K142(REAL,(W,q9,V),K193()) is V43() real ext-real Element of REAL
(W,vx,V) is V43() real ext-real Element of REAL
(W,vx,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,vx,V) is V43() real ext-real Element of REAL
K142(REAL,(W,vx,V),K193()) is V43() real ext-real Element of REAL
(W,R) is finite Element of K27( the carrier of W)
K27( the carrier of W) is finite V28() set
dom R is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom R & b1 in (W,(R /. b2)) ) } is set
{Q} is non empty V19() finite 1 -element set
(W,R) \ {Q} is finite Element of K27( the carrier of W)
e \ {Q} is Element of K27(e)
K27(e) is set
(W,R,V) is V43() real ext-real Element of REAL
(W,R,V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (W,R,V) is V43() real ext-real Element of REAL
K142(REAL,(W,R,V),K193()) is V43() real ext-real Element of REAL
(W,R) is finite Element of K27( the carrier of W)
K27( the carrier of W) is finite V28() set
dom R is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of W : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom R & b1 in (W,(R /. b2)) ) } is set
e is set
V is set
W is Relation-like Function-like set
G is non empty V73() finite MultiGraphStruct
the carrier' of G is finite set
the carrier of G is non empty finite set
P is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,P,W) is V43() real ext-real Element of REAL
(G,P,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,P,W) is V43() real ext-real Element of REAL
K142(REAL,(G,P,W),K193()) is V43() real ext-real Element of REAL
Q is Element of the carrier of G
R is Element of the carrier of G
v1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,v1,W) is V43() real ext-real Element of REAL
(G,v1,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,v1,W) is V43() real ext-real Element of REAL
K142(REAL,(G,v1,W),K193()) is V43() real ext-real Element of REAL
e is non empty V73() MultiGraphStruct
the carrier' of e is set
the carrier of e is non empty 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 set
W is Relation-like Function-like set
G is non empty V73() oriented finite MultiGraphStruct
the carrier' of G is finite set
the carrier of G is non empty finite set
P is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len P 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 the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
P ^ <*e*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
Q is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,Q,W) is V43() real ext-real Element of REAL
(G,Q,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,Q,W) is V43() real ext-real Element of REAL
K142(REAL,(G,Q,W),K193()) is V43() real ext-real Element of REAL
(G,R,W) is V43() real ext-real Element of REAL
(G,R,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,R,W) is V43() real ext-real Element of REAL
K142(REAL,(G,R,W),K193()) is V43() real ext-real Element of REAL
v1 is Element of the carrier of G
v2 is Element of the carrier of G
v3 is Element of the carrier of G
{v2} is non empty V19() finite 1 -element set
V \/ {v2} is non empty set
pe is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
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 . 1 is set
s is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of G
(G,s,W) is V43() real ext-real Element of REAL
(G,s,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,s,W) is V43() real ext-real Element of REAL
K142(REAL,(G,s,W),K193()) is V43() real ext-real Element of REAL
FT is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,FT,W) is V43() real ext-real Element of REAL
(G,FT,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,FT,W) is V43() real ext-real Element of REAL
K142(REAL,(G,FT,W),K193()) is V43() real ext-real Element of REAL
FT is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,FT,W) is V43() real ext-real Element of REAL
(G,FT,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,FT,W) is V43() real ext-real Element of REAL
K142(REAL,(G,FT,W),K193()) is V43() real ext-real Element of REAL
the Target of G is Relation-like Function-like finite V36( the carrier' of G, the carrier of G) Element of K27(K28( the carrier' of G, the carrier of G))
K28( the carrier' of G, the carrier of G) is Relation-like finite set
K27(K28( the carrier' of G, the carrier of G)) is finite V28() set
the Source of G is Relation-like Function-like finite V36( the carrier' of G, the carrier of G) Element of K27(K28( the carrier' of G, the carrier of G))
the Source of G . e is set
the Target of G . e is set
len s is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s . (len s) is set
the Target of G . (s . (len s)) 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
x is ordinal natural finite cardinal V43() real ext-real non negative set
(1 + 1) + x 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}) \ {v2} is Element of K27((V \/ {v2}))
K27((V \/ {v2})) is set
V \ {v2} is Element of K27(V)
K27(V) is set
k is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
1 + k 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
1 + (1 + k) 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
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 ^ s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of G
len s1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s . 1 is set
the Source of G . (s . 1) is set
s1 . 1 is set
the Source of G . (s1 . 1) is set
s2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of G
len s2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(G,s1) is finite Element of K27( the carrier of G)
K27( the carrier of G) is finite V28() set
dom s1 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s1 & b1 in (G,(s1 /. b2)) ) } is set
s2 . 1 is set
(G,s) is finite Element of K27( the carrier of G)
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s & b1 in (G,(s /. b2)) ) } is set
{v3} is non empty V19() finite 1 -element set
(G,s) \ {v3} is finite Element of K27( the carrier of G)
(G,s1) \/ {v3} is non empty finite set
((G,s1) \/ {v3}) \ {v3} is finite Element of K27(((G,s1) \/ {v3}))
K27(((G,s1) \/ {v3})) is finite V28() set
(G,s1) \ {v3} is finite Element of K27( the carrier of G)
(G,s1) \ {v2} is finite Element of K27( the carrier of G)
(len 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
s . ((len s1) + 1) is set
the Source of G . (s . ((len s1) + 1)) is set
s . (len s1) is set
the Target of G . (s . (len s1)) is set
s1 . (len s1) is set
the Source of G . (s2 . 1) is set
the Target of G . (s1 . (len s1)) is set
(G,s1,W) is V43() real ext-real Element of REAL
(G,s1,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,s1,W) is V43() real ext-real Element of REAL
K142(REAL,(G,s1,W),K193()) is V43() real ext-real Element of REAL
(G,s2,W) is V43() real ext-real Element of REAL
(G,s2,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,s2,W) is V43() real ext-real Element of REAL
K142(REAL,(G,s2,W),K193()) is V43() real ext-real Element of REAL
(G,s1,W) + (G,s2,W) is V43() real ext-real set
(G,s2) is finite Element of K27( the carrier of G)
dom s2 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s2 & b1 in (G,(s2 /. b2)) ) } is set
i is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
s1 . i is set
the Target of G . (s1 . i) is set
s2 /. 1 is Element of the carrier' of G
(G,P,W) is V43() real ext-real Element of REAL
(G,P,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,P,W) is V43() real ext-real Element of REAL
K142(REAL,(G,P,W),K193()) is V43() real ext-real Element of REAL
(G,P,W) + (G,s2,W) is V43() real ext-real set
vx is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,vx,W) is V43() real ext-real Element of REAL
(G,vx,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,vx,W) is V43() real ext-real Element of REAL
K142(REAL,(G,vx,W),K193()) is V43() real ext-real Element of REAL
vx is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,vx,W) is V43() real ext-real Element of REAL
(G,vx,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,vx,W) is V43() real ext-real Element of REAL
K142(REAL,(G,vx,W),K193()) is V43() real ext-real Element of REAL
vx is Element of the carrier of G
{vx} is non empty V19() finite 1 -element set
q9 is set
V \/ {vx} is non empty set
(G,P,W) is V43() real ext-real Element of REAL
(G,P,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,P,W) is V43() real ext-real Element of REAL
K142(REAL,(G,P,W),K193()) is V43() real ext-real Element of REAL
q9 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,q9,W) is V43() real ext-real Element of REAL
(G,q9,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,q9,W) is V43() real ext-real Element of REAL
K142(REAL,(G,q9,W),K193()) is V43() real ext-real Element of REAL
j is ordinal natural finite cardinal V43() real ext-real non negative set
i + j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
len q9 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
q9 . (len q9) is set
the Target of G . (q9 . (len q9)) is set
q9 ^ s2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
qx is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
len qx is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
(len q9) + 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
qx . (len qx) is set
the Target of G . (qx . (len qx)) is set
q9 . 1 is set
the Source of G . (q9 . 1) is set
qx . 1 is set
the Source of G . (qx . 1) is set
(G,q9) is finite Element of K27( the carrier of G)
dom q9 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom q9 & b1 in (G,(q9 /. b2)) ) } is set
(G,q9) \ {vx} is finite Element of K27( the carrier of G)
(G,q9) \ {v3} is finite Element of K27( the carrier of G)
V \ {v3} is Element of K27(V)
(G,qx) is finite Element of K27( the carrier of G)
dom qx is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom qx & b1 in (G,(qx /. b2)) ) } is set
(G,q9) \/ {v3} is non empty finite set
(G,qx) \ {v3} is finite Element of K27( the carrier of G)
(G,qx,W) is V43() real ext-real Element of REAL
(G,qx,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,qx,W) is V43() real ext-real Element of REAL
K142(REAL,(G,qx,W),K193()) is V43() real ext-real Element of REAL
j is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len t1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len t2 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t1 ^ t2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t1 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of G
len t1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
t1 . (len t1) is set
the Target of G . (t1 . (len t1)) is set
(G,t1) is finite Element of K27( the carrier of G)
dom t1 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom t1 & b1 in (G,(t1 /. b2)) ) } is set
t2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of G
t1 ^ t2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of G
(G,(t1 ^ t2)) is finite Element of K27( the carrier of G)
dom (t1 ^ t2) is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom (t1 ^ t2) & b1 in (G,((t1 ^ t2) /. b2)) ) } is set
(G,t1) \ {v2} is finite Element of K27( the carrier of G)
t1 . 1 is set
the Source of G . (t1 . 1) is set
(G,t1,W) is V43() real ext-real Element of REAL
(G,t1,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,t1,W) is V43() real ext-real Element of REAL
K142(REAL,(G,t1,W),K193()) is V43() real ext-real Element of REAL
(G,t2,W) is V43() real ext-real Element of REAL
(G,t2,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,t2,W) is V43() real ext-real Element of REAL
K142(REAL,(G,t2,W),K193()) is V43() real ext-real Element of REAL
(G,t1,W) + (G,t2,W) is V43() real ext-real set
(G,t1,W) + 0 is V43() real ext-real set
(G,q9,W) + (G,s2,W) is V43() real ext-real set
u is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,u,W) is V43() real ext-real Element of REAL
(G,u,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,u,W) is V43() real ext-real Element of REAL
K142(REAL,(G,u,W),K193()) is V43() real ext-real Element of REAL
u is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
(G,u,W) is V43() real ext-real Element of REAL
(G,u,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
Sum (G,u,W) is V43() real ext-real Element of REAL
K142(REAL,(G,u,W),K193()) is V43() real ext-real Element of REAL
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,s) is finite Element of K27( the carrier of G)
K27( the carrier of G) is finite V28() set
dom s is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ b1 where b1 is Element of the carrier of G : ex b2 being ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT st
( b2 in dom s & b1 in (G,(s /. b2)) ) } is set
s /. 1 is Element of the carrier' of G
(G,(s /. 1)) is set
the Source of G . (s /. 1) is set
the Target of G . (s /. 1) is set
{( the Source of G . (s /. 1)),( the Target of G . (s /. 1))} is non empty finite set
{v3} is non empty V19() finite 1 -element set
(G,s) \ {v3} is finite Element of K27( the carrier of G)
x is set
s . 1 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