REAL is non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() set
NAT is non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal Element of bool REAL
bool REAL is non trivial V52() set
COMPLEX is non empty non trivial V45() V51() V52() set
RAT is non empty non trivial V45() V46() V47() V48() V51() V52() set
INT is non empty non trivial V45() V46() V47() V48() V49() V51() V52() set
NAT is non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal set
bool NAT is non trivial V52() set
bool NAT is non trivial V52() set
[:COMPLEX,COMPLEX:] is Relation-like non trivial V33() V52() set
bool [:COMPLEX,COMPLEX:] is non trivial V52() set
[:COMPLEX,REAL:] is Relation-like non trivial V33() V34() V35() V52() set
bool [:COMPLEX,REAL:] is non trivial V52() set
1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[:1,1:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
bool [:1,1:] is V52() V56() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
bool [:[:1,1:],1:] is V52() V56() set
[:[:1,1:],REAL:] is Relation-like V33() V34() V35() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is Relation-like non trivial V33() V34() V35() V52() set
[:[:REAL,REAL:],REAL:] is Relation-like non trivial V33() V34() V35() V52() set
bool [:[:REAL,REAL:],REAL:] is non trivial V52() set
2 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
[:[:2,2:],REAL:] is Relation-like V33() V34() V35() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is non trivial V52() set
TOP-REAL 2 is non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is set
K246( the carrier of (TOP-REAL 2)) is functional non empty FinSequence-membered M12( the carrier of (TOP-REAL 2))
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non trivial V33() V52() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V52() set
[:RAT,RAT:] is Relation-like RAT -valued non trivial V33() V34() V35() V52() set
bool [:RAT,RAT:] is non trivial V52() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non trivial V33() V34() V35() V52() set
bool [:[:RAT,RAT:],RAT:] is non trivial V52() set
[:INT,INT:] is Relation-like RAT -valued INT -valued non trivial V33() V34() V35() V52() set
bool [:INT,INT:] is non trivial V52() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non trivial V33() V34() V35() V52() set
bool [:[:INT,INT:],INT:] is non trivial V52() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is set
{} is set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() ext-real non positive non negative V26() V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() V52() V53() V56() V63() V64() V65() V66() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() ext-real non positive non negative V26() V33() V34() V35() V36() V45() V46() V47() V48() V49() V50() V51() V52() V53() V56() V63() V64() V65() V66() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
3 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
0 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg 1 is non empty trivial V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() 1 -element Element of bool NAT
{1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
Seg 2 is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() 2 -element Element of bool NAT
{1,2} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
x is V17() V21() V22() ext-real non negative V26() V52() cardinal set
f is V17() V21() V22() ext-real non negative V26() V52() cardinal set
f + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
LSeg (n,f) is Element of bool the carrier of (TOP-REAL 2)
LSeg (n,x) is Element of bool the carrier of (TOP-REAL 2)
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n /. (len n) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg (n,f) is Element of bool the carrier of (TOP-REAL 2)
f + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(len n) - 1 is V22() ext-real V26() set
x is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(f + 1) + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
n /. (x + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (n,x) is Element of bool the carrier of (TOP-REAL 2)
f + 2 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
n /. (f + 2) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (n,(f + 1)) is Element of bool the carrier of (TOP-REAL 2)
n /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
1 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
f + (1 + 1) is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(LSeg (n,f)) /\ (LSeg (n,(f + 1))) is Element of bool the carrier of (TOP-REAL 2)
n /. (f + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
{(n /. (f + 1))} is non empty trivial V52() 1 -element set
(LSeg (n,f)) /\ (LSeg (n,x)) is Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
L~ n is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
union { (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n | f) is Element of bool the carrier of (TOP-REAL 2)
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg ((n | f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n | f) ) } is set
LSeg (n,f) is Element of bool the carrier of (TOP-REAL 2)
(L~ (n | f)) \/ (LSeg (n,f)) is Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
p is set
j is set
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg (n,j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
LSeg ((n | f),j) is Element of bool the carrier of (TOP-REAL 2)
p is set
j is set
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg ((n | f),j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
LSeg (n,j) is Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n | f) is Element of bool the carrier of (TOP-REAL 2)
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg ((n | f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n | f) ) } is set
LSeg (n,f) is Element of bool the carrier of (TOP-REAL 2)
(L~ (n | f)) /\ (LSeg (n,f)) is Element of bool the carrier of (TOP-REAL 2)
n /. f is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
{(n /. f)} is non empty trivial V52() 1 -element set
f - 1 is V22() ext-real V26() set
y is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(n | f) | y is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len ((n | f) | y) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg (((n | f) | y),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((n | f) | y) ) } is set
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len (n | f)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (n | f) -element Element of bool NAT
Seg f is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() f -element Element of bool NAT
dom ((n | f) | y) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len ((n | f) | y)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len ((n | f) | y) -element Element of bool NAT
Seg y is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() y -element Element of bool NAT
L~ ((n | f) | y) is Element of bool the carrier of (TOP-REAL 2)
union { (LSeg (((n | f) | y),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len ((n | f) | y) ) } is set
j is set
j is set
i is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg (((n | f) | y),i) is Element of bool the carrier of (TOP-REAL 2)
i + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
LSeg ((n | f),i) is Element of bool the carrier of (TOP-REAL 2)
LSeg (n,i) is Element of bool the carrier of (TOP-REAL 2)
(L~ ((n | f) | y)) /\ (LSeg (n,f)) is Element of bool the carrier of (TOP-REAL 2)
1 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
y + (1 + 1) is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
y + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
LSeg ((n | f),y) is Element of bool the carrier of (TOP-REAL 2)
(L~ ((n | f) | y)) \/ (LSeg ((n | f),y)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((n | f),y)) /\ (LSeg (n,f)) is Element of bool the carrier of (TOP-REAL 2)
{} \/ ((LSeg ((n | f),y)) /\ (LSeg (n,f))) is set
LSeg (n,y) is Element of bool the carrier of (TOP-REAL 2)
LSeg (n,(y + 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (n,y)) /\ (LSeg (n,(y + 1))) is Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
n ^ f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (n ^ f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
LSeg ((n ^ f),x) is Element of bool the carrier of (TOP-REAL 2)
y is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
y + (len n) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg (f,y) is Element of bool the carrier of (TOP-REAL 2)
(n ^ f) /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(n ^ f) /. (x + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(y + 1) + (len n) is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
len f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(len n) + (len f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f /. (y + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f /. y is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
0 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
LSeg (p,j) is Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ n is Element of bool the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
union { (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
n ^ f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (n ^ f) is Element of bool the carrier of (TOP-REAL 2)
len (n ^ f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg ((n ^ f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n ^ f) ) } is set
union { (LSeg ((n ^ f),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (n ^ f) ) } is set
p is set
j is set
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg (n,j) is Element of bool the carrier of (TOP-REAL 2)
j + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(len n) + (len f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
LSeg ((n ^ f),j) is Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n | f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
r is V17() V21() V22() ext-real non negative V26() V52() cardinal set
y is V17() V21() V22() ext-real non negative V26() V52() cardinal set
y + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
LSeg ((n | f),y) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((n | f),r) is Element of bool the carrier of (TOP-REAL 2)
LSeg (n,y) is Element of bool the carrier of (TOP-REAL 2)
LSeg (n,r) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (n,y)) /\ (LSeg (n,r)) is Element of bool the carrier of (TOP-REAL 2)
r + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
(LSeg ((n | f),y)) /\ (LSeg ((n | f),r)) is Element of bool the carrier of (TOP-REAL 2)
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(LSeg ((n | f),y)) /\ (LSeg ((n | f),r)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((n | f),y)) /\ (LSeg ((n | f),r)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg ((n | f),y)) /\ (LSeg ((n | f),r)) is Element of bool the carrier of (TOP-REAL 2)
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (n | f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (n | f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n /. (len n) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(n /. (len n)) `1 is V22() ext-real V26() Element of REAL
(n /. (len n)) `2 is V22() ext-real V26() Element of REAL
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(f /. 1) `1 is V22() ext-real V26() Element of REAL
(f /. 1) `2 is V22() ext-real V26() Element of REAL
n ^ f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
x is V17() V21() V22() ext-real non negative V26() V52() cardinal set
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
len (n ^ f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(n ^ f) /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((n ^ f) /. x) `1 is V22() ext-real V26() Element of REAL
(n ^ f) /. (x + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((n ^ f) /. (x + 1)) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. x) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. (x + 1)) `2 is V22() ext-real V26() Element of REAL
r is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(n ^ f) /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(n ^ f) /. (r + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
len f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
(len n) + (len f) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
n /. (r + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
n /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r - (len n) is V22() ext-real V26() set
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
n /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((n ^ f) /. r) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `2 is V22() ext-real V26() Element of REAL
(len n) + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(j + 1) + (len n) is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
f /. (j + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j + (len n) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
f /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((n ^ f) /. r) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `1 is V22() ext-real V26() Element of REAL
((n ^ f) /. r) `2 is V22() ext-real V26() Element of REAL
((n ^ f) /. (r + 1)) `2 is V22() ext-real V26() Element of REAL
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis n is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
len (X_axis n) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Y_axis n is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
len (Y_axis n) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis n is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis n is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
f is Relation-like non empty-yielding NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
Indices f is set
x is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
n /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
n /. (x + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
y is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
r is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[y,r] is set
{y,r} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{y} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{y,r},{y}} is V52() V56() set
f * (y,r) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[p,j] is set
{p,j} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p,j},{p}} is V52() V56() set
f * (p,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
Col (f,r) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like M13( the carrier of (TOP-REAL 2),K247((len f), the carrier of (TOP-REAL 2)))
len f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
K247((len f), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
Line (f,p) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like M13( the carrier of (TOP-REAL 2),K247((width f), the carrier of (TOP-REAL 2)))
width f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
K247((width f), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
j is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
i is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis i is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis i is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
len j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom j is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
dom f is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (X_axis i) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len i is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (X_axis i) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len (X_axis i)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (X_axis i) -element Element of bool NAT
len (X_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (X_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (width f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width f -element Element of bool NAT
[:(dom f),(Seg (width f)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
j /. y is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . y is set
(X_axis j) . y is V22() ext-real V26() Element of REAL
(f * (y,r)) `1 is V22() ext-real V26() Element of REAL
j /. p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . p is set
f * (p,r) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(X_axis j) . p is V22() ext-real V26() Element of REAL
(f * (p,r)) `1 is V22() ext-real V26() Element of REAL
dom (Y_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (Y_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg (len (Y_axis j)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (Y_axis j) -element Element of bool NAT
Seg (len (X_axis j)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (X_axis j) -element Element of bool NAT
(Y_axis j) . p is V22() ext-real V26() Element of REAL
(f * (p,r)) `2 is V22() ext-real V26() Element of REAL
dom i is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
i /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i . r is set
(X_axis i) . r is V22() ext-real V26() Element of REAL
i /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i . j is set
(X_axis i) . j is V22() ext-real V26() Element of REAL
(f * (p,j)) `1 is V22() ext-real V26() Element of REAL
len (Y_axis i) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (Y_axis i) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len (Y_axis i)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (Y_axis i) -element Element of bool NAT
(Y_axis i) . r is V22() ext-real V26() Element of REAL
(Y_axis i) . j is V22() ext-real V26() Element of REAL
(f * (p,j)) `2 is V22() ext-real V26() Element of REAL
(Y_axis j) . y is V22() ext-real V26() Element of REAL
(f * (y,r)) `2 is V22() ext-real V26() Element of REAL
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom n is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
L~ n is Element of bool the carrier of (TOP-REAL 2)
len n is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
union { (LSeg (n,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len n ) } is set
n /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
n /. (len n) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f is Relation-like non empty-yielding NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K246( the carrier of (TOP-REAL 2))
Indices f is set
x is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
y is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len y is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom y is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
L~ y is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (y,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len y ) } is set
union { (LSeg (y,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len y ) } is set
y /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y /. (len y) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
Seg (len y) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len y -element Element of bool NAT
{1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element Element of bool REAL
p is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
r is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom r is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
p + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
r /. p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r /. (p + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[j,j] is set
{j,j} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{j} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{j,j},{j}} is V52() V56() set
i is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
i is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[i,i] is set
{i,i} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{i} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{i,i},{i}} is V52() V56() set
f * (j,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (i,i) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j - i is V22() ext-real V26() set
abs (j - i) is V22() ext-real V26() Element of REAL
j - i is V22() ext-real V26() set
abs (j - i) is V22() ext-real V26() Element of REAL
(abs (j - i)) + (abs (j - i)) is V22() ext-real V26() set
L~ r is Element of bool the carrier of (TOP-REAL 2)
len r is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg (r,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len r ) } is set
union { (LSeg (r,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len r ) } is set
r /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r /. (len r) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
0 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
Seg x is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() x -element Element of bool NAT
y /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
p is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[r,p] is set
{r,p} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{r} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{r,p},{r}} is V52() V56() set
f * (r,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
Line (f,r) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like M13( the carrier of (TOP-REAL 2),K247((width f), the carrier of (TOP-REAL 2)))
width f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
K247((width f), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
Col (f,p) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like M13( the carrier of (TOP-REAL 2),K247((len f), the carrier of (TOP-REAL 2)))
len f is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
K247((len f), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
j is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
j is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis j is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (Y_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (Y_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg (len (Y_axis j)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (Y_axis j) -element Element of bool NAT
len j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len (Y_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len j is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (Y_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
dom j is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (X_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (X_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
y | x is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (y | x) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom (y | x) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len (y | x)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (y | x) -element Element of bool NAT
g1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
y /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j2 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[j1,j2] is set
{j1,j2} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{j1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{j1,j2},{j1}} is V52() V56() set
f * (j1,j2) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ppi is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
pj is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[ppi,pj] is set
{ppi,pj} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{ppi} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{ppi,pj},{ppi}} is V52() V56() set
(y | x) /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (ppi,pj) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g1 is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g1 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(y | x) /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((y | x) /. g1) `1 is V22() ext-real V26() Element of REAL
(y | x) /. (g1 + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
((y | x) /. (g1 + 1)) `1 is V22() ext-real V26() Element of REAL
((y | x) /. g1) `2 is V22() ext-real V26() Element of REAL
((y | x) /. (g1 + 1)) `2 is V22() ext-real V26() Element of REAL
y /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y /. (g1 + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
g1 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
(y | x) /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y /. g1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(y | x) /. (g1 + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y /. (g1 + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
L~ (y | x) is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg ((y | x),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (y | x) ) } is set
union { (LSeg ((y | x),b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len (y | x) ) } is set
(y | x) /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(y | x) /. (len (y | x)) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g1 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
{ (LSeg (g1,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
g1 /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g1 /. (len g1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
dom g1 is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
j1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
g1 /. j1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j1 + 1 is non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
j2 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
ppi is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[j2,ppi] is set
{j2,ppi} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{j2} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{j2,ppi},{j2}} is V52() V56() set
pj is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
lk is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[pj,lk] is set
{pj,lk} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{pj} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{pj,lk},{pj}} is V52() V56() set
g1 /. j1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (j2,ppi) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g1 /. (j1 + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (pj,lk) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j2 - pj is V22() ext-real V26() set
abs (j2 - pj) is V22() ext-real V26() Element of REAL
ppi - lk is V22() ext-real V26() set
abs (ppi - lk) is V22() ext-real V26() Element of REAL
(abs (j2 - pj)) + (abs (ppi - lk)) is V22() ext-real V26() set
dom (X_axis j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (X_axis j) is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg (len (X_axis j)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (X_axis j) -element Element of bool NAT
dom f is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
y /. (x + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j1 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
j2 is V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
[j1,j2] is set
{j1,j2} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{j1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{j1,j2},{j1}} is V52() V56() set
f * (j1,j2) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
Seg (width f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width f -element Element of bool NAT
[:(dom f),(Seg (width f)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
Seg (len g1) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len g1 -element Element of bool NAT
f * (r,j2) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
dom j is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
j /. j2 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . j2 is set
(Y_axis j) . j2 is V22() ext-real V26() Element of REAL
(f * (r,j2)) `2 is V22() ext-real V26() Element of REAL
j /. p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . p is set
(Y_axis j) . p is V22() ext-real V26() Element of REAL
(f * (r,p)) `2 is V22() ext-real V26() Element of REAL
(X_axis j) . j2 is V22() ext-real V26() Element of REAL
(f * (r,j2)) `1 is V22() ext-real V26() Element of REAL
(X_axis j) . p is V22() ext-real V26() Element of REAL
(f * (r,p)) `1 is V22() ext-real V26() Element of REAL
p - j2 is V22() ext-real V26() set
{ b1 where b1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b1 `1 = (f * (r,p)) `1 & (f * (r,j2)) `2 <= b1 `2 & b1 `2 <= (f * (r,p)) `2 ) } is set
|[((f * (r,p)) `1),((f * (r,p)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the