:: JORDAN7 semantic presentation

REAL is V169() V170() V171() V175() V208() V209() V211() set
NAT is V169() V170() V171() V172() V173() V174() V175() V208() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V169() V175() set
NAT is V169() V170() V171() V172() V173() V174() V175() V208() set
K6(NAT) is set
1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
INT is V169() V170() V171() V172() V173() V175() set
K7(1,1) is V25( RAT ) V25( INT ) V159() V160() V161() V162() set
RAT is V169() V170() V171() V172() V175() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V25( RAT ) V25( INT ) V159() V160() V161() V162() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V159() V160() V161() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V159() V160() V161() set
K7(K7(REAL,REAL),REAL) is V159() V160() V161() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
K7(2,2) is V25( RAT ) V25( INT ) V159() V160() V161() V162() set
K7(K7(2,2),REAL) is V159() V160() V161() set
K6(K7(K7(2,2),REAL)) is set
K288() is T_0 T_1 T_2 compact TopStruct
the carrier of K288() is set
K205() is V81() L7()
K293() is TopSpace-like TopStruct
K6(NAT) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V135() V181() V182() V183() V184() V185() V186() V187() V193() L15()
the carrier of (TOP-REAL 2) is non empty functional set
K6( the carrier of (TOP-REAL 2)) is set
K7( the carrier of (TOP-REAL 2),REAL) is V159() V160() V161() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
{} is empty Function-like functional FinSequence-membered V169() V170() V171() V172() V173() V174() V175() V208() V211() set
the empty Function-like functional FinSequence-membered V169() V170() V171() V172() V173() V174() V175() V208() V211() set is empty Function-like functional FinSequence-membered V169() V170() V171() V172() V173() V174() V175() V208() V211() set
3 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
I[01] is TopSpace-like T_0 T_1 T_2 compact SubSpace of K293()
the carrier of I[01] is set
0 is empty V10() V11() V12() ext-real non positive non negative V19() Function-like functional FinSequence-membered V122() V169() V170() V171() V172() V173() V174() V175() V208() V211() Element of NAT
5 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
K6( the carrier of I[01]) is set
[.0,1.] is V169() V170() V171() V211() Element of K6(REAL)
2 -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
2 - 1 is V11() V12() ext-real Element of REAL
P is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
g1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
P -' g1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
e is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
e + g1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(P -' g1) + g1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
e is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
g1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
e + g1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
P is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
P -' e is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Lower_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) \/ (Lower_Arc P) is non empty functional Element of K6( the carrier of (TOP-REAL 2))
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P or ( e in P & b₁ = W-min P ) ) } is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : S₁[b₁] } is set
h1 is functional Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : S₁[b₁] } is set
h1 is functional Element of K6( the carrier of (TOP-REAL 2))
h11 is functional Element of K6( the carrier of (TOP-REAL 2))
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(W-min P),(E-max P)) is functional Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(P,(E-max P),(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE E-max P,b₁,P or ( E-max P in P & b₁ = W-min P ) ) } is set
e is set
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{(W-min P),(E-max P)} is non empty functional set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
e is set
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE W-min P,b₁,P & LE b₁, E-max P,P ) } is set
e is set
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is set
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) \/ (Lower_Arc P) is non empty functional Element of K6( the carrier of (TOP-REAL 2))
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P or ( e in P & b₁ = W-min P ) ) } is set
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P or ( e in P & b₁ = W-min P ) ) } is set
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P or ( e in P & b₁ = W-min P ) ) } is set
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,e) is functional Element of K6( the carrier of (TOP-REAL 2))
{e} is non empty functional set
g1 is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,e,P ) } is set
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,g1,h1) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,e,g1) /\ (P,g1,h1) is functional Element of K6( the carrier of (TOP-REAL 2))
{g1} is non empty functional set
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
h11 is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE g1,b₁,P & LE b₁,h1,P ) } is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
g2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE g1,b₁,P or ( g1 in P & b₁ = W-min P ) ) } is set
g2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 is set
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,g1,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,e,g1) /\ (P,g1,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
{g1} is non empty functional set
h11 is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE g1,b₁,P or ( g1 in P & b₁ = W-min P ) ) } is set
g2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 is set
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{(W-min P)} is non empty functional set
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,g1,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,(W-min P),e) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,g1,(W-min P)) /\ (P,(W-min P),e) is functional Element of K6( the carrier of (TOP-REAL 2))
h1 is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE g1,b₁,P or ( g1 in P & b₁ = W-min P ) ) } is set
h11 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE W-min P,b₁,P & LE b₁,e,P ) } is set
g2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE g1,b₁,P or ( g1 in P & b₁ = W-min P ) ) } is set
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,h1,h11) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,e,g1) /\ (P,h1,h11) is functional Element of K6( the carrier of (TOP-REAL 2))
the V21() Function-like Element of (P,e,g1) /\ (P,h1,h11) is V21() Function-like Element of (P,e,g1) /\ (P,h1,h11)
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h1,b₁,P & LE b₁,h11,P ) } is set
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h21 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,e,g1) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,h1,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,e,g1) /\ (P,h1,(W-min P)) is functional Element of K6( the carrier of (TOP-REAL 2))
the V21() Function-like Element of (P,e,g1) /\ (P,h1,(W-min P)) is V21() Function-like Element of (P,e,g1) /\ (P,h1,(W-min P))
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h1,b₁,P or ( h1 in P & b₁ = W-min P ) ) } is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE e,b₁,P & LE b₁,g1,P ) } is set
g2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
P is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
TOP-REAL P is non empty TopSpace-like T_0 T_1 T_2 V135() V181() V182() V183() V184() V185() V186() V187() V193() L15()
the carrier of (TOP-REAL P) is non empty functional set
K6( the carrier of (TOP-REAL P)) is set
K7( the carrier of I[01], the carrier of (TOP-REAL P)) is set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL P))) is set
e is non empty functional Element of K6( the carrier of (TOP-REAL P))
(TOP-REAL P) | e is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL P
the carrier of ((TOP-REAL P) | e) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e))) is set
g1 is V21() V24( the carrier of I[01]) V25( the carrier of ((TOP-REAL P) | e)) Function-like V35( the carrier of I[01], the carrier of ((TOP-REAL P) | e)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e)))
[#] ((TOP-REAL P) | e) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL P) | e))
K6( the carrier of ((TOP-REAL P) | e)) is set
h1 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL P)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL P)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL P)))
h11 is functional Element of K6( the carrier of (TOP-REAL P))
h1 " h11 is Element of K6( the carrier of I[01])
h11 /\ e is functional Element of K6( the carrier of (TOP-REAL P))
rng g1 is Element of K6( the carrier of ((TOP-REAL P) | e))
g1 " (rng g1) is Element of K6( the carrier of I[01])
g1 " e is Element of K6( the carrier of I[01])
dom g1 is Element of K6( the carrier of I[01])
g2 is Element of K6( the carrier of ((TOP-REAL P) | e))
g1 " g2 is Element of K6( the carrier of I[01])
g1 " h11 is Element of K6( the carrier of I[01])
(g1 " h11) /\ (g1 " e) is Element of K6( the carrier of I[01])
[#] (TOP-REAL P) is non empty non proper functional closed Element of K6( the carrier of (TOP-REAL P))
P is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
TOP-REAL P is non empty TopSpace-like T_0 T_1 T_2 V135() V181() V182() V183() V184() V185() V186() V187() V193() L15()
the carrier of (TOP-REAL P) is non empty functional set
K6( the carrier of (TOP-REAL P)) is set
K7( the carrier of I[01], the carrier of (TOP-REAL P)) is set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL P))) is set
e is non empty functional Element of K6( the carrier of (TOP-REAL P))
(TOP-REAL P) | e is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL P
the carrier of ((TOP-REAL P) | e) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e))) is set
g1 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL P)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL P)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL P)))
rng g1 is functional Element of K6( the carrier of (TOP-REAL P))
[#] ((TOP-REAL P) | e) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL P) | e))
K6( the carrier of ((TOP-REAL P) | e)) is set
h1 is V21() V24( the carrier of I[01]) V25( the carrier of ((TOP-REAL P) | e)) Function-like V35( the carrier of I[01], the carrier of ((TOP-REAL P) | e)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL P) | e)))
dom h1 is Element of K6( the carrier of I[01])
[#] I[01] is non proper closed Element of K6( the carrier of I[01])
[#] (TOP-REAL P) is non empty non proper functional closed Element of K6( the carrier of (TOP-REAL P))
h11 is Element of K6( the carrier of ((TOP-REAL P) | e))
h1 " h11 is Element of K6( the carrier of I[01])
g2 is functional Element of K6( the carrier of (TOP-REAL P))
g2 /\ ([#] ((TOP-REAL P) | e)) is Element of K6( the carrier of ((TOP-REAL P) | e))
g1 " e is Element of K6( the carrier of I[01])
h1 " g2 is Element of K6( the carrier of I[01])
(h1 " g2) /\ ([#] I[01]) is Element of K6( the carrier of I[01])
rng h1 is Element of K6( the carrier of ((TOP-REAL P) | e))
P is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
P + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(P + 1) - 1 is V11() V12() ext-real Element of REAL
P - 1 is V11() V12() ext-real Element of REAL
(P - 1) - 1 is V11() V12() ext-real Element of REAL
K7( the carrier of I[01], the carrier of (TOP-REAL 2)) is set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2))) is set
P is functional Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is non empty functional Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | h1 is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | h1) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h1)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h1))) is set
h11 is V21() V24( the carrier of I[01]) V25( the carrier of ((TOP-REAL 2) | h1)) Function-like V35( the carrier of I[01], the carrier of ((TOP-REAL 2) | h1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | h1)))
h11 . 0 is set
h11 . 1 is set
g2 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL 2)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng g2 is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . 0 is V21() Function-like set
g2 . 1 is V21() Function-like set
rng h11 is Element of K6( the carrier of ((TOP-REAL 2) | h1))
K6( the carrier of ((TOP-REAL 2) | h1)) is set
[#] ((TOP-REAL 2) | h1) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | h1))
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g2 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL 2)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng g2 is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . 0 is V21() Function-like set
g2 . 1 is V21() Function-like set
h2 is V11() V12() ext-real Element of REAL
g2 . h2 is V21() Function-like set
h21 is V11() V12() ext-real Element of REAL
g2 . h21 is V21() Function-like set
(TOP-REAL 2) | P is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
h0 is V21() V24( the carrier of I[01]) V25( the carrier of ((TOP-REAL 2) | P)) Function-like V35( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
e is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
g2 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL 2)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng g2 is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . 0 is V21() Function-like set
g2 . 1 is V21() Function-like set
h2 is V11() V12() ext-real Element of REAL
g2 . h2 is V21() Function-like set
h21 is V11() V12() ext-real Element of REAL
g2 . h21 is V21() Function-like set
(TOP-REAL 2) | P is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
h0 is V21() V24( the carrier of I[01]) V25( the carrier of ((TOP-REAL 2) | P)) Function-like V35( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
8 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
Euclid 2 is non empty V81() V86() V87() V88() V89() L7()
the carrier of (Euclid 2) is non empty set
K6( the carrier of (Euclid 2)) is set
P is non empty functional closed compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
e is V11() V12() ext-real Element of REAL
E-max P is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Upper_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
g1 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL 2)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng g1 is functional Element of K6( the carrier of (TOP-REAL 2))
g1 . 0 is V21() Function-like set
g1 . 1 is V21() Function-like set
h1 is V21() V24( NAT ) V25( REAL ) Function-like V38() FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
h1 . 1 is V11() V12() ext-real Element of REAL
len h1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h1 . (len h1) is V11() V12() ext-real Element of REAL
rng h1 is V169() V170() V171() Element of K6(REAL)
g1 * h1 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL 2)))
K7(NAT, the carrier of (TOP-REAL 2)) is set
K6(K7(NAT, the carrier of (TOP-REAL 2))) is set
dom h1 is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
1 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h1 . (1 + 1) is V11() V12() ext-real Element of REAL
h11 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Lower_Arc P is non empty functional Element of K6( the carrier of (TOP-REAL 2))
g2 is V21() V24( the carrier of I[01]) V25( the carrier of (TOP-REAL 2)) Function-like V35( the carrier of I[01], the carrier of (TOP-REAL 2)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL 2)))
rng g2 is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . 0 is V21() Function-like set
g2 . 1 is V21() Function-like set
h2 is V21() V24( NAT ) V25( REAL ) Function-like V38() FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
h2 . 1 is V11() V12() ext-real Element of REAL
len h2 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h2 . (len h2) is V11() V12() ext-real Element of REAL
rng h2 is V169() V170() V171() Element of K6(REAL)
g2 * h2 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like Element of K6(K7(NAT, the carrier of (TOP-REAL 2)))
h21 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom h2 is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
h21 . (len h2) is V21() Function-like set
len h21 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h21) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
mid (h21,2,((len h21) -' 1)) is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h11 ^ (mid (h21,2,((len h21) -' 1))) is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
h0 is V21() V24( NAT ) V25( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len h0 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
len h11 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
len (mid (h21,2,((len h21) -' 1))) is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) + (len (mid (h21,2,((len h21) -' 1)))) is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h0) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . 1 is V21() Function-like set
rng h0 is functional Element of K6( the carrier of (TOP-REAL 2))
h0 /. (len h0) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 /. 1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. (len h0)),(h0 /. 1)) is functional Element of K6( the carrier of (TOP-REAL 2))
h0 /. 2 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. 1),(h0 /. 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,(h0 /. (len h0)),(h0 /. 1)) /\ (P,(h0 /. 1),(h0 /. 2)) is functional Element of K6( the carrier of (TOP-REAL 2))
{(h0 /. 1)} is non empty functional set
h0 /. ((len h0) -' 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. ((len h0) -' 1)),(h0 /. (len h0))) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,(h0 /. ((len h0) -' 1)),(h0 /. (len h0))) /\ (P,(h0 /. (len h0)),(h0 /. 1)) is functional Element of K6( the carrier of (TOP-REAL 2))
{(h0 /. (len h0))} is non empty functional set
dom g1 is Element of K6( the carrier of I[01])
dom h11 is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
h0 . 2 is V21() Function-like set
h11 . 2 is V21() Function-like set
h0 . (1 + 1) is V21() Function-like set
h11 . (1 + 1) is V21() Function-like set
g1 . (h1 . (1 + 1)) is V21() Function-like set
(len h0) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h0) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h0) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
0 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
dom g2 is Element of K6( the carrier of I[01])
dom h21 is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
(len h21) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h21) - 1 is V11() V12() ext-real Element of REAL
((len h21) + 1) - 1 is V11() V12() ext-real Element of REAL
(1 + 1) - 1 is V11() V12() ext-real Element of REAL
2 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(2 + 1) - 1 is V11() V12() ext-real Element of REAL
((len h21) -' 1) -' 2 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h21) -' 1) - 2 is V11() V12() ext-real Element of REAL
(((len h21) -' 1) -' 2) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
3 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(3 + 2) - 2 is V11() V12() ext-real Element of REAL
(len h2) - 2 is V11() V12() ext-real Element of REAL
5 + 3 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(len h1) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
(1 + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(len h1) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
dom h0 is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
dom (g1 * h1) is V169() V170() V171() V172() V173() V174() V208() Element of K6(NAT)
h11 . 1 is V21() Function-like set
h0 . (len h0) is V21() Function-like set
h21 . 1 is V21() Function-like set
i is set
K128(h0) is set
j0 is set
h0 . i is V21() Function-like set
h0 . j0 is V21() Function-like set
k is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
k is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h1 . k is V11() V12() ext-real Element of REAL
h0 . k is V21() Function-like set
h11 . k is V21() Function-like set
g1 . (h1 . k) is V21() Function-like set
h1 . k is V11() V12() ext-real Element of REAL
h0 . k is V21() Function-like set
h11 . k is V21() Function-like set
g1 . (h1 . k) is V21() Function-like set
k -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(k -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
k - (len h1) is V11() V12() ext-real Element of REAL
(k -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((k -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
k - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((k -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(len h2) - 1 is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . k is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (k - (len h11)) is V21() Function-like set
h21 . (((k -' (len h11)) + 2) -' 1) is V21() Function-like set
rng h21 is functional Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
((len h21) - 1) + 1 is V11() V12() ext-real Element of REAL
((len h21) + 1) - (len h21) is V11() V12() ext-real Element of REAL
(len h21) - (len h21) is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
k - (len h1) is V11() V12() ext-real Element of REAL
k -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(k -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((k -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
k - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(k -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((k -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(len h2) - 1 is V11() V12() ext-real Element of REAL
((k -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . k is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (k - (len h11)) is V21() Function-like set
h21 . (((k -' (len h11)) + 2) -' 1) is V21() Function-like set
rng h21 is functional Element of K6( the carrier of (TOP-REAL 2))
h1 . k is V11() V12() ext-real Element of REAL
h0 . k is V21() Function-like set
h11 . k is V21() Function-like set
g1 . (h1 . k) is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
((len h21) - 1) + 1 is V11() V12() ext-real Element of REAL
((len h21) + 1) - (len h21) is V11() V12() ext-real Element of REAL
(len h21) - (len h21) is V11() V12() ext-real Element of REAL
k - (len h11) is V11() V12() ext-real Element of REAL
k -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . k is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (k - (len h11)) is V21() Function-like set
k - (len h1) is V11() V12() ext-real Element of REAL
(k -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . (((k -' (len h11)) + 2) -' 1) is V21() Function-like set
k -' (len h1) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(k -' (len h1)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h1)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
k -' (len h1) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(k -' (len h1)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((k -' (len h1)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((k -' (len h1)) + 2) - 1 is V11() V12() ext-real Element of REAL
(k -' (len h1)) + (2 - 1) is V11() V12() ext-real Element of REAL
((k -' (len h1)) + 2) - 1 is V11() V12() ext-real Element of REAL
(len h1) + k is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + k) - (len h1) is V11() V12() ext-real Element of REAL
(len h1) + (k - (len h1)) is V11() V12() ext-real Element of REAL
rng (mid (h21,2,((len h21) -' 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
rng h21 is functional Element of K6( the carrier of (TOP-REAL 2))
rng (g2 * h2) is functional Element of K6( the carrier of (TOP-REAL 2))
rng (g1 * h1) is functional Element of K6( the carrier of (TOP-REAL 2))
rng h11 is functional Element of K6( the carrier of (TOP-REAL 2))
(rng h11) \/ (rng (mid (h21,2,((len h21) -' 1)))) is functional Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) \/ (Lower_Arc P) is non empty functional Element of K6( the carrier of (TOP-REAL 2))
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
h0 . i is V21() Function-like set
h1 . i is V11() V12() ext-real Element of REAL
g1 . (h1 . i) is V21() Function-like set
h11 . i is V21() Function-like set
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . i is V21() Function-like set
i - (len h11) is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . (i - (len h11)) is V21() Function-like set
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
i - (len h1) is V11() V12() ext-real Element of REAL
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h2) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h2) + 1) - 1 is V11() V12() ext-real Element of REAL
(len h2) - 1 is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
h21 . (((i -' (len h11)) + 2) -' 1) is V21() Function-like set
h2 . (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) is V21() Function-like set
(i -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((((i -' (len h11)) + 1) + 1) - 1) + 1 is V11() V12() ext-real Element of REAL
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
(i - (len h11)) + 2 is V11() V12() ext-real Element of REAL
((i - (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i - (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
((len h21) + 1) - (len h21) is V11() V12() ext-real Element of REAL
(len h21) - (len h21) is V11() V12() ext-real Element of REAL
h0 . i is V21() Function-like set
h11 . i is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) - (len h11) is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
((len h0) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h0 . ((len h0) -' 1) is V21() Function-like set
h0 /. (1 + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h11 . ((len h0) -' 1) is V21() Function-like set
((len h0) -' 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h0) -' 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(((len h0) -' 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((((len h0) -' 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((((len h0) -' 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (((len h0) -' 1) - (len h11)) is V21() Function-like set
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
((len h0) -' 1) - (len h1) is V11() V12() ext-real Element of REAL
h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) - 1 is V11() V12() ext-real Element of REAL
(((((len h0) -' 1) -' (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
(len h2) - 1 is V11() V12() ext-real Element of REAL
((len h2) - 1) - 1 is V11() V12() ext-real Element of REAL
h1 . ((len h0) -' 1) is V11() V12() ext-real Element of REAL
h11 . ((len h0) -' 1) is V21() Function-like set
g1 . (h1 . ((len h0) -' 1)) is V21() Function-like set
((len h0) -' 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h0) -' 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(((len h0) -' 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - 1 is V11() V12() ext-real Element of REAL
((len h2) - 2) - 1 is V11() V12() ext-real Element of REAL
(len h1) + (((len h2) - 2) - 1) is V11() V12() ext-real Element of REAL
((len h1) + (((len h2) - 2) - 1)) - (len h11) is V11() V12() ext-real Element of REAL
(((len h0) -' 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h2) - 2) - 1) + 2 is V11() V12() ext-real Element of REAL
((((len h0) -' 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
((len h0) -' 1) - (len h1) is V11() V12() ext-real Element of REAL
((((len h0) -' 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
0 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h0) -' 1) -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((((len h0) -' 1) -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((((len h0) -' 1) -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . (((len h0) -' 1) - (len h11)) is V21() Function-like set
h21 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((((len h0) -' 1) -' (len h11)) + 2) -' 1)) is V21() Function-like set
(len h0) - (len h11) is V11() V12() ext-real Element of REAL
h21 . ((((len h0) -' (len h11)) + 2) -' 1) is V21() Function-like set
h2 . ((((len h0) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((len h0) -' (len h11)) + 2) -' 1)) is V21() Function-like set
h11 . (len h1) is V21() Function-like set
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 . (i + 1) is V21() Function-like set
h0 . i is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h1 . i is V11() V12() ext-real Element of REAL
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
h11 . i is V21() Function-like set
g1 . (h1 . i) is V21() Function-like set
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
i - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(i - (len h11)) + 2 is V11() V12() ext-real Element of REAL
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + (1 + 1)) - 1 is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + (1 + 1)) - 1) + 1 is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
i - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(mid (h21,2,((len h21) -' 1))) . (i - (len h11)) is V21() Function-like set
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
h2 . (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
h21 . (((i -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) is V21() Function-like set
((i - (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i - (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
i - (len h11) is V11() V12() ext-real Element of REAL
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + (1 + 1)) - 1 is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + (1 + 1)) - 1) + 1 is V11() V12() ext-real Element of REAL
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
(len h1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) - (len h11) is V11() V12() ext-real Element of REAL
(0 + 2) - 1 is V11() V12() ext-real Element of REAL
((len h1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 . (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) is V21() Function-like set
h21 . (((i -' (len h11)) + 2) -' 1) is V21() Function-like set
(i - (len h11)) + 2 is V11() V12() ext-real Element of REAL
((i - (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i - (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. i),(h0 /. (i + 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
j0 is Element of K6( the carrier of (Euclid 2))
diameter j0 is V11() V12() ext-real Element of REAL
h1 . i is V11() V12() ext-real Element of REAL
h1 /. i is V11() V12() ext-real Element of REAL
h11 . i is V21() Function-like set
g1 . (h1 . i) is V21() Function-like set
h0 . i is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h1 /. (i + 1) is V11() V12() ext-real Element of REAL
[.(h1 /. i),(h1 /. (i + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
g1 .: [.(h1 /. i),(h1 /. (i + 1)).] is functional Element of K6( the carrier of (TOP-REAL 2))
k is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
x is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
y is set
g1 . y is V21() Function-like set
sy is V11() V12() ext-real Element of REAL
p1 is set
g1 . (h1 /. i) is V21() Function-like set
g1 . (h1 /. (i + 1)) is V21() Function-like set
g1 . p1 is V21() Function-like set
y is set
g1 . y is V21() Function-like set
h1 /. 1 is V11() V12() ext-real Element of REAL
sy is V11() V12() ext-real Element of REAL
h1 /. (1 + 1) is V11() V12() ext-real Element of REAL
g1 . (h1 /. (1 + 1)) is V21() Function-like set
p1 is V11() V12() ext-real Element of REAL
[.(h1 /. 1),(h1 /. (1 + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
g1 . p1 is V21() Function-like set
h1 /. 1 is V11() V12() ext-real Element of REAL
h1 /. (1 + 1) is V11() V12() ext-real Element of REAL
[.(h1 /. 1),(h1 /. (1 + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
h1 /. 1 is V11() V12() ext-real Element of REAL
h1 /. (1 + 1) is V11() V12() ext-real Element of REAL
[.(h1 /. 1),(h1 /. (1 + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
h1 /. 1 is V11() V12() ext-real Element of REAL
h1 /. (1 + 1) is V11() V12() ext-real Element of REAL
[.(h1 /. 1),(h1 /. (1 + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
y is V11() V12() ext-real Element of REAL
g1 . y is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
y is set
g1 . y is V21() Function-like set
sy is V11() V12() ext-real Element of REAL
g1 . (h1 /. (i + 1)) is V21() Function-like set
p1 is V11() V12() ext-real Element of REAL
g1 . p1 is V21() Function-like set
y is V11() V12() ext-real Element of REAL
g1 . y is V21() Function-like set
sy is set
g1 . sy is V21() Function-like set
y is set
g1 . y is V21() Function-like set
g1 . (h1 /. i) is V21() Function-like set
k is set
x is set
g1 . x is V21() Function-like set
y is V11() V12() ext-real Element of REAL
sy is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
k is Element of K6( the carrier of I[01])
g1 .: k is functional Element of K6( the carrier of (TOP-REAL 2))
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
i - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(i - (len h11)) + 2 is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
i - (len h1) is V11() V12() ext-real Element of REAL
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . (i + 1) is V21() Function-like set
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . i is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (i - (len h11)) is V21() Function-like set
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h2) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h2) + 1) - 1 is V11() V12() ext-real Element of REAL
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((((i -' (len h11)) + 1) + 1) - 1) + 1 is V11() V12() ext-real Element of REAL
(i -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h21 . (((i -' (len h11)) + 2) -' 1) is V21() Function-like set
h2 . (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) is V21() Function-like set
((i -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 /. (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
[.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) - 1 is V11() V12() ext-real Element of REAL
g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
x is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
y is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
h21 . ((((i -' (len h11)) + 2) -' 1) + 1) is V21() Function-like set
sy is set
g2 . sy is V21() Function-like set
p1 is V11() V12() ext-real Element of REAL
x is set
y is set
g2 . y is V21() Function-like set
sy is V11() V12() ext-real Element of REAL
p1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
k is Element of K6( the carrier of I[01])
g2 .: k is functional Element of K6( the carrier of (TOP-REAL 2))
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . i is V21() Function-like set
i -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(((i -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((((i -' (len h11)) + 1) + 1) - 1) + 1 is V11() V12() ext-real Element of REAL
(i -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(len h1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h11) - (len h11) is V11() V12() ext-real Element of REAL
(0 + 2) - 1 is V11() V12() ext-real Element of REAL
((len h1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 . (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((i -' (len h11)) + 2) -' 1)) is V21() Function-like set
i - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(i - (len h11)) + 2 is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
(len h2) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h2) + 1) - 1 is V11() V12() ext-real Element of REAL
h2 . ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h2 /. ((((i -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
((i -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 /. (((i -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
[.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
((i - (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i - (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . ((((i -' (len h11)) + 2) -' 1) + 1) is V21() Function-like set
g2 . (h2 . ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
h21 . (((i -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 .: [.(h2 /. (((i -' (len h11)) + 2) -' 1)),(h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)).] is functional Element of K6( the carrier of (TOP-REAL 2))
g2 . (h2 /. ((((i -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
x is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
y is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
sy is set
g2 . sy is V21() Function-like set
p1 is V11() V12() ext-real Element of REAL
x is set
y is set
g2 . y is V21() Function-like set
sy is V11() V12() ext-real Element of REAL
p1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. i,b₁,P & LE b₁,h0 /. (i + 1),P ) } is set
k is Element of K6( the carrier of I[01])
g2 .: k is functional Element of K6( the carrier of (TOP-REAL 2))
j0 is Element of K6( the carrier of (Euclid 2))
diameter j0 is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) - 1 is V11() V12() ext-real Element of REAL
(((len h0) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) is V21() Function-like set
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(len h0) - (len h1) is V11() V12() ext-real Element of REAL
((((len h0) -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h2 . (((((len h0) -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
(len h2) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h2) + 1) - 1 is V11() V12() ext-real Element of REAL
h2 /. ((((len h0) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
[.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] is V169() V170() V171() V211() Element of K6(REAL)
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
g2 .: [.(h2 /. ((((len h0) -' (len h11)) + 2) -' 1)),(h2 /. (((((len h0) -' (len h11)) + 2) -' 1) + 1)).] is functional Element of K6( the carrier of (TOP-REAL 2))
x is set
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. (len h0),b₁,P or ( h0 /. (len h0) in P & b₁ = W-min P ) ) } is set
y is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
sy is set
g2 . sy is V21() Function-like set
p1 is set
rz is V11() V12() ext-real Element of REAL
g2 . p1 is V21() Function-like set
sy is set
g2 . sy is V21() Function-like set
x is set
y is set
g2 . y is V21() Function-like set
sy is V11() V12() ext-real Element of REAL
p1 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2) : ( LE h0 /. (len h0),b₁,P or ( h0 /. (len h0) in P & b₁ = W-min P ) ) } is set
k is Element of K6( the carrier of I[01])
g2 .: k is functional Element of K6( the carrier of (TOP-REAL 2))
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
i + 2 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 2) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(i + 1) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h0 /. ((i + 1) + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 . ((i + 1) + 1) is V21() Function-like set
h1 . ((i + 1) + 1) is V11() V12() ext-real Element of REAL
h11 . ((i + 1) + 1) is V21() Function-like set
g1 . (h1 . ((i + 1) + 1)) is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((((i + 1) -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i + 1) -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + (1 + 1)) - 1 is V11() V12() ext-real Element of REAL
((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 is V11() V12() ext-real Element of REAL
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((i + 1) + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(((i + 1) + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
(((i + 1) + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((((i + 1) + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
((((i + 1) + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h2 . ((((i + 1) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . (i + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) is V21() Function-like set
h0 /. ((i + 1) + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 . ((i + 1) + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (((i + 1) + 1) - (len h11)) is V21() Function-like set
h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((i + 1) - (len h11)) + 2 is V11() V12() ext-real Element of REAL
((i + 1) + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((i + 1) + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(((i + 1) + 1) -' (len h11)) + (2 - 1) is V11() V12() ext-real Element of REAL
(((i + 1) + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((((i + 1) + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 /. (len h1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 . (len h1) is V21() Function-like set
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((((i + 1) -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i + 1) -' (len h11)) + (1 + 1) is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + (1 + 1)) - 1 is V11() V12() ext-real Element of REAL
((((i + 1) -' (len h11)) + (1 + 1)) - 1) + 1 is V11() V12() ext-real Element of REAL
(len h1) - (len h11) is V11() V12() ext-real Element of REAL
(len h1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1) is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
h0 /. ((i + 1) + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 . ((i + 1) + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (((i + 1) + 1) - (len h11)) is V21() Function-like set
((((i + 1) + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . (((((i + 1) + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
((i + 1) - (len h11)) + 2 is V11() V12() ext-real Element of REAL
(((i + 1) - (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
((((i + 1) - (len h11)) + 2) - 1) + 1 is V11() V12() ext-real Element of REAL
g2 . (h2 . (((((i + 1) -' (len h11)) + 2) -' 1) + 1)) is V21() Function-like set
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. i),(h0 /. (i + 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
i + 2 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 2) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. (i + 1)),(h0 /. (i + 2))) is functional Element of K6( the carrier of (TOP-REAL 2))
(P,(h0 /. i),(h0 /. (i + 1))) /\ (P,(h0 /. (i + 1)),(h0 /. (i + 2))) is functional Element of K6( the carrier of (TOP-REAL 2))
{(h0 /. (i + 1))} is non empty functional set
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
j0 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
j0 + 2 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (j0 + 2) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
j0 + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(j0 + 1) + 2 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. ((j0 + 1) + 2) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(j0 + 1) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(j0 + 2) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. ((j0 + 2) + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(len h0) -' 2 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(len h0) - 2 is V11() V12() ext-real Element of REAL
((len h0) -' 2) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
h1 . 2 is V11() V12() ext-real Element of REAL
g1 . (h1 . 2) is V21() Function-like set
h0 /. (0 + 2) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(len h0) - (len h1) is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
h0 /. (((len h0) -' 1) + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
j0 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. i),(h0 /. (i + 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
h0 /. j0 is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
j0 + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. (j0 + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. j0),(h0 /. (j0 + 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
h0 . j0 is V21() Function-like set
h11 . j0 is V21() Function-like set
h0 . j0 is V21() Function-like set
j0 - (len h11) is V11() V12() ext-real Element of REAL
j0 -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
(j0 -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((j0 -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((j0 -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h2 . (((j0 -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((j0 -' (len h11)) + 2) -' 1)) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (j0 - (len h11)) is V21() Function-like set
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
j0 - (len h1) is V11() V12() ext-real Element of REAL
h21 . (((j0 -' (len h11)) + 2) -' 1) is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) - 1 is V11() V12() ext-real Element of REAL
(((j0 -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
j0 - (len h1) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
j0 - (len h11) is V11() V12() ext-real Element of REAL
j0 -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(j0 -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((j0 -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
((j0 -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . j0 is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (j0 - (len h11)) is V21() Function-like set
h21 . (((j0 -' (len h11)) + 2) -' 1) is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
h1 . j0 is V11() V12() ext-real Element of REAL
h0 . j0 is V21() Function-like set
h11 . j0 is V21() Function-like set
g1 . (h1 . j0) is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
h11 . (i + 1) is V21() Function-like set
g1 . (h1 . (i + 1)) is V21() Function-like set
j0 -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(j0 -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((j0 -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
j0 - (len h11) is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(j0 + 1) - 1 is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - 1 is V11() V12() ext-real Element of REAL
((len h2) - 2) - 1 is V11() V12() ext-real Element of REAL
(len h1) + (((len h2) - 2) - 1) is V11() V12() ext-real Element of REAL
((len h1) + (((len h2) - 2) - 1)) - (len h11) is V11() V12() ext-real Element of REAL
(((len h2) - 2) - 1) + 2 is V11() V12() ext-real Element of REAL
((j0 -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
g1 . (h1 . (i + 1)) is V21() Function-like set
0 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(j0 -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((j0 -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((j0 -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
h0 . j0 is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (j0 - (len h11)) is V21() Function-like set
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
j0 - (len h1) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
h21 . (((j0 -' (len h11)) + 2) -' 1) is V21() Function-like set
h2 . (((j0 -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((j0 -' (len h11)) + 2) -' 1)) is V21() Function-like set
Seg (len h1) is V38() V45( len h1) V169() V170() V171() V172() V173() V174() V208() V209() V210() Element of K6(NAT)
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
j0 -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(j0 -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((j0 -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
j0 - (len h11) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
j0 - (len h1) is V11() V12() ext-real Element of REAL
h0 . j0 is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . (j0 - (len h11)) is V21() Function-like set
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
h21 . (((j0 -' (len h11)) + 2) -' 1) is V21() Function-like set
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
h2 . ((((i + 1) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) is V21() Function-like set
(j0 + 1) - 1 is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - 1 is V11() V12() ext-real Element of REAL
((len h2) - 2) - 1 is V11() V12() ext-real Element of REAL
(len h1) + (((len h2) - 2) - 1) is V11() V12() ext-real Element of REAL
((len h1) + (((len h2) - 2) - 1)) - (len h11) is V11() V12() ext-real Element of REAL
(((len h2) - 2) - 1) + 2 is V11() V12() ext-real Element of REAL
((j0 -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
0 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(j0 -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((j0 -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((j0 -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
h2 . (((j0 -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . (((j0 -' (len h11)) + 2) -' 1)) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
i is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
i + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 /. i is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
h0 /. (i + 1) is V21() V24( NAT ) Function-like V38() V45(2) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(P,(h0 /. i),(h0 /. (i + 1))) is functional Element of K6( the carrier of (TOP-REAL 2))
(len h0) - (len h1) is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
g1 . (h1 . (i + 1)) is V21() Function-like set
1 + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(1 + 2) - 1 is V11() V12() ext-real Element of REAL
(((len h0) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) is V21() Function-like set
(Upper_Arc P) /\ (Lower_Arc P) is functional Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty functional set
((((len h0) -' (len h11)) + 2) -' 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
((len h11) + 1) - (len h11) is V11() V12() ext-real Element of REAL
h0 . (i + 1) is V21() Function-like set
(((len h0) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
((len h1) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . ((len h0) - (len h11)) is V21() Function-like set
h1 . (i + 1) is V11() V12() ext-real Element of REAL
g1 . (h1 . (i + 1)) is V21() Function-like set
h0 . (i + 1) is V21() Function-like set
h11 . (i + 1) is V21() Function-like set
((len h1) + 1) - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) - (len h1) is V11() V12() ext-real Element of REAL
(i + 1) -' (len h11) is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
(i + 1) - (len h11) is V11() V12() ext-real Element of REAL
((len h11) + (len (mid (h21,2,((len h21) -' 1))))) - (len h11) is V11() V12() ext-real Element of REAL
(len h11) + 1 is V10() V11() V12() ext-real V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h0 . (i + 1) is V21() Function-like set
(mid (h21,2,((len h21) -' 1))) . ((i + 1) - (len h11)) is V21() Function-like set
((i + 1) -' (len h11)) + 2 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((i + 1) -' (len h11)) + 2) -' 1 is V10() V11() V12() ext-real non negative V19() V122() V169() V170() V171() V172() V173() V174() V208() Element of NAT
h21 . ((((i + 1) -' (len h11)) + 2) -' 1) is V21() Function-like set
0 + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((len h0) -' (len h11)) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
(((len h0) -' (len h11)) + 1) + 1 is non empty V10() V11() V12() ext-real positive non negative V19() V122() V169() V170() V171() V172() V173() V174() V206() V208() Element of NAT
((((len h0) -' (len h11)) + 1) + 1) - 1 is V11() V12() ext-real Element of REAL
(((len h0) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
(len h11) + ((len h2) - 2) is V11() V12() ext-real Element of REAL
((len h11) + ((len h2) - 2)) - (len h11) is V11() V12() ext-real Element of REAL
((len h2) - 2) + 2 is V11() V12() ext-real Element of REAL
h2 . ((((i + 1) -' (len h11)) + 2) -' 1) is V11() V12() ext-real Element of REAL
g2 . (h2 . ((((i + 1) -' (len h11)) + 2) -' 1)) is V21() Function-like set
(((i + 1) -' (len h11)) + 2) - 1 is V11() V12() ext-real Element of REAL
h0 . i is V21() Function-like set