:: GRAPH_5 semantic presentation

REAL is non empty V19() non finite V99() V100() V101() V105() set
NAT is ordinal V19() non finite cardinal limit_cardinal V99() V100() V101() V102() V103() V104() V105() Element of K27(REAL)
K27(REAL) is V19() non finite set
omega is ordinal V19() non finite cardinal limit_cardinal V99() V100() V101() V102() V103() V104() V105() set
K27(omega) is V19() non finite set
K27(NAT) is V19() non finite set
INT is non empty V19() non finite V99() V100() V101() V102() V103() V105() set
K141(NAT) is V42() set
COMPLEX is non empty V19() non finite V99() V105() set
RAT is non empty V19() non finite V99() V100() V101() V102() V105() set
K28(COMPLEX,COMPLEX) is Relation-like V19() non finite V88() set
K27(K28(COMPLEX,COMPLEX)) is V19() non finite set
K28(K28(COMPLEX,COMPLEX),COMPLEX) is Relation-like V19() non finite V88() set
K27(K28(K28(COMPLEX,COMPLEX),COMPLEX)) is V19() non finite set
K28(REAL,REAL) is Relation-like V19() non finite V88() V89() V90() set
K27(K28(REAL,REAL)) is V19() non finite set
K28(K28(REAL,REAL),REAL) is Relation-like V19() non finite V88() V89() V90() set
K27(K28(K28(REAL,REAL),REAL)) is V19() non finite set
K28(RAT,RAT) is Relation-like RAT -valued V19() non finite V88() V89() V90() set
K27(K28(RAT,RAT)) is V19() non finite set
K28(K28(RAT,RAT),RAT) is Relation-like RAT -valued V19() non finite V88() V89() V90() set
K27(K28(K28(RAT,RAT),RAT)) is V19() non finite set
K28(INT,INT) is Relation-like RAT -valued INT -valued V19() non finite V88() V89() V90() set
K27(K28(INT,INT)) is V19() non finite set
K28(K28(INT,INT),INT) is Relation-like RAT -valued INT -valued V19() non finite V88() V89() V90() set
K27(K28(K28(INT,INT),INT)) is V19() non finite set

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

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)

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

rng V is set
dom V is set
V . e is 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

dom e is 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

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)

dom G is set
Union G is set
P 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
dom Q is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)

Seg R is finite R -element V99() V100() V101() V102() V103() V104() Element of K27(NAT)
{ } is set

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

G . P is set
e is finite set

V is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT
{ } 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

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

K27((e *)) is set
V is functional non empty FinSequence-membered Element of K27((e *))

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
V . e is 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

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

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)

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)

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

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

rng (V ^ <*e*>) is non empty finite set
rng V is finite 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

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

len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

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

V9 is set

dom v3 is finite V99() V100() V101() V102() V103() V104() Element of K27(NAT)
v3 . R is 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) \/ () is non empty finite set
((rng pe) \/ ()) \/ (rng Eg) is non empty finite set
(rng pe) \/ (rng Eg) is finite set
((rng pe) \/ (rng Eg)) \/ () is non empty finite set
(rng (pe ^ Eg)) \/ () is non empty finite set
{e} is non empty V19() finite 1 -element set
(rng (pe ^ Eg)) \/ {e} is non empty finite 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

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

len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

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

len v3 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

len Eg is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

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

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

len pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

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

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 . 1 is set
the Source of e . (W . 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
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

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

W is non empty V73() MultiGraphStruct
the carrier' of W is set
the carrier of W is non empty 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
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

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

len v1 is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

len v2 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
pe is ordinal natural finite cardinal V43() real V45() V46() ext-real non negative V99() V100() V101() V102() V103() V104() Element of NAT

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

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

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

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

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

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

dom W is finite V99() V100() V101() V102() V103() V104() Element of K27(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
V9 is Element 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 + 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

the carrier of e is non empty 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
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

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

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

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

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 <