:: TOPREAL8 semantic presentation

REAL is set
NAT is non empty V7() V8() V9() V29() V34() V35() Element of bool REAL
bool REAL is set
NAT is non empty V7() V8() V9() V29() V34() V35() set
bool NAT is V29() set
bool NAT is V29() set
COMPLEX is set
2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
[:2,2:] is V16() set
[:[:2,2:],2:] is V16() set
bool [:[:2,2:],2:] is set
1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
[:1,1:] is V16() set
bool [:1,1:] is set
[:[:1,1:],1:] is V16() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V16() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V16() set
[:[:REAL,REAL:],REAL:] is V16() set
bool [:[:REAL,REAL:],REAL:] is set
[:[:2,2:],REAL:] is V16() set
bool [:[:2,2:],REAL:] is set
RAT is set
INT is set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty non trivial V73() V98() V99() V100() V101() V102() V103() V104() TopSpace-like strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty non trivial set
K287( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is set
{} is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative set
3 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
Sgm {} is V16() V19( NAT ) V20( NAT ) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of NAT
0 is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative Element of NAT
Seg 1 is non empty trivial V29() V36(1) Element of bool NAT
{1} is non empty trivial V36(1) set
Seg 2 is non empty V29() V36(2) Element of bool NAT
{1,2} is non empty set
K83({}) is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative set
rng {} is empty trivial with_non-empty_elements V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative set
4 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len {} is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative set
G is set
f is set
f9 is set
{f,f9} is non empty set
{f} is non empty trivial V36(1) set
{f9} is non empty trivial V36(1) set
{f9} is non empty trivial V36(1) set
the non empty non trivial V16() V19( NAT ) Function-like non constant V29() FinSequence-like FinSubsequence-like set is non empty non trivial V16() V19( NAT ) Function-like non constant V29() FinSequence-like FinSubsequence-like set
G is non empty non trivial V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is non empty non trivial set
f is non empty non trivial V16() V19( NAT ) V20(G) Function-like non constant V29() FinSequence-like FinSubsequence-like circular FinSequence of G
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is trivial V16() Function-like constant set
dom f is non empty non trivial Element of bool NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f . f9 is set
f . f9 is set
f /. 1 is Element of G
f /. (len f) is Element of G
f /. 1 is Element of G
f /. (len f) is Element of G
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng G is set
f is set
f .. G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{f} is non empty trivial V36(1) set
G " {f} is set
f9 is set
G . f9 is set
dom G is Element of bool NAT
Sgm (G " {f}) is V16() V19( NAT ) V20( NAT ) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (G " {f})) . 1 is set
G is set
f is non empty set
f9 is non empty V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
G .. f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
f9 ^ f9 is non empty V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
(f9 ^ f9) |-- G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng f9 is non empty Element of bool f
bool f is set
G .. (f9 ^ f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
rng (f9 ^ f9) is non empty Element of bool f
(f9 ^ f9) /^ (G .. (f9 ^ f9)) is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
G is non empty set
f is non empty V16() V19( NAT ) V20(G) Function-like one-to-one V29() FinSequence-like FinSubsequence-like FinSequence of G
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (len f) is Element of G
(f /. (len f)) .. f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
dom f is non empty Element of bool NAT
f . (len f) is set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f . f9 is set
G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G ^' f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(2,(len f)) -cut f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G ^ ((2,(len f)) -cut f) is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len ((2,(len f)) -cut f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len G) + (len ((2,(len f)) -cut f)) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng G is set
f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G ^' f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
f9 is set
f9 .. G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 .. (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G . (f9 .. G) is set
dom G is Element of bool NAT
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(G ^' f) . f9 is set
G . f9 is set
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
dom (G ^' f) is Element of bool NAT
(G ^' f) . (f9 .. G) is set
G is non empty V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G ^' f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len (G ^' f)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (len f) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + (len f) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng G is set
f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G ^' f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng (G ^' f) is set
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(2,(len f)) -cut f is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G ^ ((2,(len f)) -cut f) is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
G is non empty set
f is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f /. 1 is Element of G
f9 is non empty non trivial V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 /. (len f9) is Element of G
f ^' f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
(f ^' f9) /. 1 is Element of G
len (f ^' f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f ^' f9) /. (len (f ^' f9)) is Element of G
G is non empty set
K287(G) is non empty functional FinSequence-membered M12(G)
f is V16() V19( NAT ) V20(K287(G)) Function-like V29() FinSequence-like FinSubsequence-like tabular FinSequence of K287(G)
f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
len f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 /. (len f9) is Element of G
f9 is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 /. 1 is Element of G
f9 ^' f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
len (f9 ^' f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (f9 ^' f9)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f9) + (len f9) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom (f9 ^' f9) is Element of bool NAT
Indices f is set
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 ^' f9) /. h1 is Element of G
dom f9 is Element of bool NAT
f9 /. h1 is Element of G
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[h2,h1] is non empty set
{h2,h1} is non empty set
{h2} is non empty trivial V36(1) set
{{h2,h1},{h2}} is non empty set
f * (h2,h1) is Element of G
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len f9) + h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom f9 is non empty Element of bool NAT
f9 /. (h1 + 1) is Element of G
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[g1,g1] is non empty set
{g1,g1} is non empty set
{g1} is non empty trivial V36(1) set
{{g1,g1},{g1}} is non empty set
f * (g1,g1) is Element of G
(len f9) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f9 ^' f9) /. h1 is Element of G
(f9 ^' f9) /. (h1 + 1) is Element of G
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[h2,h1] is non empty set
{h2,h1} is non empty set
{h2} is non empty trivial V36(1) set
{{h2,h1},{h2}} is non empty set
f * (h2,h1) is Element of G
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h2 - g1 is V14() V15() V40() ext-real set
K144((h2 - g1)) is V14() V15() ext-real Element of REAL
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[g1,g1] is non empty set
{g1,g1} is non empty set
{g1} is non empty trivial V36(1) set
{{g1,g1},{g1}} is non empty set
f * (g1,g1) is Element of G
h1 - g1 is V14() V15() V40() ext-real set
K144((h1 - g1)) is V14() V15() ext-real Element of REAL
K144((h2 - g1)) + K144((h1 - g1)) is V14() V15() ext-real set
f9 /. (h1 + 1) is Element of G
dom f9 is Element of bool NAT
f9 /. h1 is Element of G
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len f9) + h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
g2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom f9 is non empty Element of bool NAT
(g2 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f9) + (g2 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f9) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 /. (g2 + 1) is Element of G
f9 /. ((g2 + 1) + 1) is Element of G
(f9 ^' f9) /. ((len f9) + (g2 + 1)) is Element of G
(len f9) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom f9 is non empty Element of bool NAT
f9 /. (1 + 1) is Element of G
G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f,f9) -cut G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
len ((f,f9) -cut G) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len ((f,f9) -cut G)) + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((f,f9) -cut G) . (f9 + 1) is set
f + f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G . (f + f9) is set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((f,f9) -cut G) . (f9 + 1) is set
f + f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G . (f + f9) is set
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f is set
f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
len f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((G + 1),(len f9)) -cut f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
f9 /^ G is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
<*> f is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) V20(f) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative FinSequence of f
(len f9) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom (((G + 1),(len f9)) -cut f9) is Element of bool NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(((G + 1),(len f9)) -cut f9) . h1 is set
h1 + G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 . (h1 + G) is set
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
1 + h2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len (((G + 1),(len f9)) -cut f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(G + 1) + h1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 . ((G + 1) + h1) is set
len (((G + 1),(len f9)) -cut f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (((G + 1),(len f9)) -cut f9)) + (G + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len (((G + 1),(len f9)) -cut f9)) + G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((len (((G + 1),(len f9)) -cut f9)) + G) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f9) - G is V14() V15() V40() ext-real set
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is set
f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
len f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(1,G) -cut f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
f9 | G is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 | 0 is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) V20(f) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative FinSequence of f
len (f9 | G) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (f9 | G)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f9 | G) . (f9 + 1) is set
1 + f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 . (1 + f9) is set
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is set
f is non empty set
f9 is non empty V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
G .. f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f9) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(1,((len f9) -' 1)) -cut f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
f9 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
f9 ^ f9 is non empty V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
(f9 ^ f9) -| G is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
rng f9 is non empty Element of bool f
bool f is set
G .. (f9 ^ f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len f9) - 1 is V14() V15() V40() ext-real set
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len (f9 ^ f9) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len f9) + (len f9) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
rng (f9 ^ f9) is non empty Element of bool f
Seg h1 is V29() V36(h1) Element of bool NAT
(f9 ^ f9) | (Seg h1) is V16() V19( NAT ) V19( Seg h1) V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like Element of bool [:NAT,f:]
[:NAT,f:] is V16() V29() set
bool [:NAT,f:] is V29() set
(f9 ^ f9) | h1 is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
(1,((len f9) -' 1)) -cut (f9 ^ f9) is V16() V19( NAT ) V20(f) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of f
G is non empty set
f is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 /. 1 is Element of G
(f9 /. 1) .. f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f ^' f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
(f ^' f9) :- (f9 /. 1) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng f is non empty Element of bool G
bool G is set
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(2,(len f9)) -cut f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f ^ ((2,(len f9)) -cut f9) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng (f ^' f9) is Element of bool G
<*(f9 /. 1)*> is non empty trivial V16() V19( NAT ) V20(G) Function-like constant V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of G
(f ^' f9) |-- (f9 /. 1) is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
<*(f9 /. 1)*> ^ ((f ^' f9) |-- (f9 /. 1)) is non empty V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
<*(f9 /. 1)*> ^ ((2,(len f9)) -cut f9) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 . 1 is set
<*(f9 . 1)*> is non empty trivial V16() V19( NAT ) Function-like constant V29() V36(1) FinSequence-like FinSubsequence-like set
<*(f9 . 1)*> ^ ((2,(len f9)) -cut f9) is non empty V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
(1,1) -cut f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((1 + 1),(len f9)) -cut f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
((1,1) -cut f9) ^ (((1 + 1),(len f9)) -cut f9) is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
G is non empty set
f is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 /. 1 is Element of G
(f9 /. 1) .. f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f ^' f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
(f ^' f9) -: (f9 /. 1) is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng f is non empty Element of bool G
bool G is set
f . (len f) is set
(len f) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((len f) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(2,(len f9)) -cut f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f ^ ((2,(len f9)) -cut f9) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng (f ^' f9) is Element of bool G
(f ^' f9) -| (f9 /. 1) is V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
<*(f9 /. 1)*> is non empty trivial V16() V19( NAT ) V20(G) Function-like constant V29() V36(1) FinSequence-like FinSubsequence-like FinSequence of G
((f ^' f9) -| (f9 /. 1)) ^ <*(f9 /. 1)*> is non empty V16() V19( NAT ) Function-like V29() FinSequence-like FinSubsequence-like set
(1,((len f) -' 1)) -cut f is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
((1,((len f) -' 1)) -cut f) ^ <*(f9 /. 1)*> is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
((len f),(len f)) -cut f is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
((1,((len f) -' 1)) -cut f) ^ (((len f),(len f)) -cut f) is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
G is non empty non trivial set
f is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (len f) is Element of G
f9 is non empty non trivial V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 /. 1 is Element of G
f ^' f9 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
Rotate ((f ^' f9),(f9 /. 1)) is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
f9 ^' f is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng f is non empty Element of bool G
bool G is set
dom f is non empty Element of bool NAT
f . (len f) is set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f . f9 is set
f /. f9 is Element of G
(f9 /. 1) .. f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f ^' f9) :- (f9 /. 1) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
(f ^' f9) -: (f9 /. 1) is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
((f ^' f9) -: (f9 /. 1)) /^ 1 is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((1 + 1),(len f)) -cut f is V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
rng (f ^' f9) is Element of bool G
((f ^' f9) :- (f9 /. 1)) ^ (((f ^' f9) -: (f9 /. 1)) /^ 1) is non empty V16() V19( NAT ) V20(G) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of G
G is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg (G,1) is Element of bool the carrier of (TOP-REAL 2)
G | 2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (G | 2) is Element of bool the carrier of (TOP-REAL 2)
len (G | 2) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg ((G | 2),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G | 2) ) } is set
union { (LSeg ((G | 2),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G | 2) ) } is set
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. 2 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
<*(G /. 1),(G /. 2)*> is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() V36(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
G /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg ((G /. 1),(G /. (1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like s.c.c. FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G | f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G | f),f9) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((G | f),f9) is Element of bool the carrier of (TOP-REAL 2)
len (G | f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(LSeg ((G | f),f9)) /\ (LSeg ((G | f),f9)) is Element of bool the carrier of (TOP-REAL 2)
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(LSeg ((G | f),f9)) /\ (LSeg ((G | f),f9)) is Element of bool the carrier of (TOP-REAL 2)
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like s.c.c. FinSequence of the carrier of (TOP-REAL 2)
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /^ f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G /^ f),f9) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((G /^ f),f9) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G /^ f),f9)) /\ (LSeg ((G /^ f),f9)) is Element of bool the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
<*> the carrier of (TOP-REAL 2) is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative special FinSequence of the carrier of (TOP-REAL 2)
len (G /^ f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(LSeg ((G /^ f),f9)) /\ (LSeg ((G /^ f),f9)) is Element of bool the carrier of (TOP-REAL 2)
len (G /^ f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(LSeg ((G /^ f),f9)) /\ (LSeg ((G /^ f),f9)) is Element of bool the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len (G /^ f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len G) - f is V14() V15() V40() ext-real set
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (G,(f9 + f)) is Element of bool the carrier of (TOP-REAL 2)
(f9 + 1) + f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 + f) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,(f9 + f)) is Element of bool the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len (G /^ f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like circular s.c.c. FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G | f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom (G | f) is Element of bool NAT
len (G | f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(G | f) /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(G | f) /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like circular s.c.c. FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. f is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like circular s.c.c. FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /^ f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom (G /^ f) is Element of bool NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(G /^ f) /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(G /^ f) /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f9 + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. (f9 + f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
len (G /^ f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len G) - f is V14() V15() V40() ext-real set
(len (G /^ f)) + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 + f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. (f9 + f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
(G,f) -cut f9 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len ((G,f) -cut f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((G,f) -cut f9) /. h1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(((G,f) -cut f9) /. h1) `1 is V14() V15() ext-real Element of REAL
((G,f) -cut f9) /. (h1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(((G,f) -cut f9) /. (h1 + 1)) `1 is V14() V15() ext-real Element of REAL
(((G,f) -cut f9) /. h1) `2 is V14() V15() ext-real Element of REAL
(((G,f) -cut f9) /. (h1 + 1)) `2 is V14() V15() ext-real Element of REAL
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 + G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(h1 -' 1) + G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(h1 + G) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((h1 -' 1) + G) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((h1 + G) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len ((G,f) -cut f9)) + G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((G,f) -cut f9) . (h1 + 1) is set
f9 . (h1 + G) is set
f9 /. (h1 + G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(h1 -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((G,f) -cut f9) . ((h1 -' 1) + 1) is set
f9 . ((h1 -' 1) + G) is set
f9 /. ((h1 -' 1) + G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G /. (len G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(2,(len f)) -cut f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
G ^ ((2,(len f)) -cut f) is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f /. 1) `1 is V14() V15() ext-real Element of REAL
f /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(f /. (1 + 1)) `1 is V14() V15() ext-real Element of REAL
(f /. 1) `2 is V14() V15() ext-real Element of REAL
(f /. (1 + 1)) `2 is V14() V15() ext-real Element of REAL
(len f) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len ((2,(len f)) -cut f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len ((2,(len f)) -cut f)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((len ((2,(len f)) -cut f)) + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len ((2,(len f)) -cut f)) + (1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((2,(len f)) -cut f) /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
((2,(len f)) -cut f) . 1 is set
f . (1 + 1) is set
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like circular unfolded s.c.c. FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (G,1) is Element of bool the carrier of (TOP-REAL 2)
G /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like unfolded FinSequence of the carrier of (TOP-REAL 2)
L~ (G /^ 1) is Element of bool the carrier of (TOP-REAL 2)
len (G /^ 1) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G /^ 1) ) } is set
union { (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G /^ 1) ) } is set
(LSeg (G,1)) /\ (L~ (G /^ 1)) is Element of bool the carrier of (TOP-REAL 2)
G /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. 2 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(G /. 1),(G /. 2)} is non empty set
1 + 2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) - 1 is V14() V15() V40() ext-real set
(len (G /^ 1)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
3 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
{ (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not len (G /^ 1) <= b₁ + 1 ) } is set
union { (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not len (G /^ 1) <= b₁ + 1 ) } is set
(len (G /^ 1)) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((len (G /^ 1)) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
{{}} is non empty trivial functional V36(1) set
{(LSeg (G,1))} is non empty trivial V36(1) set
h1 is set
h2 is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,(2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
h1 is Element of bool the carrier of (TOP-REAL 2)
h2 /\ h1 is set
LSeg ((G /^ 1),2) is Element of bool the carrier of (TOP-REAL 2)
h2 /\ h1 is Element of bool the carrier of (TOP-REAL 2)
h2 is set
h1 is set
h2 /\ h1 is set
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G /^ 1),g1) is Element of bool the carrier of (TOP-REAL 2)
g1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(g1 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,(g1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
INTERSECTION ({(LSeg (G,1))}, { (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not len (G /^ 1) <= b₁ + 1 ) } ) is set
(LSeg (G,1)) /\ (union { (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not len (G /^ 1) <= b₁ + 1 ) } ) is Element of bool the carrier of (TOP-REAL 2)
union {{}} is set
LSeg ((G /^ 1),1) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((G /^ 1),((len (G /^ 1)) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G /^ 1),1)) \/ (LSeg ((G /^ 1),((len (G /^ 1)) -' 1))) is Element of bool the carrier of (TOP-REAL 2)
((LSeg ((G /^ 1),1)) \/ (LSeg ((G /^ 1),((len (G /^ 1)) -' 1)))) \/ (union { (LSeg ((G /^ 1),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not len (G /^ 1) <= b₁ + 1 ) } ) is set
h1 is set
h2 is set
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G /^ 1),h1) is Element of bool the carrier of (TOP-REAL 2)
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 is set
h2 is set
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G /^ 1),h1) is Element of bool the carrier of (TOP-REAL 2)
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + ((len (G /^ 1)) -' 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(LSeg (G,1)) /\ (LSeg ((G /^ 1),((len (G /^ 1)) -' 1))) is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,((len G) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,1)) /\ (LSeg (G,((len G) -' 1))) is Element of bool the carrier of (TOP-REAL 2)
{(G /. 1)} is non empty trivial V36(1) set
(LSeg (G,1)) /\ (LSeg ((G /^ 1),1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,(1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,1)) /\ (LSeg (G,(1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
G /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(G /. (1 + 1))} is non empty trivial V36(1) set
(LSeg (G,1)) /\ ((LSeg ((G /^ 1),1)) \/ (LSeg ((G /^ 1),((len (G /^ 1)) -' 1)))) is Element of bool the carrier of (TOP-REAL 2)
((LSeg (G,1)) /\ ((LSeg ((G /^ 1),1)) \/ (LSeg ((G /^ 1),((len (G /^ 1)) -' 1))))) \/ {} is set
{(G /. 2)} is non empty trivial V36(1) set
{(G /. 1)} \/ {(G /. 2)} is non empty set
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f ^' f9 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((f ^' f9),G) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,G) is Element of bool the carrier of (TOP-REAL 2)
(f ^' f9) /. G is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. G is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f ^' f9) /. (G + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. (G + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
len (f ^' f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (((f ^' f9) /. G),((f ^' f9) /. (G + 1))) is Element of bool the carrier of (TOP-REAL 2)
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f ^' f9 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len f) + G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((f ^' f9),((len f) + G)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f9,(G + 1)) is Element of bool the carrier of (TOP-REAL 2)
((len f) + G) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f ^' f9) /. (((len f) + G) + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(len f) + (G + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f ^' f9) /. ((len f) + (G + 1)) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(G + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 /. ((G + 1) + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G + 0 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f ^' f9) /. ((len f) + G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f9 /. (G + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(len f) + (len f9) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len (f ^' f9) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (f ^' f9)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (((f ^' f9) /. ((len f) + G)),((f ^' f9) /. (((len f) + G) + 1))) is Element of bool the carrier of (TOP-REAL 2)
G is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G /. (len G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((G ^' f),(len G)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,1) is Element of bool the carrier of (TOP-REAL 2)
(len G) + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(G ^' f) /. ((len G) + 0) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (0 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((len G) + 0) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(G ^' f) /. (((len G) + 0) + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(0 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. ((0 + 1) + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (len f) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (G ^' f)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (((G ^' f) /. ((len G) + 0)),((G ^' f) /. (((len G) + 0) + 1))) is Element of bool the carrier of (TOP-REAL 2)
G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (len f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(len f) + G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f9 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f ^' f9 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((f ^' f9),((len f) + G)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f9,(G + 1)) is Element of bool the carrier of (TOP-REAL 2)
G is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
rng G is non empty Element of bool the carrier of (TOP-REAL 2)
f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (G,f) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,f)) /\ (rng G) is Element of bool the carrier of (TOP-REAL 2)
G /. f is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G /. (f + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(G /. f),(G /. (f + 1))} is non empty set
dom G is non empty Element of bool NAT
G . f is set
G . (f + 1) is set
f9 is set
f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
h1 is set
G . h1 is set
G /. h1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
1 + g1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (G,g1) is Element of bool the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f + (1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(LSeg (G,f)) /\ (LSeg (G,g1)) is Element of bool the carrier of (TOP-REAL 2)
{(G /. (f + 1))} is non empty trivial V36(1) set
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,h1) is Element of bool the carrier of (TOP-REAL 2)
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,h1) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,f)) /\ (LSeg (G,h1)) is Element of bool the carrier of (TOP-REAL 2)
(h1 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 + (1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
{(G /. f)} is non empty trivial V36(1) set
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G ^' f),f9)) /\ (LSeg ((G ^' f),f9)) is Element of bool the carrier of (TOP-REAL 2)
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
rng G is non empty Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,f9)) /\ (rng G) is Element of bool the carrier of (TOP-REAL 2)
G /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. (f9 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(G /. f9),(G /. (f9 + 1))} is non empty set
dom G is non empty Element of bool NAT
h1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G . 1 is set
G is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (len f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G ^' f),f9)) /\ (LSeg ((G ^' f),f9)) is Element of bool the carrier of (TOP-REAL 2)
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len G) + h1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len (G ^' f)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (len f) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(f9 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(h2 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + ((h2 + 1) + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom f is non empty non trivial Element of bool NAT
h1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg (f,(h2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
rng f is non empty Element of bool the carrier of (TOP-REAL 2)
(LSeg (f,(h2 + 1))) /\ (rng f) is Element of bool the carrier of (TOP-REAL 2)
f /. (h2 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. ((h2 + 1) + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(f /. (h2 + 1)),(f /. ((h2 + 1) + 1))} is non empty set
f . (len f) is set
(len G) + h2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
L~ G is non empty Element of bool the carrier of (TOP-REAL 2)
len G is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
{ (LSeg (G,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len G ) } is set
union { (LSeg (G,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len G ) } is set
f is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V29() FinSequence-like FinSubsequence-like unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2)
L~ f is non empty Element of bool the carrier of (TOP-REAL 2)
len f is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
{ (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
(L~ G) /\ (L~ f) is Element of bool the carrier of (TOP-REAL 2)
G /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(G /. 1),(f /. 1)} is non empty set
f /. (len f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G /. (len G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom G is non empty non trivial Element of bool NAT
G . (len G) is set
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. f9 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G . f9 is set
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (G ^' f)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (len f) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f ^' G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (f ^' G) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len (f ^' G)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
f9 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G ^' f),f9) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G ^' f),f9)) /\ (LSeg ((G ^' f),f9)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len G) + h1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len G) + h2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
g1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (g1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (f,(g1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(f9 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h1 + (1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (h1 + (1 + 1)) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(h1 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (f,(h1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
h1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
(len G) + h1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + (h2 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (f,(h2 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((G ^' f),f9)) /\ (LSeg ((G ^' f),f9)) is Element of bool the carrier of (TOP-REAL 2)
h1 is set
LSeg (G,f9) is Element of bool the carrier of (TOP-REAL 2)
(len G) + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 + 0 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 + 1) -' (len G) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
f9 -' (len G) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 -' (len G)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
Rotate ((G ^' f),(f /. 1)) is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom G is non empty non trivial Element of bool NAT
G . (len G) is set
rng G is non empty Element of bool the carrier of (TOP-REAL 2)
(f /. 1) .. (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f /. 1) .. G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
rng (G ^' f) is Element of bool the carrier of (TOP-REAL 2)
f9 -' ((f /. 1) .. (G ^' f)) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 -' ((f /. 1) .. (G ^' f))) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((Rotate ((G ^' f),(f /. 1))),((f9 -' ((f /. 1) .. (G ^' f))) + 1)) is Element of bool the carrier of (TOP-REAL 2)
f9 + (len (G ^' f)) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(f9 + (len (G ^' f))) -' ((f /. 1) .. (G ^' f)) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg ((Rotate ((G ^' f),(f /. 1))),((f9 + (len (G ^' f))) -' ((f /. 1) .. (G ^' f)))) is Element of bool the carrier of (TOP-REAL 2)
dom G is non empty non trivial Element of bool NAT
0 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len G) + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((G ^' f),((len G) + 0)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,(0 + 1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,1) is Element of bool the carrier of (TOP-REAL 2)
(f9 + 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f9 + (1 + 1) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom f is non empty non trivial Element of bool NAT
(len G) + 0 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. (len G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(len G) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
LSeg (G,((len G) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
{(G /. (len G))} is non empty trivial V36(1) set
f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg (f,1) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (G,((len G) -' 1))) /\ (LSeg (f,1)) is Element of bool the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((1 + 1),(len f)) -cut f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like unfolded FinSequence of the carrier of (TOP-REAL 2)
h1 /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like unfolded FinSequence of the carrier of (TOP-REAL 2)
G ^ (((1 + 1),(len f)) -cut f) is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*> the carrier of (TOP-REAL 2) is empty trivial V7() V8() V9() V11() V12() V13() V14() V15() V16() non-empty empty-yielding V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one constant functional V29() V34() V36( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V40() ext-real non positive non negative special FinSequence of the carrier of (TOP-REAL 2)
((len G) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f | (len f) is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /. 2 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
<*(f /. 1),(f /. 2)*> is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() V36(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*(f /. 2)*> is non empty trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like constant V29() V36(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
G ^ <*(f /. 2)*> is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(len f) - 1 is V14() V15() V40() ext-real set
f /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (f /^ 1) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
dom (f /^ 1) is Element of bool NAT
(((1 + 1),(len f)) -cut f) /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(f /^ 1) . 1 is set
f . (1 + 1) is set
f /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg ((G /. (len G)),((((1 + 1),(len f)) -cut f) /. 1)) is Element of bool the carrier of (TOP-REAL 2)
f /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((f /^ 1),1) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f,(1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(len f) - 1 is V14() V15() V40() ext-real set
len (f /^ 1) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
dom (f /^ 1) is Element of bool NAT
(((1 + 1),(len f)) -cut f) /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
(f /^ 1) . 1 is set
f . (1 + 1) is set
f /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg ((G /. (len G)),((((1 + 1),(len f)) -cut f) /. 1)) is Element of bool the carrier of (TOP-REAL 2)
((len G) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
1 + 2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg ((((1 + 1),(len f)) -cut f),1) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (f,1)) /\ (LSeg ((((1 + 1),(len f)) -cut f),1)) is Element of bool the carrier of (TOP-REAL 2)
{((((1 + 1),(len f)) -cut f) /. 1)} is non empty trivial V36(1) set
G is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len G is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
G /. (len G) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
L~ G is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (G,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len G ) } is set
union { (LSeg (G,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len G ) } is set
f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
G ^' f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (G ^' f) is Element of bool the carrier of (TOP-REAL 2)
len (G ^' f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg ((G ^' f),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G ^' f) ) } is set
union { (LSeg ((G ^' f),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G ^' f) ) } is set
L~ f is Element of bool the carrier of (TOP-REAL 2)
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
(L~ G) \/ (L~ f) is Element of bool the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
((1 + 1),(len f)) -cut f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (((1 + 1),(len f)) -cut f) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len f) - 1 is V14() V15() V40() ext-real set
1 - 1 is V14() V15() V40() ext-real set
<*(f /. 1)*> is non empty trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like constant V29() V36(1) FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)
<*(f /. 1)*> ^ (((1 + 1),(len f)) -cut f) is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(((1 + 1),(len f)) -cut f) /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. 1),((((1 + 1),(len f)) -cut f) /. 1)) is Element of bool the carrier of (TOP-REAL 2)
L~ (((1 + 1),(len f)) -cut f) is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg ((((1 + 1),(len f)) -cut f),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (((1 + 1),(len f)) -cut f) ) } is set
union { (LSeg ((((1 + 1),(len f)) -cut f),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (((1 + 1),(len f)) -cut f) ) } is set
(LSeg ((f /. 1),((((1 + 1),(len f)) -cut f) /. 1))) \/ (L~ (((1 + 1),(len f)) -cut f)) is Element of bool the carrier of (TOP-REAL 2)
G ^ (((1 + 1),(len f)) -cut f) is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (G ^ (((1 + 1),(len f)) -cut f)) is Element of bool the carrier of (TOP-REAL 2)
len (G ^ (((1 + 1),(len f)) -cut f)) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg ((G ^ (((1 + 1),(len f)) -cut f)),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G ^ (((1 + 1),(len f)) -cut f)) ) } is set
union { (LSeg ((G ^ (((1 + 1),(len f)) -cut f)),b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (G ^ (((1 + 1),(len f)) -cut f)) ) } is set
LSeg ((G /. (len G)),((((1 + 1),(len f)) -cut f) /. 1)) is Element of bool the carrier of (TOP-REAL 2)
(L~ G) \/ (LSeg ((G /. (len G)),((((1 + 1),(len f)) -cut f) /. 1))) is Element of bool the carrier of (TOP-REAL 2)
((L~ G) \/ (LSeg ((G /. (len G)),((((1 + 1),(len f)) -cut f) /. 1)))) \/ (L~ (((1 + 1),(len f)) -cut f)) is Element of bool the carrier of (TOP-REAL 2)
(L~ G) \/ ((LSeg ((f /. 1),((((1 + 1),(len f)) -cut f) /. 1))) \/ (L~ (((1 + 1),(len f)) -cut f))) is Element of bool the carrier of (TOP-REAL 2)
G is V16() non empty-yielding V19( NAT ) V20(K287( the carrier of (TOP-REAL 2))) Function-like V29() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K287( the carrier of (TOP-REAL 2))
Indices G is set
f is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom f is Element of bool NAT
len f is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
L~ f is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
f /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. (len f) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f9 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like non constant V29() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. FinSequence of the carrier of (TOP-REAL 2)
f9 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like non constant V29() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. FinSequence of the carrier of (TOP-REAL 2)
f9 | 2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like special unfolded FinSequence of the carrier of (TOP-REAL 2)
f9 /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like special unfolded FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
len (f9 | 2) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len h1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom h1 is non empty non trivial Element of bool NAT
h1 /. (len h1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. (1 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
len (f9 /^ 1) is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
(len f) - 1 is V14() V15() V40() ext-real set
(len (f9 /^ 1)) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h1 /. g1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
f /. g1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
h2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
[g1,h2] is non empty set
{g1,h2} is non empty set
{g1} is non empty trivial V36(1) set
{{g1,h2},{g1}} is non empty set
G * (g1,h2) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[g2,g2] is non empty set
{g2,g2} is non empty set
{g2} is non empty trivial V36(1) set
{{g2,g2},{g2}} is non empty set
G * (g2,g2) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
L~ h1 is non empty Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (h1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len h1 ) } is set
union { (LSeg (h1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len h1 ) } is set
h1 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg (g1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
union { (LSeg (g1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
g1 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g1 /. (len g1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g1 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len g1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len g1) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((len g1) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g1 /. (len g1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg (g1,((len g1) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
L~ g1 is non empty Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (g1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
union { (LSeg (g1,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
(1 + 1) - 1 is V14() V15() V40() ext-real set
h2 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len h2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
dom h2 is non empty non trivial Element of bool NAT
h2 /. (len h2) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
h2 /. g2 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
f /. (g2 + 1) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
g is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative set
[g2,g] is non empty set
{g2,g} is non empty set
{g2} is non empty trivial V36(1) set
{{g2,g},{g2}} is non empty set
G * (g2,g) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
i is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
j is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
[i,j] is non empty set
{i,j} is non empty set
{i} is non empty trivial V36(1) set
{{i,j},{i}} is non empty set
G * (i,j) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
L~ h2 is non empty Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (h2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len h2 ) } is set
union { (LSeg (h2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len h2 ) } is set
h2 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g2 is Element of bool the carrier of (TOP-REAL 2)
len g2 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg (g2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
union { (LSeg (g2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
g2 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 /. (len g2) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 is non empty non trivial V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len g2 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len g2) -' 1 is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
((len g2) -' 1) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
LSeg (g2,1) is Element of bool the carrier of (TOP-REAL 2)
L~ g2 is non empty Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (g2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
union { (LSeg (g2,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
g1 ^' g2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g is Element of bool the carrier of (TOP-REAL 2)
len g is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT
{ (LSeg (g,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
g /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g /. (len g) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg (f,1) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (f,1)) /\ (L~ h2) is Element of bool the carrier of (TOP-REAL 2)
{(h1 /. 1),(h2 /. 1)} is non empty set
(L~ g1) /\ (L~ g2) is Element of bool the carrier of (TOP-REAL 2)
g1 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
g2 /. 1 is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
{(g1 /. 1),(g2 /. 1)} is non empty set
3 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(3 + 1) - 1 is V14() V15() V40() ext-real set
2 + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
g2 /. (len g2) is V36(2) FinSequence-like V133() Element of the carrier of (TOP-REAL 2)
LSeg (g2,((len g2) -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) is Element of bool the carrier of (TOP-REAL 2)
{(g2 /. 1)} is non empty trivial V36(1) set
((1 + 1),(len h2)) -cut h2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h2 /^ 1 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /^ (1 + 1) is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h1 ^ (f /^ (1 + 1)) is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(2,(len h2)) -cut h2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h1 ^ ((2,(len h2)) -cut h2) is non empty V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h1 ^' h2 is V16() V19( NAT ) V20( the carrier of (TOP-REAL 2)) Function-like V29() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(len f) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len h1) + (len h2) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(L~ h1) \/ (L~ h2) is non empty Element of bool the carrier of (TOP-REAL 2)
(len g) + 1 is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT
(len g1) + (len g2) is non empty V7() V8() V9() V13() V14() V15() V29() V34() V40() ext-real positive non negative Element of NAT