:: SPRECT_3 semantic presentation

REAL is non empty non trivial V26() V208() V209() V210() V214() set

NAT is non empty non trivial ordinal V26() cardinal limit_cardinal V208() V209() V210() V211() V212() V213() V214() Element of bool REAL

bool REAL is non empty non trivial V26() set

INT is non empty non trivial V26() V208() V209() V210() V211() V212() V214() set

omega is non empty non trivial ordinal V26() cardinal limit_cardinal V208() V209() V210() V211() V212() V213() V214() set

bool omega is non empty non trivial V26() set

bool NAT is non empty non trivial V26() set

COMPLEX is non empty non trivial V26() V208() V214() set

1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

2 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

K348() is TopStruct

the U1 of K348() is set

[:1,1:] is V17( RAT ) V17( INT ) V26() V198() V199() V200() V201() set

RAT is non empty non trivial V26() V208() V209() V210() V211() V214() set

bool [:1,1:] is V26() V30() set

[:[:1,1:],1:] is V17( RAT ) V17( INT ) V26() V198() V199() V200() V201() set

bool [:[:1,1:],1:] is V26() V30() set

[:[:1,1:],REAL:] is V198() V199() V200() set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is non empty non trivial V26() V198() V199() V200() set

[:[:REAL,REAL:],REAL:] is non empty non trivial V26() V198() V199() V200() set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial V26() set

[:2,2:] is V17( RAT ) V17( INT ) V26() V198() V199() V200() V201() set

[:[:2,2:],REAL:] is V198() V199() V200() set

bool [:[:2,2:],REAL:] is set

RealSpace is strict MetrStruct

K386() is TopSpace-like TopStruct

bool [:REAL,REAL:] is non empty non trivial V26() set

TOP-REAL 2 is non empty TopSpace-like V112() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct

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

K230( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

[: the U1 of (TOP-REAL 2),REAL:] is non empty non trivial V26() V198() V199() V200() set

bool [: the U1 of (TOP-REAL 2),REAL:] is non empty non trivial V26() set

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

[:COMPLEX,COMPLEX:] is non empty non trivial V26() V198() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial V26() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V26() V198() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V26() set

[:RAT,RAT:] is non empty non trivial V17( RAT ) V26() V198() V199() V200() set

bool [:RAT,RAT:] is non empty non trivial V26() set

[:[:RAT,RAT:],RAT:] is non empty non trivial V17( RAT ) V26() V198() V199() V200() set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial V26() set

[:INT,INT:] is non empty non trivial V17( RAT ) V17( INT ) V26() V198() V199() V200() set

bool [:INT,INT:] is non empty non trivial V26() set

[:[:INT,INT:],INT:] is non empty non trivial V17( RAT ) V17( INT ) V26() V198() V199() V200() set

bool [:[:INT,INT:],INT:] is non empty non trivial V26() set

[:NAT,NAT:] is non empty non trivial V17( RAT ) V17( INT ) V26() V198() V199() V200() V201() set

[:[:NAT,NAT:],NAT:] is non empty non trivial V17( RAT ) V17( INT ) V26() V198() V199() V200() V201() set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial V26() set

K674() is set

{} is empty trivial ordinal natural V11() real Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V208() V209() V210() V211() V212() V213() V214() set

the empty trivial ordinal natural V11() real Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V208() V209() V210() V211() V212() V213() V214() set is empty trivial ordinal natural V11() real Function-like functional V26() V30() cardinal {} -element FinSequence-membered ext-real non positive non negative V208() V209() V210() V211() V212() V213() V214() set

[:COMPLEX,REAL:] is non empty non trivial V26() V198() V199() V200() set

bool [:COMPLEX,REAL:] is non empty non trivial V26() set

3 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

Seg 1 is non empty trivial V26() 1 -element V208() V209() V210() V211() V212() V213() Element of bool NAT

{1} is non empty trivial V26() V30() 1 -element V208() V209() V210() V211() V212() V213() set

Seg 2 is non empty V26() 2 -element V208() V209() V210() V211() V212() V213() Element of bool NAT

{1,2} is non empty V26() V30() V208() V209() V210() V211() V212() V213() set

4 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

5 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

0 is empty trivial ordinal natural V11() real Function-like functional V26() V30() cardinal {} -element FinSequence-membered V37() ext-real non positive non negative V197() V208() V209() V210() V211() V212() V213() V214() Element of NAT

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

|[0,1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

K388() is SubSpace of K386()

the U1 of K388() is set

[:(Seg 2),(Seg 2):] is V17( INT ) V17( RAT ) V26() V198() V199() V200() V201() set

f is non empty set

g is non empty V13() V16( NAT ) V17(f) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of f

len g is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g /. (len g) is Element of f

p is V13() V16( NAT ) V17(f) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of f

p ^ g is non empty V13() V16( NAT ) V17(f) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of f

len (p ^ g) is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(p ^ g) /. (len (p ^ g)) is Element of f

len p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(len p) + (len g) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

[1,1] is non empty set

{1,1} is non empty V26() V30() V208() V209() V210() V211() V212() V213() set

{{1,1},{1}} is non empty V26() V30() set

[1,2] is non empty set

{{1,2},{1}} is non empty V26() V30() set

[2,1] is non empty set

{2,1} is non empty V26() V30() V208() V209() V210() V211() V212() V213() set

{2} is non empty trivial V26() V30() 1 -element V208() V209() V210() V211() V212() V213() set

{{2,1},{2}} is non empty V26() V30() set

[2,2] is non empty set

{2,2} is non empty V26() V30() V208() V209() V210() V211() V212() V213() set

{{2,2},{2}} is non empty V26() V30() set

{[1,1],[1,2],[2,1],[2,2]} is V26() set

f is set

g is set

p is set

G is set

(f,g) ][ (p,G) is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like tabular set

Indices ((f,g) ][ (p,G)) is set

{1} is non empty trivial V26() V30() 1 -element V208() V209() V210() V211() V212() V213() Element of bool REAL

[:{1},(Seg 2):] is V17( INT ) V17( RAT ) V26() V198() V199() V200() V201() set

{2} is non empty trivial V26() V30() 1 -element V208() V209() V210() V211() V212() V213() Element of bool REAL

[:{2},(Seg 2):] is V17( INT ) V17( RAT ) V26() V198() V199() V200() V201() set

[:{1},(Seg 2):] \/ [:{2},(Seg 2):] is V26() set

{[2,1],[2,2]} is non empty V26() set

[:{1},(Seg 2):] \/ {[2,1],[2,2]} is non empty V26() set

{[1,1],[1,2]} is non empty V26() set

{[1,1],[1,2]} \/ {[2,1],[2,2]} is non empty V26() set

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

TOP-REAL f is non empty TopSpace-like V112() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct

the U1 of (TOP-REAL f) is non empty set

g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G is V11() real ext-real Element of REAL

1 - G is V11() real ext-real Element of REAL

(1 - G) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G * p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - G) * g) + (G * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - G) * g) + (G * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(1 - G) + G is V11() real ext-real Element of REAL

((1 - G) + G) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

0. (TOP-REAL f) is f -element FinSequence-like V51( TOP-REAL f) V200() Element of the U1 of (TOP-REAL f)

(G * g) + (0. (TOP-REAL f)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

- ((1 - G) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - G) * g) + (- ((1 - G) * g)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(G * g) + (((1 - G) * g) + (- ((1 - G) * g))) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(G * p) + ((1 - G) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((G * p) + ((1 - G) * g)) + (- ((1 - G) * g)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(G * p) + (((1 - G) * g) + (- ((1 - G) * g))) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(G * p) + (0. (TOP-REAL f)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

TOP-REAL f is non empty TopSpace-like V112() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct

the U1 of (TOP-REAL f) is non empty set

g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G is V11() real ext-real Element of REAL

1 - G is V11() real ext-real Element of REAL

(1 - G) * p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - G) * p) + (G * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G + {} is V11() real ext-real Element of REAL

1 - (1 - G) is V11() real ext-real Element of REAL

(1 - (1 - G)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (1 - G)) * g) + ((1 - G) * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

TOP-REAL f is non empty TopSpace-like V112() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct

the U1 of (TOP-REAL f) is non empty set

g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

g + p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(1 / 2) * (g + p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

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

(1 - (1 / 2)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(1 / 2) * p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (1 / 2)) * g) + ((1 / 2) * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

TOP-REAL f is non empty TopSpace-like V112() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct

the U1 of (TOP-REAL f) is non empty set

p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

G is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

LSeg (g,G) is closed compact Element of bool the U1 of (TOP-REAL f)

bool the U1 of (TOP-REAL f) is set

{ (((1 - b

LSeg (g,p) is closed compact Element of bool the U1 of (TOP-REAL f)

{ (((1 - b

x is V11() real ext-real Element of REAL

1 - x is V11() real ext-real Element of REAL

(1 - x) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

x * G is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - x) * g) + (x * G) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p is V11() real ext-real Element of REAL

1 - p is V11() real ext-real Element of REAL

(1 - p) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p * p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - p) * g) + (p * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

x * p is V11() real ext-real Element of REAL

p * (1 - x) is V11() real ext-real Element of REAL

(1 - p) + (p * (1 - x)) is V11() real ext-real Element of REAL

p * x is V11() real ext-real Element of REAL

1 - (p * x) is V11() real ext-real Element of REAL

p * ((1 - x) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

p * (x * G) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(p * ((1 - x) * g)) + (p * (x * G)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - p) * g) + ((p * ((1 - x) * g)) + (p * (x * G))) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - p) * g) + (p * ((1 - x) * g)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(((1 - p) * g) + (p * ((1 - x) * g))) + (p * (x * G)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(p * (1 - x)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - p) * g) + ((p * (1 - x)) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(((1 - p) * g) + ((p * (1 - x)) * g)) + (p * (x * G)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(1 - (p * x)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (p * x)) * g) + (p * (x * G)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(p * x) * G is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (p * x)) * g) + ((p * x) * G) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

x * (1 - p) is V11() real ext-real Element of REAL

(1 - x) + (x * (1 - p)) is V11() real ext-real Element of REAL

1 - (x * p) is V11() real ext-real Element of REAL

x * ((1 - p) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

x * (p * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(x * ((1 - p) * g)) + (x * (p * p)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - x) * g) + ((x * ((1 - p) * g)) + (x * (p * p))) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - x) * g) + (x * ((1 - p) * g)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(((1 - x) * g) + (x * ((1 - p) * g))) + (x * (p * p)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(x * (1 - p)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - x) * g) + ((x * (1 - p)) * g) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(((1 - x) * g) + ((x * (1 - p)) * g)) + (x * (p * p)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(1 - (x * p)) * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (x * p)) * g) + (x * (p * p)) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

(x * p) * p is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

((1 - (x * p)) * g) + ((x * p) * p) is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

1 * x is V11() real ext-real Element of REAL

1 * p is V11() real ext-real Element of REAL

{} * g is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

({} * g) + G is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

0. (TOP-REAL f) is f -element FinSequence-like V51( TOP-REAL f) V200() Element of the U1 of (TOP-REAL f)

(0. (TOP-REAL f)) + G is f -element FinSequence-like V200() Element of the U1 of (TOP-REAL f)

Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct

the U1 of (Euclid 2) is non empty set

f is non empty Element of bool the U1 of (TOP-REAL 2)

g is Element of the U1 of (Euclid 2)

p is V11() real ext-real Element of REAL

Ball (g,p) is Element of bool the U1 of (Euclid 2)

bool the U1 of (Euclid 2) is set

G is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

x is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (G,x) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

f is Element of bool the U1 of (TOP-REAL 2)

g is Element of bool the U1 of (TOP-REAL 2)

the topology of (TOP-REAL 2) is Element of bool (bool the U1 of (TOP-REAL 2))

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

TopStruct(# the U1 of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is strict TopStruct

TopSpaceMetr (Euclid 2) is TopStruct

the U1 of (TopSpaceMetr (Euclid 2)) is set

bool the U1 of (TopSpaceMetr (Euclid 2)) is set

G is Element of bool the U1 of (TopSpaceMetr (Euclid 2))

p is Element of bool the U1 of (TopSpaceMetr (Euclid 2))

x is Element of the U1 of (Euclid 2)

p is V11() real ext-real set

Ball (x,p) is Element of bool the U1 of (Euclid 2)

bool the U1 of (Euclid 2) is set

r is V11() real ext-real Element of REAL

Ball (x,r) is Element of bool the U1 of (Euclid 2)

s is Element of bool the U1 of (TOP-REAL 2)

f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (f,g) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

G is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (p,G) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

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

p `2 is V11() real ext-real Element of REAL

(LSeg (f,g)) /\ (LSeg (p,G)) is closed Element of bool the U1 of (TOP-REAL 2)

x is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

x `2 is V11() real ext-real Element of REAL

f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (f,g) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (g,p) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg (f,g)) /\ (LSeg (g,p)) is closed Element of bool the U1 of (TOP-REAL 2)

{g} is non empty trivial V26() 1 -element set

G is set

x is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

x `2 is V11() real ext-real Element of REAL

g `2 is V11() real ext-real Element of REAL

x `1 is V11() real ext-real Element of REAL

g `1 is V11() real ext-real Element of REAL

f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (f,g) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

G is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg (G,p) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg (f,g)) /\ (LSeg (G,p)) is closed Element of bool the U1 of (TOP-REAL 2)

{p} is non empty trivial V26() 1 -element set

x is set

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

p `2 is V11() real ext-real Element of REAL

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

p `1 is V11() real ext-real Element of REAL

p `1 is V11() real ext-real Element of REAL

p `2 is V11() real ext-real Element of REAL

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G is V13() non empty-yielding V16( NAT ) V17(K230( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K230( the U1 of (TOP-REAL 2))

width G is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

len G is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G * (p,f) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(G * (p,f)) `2 is V11() real ext-real Element of REAL

G * (p,g) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(G * (p,g)) `2 is V11() real ext-real Element of REAL

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G is V13() non empty-yielding V16( NAT ) V17(K230( the U1 of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K230( the U1 of (TOP-REAL 2))

width G is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

len G is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G * (g,f) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(G * (g,f)) `1 is V11() real ext-real Element of REAL

G * (p,f) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(G * (p,f)) `1 is V11() real ext-real Element of REAL

f is Element of bool the U1 of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

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

proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

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

[: the U1 of ((TOP-REAL 2) | f),REAL:] is V198() V199() V200() set

bool [: the U1 of ((TOP-REAL 2) | f),REAL:] is set

K500(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K763(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

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

proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

K501(((TOP-REAL 2) | f),(proj2 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

K501(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner f),(NE-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

SpStSeq f is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (SpStSeq f) is closed compact Element of bool the U1 of (TOP-REAL 2)

SE-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

K500(((TOP-REAL 2) | f),(proj2 | f)) is V11() real ext-real Element of REAL

K763(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(E-bound f),(S-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

LSeg ((NE-corner f),(SE-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg ((NW-corner f),(NE-corner f))) \/ (LSeg ((NE-corner f),(SE-corner f))) is closed Element of bool the U1 of (TOP-REAL 2)

SW-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

|[(W-bound f),(S-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

LSeg ((SE-corner f),(SW-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

LSeg ((SW-corner f),(NW-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg ((SE-corner f),(SW-corner f))) \/ (LSeg ((SW-corner f),(NW-corner f))) is closed Element of bool the U1 of (TOP-REAL 2)

((LSeg ((NW-corner f),(NE-corner f))) \/ (LSeg ((NE-corner f),(SE-corner f)))) \/ ((LSeg ((SE-corner f),(SW-corner f))) \/ (LSeg ((SW-corner f),(NW-corner f)))) is closed Element of bool the U1 of (TOP-REAL 2)

f is non empty compact Element of bool the U1 of (TOP-REAL 2)

N-min f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

N-most f is Element of bool the U1 of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

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

proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

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

[: the U1 of ((TOP-REAL 2) | f),REAL:] is V198() V199() V200() set

bool [: the U1 of ((TOP-REAL 2) | f),REAL:] is set

K500(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K763(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

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

proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

K501(((TOP-REAL 2) | f),(proj2 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

K501(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner f),(NE-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg ((NW-corner f),(NE-corner f))) /\ f is Element of bool the U1 of (TOP-REAL 2)

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

proj1 | (N-most f) is V13() V16( the U1 of ((TOP-REAL 2) | (N-most f))) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | (N-most f)), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | (N-most f)),REAL:]

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

[: the U1 of ((TOP-REAL 2) | (N-most f)),REAL:] is V198() V199() V200() set

bool [: the U1 of ((TOP-REAL 2) | (N-most f)),REAL:] is set

K500(((TOP-REAL 2) | (N-most f)),(proj1 | (N-most f))) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | (N-most f)),REAL,(proj1 | (N-most f)), the U1 of ((TOP-REAL 2) | (N-most f))) is V208() V209() V210() Element of bool REAL

K763(K330( the U1 of ((TOP-REAL 2) | (N-most f)),REAL,(proj1 | (N-most f)), the U1 of ((TOP-REAL 2) | (N-most f)))) is V11() real ext-real Element of REAL

|[K500(((TOP-REAL 2) | (N-most f)),(proj1 | (N-most f))),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

f is Element of bool the U1 of (TOP-REAL 2)

NW-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

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

proj1 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj1 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

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

[: the U1 of ((TOP-REAL 2) | f),REAL:] is V198() V199() V200() set

bool [: the U1 of ((TOP-REAL 2) | f),REAL:] is set

K500(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K763(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

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

proj2 is V13() V16( the U1 of (TOP-REAL 2)) V17( REAL ) Function-like V40( the U1 of (TOP-REAL 2), REAL ) V198() V199() V200() Element of bool [: the U1 of (TOP-REAL 2),REAL:]

proj2 | f is V13() V16( the U1 of ((TOP-REAL 2) | f)) V17( REAL ) Function-like V40( the U1 of ((TOP-REAL 2) | f), REAL ) V198() V199() V200() Element of bool [: the U1 of ((TOP-REAL 2) | f),REAL:]

K501(((TOP-REAL 2) | f),(proj2 | f)) is V11() real ext-real Element of REAL

K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f)) is V208() V209() V210() Element of bool REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj2 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(W-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

NE-corner f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

K501(((TOP-REAL 2) | f),(proj1 | f)) is V11() real ext-real Element of REAL

K762(K330( the U1 of ((TOP-REAL 2) | f),REAL,(proj1 | f), the U1 of ((TOP-REAL 2) | f))) is V11() real ext-real Element of REAL

|[(E-bound f),(N-bound f)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V198() V199() V200() Element of the U1 of (TOP-REAL 2)

LSeg ((NW-corner f),(NE-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

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

(NE-corner f) `2 is V11() real ext-real Element of REAL

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

f /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

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

L~ f is closed compact Element of bool the U1 of (TOP-REAL 2)

{(f /. 1)} is non empty trivial V26() 1 -element set

g is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g `1 is V11() real ext-real Element of REAL

g `2 is V11() real ext-real Element of REAL

LSeg (g,(f /. 1)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg (g,(f /. 1))) /\ (L~ f) is closed Element of bool the U1 of (TOP-REAL 2)

<*g*> is non empty trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like special M12( the U1 of (TOP-REAL 2),K231(1, the U1 of (TOP-REAL 2)))

K231(1, the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

<*g*> ^ f is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

<*g,(f /. 1)*> is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() 2 -element FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

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

dom G is non empty non trivial V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

len <*g,(f /. 1)*> is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

1 + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(len <*g,(f /. 1)*>) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

mid (<*g,(f /. 1)*>,1,((len <*g,(f /. 1)*>) -' 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

<*g,(f /. 1)*> /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

<*(<*g,(f /. 1)*> /. 1)*> is non empty trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like special M12( the U1 of (TOP-REAL 2),K231(1, the U1 of (TOP-REAL 2)))

L~ <*g,(f /. 1)*> is closed compact Element of bool the U1 of (TOP-REAL 2)

(L~ <*g,(f /. 1)*>) /\ (L~ f) is closed Element of bool the U1 of (TOP-REAL 2)

f . 1 is set

{(f . 1)} is non empty trivial V26() 1 -element set

<*g,(f /. 1)*> . (len <*g,(f /. 1)*>) is set

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

len g is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

L~ (mid (g,1,f)) is closed compact Element of bool the U1 of (TOP-REAL 2)

L~ g is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

g /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g /. (len g) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g /. f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

len (mid (g,1,f)) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

G + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg ((mid (g,1,f)),G) is closed Element of bool the U1 of (TOP-REAL 2)

f -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(f -' 1) + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(G + 1) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (g,((G + 1) -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)

g /. (G + 1) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

dom p is V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

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

L~ (mid (p,f,g)) is closed compact Element of bool the U1 of (TOP-REAL 2)

L~ p is closed compact Element of bool the U1 of (TOP-REAL 2)

len p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

f + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

len p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

L~ (mid (p,f,g)) is closed compact Element of bool the U1 of (TOP-REAL 2)

LSeg (p,f) is closed Element of bool the U1 of (TOP-REAL 2)

mid (p,(f + 1),g) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (p,(f + 1),g)) is closed compact Element of bool the U1 of (TOP-REAL 2)

(LSeg (p,f)) \/ (L~ (mid (p,(f + 1),g))) is closed Element of bool the U1 of (TOP-REAL 2)

{ (LSeg (p,b

{ (LSeg (p,b

{(LSeg (p,f))} is non empty trivial V26() 1 -element set

{ (LSeg (p,b

p is set

r is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (p,r) is closed Element of bool the U1 of (TOP-REAL 2)

p is set

r is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (p,r) is closed Element of bool the U1 of (TOP-REAL 2)

union { (LSeg (p,b

union { (LSeg (p,b

union {(LSeg (p,f))} is set

(union { (LSeg (p,b

(union { (LSeg (p,b

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

len p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

L~ (mid (p,f,g)) is closed compact Element of bool the U1 of (TOP-REAL 2)

mid (p,f,(g -' 1)) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (mid (p,f,(g -' 1))) is closed compact Element of bool the U1 of (TOP-REAL 2)

LSeg (p,(g -' 1)) is closed Element of bool the U1 of (TOP-REAL 2)

(L~ (mid (p,f,(g -' 1)))) \/ (LSeg (p,(g -' 1))) is closed Element of bool the U1 of (TOP-REAL 2)

{ (LSeg (p,b

{ (LSeg (p,b

{(LSeg (p,(g -' 1)))} is non empty trivial V26() 1 -element set

{ (LSeg (p,b

p is set

r is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (p,r) is closed Element of bool the U1 of (TOP-REAL 2)

p is set

r is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (p,r) is closed Element of bool the U1 of (TOP-REAL 2)

union { (LSeg (p,b

union { (LSeg (p,b

union {(LSeg (p,(g -' 1)))} is set

(union { (LSeg (p,b

(union { (LSeg (p,b

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

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

len f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

f /. (len f) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

g /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(g /. 1) `1 is V11() real ext-real Element of REAL

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

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

L~ f is closed compact Element of bool the U1 of (TOP-REAL 2)

L~ g is closed compact Element of bool the U1 of (TOP-REAL 2)

LSeg ((f /. (len f)),(g /. 1)) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

(LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) is closed Element of bool the U1 of (TOP-REAL 2)

{(f /. (len f))} is non empty trivial V26() 1 -element set

(LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) is closed Element of bool the U1 of (TOP-REAL 2)

{(g /. 1)} is non empty trivial V26() 1 -element set

f ^ g is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

len g is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

dom g is V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

<*(f /. (len f))*> is non empty trivial V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like constant V26() 1 -element FinSequence-like FinSubsequence-like special M12( the U1 of (TOP-REAL 2),K231(1, the U1 of (TOP-REAL 2)))

K231(1, the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))

<*(f /. (len f))*> ^ g is non empty V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

dom f is V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

f . (len f) is set

(<*(f /. (len f))*> ^ g) . 1 is set

len (<*(f /. (len f))*> ^ g) is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

len <*(f /. (len f))*> is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(len <*(f /. (len f))*>) + (len g) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(len g) + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

1 + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

(len (<*(f /. (len f))*> ^ g)) -' 2 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

((len (<*(f /. (len f))*> ^ g)) -' 2) + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(1 + 1) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(<*(f /. (len f))*> ^ g) /^ ((1 + 1) -' 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

((<*(f /. (len f))*> ^ g) /^ ((1 + 1) -' 1)) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

(<*(f /. (len f))*> ^ g) /^ 1 is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

((<*(f /. (len f))*> ^ g) /^ 1) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

g | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

(len (<*(f /. (len f))*> ^ g)) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

(((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

g | ((((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

(len g) -' 1 is ordinal natural V11() real V26() cardinal V37() ext-real non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

((len g) -' 1) + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

g | (((len g) -' 1) + 1) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

g | (len g) is V13() V16( NAT ) V17( the U1 of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)

L~ (<*(f /. (len f))*> ^ g) is closed compact Element of bool the U1 of (TOP-REAL 2)

(L~ f) /\ (L~ (<*(f /. (len f))*> ^ g)) is closed Element of bool the U1 of (TOP-REAL 2)

(LSeg ((f /. (len f)),(g /. 1))) \/ (L~ g) is closed Element of bool the U1 of (TOP-REAL 2)

(L~ f) /\ ((LSeg ((f /. (len f)),(g /. 1))) \/ (L~ g)) is closed Element of bool the U1 of (TOP-REAL 2)

(L~ f) /\ (LSeg ((f /. (len f)),(g /. 1))) is closed Element of bool the U1 of (TOP-REAL 2)

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

((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ ((L~ f) /\ (L~ g)) is closed Element of bool the U1 of (TOP-REAL 2)

((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ {} is set

{((<*(f /. (len f))*> ^ g) . 1)} is non empty trivial V26() 1 -element set

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

L~ f is closed compact Element of bool the U1 of (TOP-REAL 2)

f /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

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

(R_Cut (f,g)) /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

Index (g,f) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

len f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

dom f is V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

f . 1 is set

len (R_Cut (f,g)) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(Index (g,f)) + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(R_Cut (f,g)) . 1 is set

f is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

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

len g is non empty ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (g,f) is closed Element of bool the U1 of (TOP-REAL 2)

g /. f is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

L~ g is non empty closed compact Element of bool the U1 of (TOP-REAL 2)

g /. 1 is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g /. (len g) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

p is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

G is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg ((g /. f),p) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

f + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g /. (f + 1) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

LSeg ((g /. f),(g /. (f + 1))) is closed compact Element of bool the U1 of (TOP-REAL 2)

{ (((1 - b

dom g is non empty non trivial V26() V208() V209() V210() V211() V212() V213() Element of bool NAT

x is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (g,x) is closed Element of bool the U1 of (TOP-REAL 2)

p is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

LSeg (g,p) is closed Element of bool the U1 of (TOP-REAL 2)

x + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

p + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

g /. x is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

g /. (x + 1) is 2 -element FinSequence-like V200() Element of the U1 of (TOP-REAL 2)

(LSeg (g,p)) /\ (LSeg (g,f)) is closed Element of bool the U1 of (TOP-REAL 2)

(LSeg (g,x)) /\ (LSeg (g,f)) is closed Element of bool the U1 of (TOP-REAL 2)

1 + 1 is non empty ordinal natural V11() real V26() cardinal V37() ext-real positive non negative V197() V208() V209() V210() V211() V212() V213() Element of NAT

p + (1 + 1) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(p + 1) + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

p + 2 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

{(g /. f)} is non empty trivial V26() 1 -element set

{p} is non empty trivial V26() 1 -element set

f + (1 + 1) is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

(f + 1) + 1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT

{(g /. (f + 1))