:: SPRECT_4 semantic presentation

REAL is V204() V205() V206() V210() set

NAT is V204() V205() V206() V207() V208() V209() V210() Element of K6(REAL)

K6(REAL) is set

NAT is V204() V205() V206() V207() V208() V209() V210() set

K6(NAT) is set

K6(NAT) is set

1 is non empty V10() V11() V12() V91() ext-real positive V193() V204() V205() V206() V207() V208() V209() Element of NAT

2 is non empty V10() V11() V12() V91() ext-real positive V193() V204() V205() V206() V207() V208() V209() Element of NAT

K316() is TopStruct

the U1 of K316() is set

K7(1,1) is set

K6(K7(1,1)) is set

K7(K7(1,1),1) is set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is set

K7(K7(REAL,REAL),REAL) is set

K6(K7(K7(REAL,REAL),REAL)) is set

K7(2,2) is set

K7(K7(2,2),REAL) is set

K6(K7(K7(2,2),REAL)) is set

K344() is V175() L15()

K354() is TopSpace-like TopStruct

COMPLEX is V204() V210() set

RAT is V204() V205() V206() V207() V210() set

INT is V204() V205() V206() V207() V208() V210() set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty V47() TopSpace-like T_2 V108() V139() V140() V141() V142() V143() V144() V145() strict RLTopStruct

the U1 of (TOP-REAL 2) is non empty V2() functional set

K198( the U1 of (TOP-REAL 2)) is M11( the U1 of (TOP-REAL 2))

K7( the U1 of (TOP-REAL 2),REAL) is set

K6(K7( the U1 of (TOP-REAL 2),REAL)) is set

K6( the U1 of (TOP-REAL 2)) is set

{} is empty V2() Function-like functional V204() V205() V206() V207() V208() V209() V210() set

K33() is empty V2() V10() V11() V12() Function-like functional V91() ext-real V193() V204() V205() V206() V207() V208() V209() V210() Element of NAT

K356() is SubSpace of K354()

the U1 of K356() is set

1 / 2 is V11() V12() ext-real Element of REAL

4 is non empty V10() V11() V12() V91() ext-real positive V193() V204() V205() V206() V207() V208() V209() Element of NAT

len {} is V31() set

f is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

L~ f is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

g is functional closed Element of K6( the U1 of (TOP-REAL 2))

First_Point ((L~ f),(f /. 1),(f /. (len f)),g) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))))) /\ g is functional Element of K6( the U1 of (TOP-REAL 2))

{(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))} is non empty V2() functional set

(L~ f) /\ g is functional Element of K6( the U1 of (TOP-REAL 2))

1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

dom f is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)

p1 is set

p2 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f . 1 is V13() Function-like set

<*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

len <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

L~ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f . 1 is V13() Function-like set

mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))) is functional Element of K6( the U1 of (TOP-REAL 2))

<*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

(mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) ^ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ ((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) ^ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))*>) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))))) \/ (LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) is functional Element of K6( the U1 of (TOP-REAL 2))

f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),g))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

dom (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)

(mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) . (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))))) is V13() Function-like set

f . (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) is V13() Function-like set

f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f . 1 is V13() Function-like set

f . 1 is V13() Function-like set

f is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

g is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

L_Cut (f,g) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (L_Cut (f,g)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

dom f is V204() V205() V206() V207() V208() V209() Element of K6(NAT)

f . (len f) is V13() Function-like set

<*g*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

len (L_Cut (f,g)) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

L~ f is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

g is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

i is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

mid (f,i,(len f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (f,i,(len f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f /. i is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len (mid (f,i,(len f))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

w is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

w + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg ((mid (f,i,(len f))),w) is functional Element of K6( the U1 of (TOP-REAL 2))

(len f) -' i is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' i) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

w + i is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

i + w is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(i + w) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((i + w) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

i + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. ((i + w) -' 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg (f,((i + w) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

f is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

L~ f is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

g is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

i is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

w is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,w) is functional Element of K6( the U1 of (TOP-REAL 2))

w + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. (w + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg (g,(f /. (w + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

f /. w is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((f /. w),(f /. (w + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

dom f is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)

z2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,z2) is functional Element of K6( the U1 of (TOP-REAL 2))

p1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,p1) is functional Element of K6( the U1 of (TOP-REAL 2))

z2 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

p1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. z2 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f /. (z2 + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(LSeg (f,z2)) /\ (LSeg (f,w)) is functional Element of K6( the U1 of (TOP-REAL 2))

1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

w + (1 + 1) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(w + 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

{(f /. (w + 1))} is non empty V2() functional set

{g} is non empty V2() functional set

(LSeg (f,p1)) /\ (LSeg (f,w)) is functional Element of K6( the U1 of (TOP-REAL 2))

p1 + (1 + 1) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(p1 + 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

{(f /. w)} is non empty V2() functional set

LSeg (i,(f /. (w + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

f is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like one-to-one FinSequence-like special unfolded s.n.c. being_S-Seq FinSequence of the U1 of (TOP-REAL 2)

L~ f is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

f /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

g is functional closed Element of K6( the U1 of (TOP-REAL 2))

Last_Point ((L~ f),(f /. 1),(f /. (len f)),g) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))))) /\ g is functional Element of K6( the U1 of (TOP-REAL 2))

{(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))} is non empty V2() functional set

(L~ f) /\ g is functional Element of K6( the U1 of (TOP-REAL 2))

1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

p2 is set

z1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1)) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like set

L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))) is functional Element of K6( the U1 of (TOP-REAL 2))

f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like set

LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f))) is functional Element of K6( the U1 of (TOP-REAL 2))

dom f is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)

<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f)))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f)))) \/ (LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) is functional Element of K6( the U1 of (TOP-REAL 2))

f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

dom (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)

(mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) . 1 is V13() Function-like set

f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1) is V13() Function-like set

dom f is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)

f . (len f) is V13() Function-like set

f is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

f /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

L~ f is non empty functional closed V78( TOP-REAL 2) non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))

N-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

N-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))

NW-corner (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

W-bound (L~ f) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ f) is strict T_2 SubSpace of TOP-REAL 2

proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V38( the U1 of (TOP-REAL 2), REAL ) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))

proj1 | (L~ f) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ f))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ f)), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ f)),REAL))

the U1 of ((TOP-REAL 2) | (L~ f)) is set

K7( the U1 of ((TOP-REAL 2) | (L~ f)),REAL) is set

K6(K7( the U1 of ((TOP-REAL 2) | (L~ f)),REAL)) is set

K468(((TOP-REAL 2) | (L~ f)),(proj1 | (L~ f))) is V11() V12() ext-real Element of REAL

N-bound (L~ f) is V11() V12() ext-real Element of REAL

proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V38( the U1 of (TOP-REAL 2), REAL ) Element of K6(K7( the U1 of (TOP-REAL 2),REAL))

proj2 | (L~ f) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ f))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ f)), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ f)),REAL))

K469(((TOP-REAL 2) | (L~ f)),(proj2 | (L~ f))) is V11() V12() ext-real Element of REAL

|[(W-bound (L~ f)),(N-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

NE-corner (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

E-bound (L~ f) is V11() V12() ext-real Element of REAL

K469(((TOP-REAL 2) | (L~ f)),(proj1 | (L~ f))) is V11() V12() ext-real Element of REAL

|[(E-bound (L~ f)),(N-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) is functional closed closed V78( TOP-REAL 2) V78( TOP-REAL 2) horizontal Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))

(TOP-REAL 2) | (N-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (N-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (N-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ f))),REAL))

the U1 of ((TOP-REAL 2) | (N-most (L~ f))) is set

K7( the U1 of ((TOP-REAL 2) | (N-most (L~ f))),REAL) is set

K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ f))),REAL)) is set

K468(((TOP-REAL 2) | (N-most (L~ f))),(proj1 | (N-most (L~ f)))) is V11() V12() ext-real Element of REAL

|[K468(((TOP-REAL 2) | (N-most (L~ f))),(proj1 | (N-most (L~ f)))),(N-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LeftComp f is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))

RightComp f is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))

SpStSeq (L~ f) is non empty V2() V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like non constant FinSequence-like circular special unfolded s.c.c. standard rectangular clockwise_oriented FinSequence of the U1 of (TOP-REAL 2)

LeftComp (SpStSeq (L~ f)) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))

GoB f is V13() non empty-yielding V16( NAT ) V17(K198( the U1 of (TOP-REAL 2))) Function-like FinSequence-like tabular V242() V243() V244() V245() FinSequence of K198( the U1 of (TOP-REAL 2))

len (GoB f) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

width (GoB f) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

i is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(GoB f) * (i,(width (GoB f))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

1 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(width (GoB f)) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((width (GoB f)) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

[i,(width (GoB f))] is non empty set

Indices (GoB f) is set

i + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

[(i + 1),(width (GoB f))] is non empty set

dom f is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)

dom (GoB f) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)

f /. (1 + 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(GoB f) * ((i + 1),(width (GoB f))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

right_cell (f,1) is functional Element of K6( the U1 of (TOP-REAL 2))

cell ((GoB f),i,((width (GoB f)) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

(GoB f) * (i,((width (GoB f)) -' 1)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

Int (cell ((GoB f),i,((width (GoB f)) -' 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

Int (right_cell (f,1)) is functional Element of K6( the U1 of (TOP-REAL 2))

L~ (SpStSeq (L~ f)) is non empty functional closed V78( TOP-REAL 2) non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))

W-bound (L~ (SpStSeq (L~ f))) is V11() V12() ext-real Element of REAL

(TOP-REAL 2) | (L~ (SpStSeq (L~ f))) is strict T_2 SubSpace of TOP-REAL 2

proj1 | (L~ (SpStSeq (L~ f))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),REAL))

the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))) is set

K7( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),REAL) is set

K6(K7( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),REAL)) is set

K468(((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),(proj1 | (L~ (SpStSeq (L~ f))))) is V11() V12() ext-real Element of REAL

S-bound (L~ (SpStSeq (L~ f))) is V11() V12() ext-real Element of REAL

proj2 | (L~ (SpStSeq (L~ f))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),REAL))

K468(((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),(proj2 | (L~ (SpStSeq (L~ f))))) is V11() V12() ext-real Element of REAL

S-bound (L~ f) is V11() V12() ext-real Element of REAL

K468(((TOP-REAL 2) | (L~ f)),(proj2 | (L~ f))) is V11() V12() ext-real Element of REAL

N-bound (L~ (SpStSeq (L~ f))) is V11() V12() ext-real Element of REAL

K469(((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),(proj2 | (L~ (SpStSeq (L~ f))))) is V11() V12() ext-real Element of REAL

E-bound (L~ (SpStSeq (L~ f))) is V11() V12() ext-real Element of REAL

K469(((TOP-REAL 2) | (L~ (SpStSeq (L~ f)))),(proj1 | (L~ (SpStSeq (L~ f))))) is V11() V12() ext-real Element of REAL

(GoB f) * ((i + 1),((width (GoB f)) -' 1)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(1 / 2) * ((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 is V11() V12() ext-real Element of REAL

((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `1 is V11() V12() ext-real Element of REAL

(1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `1) is V11() V12() ext-real Element of REAL

(N-min (L~ f)) `1 is V11() V12() ext-real Element of REAL

((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 is V11() V12() ext-real Element of REAL

((N-min (L~ f)) `1) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) is V11() V12() ext-real Element of REAL

(1 / 2) * (((N-min (L~ f)) `1) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) is V11() V12() ext-real Element of REAL

(1 / 2) * ((N-min (L~ f)) `1) is V11() V12() ext-real Element of REAL

(1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) is V11() V12() ext-real Element of REAL

((1 / 2) * ((N-min (L~ f)) `1)) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) is V11() V12() ext-real Element of REAL

((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 is V11() V12() ext-real Element of REAL

((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `2 is V11() V12() ext-real Element of REAL

(1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `2) is V11() V12() ext-real Element of REAL

(N-min (L~ f)) `2 is V11() V12() ext-real Element of REAL

((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 is V11() V12() ext-real Element of REAL

((N-min (L~ f)) `2) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) is V11() V12() ext-real Element of REAL

(1 / 2) * (((N-min (L~ f)) `2) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) is V11() V12() ext-real Element of REAL

(N-bound (L~ f)) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) is V11() V12() ext-real Element of REAL

(1 / 2) * ((N-bound (L~ f)) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) is V11() V12() ext-real Element of REAL

(1 / 2) * (N-bound (L~ f)) is V11() V12() ext-real Element of REAL

(1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) is V11() V12() ext-real Element of REAL

((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) is V11() V12() ext-real Element of REAL

(1 / 2) * (W-bound (L~ f)) is V11() V12() ext-real Element of REAL

((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) is V11() V12() ext-real Element of REAL

(1 / 2) * (S-bound (L~ f)) is V11() V12() ext-real Element of REAL

((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) is V11() V12() ext-real Element of REAL

((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) is V11() V12() ext-real Element of REAL

(1 / 2) * (E-bound (L~ f)) is V11() V12() ext-real Element of REAL

((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) is V11() V12() ext-real Element of REAL

(GoB f) * (1,((width (GoB f)) -' 1)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (1,((width (GoB f)) -' 1))) `1 is V11() V12() ext-real Element of REAL

(GoB f) * (1,1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (1,1)) `1 is V11() V12() ext-real Element of REAL

N-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

K469(((TOP-REAL 2) | (N-most (L~ f))),(proj1 | (N-most (L~ f)))) is V11() V12() ext-real Element of REAL

|[K469(((TOP-REAL 2) | (N-most (L~ f))),(proj1 | (N-most (L~ f)))),(N-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(N-max (L~ f)) `1 is V11() V12() ext-real Element of REAL

(GoB f) * ((len (GoB f)),((width (GoB f)) -' 1)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 is V11() V12() ext-real Element of REAL

(GoB f) * ((len (GoB f)),1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * ((len (GoB f)),1)) `1 is V11() V12() ext-real Element of REAL

(GoB f) * ((i + 1),1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * ((i + 1),1)) `2 is V11() V12() ext-real Element of REAL

((GoB f) * (1,1)) `2 is V11() V12() ext-real Element of REAL

((GoB f) * ((i + 1),(width (GoB f)))) `2 is V11() V12() ext-real Element of REAL

(GoB f) * (1,(width (GoB f))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (1,(width (GoB f)))) `2 is V11() V12() ext-real Element of REAL

RightComp (SpStSeq (L~ f)) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))

{ b

z1 is set

z1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

P is functional Element of K6( the U1 of (TOP-REAL 2))

Red9 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ Red9 is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

Red9 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red9 /. (len Red9) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(len f) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

<*(NW-corner (L~ f))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

f /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner (L~ f)),(N-min (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

1 + 2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,1) is functional Element of K6( the U1 of (TOP-REAL 2))

LSeg (f,(1 + 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,1)) /\ (LSeg (f,(1 + 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

{(f /. (1 + 1))} is non empty V2() functional set

2 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' 1) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(len f) -' 2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' 2) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(((len f) -' 1) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((len f) -' 2) + 2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,((len f) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

LSeg (f,((len f) -' 2)) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) is functional Element of K6( the U1 of (TOP-REAL 2))

f /. ((len f) -' 1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

{(f /. ((len f) -' 1))} is non empty V2() functional set

f /. 2 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg ((f /. 1),(f /. 2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

((GoB f) * (i,((width (GoB f)) -' 1))) `1 is V11() V12() ext-real Element of REAL

(GoB f) * (i,1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((GoB f) * (i,1)) `1 is V11() V12() ext-real Element of REAL

(f /. 2) `2 is V11() V12() ext-real Element of REAL

<*((GoB f) * ((i + 1),(width (GoB f))))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

<*((GoB f) * (i,((width (GoB f)) -' 1)))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

<*((GoB f) * (i,((width (GoB f)) -' 1))),((GoB f) * ((i + 1),(width (GoB f))))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

<*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)

LSeg ((N-min (L~ f)),(f /. ((len f) -' 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(LSeg ((N-min (L~ f)),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))

{(N-min (L~ f))} is non empty V2() functional set

(NW-corner (L~ f)) `2 is V11() V12() ext-real Element of REAL

(NW-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL

(f /. 2) `1 is V11() V12() ext-real Element of REAL

LSeg ((NW-corner (L~ f)),(f /. 2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

LSeg ((N-min (L~ f)),(f /. 2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(LSeg ((N-min (L~ f)),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))

((GoB f) * (i,(width (GoB f)))) `2 is V11() V12() ext-real Element of REAL

(((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) `2 is V11() V12() ext-real Element of REAL

((GoB f) * (i,((width (GoB f)) -' 1))) `2 is V11() V12() ext-real Element of REAL

(((GoB f) * (i,((width (GoB f)) -' 1))) `2) + (((GoB f) * ((i + 1),(width (GoB f)))) `2) is V11() V12() ext-real Element of REAL

(((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2 is V11() V12() ext-real Element of REAL

((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 is V11() V12() ext-real Element of REAL

(1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) is V11() V12() ext-real Element of REAL

LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

LSeg ((f /. ((len f) -' 1)),(f /. (len f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(1 / 2) * ((GoB f) * (i,((width (GoB f)) -' 1))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

1 - (1 / 2) is V11() V12() ext-real Element of REAL

(1 - (1 / 2)) * ((GoB f) * (i,(width (GoB f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

((1 / 2) * ((GoB f) * (i,((width (GoB f)) -' 1)))) + ((1 - (1 / 2)) * ((GoB f) * (i,(width (GoB f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `1 is V11() V12() ext-real Element of REAL

((GoB f) * (i,((width (GoB f)) -' 1))) + (N-min (L~ f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

(((GoB f) * (i,((width (GoB f)) -' 1))) + (N-min (L~ f))) `1 is V11() V12() ext-real Element of REAL

(1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + (N-min (L~ f))) `1) is V11() V12() ext-real Element of REAL

((N-min (L~ f)) `1) + ((N-min (L~ f)) `1) is V11() V12() ext-real Element of REAL

(1 / 2) * (((N-min (L~ f)) `1) + ((N-min (L~ f)) `1)) is V11() V12() ext-real Element of REAL

(1 + 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(((len f) -' 1) -' 1) + 2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

mid (f,G,Red9) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (f,G,Red9)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(L~ (mid (f,G,Red9))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) is functional Element of K6( the U1 of (TOP-REAL 2))

u1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len (mid (f,G,Red9)) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg ((mid (f,G,Red9)),Red) is functional Element of K6( the U1 of (TOP-REAL 2))

Red9 -' G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(Red9 -' G) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red + G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(Red + G) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((Red + G) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((Red9 -' G) + 1) + G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(Red9 -' G) + G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

((Red9 -' G) + G) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

Red9 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

f . 1 is V13() Function-like set

{(f . 1)} is non empty V2() functional set

{(f /. 1)} is non empty V2() functional set

LSeg (f,((Red + G) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((Red + G) -' 1))) /\ (LSeg (f,((len f) -' 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

G is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

mid (f,G,((len f) -' 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (f,G,((len f) -' 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(L~ (mid (f,G,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) is functional Element of K6( the U1 of (TOP-REAL 2))

mid (f,G,((len f) -' 2)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (f,G,((len f) -' 2))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((len f) -' 2))) \/ (L~ (mid (f,G,((len f) -' 2)))) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((len f) -' 2))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) is functional Element of K6( the U1 of (TOP-REAL 2))

LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))

G is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

{((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} is non empty V2() functional set

(Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} is non empty set

(L~ f) /\ ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) is functional Element of K6( the U1 of (TOP-REAL 2))

(L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) is functional Element of K6( the U1 of (TOP-REAL 2))

(L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} is functional Element of K6( the U1 of (TOP-REAL 2))

((L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1))))) \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) is functional Element of K6( the U1 of (TOP-REAL 2))

{} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) is set

LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

{ (((1 - b

(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))

Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

u1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

mid (f,Red9,u1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (f,Red9,u1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))

(L~ (mid (f,Red9,u1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))

Red is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)

len (mid (f,Red9,u1)) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

u2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

u2 + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg ((mid (f,Red9,u1)),u2) is functional Element of K6( the U1 of (TOP-REAL 2))

u1 -' Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(u1 -' Red9) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

u2 + Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

(u2 + Red9) -' 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT

LSeg (f,((u2 + Red9) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))

(L~ f) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg ((f /. ((len f) -' 1)),(f /. (len f)))) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg (f,((len f) -' 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

(LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) is functional Element of K6( the U1 of (TOP-REAL 2))

f . 1 is V13() Function-like set

{(f . 1)} is non empty V2() functional set

{(f /. 1)} is non empty V2() functional