REAL is V172() V173() V174() V178() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V172() V173() V174() V175() V176() V177() V178() Element of bool REAL
bool REAL is set
omega is non empty epsilon-transitive epsilon-connected ordinal V32() V37() V38() V172() V173() V174() V175() V176() V177() V178() set
bool omega is V32() set
bool NAT is V32() set
COMPLEX is V172() V178() set
RAT is V172() V173() V174() V175() V178() set
INT is V172() V173() V174() V175() V176() V178() set
[:COMPLEX,COMPLEX:] is V15() set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V15() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is V15() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is V15() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is V15() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is V15() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is V15() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is V15() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is V15() V32() set
[:[:NAT,NAT:],NAT:] is V15() V32() set
bool [:[:NAT,NAT:],NAT:] is V32() set
K266() is set
1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
I[01] is TopStruct
the carrier of I[01] is set
[:1,1:] is V15() set
bool [:1,1:] is set
[:[:1,1:],1:] is V15() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V15() set
bool [:[:1,1:],REAL:] is set
2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
[:2,2:] is V15() set
[:[:2,2:],REAL:] is V15() set
bool [:[:2,2:],REAL:] is set
K408() is V111() L7()
K418() is TopSpace-like TopStruct
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V138() V184() V185() V186() V187() V188() V189() V190() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
bool the carrier of (TOP-REAL 2) is set
{} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set
the ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set
3 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V45() V172() V173() V174() V175() V176() V177() V178() Element of NAT
K419(0,1) is non empty strict TopSpace-like SubSpace of K418()
K420() is TopSpace-like SubSpace of K418()
the carrier of K420() is set
K75({}) is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set
rng {} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set
len {} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() set
P is ext-real V14() real set
p1 is ext-real V14() real set
|[P,p1]| is non empty non trivial V15() V18( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V164() Element of the carrier of (TOP-REAL 2)
p2 is ext-real V14() real set
f1 is ext-real V14() real set
|[p2,f1]| is non empty non trivial V15() V18( NAT ) Function-like V32() V39(2) FinSequence-like FinSubsequence-like V164() Element of the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
Rev P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p1 + p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
LSeg (P,p1) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((Rev P),p2) is Element of bool the carrier of (TOP-REAL 2)
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + (p2 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
dom (Rev P) is V172() V173() V174() V175() V176() V177() Element of bool NAT
len (Rev P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p1 + 1) + p2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (p1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p1),(P /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(Rev P) /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((Rev P) /. (p2 + 1)),(P /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(Rev P) /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((Rev P) /. p2),((Rev P) /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (Rev P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
P | p2 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (P | p2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg ((P | p2),p1) is Element of bool the carrier of (TOP-REAL 2)
LSeg (P,p1) is Element of bool the carrier of (TOP-REAL 2)
dom (P | p2) is V172() V173() V174() V175() V176() V177() Element of bool NAT
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(P | p2) /. p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P | p2) /. (p1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P | p2) /. p1),((P | p2) /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p1),((P | p2) /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. (p1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p1),(P /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
P /^ p2 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((P /^ p2),p1) is Element of bool the carrier of (TOP-REAL 2)
p2 + p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
LSeg (P,(p2 + p1)) is Element of bool the carrier of (TOP-REAL 2)
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) - p2 is ext-real V14() real V44() set
1 + p2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (P /^ p2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom (P /^ p2) is V172() V173() V174() V175() V176() V177() Element of bool NAT
(p1 + 1) + p2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
(P /^ p2) /. p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P /^ p2) /. (p1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P /^ p2) /. p1),((P /^ p2) /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. (p1 + p2) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p1 + p2)),((P /^ p2) /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. ((p1 + 1) + p2) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p1 + p2)),(P /. ((p1 + 1) + p2))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(p1 + p2) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. ((p1 + p2) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p1 + p2)),(P /. ((p1 + p2) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) - p2 is ext-real V14() real V44() set
p2 + (p1 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p2 + p1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (P /^ p2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) - p2 is ext-real V14() real V44() set
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
(len P) - p2 is ext-real V14() real V44() set
P /^ p2 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((P /^ p2),p1) is Element of bool the carrier of (TOP-REAL 2)
p2 + p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
LSeg (P,(p2 + p1)) is Element of bool the carrier of (TOP-REAL 2)
(p1 + 1) + p2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P ^ p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg ((P ^ p1),p2) is Element of bool the carrier of (TOP-REAL 2)
LSeg (P,p2) is Element of bool the carrier of (TOP-REAL 2)
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
len (P ^ p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (len p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p2),(P /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(P ^ p1) /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P ^ p1) /. p2),(P /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(P ^ p1) /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P ^ p1) /. p2),((P ^ p1) /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P ^ p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
(len P) + p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg ((P ^ p1),((len P) + p2)) is closed Element of bool the carrier of (TOP-REAL 2)
LSeg (p1,p2) is Element of bool the carrier of (TOP-REAL 2)
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (p2 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
((len P) + p2) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (len p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (P ^ p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom p1 is V172() V173() V174() V175() V176() V177() Element of bool NAT
p1 /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p1 /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((p1 /. p2),(p1 /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(P ^ p1) /. ((len P) + p2) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P ^ p1) /. ((len P) + p2)),(p1 /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(P ^ p1) /. ((len P) + (p2 + 1)) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P ^ p1) /. ((len P) + p2)),((P ^ p1) /. ((len P) + (p2 + 1)))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (p2 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (len p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
((len P) + p2) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (P ^ p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. (len P) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P ^ p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg ((P ^ p1),(len P)) is closed Element of bool the carrier of (TOP-REAL 2)
p1 /. 1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (len P)),(p1 /. 1)) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
dom p1 is V172() V173() V174() V175() V176() V177() Element of bool NAT
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) + (len p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len (P ^ p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
(P ^ p1) /. (len P) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P ^ p1) /. ((len P) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P ^ p1) /. (len P)),((P ^ p1) /. ((len P) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LSeg ((P /. (len P)),((P ^ p1) /. ((len P) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P -: p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (P -: p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg ((P -: p1),p2) is Element of bool the carrier of (TOP-REAL 2)
LSeg (P,p2) is Element of bool the carrier of (TOP-REAL 2)
p1 .. P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P | (p1 .. P) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
rng P is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P :- p1 is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 .. P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg ((P :- p1),(p2 + 1)) is closed Element of bool the carrier of (TOP-REAL 2)
p2 + (p1 .. P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg (P,(p2 + (p1 .. P))) is closed Element of bool the carrier of (TOP-REAL 2)
len (P :- p1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(len P) - (p1 .. P) is ext-real V14() real V44() set
((len P) - (p1 .. P)) + 1 is ext-real V14() real V44() set
1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + (1 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p2 + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p2 + 1) + (p1 .. P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom (P :- p1) is non empty V172() V173() V174() V175() V176() V177() Element of bool NAT
(P :- p1) /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P :- p1) /. ((p2 + 1) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((P :- p1) /. (p2 + 1)),((P :- p1) /. ((p2 + 1) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. (p2 + (p1 .. P)) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p2 + (p1 .. P))),((P :- p1) /. ((p2 + 1) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P /. ((p2 + 1) + (p1 .. P)) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p2 + (p1 .. P))),(P /. ((p2 + 1) + (p1 .. P)))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(p2 + (p1 .. P)) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. ((p2 + (p1 .. P)) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. (p2 + (p1 .. P))),(P /. ((p2 + (p1 .. P)) + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
p2 + 2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p1 .. P) + (p2 + 1) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(p2 + (p1 .. P)) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
<*> the carrier of (TOP-REAL 2) is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like functional V32() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered real V44() V172() V173() V174() V175() V176() V177() V178() FinSequence of the carrier of (TOP-REAL 2)
L~ (<*> the carrier of (TOP-REAL 2)) is closed Element of bool the carrier of (TOP-REAL 2)
len (<*> the carrier of (TOP-REAL 2)) is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() non-empty empty-yielding functional V32() V37() V39( {} ) FinSequence-like FinSequence-membered real V44() V45() V172() V173() V174() V175() V176() V177() V178() Element of NAT
{ (LSeg ((<*> the carrier of (TOP-REAL 2)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*> the carrier of (TOP-REAL 2)) ) } is set
union { (LSeg ((<*> the carrier of (TOP-REAL 2)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*> the carrier of (TOP-REAL 2)) ) } is set
P is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
<*P*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*P*> is closed Element of bool the carrier of (TOP-REAL 2)
len <*P*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (<*P*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P*> ) } is set
union { (LSeg (<*P*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P*> ) } is set
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
f1 is set
f2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg (P,f2) is closed Element of bool the carrier of (TOP-REAL 2)
f2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg (P,p2) is closed Element of bool the carrier of (TOP-REAL 2)
P /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p2),(P /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p2),(P /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LSeg (P,p2) is closed Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (p1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p1),(P /. (p1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LSeg (P,p1) is closed Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
LSeg (P,p2) is closed Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
rng P is set
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is set
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. (p2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. p2),(P /. (p2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
f1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
f1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
f2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
f2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. (f2 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. f2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. f2),(P /. (f2 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
P /. (len P) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
<*p1*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P ^ <*p1*> is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (P ^ <*p1*>) is closed Element of bool the carrier of (TOP-REAL 2)
len (P ^ <*p1*>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((P ^ <*p1*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (P ^ <*p1*>) ) } is set
union { (LSeg ((P ^ <*p1*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (P ^ <*p1*>) ) } is set
LSeg ((P /. (len P)),p1) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(L~ P) \/ (LSeg ((P /. (len P)),p1)) is non empty Element of bool the carrier of (TOP-REAL 2)
(len P) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom (P ^ <*p1*>) is non empty V172() V173() V174() V175() V176() V177() Element of bool NAT
(P ^ <*p1*>) /. ((len P) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P ^ <*p1*>) | ((len P) + 1) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
(P ^ <*p1*>) | (len P) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(P ^ <*p1*>) /. (len P) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
P /. 1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
<*p1*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*p1*> ^ P is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (<*p1*> ^ P) is closed Element of bool the carrier of (TOP-REAL 2)
len (<*p1*> ^ P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((<*p1*> ^ P),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*p1*> ^ P) ) } is set
union { (LSeg ((<*p1*> ^ P),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*p1*> ^ P) ) } is set
LSeg (p1,(P /. 1)) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(LSeg (p1,(P /. 1))) \/ (L~ P) is non empty Element of bool the carrier of (TOP-REAL 2)
len <*p1*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
1 + (len P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
f1 is set
f2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(<*p1*> ^ P) /. P1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(<*p1*> ^ P) /. (P1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (((<*p1*> ^ P) /. P1),((<*p1*> ^ P) /. (P1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
P2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() set
P2 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
p4 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
P /. (p4 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. p4 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
f1 is set
f2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
(<*p1*> ^ P) /. (1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(<*p1*> ^ P) /. 1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
f2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
P /. P1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P /. (P1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((P /. P1),(P /. (P1 + 1))) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
dom P is V172() V173() V174() V175() V176() V177() Element of bool NAT
(<*p1*> ^ P) /. (P1 + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
(P1 + 1) + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
(<*p1*> ^ P) /. ((P1 + 1) + 1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
f2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
P is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
<*P,p1*> is non empty non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*P,p1*> is closed Element of bool the carrier of (TOP-REAL 2)
len <*P,p1*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (<*P,p1*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P,p1*> ) } is set
union { (LSeg (<*P,p1*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P,p1*> ) } is set
LSeg (P,p1) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
<*P*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len <*P*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
<*p1*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
<*P*> ^ <*p1*> is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
1 + 1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
L~ (<*P*> ^ <*p1*>) is closed Element of bool the carrier of (TOP-REAL 2)
len (<*P*> ^ <*p1*>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((<*P*> ^ <*p1*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*P*> ^ <*p1*>) ) } is set
union { (LSeg ((<*P*> ^ <*p1*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*P*> ^ <*p1*>) ) } is set
L~ <*P*> is closed Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (<*P*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P*> ) } is set
union { (LSeg (<*P*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*P*> ) } is set
<*P*> /. (len <*P*>) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg ((<*P*> /. (len <*P*>)),p1) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(L~ <*P*>) \/ (LSeg ((<*P*> /. (len <*P*>)),p1)) is non empty Element of bool the carrier of (TOP-REAL 2)
(L~ <*P*>) \/ (LSeg (P,p1)) is non empty Element of bool the carrier of (TOP-REAL 2)
{} \/ (LSeg (P,p1)) is non empty set
P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ P is closed Element of bool the carrier of (TOP-REAL 2)
len P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
union { (LSeg (P,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len P ) } is set
Rev P is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Rev P) is closed Element of bool the carrier of (TOP-REAL 2)
len (Rev P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((Rev P),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev P) ) } is set
union { (LSeg ((Rev P),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev P) ) } is set
p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ p1 is closed Element of bool the carrier of (TOP-REAL 2)
len p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (p1,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p1 ) } is set
union { (LSeg (p1,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len p1 ) } is set
Rev p1 is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Rev p1) is closed Element of bool the carrier of (TOP-REAL 2)
len (Rev p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((Rev p1),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev p1) ) } is set
union { (LSeg ((Rev p1),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev p1) ) } is set
p2 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
<*p2*> is non empty trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() V39(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 ^ <*p2*> is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p1 ^ <*p2*>) is closed Element of bool the carrier of (TOP-REAL 2)
len (p1 ^ <*p2*>) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((p1 ^ <*p2*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p1 ^ <*p2*>) ) } is set
union { (LSeg ((p1 ^ <*p2*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (p1 ^ <*p2*>) ) } is set
Rev (p1 ^ <*p2*>) is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Rev (p1 ^ <*p2*>)) is closed Element of bool the carrier of (TOP-REAL 2)
len (Rev (p1 ^ <*p2*>)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((Rev (p1 ^ <*p2*>)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev (p1 ^ <*p2*>)) ) } is set
union { (LSeg ((Rev (p1 ^ <*p2*>)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev (p1 ^ <*p2*>)) ) } is set
L~ <*p2*> is closed Element of bool the carrier of (TOP-REAL 2)
len <*p2*> is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg (<*p2*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p2*> ) } is set
union { (LSeg (<*p2*>,b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len <*p2*> ) } is set
Rev <*p2*> is V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (Rev <*p2*>) is closed Element of bool the carrier of (TOP-REAL 2)
len (Rev <*p2*>) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((Rev <*p2*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev <*p2*>) ) } is set
union { (LSeg ((Rev <*p2*>),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (Rev <*p2*>) ) } is set
(Rev p1) /. 1 is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
p1 /. (len p1) is V39(2) FinSequence-like V164() Element of the carrier of (TOP-REAL 2)
LSeg (p2,((Rev p1) /. 1)) is non empty closed compact V217( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(LSeg (p2,((Rev p1) /. 1))) \/ (L~ (Rev p1)) is non empty Element of bool the carrier of (TOP-REAL 2)
<*p2*> ^ (Rev p1) is non empty V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (<*p2*> ^ (Rev p1)) is closed Element of bool the carrier of (TOP-REAL 2)
len (<*p2*> ^ (Rev p1)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT
{ (LSeg ((<*p2*> ^ (Rev p1)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V32() V37() real V44() V45() V172() V173() V174() V175() V176() V177() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (<*p2*> ^ (Rev p1)) ) } is set
union { (LSeg ((<*p2*> ^ (Rev p1)),b1)) where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14()