:: 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

{ b

{ b

h1 is functional Element of K6( the carrier of (TOP-REAL 2))

{ b

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

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

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

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

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

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

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

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

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

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

{ b

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

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

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

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

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

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

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

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

{ b

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

{ b

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