TOPREAL4

:: TOPREAL4 semantic presentation

REAL is V140() V141() V142() V146() set
NAT is V140() V141() V142() V143() V144() V145() V146() Element of K19(REAL)
K19(REAL) is set
omega is V140() V141() V142() V143() V144() V145() V146() set
K19(omega) is set
K19(NAT) is set
1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
K20(1,1) is set
K19(K20(1,1)) is set
K20(K20(1,1),1) is set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
K20(2,2) is set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
COMPLEX is V140() V146() set
RAT is V140() V141() V142() V143() V146() set
INT is V140() V141() V142() V143() V144() V146() set
K19(K20(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V106() V152() V153() V154() V155() V156() V157() V158() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K19( the carrier of (TOP-REAL 2)) is set
{} is functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set
the functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set is functional empty FinSequence-membered V140() V141() V142() V143() V144() V145() V146() set
3 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
0 is functional empty ext-real non positive non negative ordinal natural V25() real FinSequence-membered V92() V93() V140() V141() V142() V143() V144() V145() V146() Element of NAT
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
p is TopStruct
the carrier of p is set
K19( the carrier of p) is set
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
union { (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
union { (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ RR is Element of K19( the carrier of (TOP-REAL 2))
len RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
union { (LSeg (RR,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len RR ) } is set
RR /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR /. (len RR) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len RR) is V33() V40( len RR) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom RR is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is Element of K19( the carrier of (TOP-REAL 2))
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
RR is Element of K19( the carrier of (TOP-REAL 2))
RR /\ RR is Element of K19( the carrier of (TOP-REAL 2))
{q,R} is non empty set
RR \/ RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is non empty Element of K19( the carrier of (TOP-REAL 2))
P12 is non empty Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `2) + (q `2) is ext-real V25() real Element of REAL
((p `2) + (q `2)) / 2 is ext-real V25() real Element of REAL
|[(p `1),(((p `2) + (q `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) \/ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `1) + (q `1) is ext-real V25() real Element of REAL
((p `1) + (q `1)) / 2 is ext-real V25() real Element of REAL
|[(((p `1) + (q `1)) / 2),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) \/ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[(p `1),(q `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (p,|[(p `1),(q `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
RR is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,RR) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
LSeg (|[(q `1),(p `2)]|,q) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (p,|[(q `1),(p `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R is ext-real V25() real Element of REAL
RR is Element of the carrier of (Euclid 2)
Ball (RR,R) is Element of K19( the carrier of (Euclid 2))
K19( the carrier of (Euclid 2)) is set
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
(p `1) + (q `1) is ext-real V25() real Element of REAL
((p `1) + (q `1)) / 2 is ext-real V25() real Element of REAL
|[(((p `1) + (q `1)) / 2),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(q `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(q `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(q `1),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(q `1),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
(p `2) + (q `2) is ext-real V25() real Element of REAL
((p `2) + (q `2)) / 2 is ext-real V25() real Element of REAL
|[(p `1),(((p `2) + (q `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(p `1),(q `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(p `1),(q `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(p `1),(q `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(p `1),(q `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(p `1),(q `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p,|[(q `1),(p `2)]|,q*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ <*p,|[(q `1),(p `2)]|,q*> is Element of K19( the carrier of (TOP-REAL 2))
len <*p,|[(q `1),(p `2)]|,q*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
union { (LSeg (<*p,|[(q `1),(p `2)]|,q*>,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len <*p,|[(q `1),(p `2)]|,q*> ) } is set
RR is Element of K19( the carrier of (TOP-REAL 2))
P11 is Element of K19( the carrier of (TOP-REAL 2))
|[(p `1),(q `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
|[(q `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
RR is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p `1 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
RR is Element of K19( the carrier of (TOP-REAL 2))
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `2 is ext-real V25() real Element of REAL
p `1 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. 1) `2 is ext-real V25() real Element of REAL
LSeg (q,1) is Element of K19( the carrier of (TOP-REAL 2))
(q /. 1) `1 is ext-real V25() real Element of REAL
((q /. 1) `1) + (p `1) is ext-real V25() real Element of REAL
(((q /. 1) `1) + (p `1)) / 2 is ext-real V25() real Element of REAL
|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
union { (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
q | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (q | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | 1) ) } is set
union { (LSeg ((q | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | 1) ) } is set
LSeg ((q /. 1),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | 1)) \/ (LSeg ((q /. 1),p)) is Element of K19( the carrier of (TOP-REAL 2))
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (1 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. 1),|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|)) \/ (LSeg (|[((((q /. 1) `1) + (p `1)) / 2),((q /. 1) `2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q /. 1),(q /. (1 + 1))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom q) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (q | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p `1 is ext-real V25() real Element of REAL
p `2 is ext-real V25() real Element of REAL
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. 1) `1 is ext-real V25() real Element of REAL
LSeg (q,1) is Element of K19( the carrier of (TOP-REAL 2))
(q /. 1) `2 is ext-real V25() real Element of REAL
((q /. 1) `2) + (p `2) is ext-real V25() real Element of REAL
(((q /. 1) `2) + (p `2)) / 2 is ext-real V25() real Element of REAL
|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
union { (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
q | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (q | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | 1) ) } is set
union { (LSeg ((q | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | 1) ) } is set
LSeg ((q /. 1),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | 1)) \/ (LSeg ((q /. 1),p)) is Element of K19( the carrier of (TOP-REAL 2))
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
LSeg ((q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((q /. 1),|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|)) \/ (LSeg (|[((q /. 1) `1),((((q /. 1) `2) + (p `2)) / 2)]|,p)) is Element of K19( the carrier of (TOP-REAL 2))
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (1 + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg ((q /. 1),(q /. (1 + 1))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom q) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (q | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
<*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom q is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
union { (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
R is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
R /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len R is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. (len R) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ R is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
union { (LSeg (R,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len R ) } is set
RR is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,RR) is Element of K19( the carrier of (TOP-REAL 2))
q /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q | RR is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(q | RR) ^ <*p*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (q | RR) is Element of K19( the carrier of (TOP-REAL 2))
len (q | RR) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((q | RR),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | RR) ) } is set
union { (LSeg ((q | RR),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (q | RR) ) } is set
LSeg ((q /. RR),p) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (q | RR)) \/ (LSeg ((q /. RR),p)) is Element of K19( the carrier of (TOP-REAL 2))
Seg RR is V33() V40(RR) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q | (Seg RR) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
dom (q | RR) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
(dom q) /\ (Seg RR) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
Seg (len R) is V33() V40( len R) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom R is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q /. (RR + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len q) is V33() V40( len q) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
LSeg ((q /. RR),(q /. (RR + 1))) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q /. (RR + 1)),(q /. RR)) is Element of K19( the carrier of (TOP-REAL 2))
(q /. RR) `1 is ext-real V25() real Element of REAL
(q /. RR) `2 is ext-real V25() real Element of REAL
|[((q /. RR) `1),((q /. RR) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
(q /. (RR + 1)) `1 is ext-real V25() real Element of REAL
(q /. (RR + 1)) `2 is ext-real V25() real Element of REAL
|[((q /. (RR + 1)) `1),((q /. (RR + 1)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
len <*p*> is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + (len <*p*>) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. RR is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (R,RR) is Element of K19( the carrier of (TOP-REAL 2))
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ b₁ where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ <= len R ) } is set
r9 is set
x is set
R . r9 is set
R . x is set
q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
R /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(P2 + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q | RR) /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,P2)) /\ (LSeg (q,RR)) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. RR)} is non empty set
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
(q | RR) /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. P2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
LSeg (q,q) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,q)) /\ (LSeg (q,RR)) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. RR)} is non empty set
LSeg (q,q) is Element of K19( the carrier of (TOP-REAL 2))
(q | RR) /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q . q is set
(q | RR) . q is set
R . q is set
(q | RR) . P2 is set
q . P2 is set
r is ext-real non negative ordinal natural V25() real set
r + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
{(R /. (r + 1))} is non empty set
(r + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
r + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(q | RR) /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(RR + 1) + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + (1 + 1) is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
RR + 2 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r)) /\ (LSeg (q,(r + 1))) is Element of K19( the carrier of (TOP-REAL 2))
{(q /. (r + 1))} is non empty set
LSeg ((q | RR),(r + 1)) is Element of K19( the carrier of (TOP-REAL 2))
r9 is ext-real non negative ordinal natural V25() real set
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (R,r9) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,r9) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r9) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (q,r)) /\ (LSeg (q,r9)) is Element of K19( the carrier of (TOP-REAL 2))
0 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),r) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (q,r9)) /\ (LSeg (R,r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r9)) /\ ((LSeg (q,r9)) /\ (LSeg (R,r))) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r9)) /\ (LSeg (q,r9)) is Element of K19( the carrier of (TOP-REAL 2))
((LSeg (R,r9)) /\ (LSeg (q,r9))) /\ (LSeg (R,r)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg (R,r)) /\ (LSeg (R,r9)) is Element of K19( the carrier of (TOP-REAL 2))
r is ext-real non negative ordinal natural V25() real set
r + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
R /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. r) `1 is ext-real V25() real Element of REAL
R /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(R /. (r + 1)) `1 is ext-real V25() real Element of REAL
(R /. r) `2 is ext-real V25() real Element of REAL
(R /. (r + 1)) `2 is ext-real V25() real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (q /. RR) `1 & (q /. RR) `2 <= b₁ `2 & b₁ `2 <= (q /. (RR + 1)) `2 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (q /. RR) `1 & (q /. (RR + 1)) `2 <= b₁ `2 & b₁ `2 <= (q /. RR) `2 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `1 is ext-real V25() real Element of REAL
q `2 is ext-real V25() real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = (q /. RR) `2 & (q /. RR) `1 <= b₁ `1 & b₁ `1 <= (q /. (RR + 1)) `1 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `2 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = (q /. RR) `2 & (q /. (RR + 1)) `1 <= b₁ `1 & b₁ `1 <= (q /. RR) `1 ) } is set
q is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q `2 is ext-real V25() real Element of REAL
q `1 is ext-real V25() real Element of REAL
(q | RR) /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. (r + 1) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
q /. r is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(q | RR) /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
Seg (len (q | RR)) is V33() V40( len (q | RR)) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
q is set
P2 is set
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,P2) is Element of K19( the carrier of (TOP-REAL 2))
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
LSeg ((q | RR),P2) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (q,P2) is Element of K19( the carrier of (TOP-REAL 2))
q is set
q is set
q is set
P2 is set
P2 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((q | RR),P2) is Element of K19( the carrier of (TOP-REAL 2))
P2 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (R,P2) is Element of K19( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(p /. 2) `2 is ext-real V25() real Element of REAL
(p /. 1) `2 is ext-real V25() real Element of REAL
(p /. 1) `1 is ext-real V25() real Element of REAL
(p /. 2) `1 is ext-real V25() real Element of REAL
((p /. 1) `1) + ((p /. 2) `1) is ext-real V25() real Element of REAL
(((p /. 1) `1) + ((p /. 2) `1)) / 2 is ext-real V25() real Element of REAL
|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ p is Element of K19( the carrier of (TOP-REAL 2))
len p is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (p,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
union { (LSeg (p,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
p | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 1) ) } is set
union { (LSeg ((p | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 1) ) } is set
LSeg ((p /. 1),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 1)) \/ (LSeg ((p /. 1),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
p | 2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 2) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 2) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 2),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 2) ) } is set
union { (LSeg ((p | 2),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 2) ) } is set
LSeg ((p /. 2),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 2)) \/ (LSeg ((p /. 2),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
len q is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
q /. (len q) is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
L~ q is Element of K19( the carrier of (TOP-REAL 2))
{ (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
union { (LSeg (q,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len q ) } is set
LSeg ((p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|) is Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(LSeg ((p /. 1),|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|)) \/ (LSeg (|[((((p /. 1) `1) + ((p /. 2) `1)) / 2),((p /. 1) `2)]|,(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
Seg (len p) is V33() V40( len p) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom p is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
1 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg (p,1) is Element of K19( the carrier of (TOP-REAL 2))
Seg 2 is non empty V33() V40(2) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 2) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
K20(NAT, the carrier of (TOP-REAL 2)) is set
K19(K20(NAT, the carrier of (TOP-REAL 2))) is set
(dom p) /\ (Seg 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 2) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
P11 is set
P12 is set
R9 is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
LSeg ((p | 2),R9) is Element of K19( the carrier of (TOP-REAL 2))
R9 + 1 is non empty ext-real positive non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
(len (p | 2)) - 1 is ext-real V25() real Element of REAL
(1 + 1) - 1 is ext-real V25() real Element of REAL
(R9 + 1) - 1 is ext-real V25() real Element of REAL
{(p /. 2)} is non empty set
Seg 1 is non empty V33() V40(1) V140() V141() V142() V143() V144() V145() Element of K19(NAT)
p | (Seg 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of (TOP-REAL 2)))
(dom p) /\ (Seg 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
dom (p | 1) is V140() V141() V142() V143() V144() V145() Element of K19(NAT)
LSeg ((p | 2),1) is Element of K19( the carrier of (TOP-REAL 2))
p is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p /. 2 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
p /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (TOP-REAL 2)
(p /. 2) `1 is ext-real V25() real Element of REAL
(p /. 1) `1 is ext-real V25() real Element of REAL
(p /. 1) `2 is ext-real V25() real Element of REAL
(p /. 2) `2 is ext-real V25() real Element of REAL
((p /. 1) `2) + ((p /. 2) `2) is ext-real V25() real Element of REAL
(((p /. 1) `2) + ((p /. 2) `2)) / 2 is ext-real V25() real Element of REAL
|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]| is Relation-like NAT -defined Function-like non empty V33() V40(2) FinSequence-like FinSubsequence-like V132() Element of the carrier of (TOP-REAL 2)
<*(p /. 1),|[((p /. 1) `1),((((p /. 1) `2) + ((p /. 2) `2)) / 2)]|,(p /. 2)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V33() V40(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ p is Element of K19( the carrier of (TOP-REAL 2))
len p is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg (p,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
union { (LSeg (p,b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len p ) } is set
p | 1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 1) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 1) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 1) ) } is set
union { (LSeg ((p | 1),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 1) ) } is set
LSeg ((p /. 1),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 1)) \/ (LSeg ((p /. 1),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
p | 2 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (p | 2) is Element of K19( the carrier of (TOP-REAL 2))
len (p | 2) is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT
{ (LSeg ((p | 2),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 2) ) } is set
union { (LSeg ((p | 2),b₁)) where b₁ is ext-real non negative ordinal natural V25() real V92() V93() V140() V141() V142() V143() V144() V145() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (p | 2) ) } is set
LSeg ((p /. 2),(p /. 2)) is Element of K19( the carrier of (TOP-REAL 2))
(L~ (p | 2)) \/ (LSeg ((p /. 2),(p /. 2))) is Element of K19( the carrier of (TOP-REAL 2))
q is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
q /. 1 is V40(2) FinSequence-like V132() Element of the carrier of (