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 - b1) * ((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))))))) + (b1 * (First_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * (f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)))) + (b1 * (First_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * g) + (b1 * (f /. (w + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (f /. w)) + (b1 * (f /. (w + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * i) + (b1 * (f /. (w + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is 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))
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 - b1) * (Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) + (b1 * (f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is 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))
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 - b1) * ((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1)) + (b1 * (Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * (Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) + (b1 * (f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) + (b1 * ((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (Last_Point ((L~ f),(f /. 1),(f /. (len f)),g))) + (b1 * ((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),g)),f)) + 1),(len f))) /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (NW-corner (L~ f))) + (b1 * (NE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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))
{ b1 where b1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2) : ( not b1 `1 <= W-bound (L~ (SpStSeq (L~ f))) & not E-bound (L~ (SpStSeq (L~ f))) <= b1 `1 & not b1 `2 <= S-bound (L~ (SpStSeq (L~ f))) & not N-bound (L~ (SpStSeq (L~ f))) <= b1 `2 ) } is set
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 - b1) * (NW-corner (L~ f))) + (b1 * (N-min (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (f /. 1)) + (b1 * (f /. 2))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
((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 - b1) * (N-min (L~ f))) + (b1 * (f /. ((len f) -' 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner (L~ f))) + (b1 * (f /. 2))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
LSeg ((N-min (L~ f)),(f /. 2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (N-min (L~ f))) + (b1 * (f /. 2))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) + (b1 * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
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 - b1) * (f /. ((len f) -' 1))) + (b1 * (f /. (len f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) + (b1 * (f /. ((len f) -' 1)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
((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 - b1) * (f /. ((len f) -' 1))) + (b1 * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(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 - b1) * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) + (b1 * ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } 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)))))))) /\ (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