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 - b1) * g) + (b1 * G)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg (g,p) is closed compact Element of bool the U1 of (TOP-REAL f)
{ (((1 - b1) * g) + (b1 * p)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * G) + (b1 * x)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * f) + (b1 * g)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * p) + (b1 * G)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * f) + (b1 * g)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * g) + (b1 * p)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * f) + (b1 * g)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * G) + (b1 * p)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * (NE-corner f)) + (b1 * (SE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (SE-corner f)) + (b1 * (SW-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg ((SW-corner f),(NW-corner f)) is closed compact Element of bool the U1 of (TOP-REAL 2)
{ (((1 - b1) * (SW-corner f)) + (b1 * (NW-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (NW-corner f)) + (b1 * (NE-corner f))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * g) + (b1 * (f /. 1))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g <= b1 ) } is set
{ (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f + 1 <= b1 & not g <= b1 ) } is set
{(LSeg (p,f))} is non empty trivial V26() 1 -element set
{ (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f + 1 <= b1 & not g <= b1 ) } \/ {(LSeg (p,f))} is non empty set
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,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g <= b1 ) } is set
union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f + 1 <= b1 & not g <= b1 ) } is set
union {(LSeg (p,f))} is set
(union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f + 1 <= b1 & not g <= b1 ) } ) \/ (union {(LSeg (p,f))}) is set
(union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f + 1 <= b1 & not g <= b1 ) } ) \/ (LSeg (p,f)) 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 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,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g <= b1 ) } is set
{ (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g -' 1 <= b1 ) } is set
{(LSeg (p,(g -' 1)))} is non empty trivial V26() 1 -element set
{ (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g -' 1 <= b1 ) } \/ {(LSeg (p,(g -' 1)))} is non empty set
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,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g <= b1 ) } is set
union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g -' 1 <= b1 ) } is set
union {(LSeg (p,(g -' 1)))} is set
(union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g -' 1 <= b1 ) } ) \/ (union {(LSeg (p,(g -' 1)))}) is set
(union { (LSeg (p,b1)) where b1 is ordinal natural V11() real V26() cardinal V37() ext-real V197() V208() V209() V210() V211() V212() V213() Element of NAT : ( f <= b1 & not g -' 1 <= b1 ) } ) \/ (LSeg (p,(g -' 1))) is 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)
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 - b1) * (f /. (len f))) + (b1 * (g /. 1))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(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 - b1) * (g /. f)) + (b1 * p)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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 - b1) * (g /. f)) + (b1 * (g /. (f + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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))