:: JGRAPH_1 semantic presentation

REAL is V181() V182() V183() V187() V283() V284() V286() set

NAT is non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() Element of bool REAL

bool REAL is set

{} is set

RAT is V181() V182() V183() V184() V187() set

the V1() non-empty empty-yielding V4( NAT ) V5( RAT ) Function-like one-to-one constant functional empty ordinal natural V28() real ext-real non positive non negative finite finite-yielding V45() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V172() V173() V174() V181() V182() V183() V184() V185() V186() V187() V283() V284() V285() V286() set is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) Function-like one-to-one constant functional empty ordinal natural V28() real ext-real non positive non negative finite finite-yielding V45() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V172() V173() V174() V181() V182() V183() V184() V185() V186() V187() V283() V284() V285() V286() set

1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

{{},1} is finite set

COMPLEX is V181() V187() set

INT is V181() V182() V183() V184() V185() V187() set

[:COMPLEX,COMPLEX:] is V1() complex-yielding set

bool [:COMPLEX,COMPLEX:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is V1() complex-yielding set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:REAL,REAL:] is V1() complex-yielding V172() V173() set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is V1() complex-yielding V172() V173() set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is V1() V5( RAT ) complex-yielding V172() V173() set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is V1() V5( RAT ) complex-yielding V172() V173() set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is V1() V5( RAT ) V5( INT ) complex-yielding V172() V173() set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is V1() V5( RAT ) V5( INT ) complex-yielding V172() V173() set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is V1() V5( RAT ) V5( INT ) complex-yielding V172() V173() V174() set

[:[:NAT,NAT:],NAT:] is V1() V5( RAT ) V5( INT ) complex-yielding V172() V173() V174() set

bool [:[:NAT,NAT:],NAT:] is set

omega is non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() set

bool omega is non trivial non finite set

bool NAT is non trivial non finite set

K312() is set

[:1,1:] is V1() V5( RAT ) V5( INT ) finite complex-yielding V172() V173() V174() set

bool [:1,1:] is finite V45() set

[:[:1,1:],1:] is V1() V5( RAT ) V5( INT ) finite complex-yielding V172() V173() V174() set

bool [:[:1,1:],1:] is finite V45() set

[:[:1,1:],REAL:] is V1() complex-yielding V172() V173() set

bool [:[:1,1:],REAL:] is set

2 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

[:2,2:] is V1() V5( RAT ) V5( INT ) finite complex-yielding V172() V173() V174() set

[:[:2,2:],REAL:] is V1() complex-yielding V172() V173() set

bool [:[:2,2:],REAL:] is set

K510() is non empty V130() L10()

the carrier of K510() is non empty set

K515() is non empty L10()

K516() is non empty V130() M20(K515())

K517() is non empty V130() V152() V209() M23(K515(),K516())

K519() is non empty V130() V152() V154() V156() L10()

K520() is non empty V130() V152() V209() M20(K519())

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict RLTopStruct

the carrier of (TOP-REAL 2) is functional non empty set

K302( the carrier of (TOP-REAL 2)) is functional non empty FinSequence-membered M9( the carrier of (TOP-REAL 2))

bool the carrier of (TOP-REAL 2) is set

[: the carrier of (TOP-REAL 2),REAL:] is V1() complex-yielding V172() V173() set

bool [: the carrier of (TOP-REAL 2),REAL:] is set

K711() is non empty strict TopSpace-like TopStruct

the carrier of K711() is non empty set

RealSpace is non empty strict Reflexive discerning V105() triangle Discerning MetrStruct

K716() is TopSpace-like TopStruct

the carrier of K716() is set

3 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

I[01] is non empty strict TopSpace-like SubSpace of K716()

the carrier of I[01] is non empty set

0 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

5 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

bool the carrier of I[01] is set

K717(0,1) is non empty strict TopSpace-like SubSpace of K716()

[.0,1.] is V181() V182() V183() V286() Element of bool REAL

f is non empty V76() MultiGraphStruct

the carrier' of f is set

the carrier of f is non empty set

g is V1() V4( NAT ) V5( the carrier' of f) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f

a is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

b is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

c is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

d is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a . c is set

a . d is set

c is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

d is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a . c is set

a . d is set

f is set

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

f is set

(f) is MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier of (f) is set

f is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len f) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

g is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g . a is set

f . a is set

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

f . (a + 1) is set

[(f . a),(f . (a + 1))] is set

{(f . a),(f . (a + 1))} is finite set

{(f . a)} is non empty trivial finite 1 -element set

{{(f . a),(f . (a + 1))},{(f . a)}} is finite V45() set

(a + 1) - 1 is V28() real ext-real Element of REAL

(len f) - 1 is V28() real ext-real Element of REAL

g is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

b is ordinal natural V28() real ext-real non negative finite cardinal set

g . b is set

a . b is set

(len f) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len f) - 1 is V28() real ext-real Element of REAL

f . b is set

b + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

f . (b + 1) is set

[(f . b),(f . (b + 1))] is set

{(f . b),(f . (b + 1))} is finite set

{(f . b)} is non empty trivial finite 1 -element set

{{(f . b),(f . (b + 1))},{(f . b)}} is finite V45() set

(len f) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

((len f) + 1) - 1 is V28() real ext-real Element of REAL

1 - 1 is V28() real ext-real Element of REAL

0 - 1 is V28() real ext-real Element of REAL

f is non empty set

(f) is MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier of (f) is non empty set

f is non empty set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(g) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

rng (g) is finite set

a is set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

((len g) -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

dom (g) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

b is set

(g) . b is set

len (g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

Seg (len (g)) is finite len (g) -element V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

c is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) - 1 is V28() real ext-real Element of REAL

c + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

g . (c + 1) is set

rng g is finite Element of bool f

bool f is set

g . c is set

(g) . c is set

[(g . c),(g . (c + 1))] is set

{(g . c),(g . (c + 1))} is finite set

{(g . c)} is non empty trivial finite 1 -element set

{{(g . c),(g . (c + 1))},{(g . c)}} is finite V45() set

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(g) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

f is non empty set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(f,a) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of (f)

len (f,a) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(f,a) . g is set

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len a) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

((len a) -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len a) - 1 is V28() real ext-real Element of REAL

g + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

dom a is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

a . (g + 1) is set

rng a is finite Element of bool f

bool f is set

a . g is set

[(a . g),(a . (g + 1))] is set

{(a . g),(a . (g + 1))} is finite set

{(a . g)} is non empty trivial finite 1 -element set

{{(a . g),(a . (g + 1))},{(a . g)}} is finite V45() set

f is non empty set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of (f)

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) - 1 is V28() real ext-real Element of REAL

((len g) - 1) + 1 is V28() real ext-real Element of REAL

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

((len g) -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

len (f,g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len (f,g)) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

the carrier of (f) is non empty set

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g . a is set

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

rng g is finite Element of bool f

bool f is set

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g . a is set

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

g . (a + 1) is set

(f,g) . a is set

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

rng g is finite Element of bool f

bool f is set

(pr2 (f,f)) . ((g . a),(g . (a + 1))) is set

[(g . a),(g . (a + 1))] is set

{(g . a),(g . (a + 1))} is finite set

{(g . a)} is non empty trivial finite 1 -element set

{{(g . a),(g . (a + 1))},{(g . a)}} is finite V45() set

(pr2 (f,f)) . [(g . a),(g . (a + 1))] is set

the Target of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

[: the carrier' of (f), the carrier of (f):] is V1() set

bool [: the carrier' of (f), the carrier of (f):] is set

the Target of (f) . ((f,g) . a) is set

c is Element of the carrier of (f)

(pr1 (f,f)) . ((g . a),(g . (a + 1))) is set

(pr1 (f,f)) . [(g . a),(g . (a + 1))] is set

the Source of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

the Source of (f) . ((f,g) . a) is set

b is Element of the carrier of (f)

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(f,g) . a is set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

((len g) + 1) - 1 is V28() real ext-real Element of REAL

1 - 1 is V28() real ext-real Element of REAL

0 - 1 is V28() real ext-real Element of REAL

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len (f,g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len (f,g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

the Source of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

the carrier of (f) is non empty set

[: the carrier' of (f), the carrier of (f):] is V1() set

bool [: the carrier' of (f), the carrier of (f):] is set

the Target of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

((len g) -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(f,g) . (a + 1) is set

the Source of (f) . ((f,g) . (a + 1)) is set

(f,g) . a is set

the Target of (f) . ((f,g) . a) is set

(len g) - 1 is V28() real ext-real Element of REAL

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

g . a is set

rng g is finite Element of bool f

bool f is set

(a + 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

g . ((a + 1) + 1) is set

g . (a + 1) is set

(pr2 (f,f)) . ((g . a),(g . (a + 1))) is set

[(g . a),(g . (a + 1))] is set

{(g . a),(g . (a + 1))} is finite set

{(g . a)} is non empty trivial finite 1 -element set

{{(g . a),(g . (a + 1))},{(g . a)}} is finite V45() set

(pr2 (f,f)) . [(g . a),(g . (a + 1))] is set

b is Element of the carrier of (f)

(pr1 (f,f)) . ((g . (a + 1)),(g . ((a + 1) + 1))) is set

[(g . (a + 1)),(g . ((a + 1) + 1))] is set

{(g . (a + 1)),(g . ((a + 1) + 1))} is finite set

{(g . (a + 1))} is non empty trivial finite 1 -element set

{{(g . (a + 1)),(g . ((a + 1) + 1))},{(g . (a + 1))}} is finite V45() set

(pr1 (f,f)) . [(g . (a + 1)),(g . ((a + 1) + 1))] is set

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(g) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

f is non empty set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier of (f) is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

the carrier' of (f) is set

a is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

len (f,g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

((len g) -' 1) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

b is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a /. b is Element of the carrier of (f)

b + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

a /. (b + 1) is Element of the carrier of (f)

(f,g) . b is set

(len g) - 1 is V28() real ext-real Element of REAL

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

g . (b + 1) is set

rng g is finite Element of bool f

bool f is set

g . b is set

(pr1 (f,f)) . ((g . b),(g . (b + 1))) is set

[(g . b),(g . (b + 1))] is set

{(g . b),(g . (b + 1))} is finite set

{(g . b)} is non empty trivial finite 1 -element set

{{(g . b),(g . (b + 1))},{(g . b)}} is finite V45() set

(pr1 (f,f)) . [(g . b),(g . (b + 1))] is set

(pr2 (f,f)) . ((g . b),(g . (b + 1))) is set

(pr2 (f,f)) . [(g . b),(g . (b + 1))] is set

a . (b + 1) is set

the Target of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

[: the carrier' of (f), the carrier of (f):] is V1() set

bool [: the carrier' of (f), the carrier of (f):] is set

the Target of (f) . ((f,g) . b) is set

a . b is set

the Source of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

the Source of (f) . ((f,g) . b) is set

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) - 1 is V28() real ext-real Element of REAL

((len g) - 1) + 1 is V28() real ext-real Element of REAL

(len (f,g)) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

f is non empty set

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

a is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

b is finite set

card b is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of omega

Seg (len g) is finite len g -element V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

card (Seg (len g)) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of omega

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

bool (f,g) is finite V45() set

bool g is finite V45() set

the carrier of (f) is non empty set

c is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSubsequence-like Element of bool (f,g)

Seq c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

O is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of (f)

d is V1() V4( NAT ) V5(f) Function-like finite FinSubsequence-like Element of bool g

Seq d is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

I is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

len I is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len O is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len O) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

dom d is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

Sgm (dom d) is V1() V4( NAT ) V5( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-yielding V172() V173() V174() FinSequence of NAT

rng (Sgm (dom d)) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool REAL

d * (Sgm (dom d)) is V1() V4( NAT ) V5(f) Function-like finite set

dom a is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

dom (Sgm (dom d)) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

len (Sgm (dom d)) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

P is finite set

card P is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of omega

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier of (f) is non empty set

the carrier' of (f) is set

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

bool (f,g) is finite V45() set

a is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

bool a is finite V45() set

a . 1 is set

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a . (len a) is set

b is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSubsequence-like Element of bool (f,g)

Seq b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

d is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of (f)

c is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSubsequence-like Element of bool a

Seq c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

O is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

O . 1 is set

len O is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

O . (len O) is set

I is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

f is non empty set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

a is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

(f,a) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

rng (f,a) is finite Element of bool the carrier' of (f)

bool the carrier' of (f) is set

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

rng (f,g) is finite Element of bool the carrier' of (f)

len (f,a) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len a) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len a) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len a) - 1 is V28() real ext-real Element of REAL

bool (f,g) is finite V45() set

bool g is finite V45() set

the carrier of (f) is non empty set

b is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSubsequence-like Element of bool (f,g)

Seq b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

d is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of (f)

c is V1() V4( NAT ) V5(f) Function-like finite FinSubsequence-like Element of bool g

Seq c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

O is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

dom b is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

Sgm (dom b) is V1() V4( NAT ) V5( NAT ) Function-like finite FinSequence-like FinSubsequence-like complex-yielding V172() V173() V174() FinSequence of NAT

rng (Sgm (dom b)) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool REAL

b * (Sgm (dom b)) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite set

rng b is finite Element of bool the carrier' of (f)

rng d is finite Element of bool the carrier' of (f)

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len g) - 1 is V28() real ext-real Element of REAL

I is set

dom (f,a) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

P is set

(f,a) . P is set

Seg (len (f,a)) is finite len (f,a) -element V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

f1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

f1 + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

len d is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len d) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

O /. f1 is Element of the carrier of (f)

O /. (f1 + 1) is Element of the carrier of (f)

d . f1 is set

dom d is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

dom (f,g) is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

Q is set

(f,g) . Q is set

len (f,g) is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

Seg (len (f,g)) is finite len (f,g) -element V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

g1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len g) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g1 + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

g . g1 is set

g . (g1 + 1) is set

[(g . g1),(g . (g1 + 1))] is set

{(g . g1),(g . (g1 + 1))} is finite set

{(g . g1)} is non empty trivial finite 1 -element set

{{(g . g1),(g . (g1 + 1))},{(g . g1)}} is finite V45() set

dom g is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

rng g is finite Element of bool f

bool f is set

the Source of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

[: the carrier' of (f), the carrier of (f):] is V1() set

bool [: the carrier' of (f), the carrier of (f):] is set

the Source of (f) . ((g . g1),(g . (g1 + 1))) is set

the Source of (f) . [(g . g1),(g . (g1 + 1))] is set

a . f1 is set

a . (f1 + 1) is set

[(a . f1),(a . (f1 + 1))] is set

{(a . f1),(a . (f1 + 1))} is finite set

{(a . f1)} is non empty trivial finite 1 -element set

{{(a . f1),(a . (f1 + 1))},{(a . f1)}} is finite V45() set

the Target of (f) is V1() V4( the carrier' of (f)) V5( the carrier of (f)) Function-like total V18( the carrier' of (f), the carrier of (f)) Element of bool [: the carrier' of (f), the carrier of (f):]

the Target of (f) . ((g . g1),(g . (g1 + 1))) is set

the Target of (f) . [(g . g1),(g . (g1 + 1))] is set

len O is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

f is non empty set

g is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

g . 1 is set

len g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g . (len g) is set

a is V1() V4( NAT ) V5(f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of f

a . 1 is set

len a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a . (len a) is set

(f) is non empty V76() MultiGraphStruct

[:f,f:] is V1() set

pr1 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

[:[:f,f:],f:] is V1() set

bool [:[:f,f:],f:] is set

pr2 (f,f) is V1() V4([:f,f:]) V5(f) Function-like total V18([:f,f:],f) Element of bool [:[:f,f:],f:]

MultiGraphStruct(# f,[:f,f:],(pr1 (f,f)),(pr2 (f,f)) #) is strict MultiGraphStruct

the carrier' of (f) is set

(f,g) is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (f)

bool (f,g) is finite V45() set

bool g is finite V45() set

the carrier of (f) is non empty set

b is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSubsequence-like Element of bool (f,g)

Seq b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

d is V1() V4( NAT ) V5( the carrier' of (f)) Function-like finite FinSequence-like FinSubsequence-like oriented simple Chain of (f)

c is V1() V4( NAT ) V5(f) Function-like finite FinSubsequence-like Element of bool g

Seq c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like set

O is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

I is V1() V4( NAT ) V5( the carrier of (f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (f)

len I is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len O is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

len d is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len d) + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

P is set

K48(a) is finite set

f1 is set

a . P is set

a . f1 is set

dom a is finite V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

Seg (len a) is finite len a -element V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of bool NAT

Q is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

TOP-REAL f is non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict RLTopStruct

the carrier of (TOP-REAL f) is functional non empty set

f is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,g) is functional Element of bool the carrier of (TOP-REAL 2)

LSeg (f,a) is functional Element of bool the carrier of (TOP-REAL 2)

f is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

LSeg (f,1) is functional Element of bool the carrier of (TOP-REAL 2)

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

(len f) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

LSeg (f,((len f) -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)

a is ordinal natural V28() real ext-real non negative finite cardinal set

g is ordinal natural V28() real ext-real non negative finite cardinal set

g + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,g) is functional Element of bool the carrier of (TOP-REAL 2)

LSeg (f,a) is functional Element of bool the carrier of (TOP-REAL 2)

0 + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len f) - 1 is V28() real ext-real Element of REAL

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,g)) /\ (LSeg (f,a)) is functional Element of bool the carrier of (TOP-REAL 2)

( the carrier of (TOP-REAL 2)) is non empty V76() MultiGraphStruct

[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):] is V1() set

pr1 ( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is V1() V4([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]) V5( the carrier of (TOP-REAL 2)) Function-like total V18([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2)) Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]

[:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is V1() set

bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):] is set

pr2 ( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is V1() V4([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):]) V5( the carrier of (TOP-REAL 2)) Function-like total V18([: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2)) Element of bool [:[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):], the carrier of (TOP-REAL 2):]

MultiGraphStruct(# the carrier of (TOP-REAL 2),[: the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2):],(pr1 ( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))),(pr2 ( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) #) is strict MultiGraphStruct

f is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

( the carrier of (TOP-REAL 2),f) is V1() V4( NAT ) V5( the carrier' of ( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of ( the carrier of (TOP-REAL 2))

the carrier' of ( the carrier of (TOP-REAL 2)) is set

the carrier of ( the carrier of (TOP-REAL 2)) is non empty set

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g is V1() V4( NAT ) V5( the carrier of ( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ( the carrier of (TOP-REAL 2))

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,a) is functional Element of bool the carrier of (TOP-REAL 2)

b is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

b + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,b) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

f . a is V1() Function-like set

{(f . a)} is functional non empty trivial finite 1 -element set

f . b is V1() Function-like set

f . (b + 1) is V1() Function-like set

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

f . (a + 1) is V1() Function-like set

{(f . (a + 1))} is functional non empty trivial finite 1 -element set

f . b is V1() Function-like set

f . (b + 1) is V1() Function-like set

f /. a is V1() V4( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like complex-yielding V172() V173() Element of the carrier of (TOP-REAL 2)

f /. (a + 1) is V1() V4( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like complex-yielding V172() V173() Element of the carrier of (TOP-REAL 2)

LSeg ((f /. a),(f /. (a + 1))) is functional Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

f /. b is V1() V4( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like complex-yielding V172() V173() Element of the carrier of (TOP-REAL 2)

f /. (b + 1) is V1() V4( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like complex-yielding V172() V173() Element of the carrier of (TOP-REAL 2)

LSeg ((f /. b),(f /. (b + 1))) is functional Element of bool the carrier of (TOP-REAL 2)

{ (((1 - b

f . b is V1() Function-like set

f . (b + 1) is V1() Function-like set

f . a is V1() Function-like set

f . (a + 1) is V1() Function-like set

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

f . a is V1() Function-like set

{(f . a)} is functional non empty trivial finite 1 -element set

f . b is V1() Function-like set

f . (b + 1) is V1() Function-like set

f . (a + 1) is V1() Function-like set

{(f . (a + 1))} is functional non empty trivial finite 1 -element set

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

f . a is V1() Function-like set

{(f . a)} is functional non empty trivial finite 1 -element set

f . b is V1() Function-like set

f . (b + 1) is V1() Function-like set

f . (a + 1) is V1() Function-like set

{(f . (a + 1))} is functional non empty trivial finite 1 -element set

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

a + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,a) is functional Element of bool the carrier of (TOP-REAL 2)

b is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

b + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

LSeg (f,b) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

(LSeg (f,a)) /\ (LSeg (f,b)) is functional Element of bool the carrier of (TOP-REAL 2)

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

f is V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

( the carrier of (TOP-REAL 2),f) is V1() V4( NAT ) V5( the carrier' of ( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like oriented Chain of ( the carrier of (TOP-REAL 2))

the carrier' of ( the carrier of (TOP-REAL 2)) is set

f . 1 is V1() Function-like set

len f is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

f . (len f) is V1() Function-like set

the carrier of ( the carrier of (TOP-REAL 2)) is non empty set

(len f) -' 1 is ordinal natural V28() real ext-real non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V283() V284() V285() Element of NAT

g is V1() V4( NAT ) V5( the carrier of ( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ( the carrier of (TOP-REAL 2))

1 + 1 is non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() Element of NAT

(len f) - 1 is V28() real ext-real Element of REAL

((len f) -' 1) + 1 is non