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 set
((u2 + Red9) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
((u2 + Red9) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
<*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(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)
<*((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 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,(width (GoB f))))))*> ^ <*((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 FinSequence of the U1 of (TOP-REAL 2)
(L~ (SpStSeq (L~ f))) /\ (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 Element of K6( the U1 of (TOP-REAL 2))
((GoB f) * (i,(width (GoB f)))) `1 is V11() V12() ext-real Element of REAL
(((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 is V11() V12() ext-real Element of REAL
((GoB f) * ((i + 1),(width (GoB f)))) `1 is V11() V12() ext-real Element of REAL
(((GoB f) * (i,((width (GoB f)) -' 1))) `1) + (((GoB f) * ((i + 1),(width (GoB f)))) `1) is V11() V12() ext-real Element of REAL
(((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `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))))) `1) is V11() V12() ext-real Element of REAL
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(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 /. 1),(f /. (1 + 1))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (f /. 1)) + (b1 * (f /. (1 + 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)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(1 - (1 / 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)
((1 / 2) * ((GoB f) * (i,(width (GoB f))))) + ((1 - (1 / 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)
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) 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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) + (b1 * (f /. 2))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((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)))) 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))))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) is V11() V12() ext-real Element of REAL
((N-min (L~ f)) `2) + ((N-min (L~ f)) `2) is V11() V12() ext-real Element of REAL
(1 / 2) * (((N-min (L~ f)) `2) + ((N-min (L~ f)) `2)) is V11() V12() ext-real Element of REAL
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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) 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
u2 + 2 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,((u2 + Red9) -' 1)) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg (f,1)) is functional Element of K6( the U1 of (TOP-REAL 2))
((u2 + Red9) -' 1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
{(f /. 2)} is non empty V2() functional set
Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,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~ (mid (f,2,Red9)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ (mid (f,2,Red9))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) is functional Element of K6( the U1 of (TOP-REAL 2))
mid (f,(2 + 1),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,(2 + 1),Red9)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
LSeg (f,2) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),Red9))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (f,2)) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))
Red9 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 + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((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 + 1),(width (GoB f))))))) + (b1 * ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ f)),(N-min (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
Red9 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)))) /\ (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} is non empty V2() functional set
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} is non empty V2() functional set
(L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB 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)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) is functional Element of K6( the U1 of (TOP-REAL 2))
{} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg ((f /. 1),(f /. (1 + 1)))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (f,((u2 + Red9) -' 1))) /\ (LSeg (f,1)) is functional Element of K6( the U1 of (TOP-REAL 2))
((u2 + Red9) -' 1) + 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
(L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} is non empty V2() functional set
<*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((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)
Red9 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 Red9 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
dom Red9 is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
L~ Red9 is non empty 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)
Red9 /. (len Red9) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ 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~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
NW-corner (L~ (SpStSeq (L~ f))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
|[(W-bound (L~ (SpStSeq (L~ f)))),(N-bound (L~ (SpStSeq (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(L~ Red9) /\ (L~ (SpStSeq (L~ f))) is functional Element of K6( the U1 of (TOP-REAL 2))
(L~ f) /\ (L~ Red9) is functional Element of K6( the U1 of (TOP-REAL 2))
Red9 . (len Red9) is V13() Function-like set
Red 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)
dom Red is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
Red /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Red . 1 is V13() Function-like set
L~ Red is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ (SpStSeq (L~ f))) /\ (L~ Red) is functional Element of K6( the U1 of (TOP-REAL 2))
{(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} is non empty V2() functional set
(L~ Red) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(L~ Red) /\ (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 Element of K6( the U1 of (TOP-REAL 2))
len Red is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
Red /. (len Red) 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)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 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 * (First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))))))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))))))))),((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) * (First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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))))))))))) + (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
Red2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
RB2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,Red2,RB2) 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,Red2,RB2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(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)))))))) /\ (L~ (SpStSeq (L~ f))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) + (b1 * (First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((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) * (First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) + (b1 * ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
Red2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
RB2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,Red2,RB2) 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,Red2,RB2)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
Red2 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)
Red2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
len Red2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
dom Red2 is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
Rev Red2 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)
(Rev Red2) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Red2 /. (len Red2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Red2 . (len Red2) is V13() Function-like set
((Rev Red2) /. 1) `2 is V11() V12() ext-real Element of REAL
L~ (Rev Red2) is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
L~ Red2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ Red2) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 (((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)))))))) /\ (L~ Red2) is functional Element of K6( the U1 of (TOP-REAL 2))
{(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 non empty V2() functional set
(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))))))))))) /\ (L~ Red2) is functional Element of K6( the U1 of (TOP-REAL 2))
<*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ (Rev Red2) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence 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)))) /\ (L~ Red2) is functional Element of K6( the U1 of (TOP-REAL 2))
(L~ (SpStSeq (L~ f))) /\ (L~ Red2) is functional Element of K6( the U1 of (TOP-REAL 2))
R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((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)
Red1 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 Red1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
dom Red1 is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
Red1 /. (len Red1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Red1 . (len Red1) is V13() Function-like set
Red1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(Red1 /. (len Red1)) `1 is V11() V12() ext-real Element of REAL
L~ Red1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ Red1) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red1) is functional Element of K6( the U1 of (TOP-REAL 2))
{(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} is non empty V2() functional set
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) is functional Element of K6( the U1 of (TOP-REAL 2))
Red1 ^ <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((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)
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ Red1) is functional Element of K6( the U1 of (TOP-REAL 2))
(L~ (SpStSeq (L~ f))) /\ (L~ Red1) is functional Element of K6( the U1 of (TOP-REAL 2))
len (Rev Red2) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
RB2 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 RB2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
RB2 /. (len RB2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(Rev Red2) /. (len Red2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
RB2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
L~ RB2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ Red2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 non empty functional Element of K6( 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)))) /\ (L~ RB2) is functional Element of K6( 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)))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))))))))),((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 (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) is set
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like special FinSequence of the U1 of (TOP-REAL 2)
RB1 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)
RB1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
len <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
len RB1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(len Red1) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
RB1 /. (len RB1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
L~ RB1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ Red1) \/ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
{} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) is set
<*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((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)
SE-corner (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
|[(E-bound (L~ f)),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (NE-corner (L~ f))) + (b1 * (SE-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)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))
SW-corner (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
|[(W-bound (L~ f)),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-corner (L~ f))) + (b1 * (SW-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (NW-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))
((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((N-min (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (N-min (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)),(N-min (L~ f)))) \/ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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 * (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ RB1) is functional Element of K6( the U1 of (TOP-REAL 2))
{(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} \/ {} is non empty set
(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 is V11() V12() ext-real Element of REAL
<*(NW-corner (L~ f))*> ^ RB1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
i1 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~ i1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
LSeg ((NW-corner (L~ f)),(RB1 /. 1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (NW-corner (L~ f))) + (b1 * (RB1 /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ i1) is functional Element of K6( the U1 of (TOP-REAL 2))
{} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1)) is set
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
mid (f,2,((E-min (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M2 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~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((S-min (L~ f)) .. f),(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)
M1 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~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M2 /. 1 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)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
M1 is set
u is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `2 is V11() V12() ext-real Element of REAL
(f /. (len f)) `2 is V11() V12() ext-real Element of REAL
(f /. 1) `2 is V11() V12() ext-real Element of REAL
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-min (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-min (L~ f)) `2 is V11() V12() ext-real Element of REAL
len i1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
i1 /. (len i1) 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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M2) is functional Element of K6( the U1 of (TOP-REAL 2))
i1 ^ M2 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 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)
RB1 ^ (mid (f,2,((E-min (L~ f)) .. f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
<*(NW-corner (L~ f))*> ^ (RB1 ^ (mid (f,2,((E-min (L~ f)) .. f)))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `1 is V11() V12() ext-real Element of REAL
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `1 is V11() V12() ext-real Element of REAL
len (mid (f,2,((E-min (L~ f)) .. f))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 is V11() V12() ext-real Element of REAL
f /. ((E-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((E-min (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(E-min (L~ f)) `1 is V11() V12() ext-real Element of REAL
L~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
LSeg ((i1 /. (len i1)),(M2 /. 1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (i1 /. (len i1))) + (b1 * (M2 /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(L~ i1) \/ (LSeg ((i1 /. (len i1)),(M2 /. 1))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
((L~ i1) \/ (LSeg ((i1 /. (len i1)),(M2 /. 1)))) \/ (L~ M2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
((S-max (L~ f)) .. f) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((S-max (L~ f)) .. f),((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)
M3 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~ M3 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
((E-max (L~ f)) .. f) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,1,((E-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M2 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~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
M2 /. (len M2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. (len M2)) `1 is V11() V12() ext-real Element of REAL
f /. ((E-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((E-max (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(E-max (L~ f)) `1 is V11() V12() ext-real Element of REAL
M2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. 1) `1 is V11() V12() ext-real Element of REAL
(f /. 1) `1 is V11() V12() ext-real Element of REAL
(NE-corner (L~ f)) `2 is V11() V12() ext-real Element of REAL
len M3 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M3 /. (len M3) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((M3 /. (len M3)),((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) * (M3 /. (len M3))) + (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 ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M3) is functional Element of K6( the U1 of (TOP-REAL 2))
{(M3 /. (len M3))} is non empty V2() functional set
M3 ^ RB2 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 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 M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `2 is V11() V12() ext-real Element of REAL
(RB2 /. (len RB2)) `2 is V11() V12() ext-real Element of REAL
dom (mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `2 is V11() V12() ext-real Element of REAL
(mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-max (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-max (L~ f)) `2 is V11() V12() ext-real Element of REAL
L~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
((L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(L~ M3) \/ ((LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3))) 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 * (M3 /. (len M3)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3)))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
((S-min (L~ f)) .. f) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((S-min (L~ f)) .. f),((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)
M3 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~ M3 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
((E-max (L~ f)) .. f) + 1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,1,((E-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M2 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~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
rng f is non empty V2() set
M2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
len M3 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M3 /. (len M3) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((M3 /. (len M3)),((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) * (M3 /. (len M3))) + (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 ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M3) is functional Element of K6( the U1 of (TOP-REAL 2))
{(M3 /. (len M3))} is non empty V2() functional set
M3 ^ RB2 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 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~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
((L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(L~ M3) \/ ((LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
dom M2 is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M2) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
<*(NW-corner (L~ f))*> ^ M2 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 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)
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `1 is V11() V12() ext-real Element of REAL
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) is functional Element of K6( the U1 of (TOP-REAL 2))
(NE-corner (L~ f)) `2 is V11() V12() ext-real Element of REAL
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `1 is V11() V12() ext-real Element of REAL
len (mid (f,1,((E-max (L~ f)) .. f))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(mid (f,1,((E-max (L~ f)) .. f))) /. (len (mid (f,1,((E-max (L~ f)) .. f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,1,((E-max (L~ f)) .. f))) /. (len (mid (f,1,((E-max (L~ f)) .. f))))) `1 is V11() V12() ext-real Element of REAL
f /. ((E-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((E-max (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(E-max (L~ f)) `1 is V11() V12() ext-real Element of REAL
L~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
LSeg ((NW-corner (L~ f)),(M2 /. 1)) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (NW-corner (L~ f))) + (b1 * (M2 /. 1))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ f)),(M2 /. 1))) \/ (L~ M2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `2 is V11() V12() ext-real Element of REAL
(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 is V11() V12() ext-real Element of REAL
dom (mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `2 is V11() V12() ext-real Element of REAL
(mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-min (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-min (L~ f)) `2 is V11() V12() ext-real Element of REAL
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3))) 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 * (M3 /. (len M3)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3)))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
W-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(RB2 /. 1) `1 is V11() V12() ext-real Element of REAL
(SE-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL
(NE-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL
(RB2 /. (len RB2)) `1 is V11() V12() ext-real Element of REAL
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
M2 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~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M2 /. (len M2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. (len M2)) `2 is V11() V12() ext-real Element of REAL
f /. ((N-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((N-max (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(N-max (L~ f)) `2 is V11() V12() ext-real Element of REAL
M2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-max (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-max (L~ f)) `2 is V11() V12() ext-real Element of REAL
W-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(W-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
mid (f,((W-min (L~ f)) .. f),((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)
M2 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~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M2 /. (len M2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((M2 /. (len M2)),((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) * (M2 /. (len M2))) + (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 ((M2 /. (len M2)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M2) is functional Element of K6( the U1 of (TOP-REAL 2))
{(M2 /. (len M2))} is non empty V2() functional set
M2 ^ RB2 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M1 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)
mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 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~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `2 is V11() V12() ext-real Element of REAL
f /. ((N-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((N-max (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(N-max (L~ f)) `2 is V11() V12() ext-real Element of REAL
(SE-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL
(NE-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `1 is V11() V12() ext-real Element of REAL
(RB2 /. (len RB2)) `1 is V11() V12() ext-real Element of REAL
dom (mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) is V204() V205() V206() V207() V208() V209() Element of K6(NAT)
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `1 is V11() V12() ext-real Element of REAL
(mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) /. 1) `1 is V11() V12() ext-real Element of REAL
f /. ((W-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((W-min (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(W-min (L~ f)) `1 is V11() V12() ext-real Element of REAL
L~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ M2) \/ (LSeg ((M2 /. (len M2)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
((L~ M2) \/ (LSeg ((M2 /. (len M2)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((M2 /. (len M2)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(L~ M2) \/ ((LSeg ((M2 /. (len M2)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-max (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-max (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-max (L~ 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)))))),(M2 /. (len M2))) 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 * (M2 /. (len M2)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M2 /. (len M2)))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
(SW-corner (L~ f)) `2 is V11() V12() ext-real Element of REAL
(SE-corner (L~ f)) `2 is V11() V12() ext-real Element of REAL
(RB1 /. 1) `2 is V11() V12() ext-real Element of REAL
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
Rev (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
L~ (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
M3 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~ M3 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
M3 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M3 /. 1) `1 is V11() V12() ext-real Element of REAL
f /. ((W-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((W-min (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(W-min (L~ f)) `1 is V11() V12() ext-real Element of REAL
len M3 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M3 /. (len M3) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M3 /. (len M3)) `1 is V11() V12() ext-real Element of REAL
f /. ((E-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((E-min (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(E-min (L~ f)) `1 is V11() V12() ext-real Element of REAL
(SW-corner (L~ f)) `1 is V11() V12() ext-real Element of REAL
S-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
S-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SW-corner (L~ f)),(SE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SW-corner (L~ f))) + (b1 * (SE-corner (L~ f)))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((SW-corner (L~ f)),(SE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (S-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (S-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (S-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (S-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (S-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (S-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
LSeg ((SE-corner (L~ f)),(NE-corner (L~ f))) is functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
{ (((1 - b1) * (SE-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 ((SE-corner (L~ f)),(NE-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (E-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (E-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (E-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (E-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (E-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (E-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K468(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(N-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
E-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ f)),K469(((TOP-REAL 2) | (E-most (L~ f))),(proj2 | (E-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(E-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
rng f is non empty V2() set
mid (f,2,((E-min (L~ f)) .. f)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M3 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~ M3 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
M3 /. 1 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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 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)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) + (b1 * (M3 /. 1))) 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)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) /\ (L~ M3) is functional Element of K6( the U1 of (TOP-REAL 2))
{(M3 /. 1)} is non empty V2() functional set
RB1 ^ M3 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like FinSequence-like FinSequence of the U1 of (TOP-REAL 2)
M2 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 M2 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M2 /. (len M2) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. (len M2)) `1 is V11() V12() ext-real Element of REAL
len (mid (f,2,((E-min (L~ f)) .. f))) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f)))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 is V11() V12() ext-real Element of REAL
f /. ((E-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((E-min (L~ f)) .. f)) `1 is V11() V12() ext-real Element of REAL
(E-min (L~ f)) `1 is V11() V12() ext-real Element of REAL
dom RB1 is non empty V2() V204() V205() V206() V207() V208() V209() Element of K6(NAT)
M2 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M2 /. 1) `1 is V11() V12() ext-real Element of REAL
(RB1 /. 1) `1 is V11() V12() ext-real Element of REAL
L~ M2 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
(L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
((L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1)))) \/ (L~ M3) is non empty functional Element of K6( the U1 of (TOP-REAL 2))
W-min (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K468(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(W-min (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
S-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[K469(((TOP-REAL 2) | (S-most (L~ f))),(proj1 | (S-most (L~ f)))),(S-bound (L~ f))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(S-max (L~ f)) .. f is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
mid (f,((S-min (L~ f)) .. f),(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)
M1 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~ M1 is non empty functional closed V78( TOP-REAL 2) Element of K6( the U1 of (TOP-REAL 2))
len M1 is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
M1 /. (len M1) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. (len M1)) `2 is V11() V12() ext-real Element of REAL
(f /. (len f)) `2 is V11() V12() ext-real Element of REAL
(f /. 1) `2 is V11() V12() ext-real Element of REAL
M1 /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(M1 /. 1) `2 is V11() V12() ext-real Element of REAL
f /. ((S-min (L~ f)) .. f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(f /. ((S-min (L~ f)) .. f)) `2 is V11() V12() ext-real Element of REAL
(S-min (L~ f)) `2 is V11() V12() ext-real Element of REAL
W-max (L~ f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-most (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) /\ (L~ f) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (W-most (L~ f)) is strict T_2 SubSpace of TOP-REAL 2
proj2 | (W-most (L~ f)) is V13() V16( the U1 of ((TOP-REAL 2) | (W-most (L~ f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (W-most (L~ f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL))
the U1 of ((TOP-REAL 2) | (W-most (L~ f))) is set
K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (W-most (L~ f))),REAL)) is set
K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ f)),K469(((TOP-REAL 2) | (W-most (L~ f))),(proj2 | (W-most (L~ f))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
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 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))
Rev 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 FinSequence of the U1 of (TOP-REAL 2)
LeftComp (Rev f) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))
RightComp (Rev f) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))
L~ (Rev 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~ (Rev f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Rev f)) is functional Element of K6( the U1 of (TOP-REAL 2))
NW-corner (L~ (Rev f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Rev f)) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Rev f)) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (L~ (Rev f)) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Rev f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (Rev f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rev f))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Rev f))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Rev f))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rev f))),REAL)) is set
K468(((TOP-REAL 2) | (L~ (Rev f))),(proj1 | (L~ (Rev f)))) is V11() V12() ext-real Element of REAL
N-bound (L~ (Rev f)) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Rev f)) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Rev f)))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (Rev f))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rev f))),REAL))
K469(((TOP-REAL 2) | (L~ (Rev f))),(proj2 | (L~ (Rev f)))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Rev f))),(N-bound (L~ (Rev f)))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Rev f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Rev f)) is V11() V12() ext-real Element of REAL
K469(((TOP-REAL 2) | (L~ (Rev f))),(proj1 | (L~ (Rev f)))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Rev f))),(N-bound (L~ (Rev f)))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Rev f))),(NE-corner (L~ (Rev 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~ (Rev f)))) + (b1 * (NE-corner (L~ (Rev f))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ (Rev f))),(NE-corner (L~ (Rev f))))) /\ (L~ (Rev f)) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Rev f))) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Rev f))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f)))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f)))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f)))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f)))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rev f)))),REAL)) is set
K468(((TOP-REAL 2) | (N-most (L~ (Rev f)))),(proj1 | (N-most (L~ (Rev f))))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (N-most (L~ (Rev f)))),(proj1 | (N-most (L~ (Rev f))))),(N-bound (L~ (Rev 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
(Rev f) /. (len f) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
len (Rev f) is V10() V11() V12() V91() ext-real V193() V204() V205() V206() V207() V208() V209() Element of NAT
(Rev f) /. (len (Rev f)) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
(Rev f) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
Rev 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 FinSequence of the U1 of (TOP-REAL 2)
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 FinSequence 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))
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)
Rotate (f,(N-min (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 FinSequence of the U1 of (TOP-REAL 2)
L~ (Rotate (f,(N-min (L~ f)))) is non empty functional closed V78( TOP-REAL 2) non horizontal non vertical Element of K6( the U1 of (TOP-REAL 2))
rng f is non empty V2() set
(Rotate (f,(N-min (L~ f)))) /. 1 is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
N-min (L~ (Rotate (f,(N-min (L~ f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
N-most (L~ (Rotate (f,(N-min (L~ f))))) is functional Element of K6( the U1 of (TOP-REAL 2))
NW-corner (L~ (Rotate (f,(N-min (L~ f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
W-bound (L~ (Rotate (f,(N-min (L~ f))))) is V11() V12() ext-real Element of REAL
(TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f))))) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (L~ (Rotate (f,(N-min (L~ f))))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f))))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),REAL))
the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))) is set
K7( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),REAL)) is set
K468(((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),(proj1 | (L~ (Rotate (f,(N-min (L~ f))))))) is V11() V12() ext-real Element of REAL
N-bound (L~ (Rotate (f,(N-min (L~ f))))) is V11() V12() ext-real Element of REAL
proj2 | (L~ (Rotate (f,(N-min (L~ f))))) is V13() V16( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f))))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),REAL))
K469(((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),(proj2 | (L~ (Rotate (f,(N-min (L~ f))))))) is V11() V12() ext-real Element of REAL
|[(W-bound (L~ (Rotate (f,(N-min (L~ f)))))),(N-bound (L~ (Rotate (f,(N-min (L~ f))))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
NE-corner (L~ (Rotate (f,(N-min (L~ f))))) is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
E-bound (L~ (Rotate (f,(N-min (L~ f))))) is V11() V12() ext-real Element of REAL
K469(((TOP-REAL 2) | (L~ (Rotate (f,(N-min (L~ f)))))),(proj1 | (L~ (Rotate (f,(N-min (L~ f))))))) is V11() V12() ext-real Element of REAL
|[(E-bound (L~ (Rotate (f,(N-min (L~ f)))))),(N-bound (L~ (Rotate (f,(N-min (L~ f))))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (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~ (Rotate (f,(N-min (L~ f))))))) + (b1 * (NE-corner (L~ (Rotate (f,(N-min (L~ f)))))))) where b1 is V11() V12() ext-real Element of REAL : ( K33() <= b1 & b1 <= 1 ) } is set
(LSeg ((NW-corner (L~ (Rotate (f,(N-min (L~ f)))))),(NE-corner (L~ (Rotate (f,(N-min (L~ f)))))))) /\ (L~ (Rotate (f,(N-min (L~ f))))) is functional Element of K6( the U1 of (TOP-REAL 2))
(TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f)))))) is strict T_2 SubSpace of TOP-REAL 2
proj1 | (N-most (L~ (Rotate (f,(N-min (L~ f)))))) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f)))))))) V17( REAL ) Function-like V38( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))), REAL ) Element of K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))),REAL))
the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))) is set
K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))),REAL) is set
K6(K7( the U1 of ((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))),REAL)) is set
K468(((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))),(proj1 | (N-most (L~ (Rotate (f,(N-min (L~ f)))))))) is V11() V12() ext-real Element of REAL
|[K468(((TOP-REAL 2) | (N-most (L~ (Rotate (f,(N-min (L~ f))))))),(proj1 | (N-most (L~ (Rotate (f,(N-min (L~ f)))))))),(N-bound (L~ (Rotate (f,(N-min (L~ f))))))]| is V13() Function-like V33(2) FinSequence-like V196() Element of the U1 of (TOP-REAL 2)
RightComp (Rotate (f,(N-min (L~ f)))) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))
LeftComp (Rotate (f,(N-min (L~ f)))) is non empty functional being_Region Element of K6( the U1 of (TOP-REAL 2))