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 - b1) * (f /. a)) + (b1 * (f /. (a + 1)))) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * (f /. b)) + (b1 * (f /. (b + 1)))) where b1 is V28() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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