:: SPPOL_2 semantic presentation

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

union { (LSeg ((<*> the carrier of (TOP-REAL 2)),b

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*>,b

union { (LSeg (<*P*>,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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

union { (LSeg (P,b

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*>),b

union { (LSeg ((P ^ <*p1*>),b

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

union { (LSeg (P,b

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

union { (LSeg ((<*p1*> ^ P),b

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*>,b

union { (LSeg (<*P,p1*>,b

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*>),b

union { (LSeg ((<*P*> ^ <*p1*>),b

L~ <*P*> is closed Element of bool the carrier of (TOP-REAL 2)

{ (LSeg (<*P*>,b

union { (LSeg (<*P*>,b

<*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,b

union { (LSeg (P,b

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

union { (LSeg ((Rev P),b

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

union { (LSeg (p1,b

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

union { (LSeg ((Rev p1),b

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*>),b

union { (LSeg ((p1 ^ <*p2*>),b

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*>)),b

union { (LSeg ((Rev (p1 ^ <*p2*>)),b

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*>,b

union { (LSeg (<*p2*>,b

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*>),b

union { (LSeg ((Rev <*p2*>),b

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

union { (LSeg ((<*p2*> ^ (Rev p1)),b