:: GOBOARD2 semantic presentation

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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len (n | f) ) } is set
union { (LSeg ((n | f),b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len (n ^ f) ) } is set
union { (LSeg ((n ^ f),b₁)) where b₁ 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 <= b₁ & b₁ + 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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len n ) } is set
union { (LSeg (n,b₁)) where b₁ 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 <= b₁ & b₁ + 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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len y ) } is set
union { (LSeg (y,b₁)) where b₁ 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 <= b₁ & b₁ + 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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len r ) } is set
union { (LSeg (r,b₁)) where b₁ 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 <= b₁ & b₁ + 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),b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len (y | x) ) } is set
union { (LSeg ((y | x),b₁)) where b₁ 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 <= b₁ & b₁ + 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,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len g1 ) } is set
union { (LSeg (g1,b₁)) where b₁ 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 <= b₁ & b₁ + 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
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (f * (r,p)) `1 & (f * (r,j2)) `2 <= b<sub>1</sub> `2 & b₁ `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 carrier of (TOP-REAL 2)
g2 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
Seg lk is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() lk -element Element of bool NAT
p - g2 is V22() ext-real V26() set
g 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 - lk is V22() ext-real V26() set
[r,(p - g2)] is set
{r,(p - g2)} is V45() V46() V47() V52() V63() V64() V65() set
{{r,(p - g2)},{r}} is V52() V56() set
g2 is V17() V21() V22() ext-real non negative V26() V52() cardinal set
p - g2 is V22() ext-real V26() set
g 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 * (r,g) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf 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 * (r,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 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 g2 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 ^ g2 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 g2 is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
lg + 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 - lg is V22() ext-real V26() set
p - (lg + 1) is V22() ext-real V26() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
ma 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
qa 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
[ma,qa] is set
{ma,qa} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{ma} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{ma,qa},{ma}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (ma,qa) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[r,(p - (lg + 1))] is set
{r,(p - (lg + 1))} is V45() V46() V47() V52() V63() V64() V65() set
{{r,(p - (lg + 1))},{r}} is V52() V56() 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
f * (r,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[r,(p - lg)] is set
{r,(p - lg)} is V45() V46() V47() V52() V63() V64() V65() set
{{r,(p - lg)},{r}} is V52() V56() set
lf 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 * (r,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p1 - ma is V22() ext-real V26() set
abs (p1 - ma) is V22() ext-real V26() Element of REAL
ma - qa is V22() ext-real V26() set
abs (ma - qa) is V22() ext-real V26() Element of REAL
(abs (p1 - ma)) + (abs (ma - qa)) is V22() ext-real V26() set
(p - lg) - (p - (lg + 1)) is V22() ext-real V26() set
abs ((p - lg) - (p - (lg + 1))) is V22() ext-real V26() Element of REAL
0 + (abs ((p - lg) - (p - (lg + 1)))) is V22() ext-real V26() set
lg 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 - lg is V22() ext-real V26() set
lf 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g 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 g is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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
lf 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
[lg,lf] is set
{lg,lf} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lg} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lg,lf},{lg}} is V52() V56() 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
f * (lg,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p - 1 is V22() ext-real V26() set
[r,(p - 1)] is set
{r,(p - 1)} is V45() V46() V47() V52() V63() V64() V65() set
{{r,(p - 1)},{r}} is V52() V56() set
ma 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 * (r,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg - x is V22() ext-real V26() set
abs (lg - x) is V22() ext-real V26() Element of REAL
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V22() ext-real V26() set
p - (p - 1) is V22() ext-real V26() set
abs (p - (p - 1)) is V22() ext-real V26() Element of REAL
0 + (abs (p - (p - 1))) is V22() ext-real V26() set
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
|[((f * (r,j2)) `1),((f * (r,j2)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (y,x) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (r,j2)),(f * (r,p))) is Element of bool the carrier of (TOP-REAL 2)
L~ g is Element of bool the carrier of (TOP-REAL 2)
len g 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 (g,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ 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 <= b₁ & b₁ + 1 <= len g ) } is set
(len g1) + (len g2) 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
p1 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
p1 - (len g1) is V22() ext-real V26() set
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
Seg (len j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len j -element Element of bool NAT
g /. (len g1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma 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
ma + (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
p - ma is V22() ext-real V26() set
g2 /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa 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 * (r,qa) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . qa is set
(Y_axis j) . qa is V22() ext-real V26() Element of REAL
(f * (r,qa)) `2 is V22() ext-real V26() Element of REAL
(X_axis j) . qa is V22() ext-real V26() Element of REAL
(f * (r,qa)) `1 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
p - (len g2) is V22() ext-real V26() set
ma `2 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
p1 is set
ma is set
ma 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 (g,ma) is Element of bool the carrier of (TOP-REAL 2)
ma + 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 (g1,ma) is Element of bool the carrier of (TOP-REAL 2)
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `1 is V22() ext-real V26() Element of REAL
qa `2 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
qa1 `2 is V22() ext-real V26() Element of REAL
|[(qa `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
|[(qa `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (qa1,qa) is Element of bool the carrier of (TOP-REAL 2)
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = qa `1 & qa1 `2 <= b₁ `2 & b<sub>1</sub> `2 <= qa `2 ) } is set
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
lma `2 is V22() ext-real V26() Element of REAL
{qa} is non empty trivial V52() 1 -element set
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = qa `1 & qa `2 <= b₁ `2 & b<sub>1</sub> `2 <= qa1 `2 ) } is set
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
lma `2 is V22() ext-real V26() Element of REAL
p1 is set
(L~ (y | x)) \/ (LSeg (y,x)) is Element of bool the carrier of (TOP-REAL 2)
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
qa is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa 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 + 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
qa - 1 is V22() ext-real V26() set
qa1 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
qa1 + 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 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
g /. qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (f * (r,p)) `1 & (f * (r,j2)) `2 <= b₁ `2 & b<sub>1</sub> `2 <= lma `2 ) } is set
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. lk is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
|[(lma `1),(lma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa1) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (r,j2)),lma) is Element of bool the carrier of (TOP-REAL 2)
qa 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
qa + 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
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (qa + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (f * (r,p)) `1 & lma `2 <= b<sub>1</sub> `2 & b₁ `2 <= qa1 `2 ) } is set
lma `1 is V22() ext-real V26() Element of REAL
|[(lma `1),(lma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
c<sub>33</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
c<sub>33</sub> `2 is V22() ext-real V26() Element of REAL
qa1 `1 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the carrier of (TOP-REAL 2)
LSeg (lma,qa1) is Element of bool the carrier of (TOP-REAL 2)
qa 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
g /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(len g1) + (len g2) 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 + 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
g /. (len g) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. lk is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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 * (r,lg) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(f * (r,p)) `1 is V22() ext-real V26() Element of REAL
(f * (r,p)) `2 is V22() ext-real V26() Element of REAL
(f * (r,j2)) `2 is V22() ext-real V26() Element of REAL
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (f * (r,p)) `1 & (f * (r,p)) `2 <= b<sub>1</sub> `2 & b₁ `2 <= (f * (r,j2)) `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 carrier of (TOP-REAL 2)
j2 - p is V22() ext-real V26() set
l 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
g2 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 g2 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 g2 is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
g1 ^ g2 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)
lg 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 + lg 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 l is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() l -element Element of bool NAT
l + 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 + lg)] is set
{r,(p + lg)} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{r,(p + lg)},{r}} is V52() V56() set
Seg (len g2) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len g2 -element Element of bool NAT
lg 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 + lg 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g 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 g is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p + (lg + 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 * (r,(p + (lg + 1))) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[r,(p + (lg + 1))] is set
{r,(p + (lg + 1))} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{r,(p + (lg + 1))},{r}} is V52() V56() set
p + lg 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 * (r,(p + lg)) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[r,(p + lg)] is set
{r,(p + lg)} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{r,(p + lg)},{r}} is V52() V56() set
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
(p + lg) - (p + (lg + 1)) is V22() ext-real V26() set
abs ((p + lg) - (p + (lg + 1))) is V22() ext-real V26() Element of REAL
0 + (abs ((p + lg) - (p + (lg + 1)))) is V22() ext-real V26() set
- 1 is V22() ext-real non positive V26() set
abs (- 1) is V22() ext-real V26() Element of REAL
abs 1 is V22() ext-real V26() Element of REAL
lg 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
lf 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
[lg,lf] is set
{lg,lf} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lg} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lg,lf},{lg}} is V52() V56() 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
f * (lg,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
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
f * (r,(p + 1)) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[r,(p + 1)] is set
{r,(p + 1)} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{r,(p + 1)},{r}} is V52() V56() set
lg - x is V22() ext-real V26() set
abs (lg - x) is V22() ext-real V26() Element of REAL
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V22() ext-real V26() set
p - (p + 1) is V22() ext-real V26() set
abs (p - (p + 1)) is V22() ext-real V26() Element of REAL
0 + (abs (p - (p + 1))) is V22() ext-real V26() set
p - p is V22() ext-real V26() set
(p - p) + (- 1) is V22() ext-real V26() set
abs ((p - p) + (- 1)) is V22() ext-real V26() Element of REAL
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
(f * (r,j2)) `1 is V22() ext-real V26() Element of REAL
|[((f * (r,j2)) `1),((f * (r,j2)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-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
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
(X_axis j) . j2 is V22() ext-real V26() Element of REAL
(X_axis j) . p is V22() ext-real V26() Element of REAL
LSeg (y,x) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (r,p)),(f * (r,j2))) is Element of bool the carrier of (TOP-REAL 2)
L~ g is Element of bool the carrier of (TOP-REAL 2)
len g 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 (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
(len g1) + (len g2) 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 - (len g1) is V22() ext-real V26() set
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p1 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 + p1 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 j) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len j -element Element of bool NAT
g /. (len g1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
p1 + (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
g2 /. p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. (p + p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . (p + p1) is set
f * (r,(p + p1)) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(Y_axis j) . (p + p1) is V22() ext-real V26() Element of REAL
(f * (r,(p + p1))) `2 is V22() ext-real V26() Element of REAL
(X_axis j) . (p + p1) is V22() ext-real V26() Element of REAL
(f * (r,(p + p1))) `1 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
p + l 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
rng j is V52() set
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
rng j is V52() set
x is set
p1 is set
ma 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 (g,ma) is Element of bool the carrier of (TOP-REAL 2)
ma + 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 (g1,ma) is Element of bool the carrier of (TOP-REAL 2)
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `1 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `1 is V22() ext-real V26() Element of REAL
qa `2 is V22() ext-real V26() Element of REAL
|[(ma `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
|[(ma `1),(ma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (qa,ma) is Element of bool the carrier of (TOP-REAL 2)
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = ma `1 & qa `2 <= b₁ `2 & b<sub>1</sub> `2 <= ma `2 ) } is set
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
qa1 `2 is V22() ext-real V26() Element of REAL
{ma} is non empty trivial V52() 1 -element set
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = ma `1 & ma `2 <= b₁ `2 & b<sub>1</sub> `2 <= qa `2 ) } is set
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
qa1 `2 is V22() ext-real V26() Element of REAL
x is set
(L~ (y | x)) \/ (LSeg (y,x)) is Element of bool the carrier of (TOP-REAL 2)
p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p1 `1 is V22() ext-real V26() Element of REAL
p1 `2 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `2 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma 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
ma - 1 is V22() ext-real V26() set
qa 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
qa + 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 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
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (f * (r,p)) `1 & qa1 `2 <= b₁ `2 & b<sub>1</sub> `2 <= (f * (r,j2)) `2 ) } is set
p + l 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
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. l is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (r,j2)),qa1) is Element of bool the carrier of (TOP-REAL 2)
ma 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
ma + 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
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `2 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = (f * (r,p)) `1 & qa `2 <= b<sub>1</sub> `2 & b₁ `2 <= qa1 `2 ) } is set
qa1 `1 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
qa `1 is V22() ext-real V26() Element of REAL
|[(qa `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,ma) is Element of bool the carrier of (TOP-REAL 2)
LSeg (qa,qa1) is Element of bool the carrier of (TOP-REAL 2)
ma 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
g /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(len g1) + l 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
g /. (len g) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. l is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p + l 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 * (r,(p + l)) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lk 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~ lk is Element of bool the carrier of (TOP-REAL 2)
len 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
{ (LSeg (lk,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len lk ) } is set
union { (LSeg (lk,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len lk ) } is set
lk /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lk /. (len lk) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
l 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~ l is Element of bool the carrier of (TOP-REAL 2)
len l 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 (l,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len l ) } is set
union { (LSeg (l,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len l ) } is set
l /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
l /. (len l) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (j1,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. j1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . j1 is set
(X_axis j) . j1 is V22() ext-real V26() Element of REAL
(f * (j1,p)) `1 is V22() ext-real V26() Element of REAL
j /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . r is set
(X_axis j) . r is V22() ext-real V26() Element of REAL
(f * (r,p)) `1 is V22() ext-real V26() Element of REAL
(Y_axis j) . j1 is V22() ext-real V26() Element of REAL
(f * (j1,p)) `2 is V22() ext-real V26() Element of REAL
(Y_axis j) . r is V22() ext-real V26() Element of REAL
(f * (r,p)) `2 is V22() ext-real V26() Element of REAL
r - j1 is V22() ext-real V26() set
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (f * (r,p)) `2 & (f * (j1,p)) `1 <= b₁ `1 & b<sub>1</sub> `1 <= (f * (r,p)) `1 ) } 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 carrier of (TOP-REAL 2)
g2 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
Seg lk is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() lk -element Element of bool NAT
r - g2 is V22() ext-real V26() set
g 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 - lk is V22() ext-real V26() set
[(r - g2),p] is set
{(r - g2),p} is V45() V46() V47() V52() V63() V64() V65() set
{(r - g2)} is non empty trivial V45() V46() V47() V52() V61() V62() V63() V64() V65() 1 -element set
{{(r - g2),p},{(r - g2)}} is V52() V56() set
g2 is V17() V21() V22() ext-real non negative V26() V52() cardinal set
r - g2 is V22() ext-real V26() set
g 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 * (g,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf 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 * (lf,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 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 g2 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 ^ g2 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 g2 is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
lg + 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 - lg is V22() ext-real V26() set
r - (lg + 1) is V22() ext-real V26() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
ma 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
qa 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
[ma,qa] is set
{ma,qa} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{ma} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{ma,qa},{ma}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (ma,qa) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[(r - (lg + 1)),p] is set
{(r - (lg + 1)),p} is V45() V46() V47() V52() V63() V64() V65() set
{(r - (lg + 1))} is non empty trivial V45() V46() V47() V52() V61() V62() V63() V64() V65() 1 -element set
{{(r - (lg + 1)),p},{(r - (lg + 1))}} is V52() V56() 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
f * (x,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[(r - lg),p] is set
{(r - lg),p} is V45() V46() V47() V52() V63() V64() V65() set
{(r - lg)} is non empty trivial V45() V46() V47() V52() V61() V62() V63() V64() V65() 1 -element set
{{(r - lg),p},{(r - lg)}} is V52() V56() set
lf 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 * (lf,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p1 - ma is V22() ext-real V26() set
abs (p1 - ma) is V22() ext-real V26() Element of REAL
ma - qa is V22() ext-real V26() set
abs (ma - qa) is V22() ext-real V26() Element of REAL
(abs (p1 - ma)) + (abs (ma - qa)) is V22() ext-real V26() set
(r - lg) - (r - (lg + 1)) is V22() ext-real V26() set
abs ((r - lg) - (r - (lg + 1))) is V22() ext-real V26() Element of REAL
(abs ((r - lg) - (r - (lg + 1)))) + 0 is V22() ext-real V26() set
lg 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 - lg is V22() ext-real V26() set
lf 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g 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 g is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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
lf 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
[lg,lf] is set
{lg,lf} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lg} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lg,lf},{lg}} is V52() V56() 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
f * (lg,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r - 1 is V22() ext-real V26() set
[(r - 1),p] is set
{(r - 1),p} is V45() V46() V47() V52() V63() V64() V65() set
{(r - 1)} is non empty trivial V45() V46() V47() V52() V61() V62() V63() V64() V65() 1 -element set
{{(r - 1),p},{(r - 1)}} is V52() V56() set
ma 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 * (ma,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg - x is V22() ext-real V26() set
abs (lg - x) is V22() ext-real V26() Element of REAL
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V22() ext-real V26() set
r - (r - 1) is V22() ext-real V26() set
abs (r - (r - 1)) is V22() ext-real V26() Element of REAL
(abs (r - (r - 1))) + 0 is V22() ext-real V26() set
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
|[((f * (j1,p)) `1),((f * (j1,p)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (y,x) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (j1,p)),(f * (r,p))) is Element of bool the carrier of (TOP-REAL 2)
L~ g is Element of bool the carrier of (TOP-REAL 2)
len g 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 (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
(len g1) + (len g2) 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
p1 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
p1 - (len g1) is V22() ext-real V26() set
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (len g1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma 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
ma + (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
r - ma is V22() ext-real V26() set
g2 /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa 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 * (qa,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . qa is set
(X_axis j) . qa is V22() ext-real V26() Element of REAL
(f * (qa,p)) `1 is V22() ext-real V26() Element of REAL
(Y_axis j) . qa is V22() ext-real V26() Element of REAL
(f * (qa,p)) `2 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
r - (len g2) is V22() ext-real V26() set
ma `1 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
p1 is set
ma is set
ma 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 (g,ma) is Element of bool the carrier of (TOP-REAL 2)
ma + 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 (g1,ma) is Element of bool the carrier of (TOP-REAL 2)
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `2 is V22() ext-real V26() Element of REAL
qa `1 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
qa1 `1 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
|[(qa `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (qa1,qa) is Element of bool the carrier of (TOP-REAL 2)
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = qa `2 & qa1 `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa `1 ) } is set
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
lma `1 is V22() ext-real V26() Element of REAL
{qa} is non empty trivial V52() 1 -element set
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = qa `2 & qa `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa1 `1 ) } is set
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
lma `1 is V22() ext-real V26() Element of REAL
p1 is set
(L~ (y | x)) \/ (LSeg (y,x)) is Element of bool the carrier of (TOP-REAL 2)
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
qa is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa 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
qa - 1 is V22() ext-real V26() set
qa1 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
qa1 + 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 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
g /. qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = (f * (r,p)) `2 & (f * (j1,p)) `1 <= b<sub>1</sub> `1 & b₁ `1 <= lma `1 ) } is set
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. lk is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `2 is V22() ext-real V26() Element of REAL
|[(lma `1),(lma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa1) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (j1,p)),lma) is Element of bool the carrier of (TOP-REAL 2)
qa 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
qa + 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
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (qa + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (f * (r,p)) `2 & lma `1 <= b₁ `1 & b<sub>1</sub> `1 <= qa1 `1 ) } is set
lma `2 is V22() ext-real V26() Element of REAL
|[(lma `1),(lma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
c₃₃ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
c₃₃ `1 is V22() ext-real V26() Element of REAL
qa1 `2 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the carrier of (TOP-REAL 2)
LSeg (lma,qa1) is Element of bool the carrier of (TOP-REAL 2)
qa 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
g /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(len g1) + (len g2) 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
g /. (len g) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. lk is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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 * (lg,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(f * (r,p)) `2 is V22() ext-real V26() Element of REAL
(f * (r,p)) `1 is V22() ext-real V26() Element of REAL
(f * (j1,p)) `1 is V22() ext-real V26() Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (f * (r,p)) `2 & (f * (r,p)) `1 <= b₁ `1 & b<sub>1</sub> `1 <= (f * (j1,p)) `1 ) } 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 carrier of (TOP-REAL 2)
j1 - r is V22() ext-real V26() set
l 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
g2 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 g2 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 g2 is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
g1 ^ g2 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)
lg 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 + lg 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 l is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() l -element Element of bool NAT
l + 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
[(r + lg),p] is set
{(r + lg),p} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{(r + lg)} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{(r + lg),p},{(r + lg)}} is V52() V56() set
Seg (len g2) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len g2 -element Element of bool NAT
lg 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 + lg 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g 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 g is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
lg 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
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g2 /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r + (lg + 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 * ((r + (lg + 1)),p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[(r + (lg + 1)),p] is set
{(r + (lg + 1)),p} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{(r + (lg + 1))} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{(r + (lg + 1)),p},{(r + (lg + 1))}} is V52() V56() set
r + lg 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 * ((r + lg),p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[(r + lg),p] is set
{(r + lg),p} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{(r + lg)} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{(r + lg),p},{(r + lg)}} is V52() V56() set
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
(r + lg) - (r + (lg + 1)) is V22() ext-real V26() set
abs ((r + lg) - (r + (lg + 1))) is V22() ext-real V26() Element of REAL
(abs ((r + lg) - (r + (lg + 1)))) + 0 is V22() ext-real V26() set
- 1 is V22() ext-real non positive V26() set
abs (- 1) is V22() ext-real V26() Element of REAL
abs 1 is V22() ext-real V26() Element of REAL
lg 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
lf 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
[lg,lf] is set
{lg,lf} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lg} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lg,lf},{lg}} is V52() V56() 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
p1 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,p1] is set
{x,p1} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,p1},{x}} is V52() V56() set
f * (lg,lf) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (x,p1) 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
f * ((r + 1),p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
[(r + 1),p] is set
{(r + 1),p} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{(r + 1)} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{(r + 1),p},{(r + 1)}} is V52() V56() set
lg - x is V22() ext-real V26() set
abs (lg - x) is V22() ext-real V26() Element of REAL
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V22() ext-real V26() set
r - (r + 1) is V22() ext-real V26() set
abs (r - (r + 1)) is V22() ext-real V26() Element of REAL
(abs (r - (r + 1))) + 0 is V22() ext-real V26() set
r - r is V22() ext-real V26() set
(r - r) + (- 1) is V22() ext-real V26() set
abs ((r - r) + (- 1)) is V22() ext-real V26() Element of REAL
lg 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
lg + 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
lf 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
[lf,x] is set
{lf,x} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{lf} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{lf,x},{lf}} is V52() V56() set
p1 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
ma 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
[p1,ma] is set
{p1,ma} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{p1} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{p1,ma},{p1}} is V52() V56() set
g /. lg is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (lf,x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (lg + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p1,ma) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lf - p1 is V22() ext-real V26() set
abs (lf - p1) is V22() ext-real V26() Element of REAL
x - ma is V22() ext-real V26() set
abs (x - ma) is V22() ext-real V26() Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V22() ext-real V26() set
(f * (j1,p)) `2 is V22() ext-real V26() Element of REAL
|[((f * (j1,p)) `1),((f * (j1,p)) `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
j /. j1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . j1 is set
(X_axis j) . j1 is V22() ext-real V26() Element of REAL
j /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . r is set
(X_axis j) . r is V22() ext-real V26() Element of REAL
(Y_axis j) . j1 is V22() ext-real V26() Element of REAL
(Y_axis j) . r is V22() ext-real V26() Element of REAL
LSeg (y,x) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (r,p)),(f * (j1,p))) is Element of bool the carrier of (TOP-REAL 2)
L~ g is Element of bool the carrier of (TOP-REAL 2)
len g 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 (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
(len g1) + (len g2) 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 - (len g1) is V22() ext-real V26() set
p1 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 + p1 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
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. x is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (len g1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
p1 + (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
g2 /. p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j /. (r + p1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
j . (r + p1) is set
f * ((r + p1),p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(X_axis j) . (r + p1) is V22() ext-real V26() Element of REAL
(f * ((r + p1),p)) `1 is V22() ext-real V26() Element of REAL
(Y_axis j) . (r + p1) is V22() ext-real V26() Element of REAL
(f * ((r + p1),p)) `2 is V22() ext-real V26() Element of REAL
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
r + l 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
rng j is V52() set
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
rng j is V52() set
x is set
p1 is set
ma 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 (g,ma) is Element of bool the carrier of (TOP-REAL 2)
ma + 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 (g1,ma) is Element of bool the carrier of (TOP-REAL 2)
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma `2 is V22() ext-real V26() Element of REAL
ma `1 is V22() ext-real V26() Element of REAL
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `2 is V22() ext-real V26() Element of REAL
qa `1 is V22() ext-real V26() Element of REAL
|[(qa `1),(ma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
|[(ma `1),(ma `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (qa,ma) is Element of bool the carrier of (TOP-REAL 2)
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = ma `2 & qa `1 <= b₁ `1 & b<sub>1</sub> `1 <= ma `1 ) } is set
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
qa1 `1 is V22() ext-real V26() Element of REAL
{ma} is non empty trivial V52() 1 -element set
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = ma `2 & ma `1 <= b₁ `1 & b<sub>1</sub> `1 <= qa `1 ) } is set
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
qa1 `1 is V22() ext-real V26() Element of REAL
x is set
(L~ (y | x)) \/ (LSeg (y,x)) is Element of bool the carrier of (TOP-REAL 2)
p1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p1 `2 is V22() ext-real V26() Element of REAL
p1 `1 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `1 is V22() ext-real V26() Element of REAL
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma is V17() V21() V22() ext-real non negative V26() V52() cardinal set
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ma 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
ma - 1 is V22() ext-real V26() set
qa 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
qa + 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 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
g /. qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (f * (r,p)) `2 & qa1 `1 <= b₁ `1 & b<sub>1</sub> `1 <= (f * (j1,p)) `1 ) } is set
r + l 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
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. l is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `2 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f * (j1,p)),qa1) is Element of bool the carrier of (TOP-REAL 2)
ma 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
ma + 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
g /. ma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g /. (ma + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa `1 is V22() ext-real V26() Element of REAL
qa1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
qa1 `1 is V22() ext-real V26() Element of REAL
{ b₁ where b₁ is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2) : ( b₁ `2 = (f * (r,p)) `2 & qa `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa1 `1 ) } is set
qa1 `2 is V22() ext-real V26() Element of REAL
|[(qa1 `1),(qa1 `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
lma is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lma `1 is V22() ext-real V26() Element of REAL
qa `2 is V22() ext-real V26() Element of REAL
|[(qa `1),(qa `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
LSeg (g,ma) is Element of bool the carrier of (TOP-REAL 2)
LSeg (qa,qa1) is Element of bool the carrier of (TOP-REAL 2)
ma 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
g /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(len g1) + l 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
g /. (len g) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
g2 /. l is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r + l 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 * ((r + l),p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lk 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~ lk is Element of bool the carrier of (TOP-REAL 2)
len 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
{ (LSeg (lk,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len lk ) } is set
union { (LSeg (lk,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len lk ) } is set
lk /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
lk /. (len lk) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
l 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~ l is Element of bool the carrier of (TOP-REAL 2)
len l 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 (l,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len l ) } is set
union { (LSeg (l,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len l ) } is set
l /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
l /. (len l) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ppi 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~ ppi is Element of bool the carrier of (TOP-REAL 2)
len 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
{ (LSeg (ppi,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len ppi ) } is set
union { (LSeg (ppi,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len ppi ) } is set
ppi /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
ppi /. (len ppi) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
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)
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,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len r ) } is set
union { (LSeg (r,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 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)
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 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 x is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
L~ x is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (x,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len x ) } is set
union { (LSeg (x,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len x ) } is set
x /. 1 is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
x /. (len x) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
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)
L~ y is Element of bool 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
{ (LSeg (y,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len y ) } is set
union { (LSeg (y,b<sub>1</sub>)) where b<sub>1</sub> 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 <= b<sub>1</sub> & b<sub>1</sub> + 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)
dom y is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool 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
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
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
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
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
[j,i] is set
{j,i} 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,i},{j}} is V52() V56() set
y /. r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (p,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
y /. (r + 1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f * (j,i) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p - j is V22() ext-real V26() set
abs (p - j) 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 (p - j)) + (abs (j - i)) is V22() ext-real V26() set
n is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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 REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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
dom f is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
[:(dom n),(dom f):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
Seg (len n) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len n -element Element of bool NAT
Seg (len f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len f -element Element of bool NAT
[:(Seg (len n)),(Seg (len f)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
x 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
[x,y] is set
{x,y} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{x} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{x,y},{x}} is V52() V56() set
n . x is V22() ext-real V26() Element of REAL
f . y 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 . r is V22() ext-real V26() Element of 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
f . p is V22() ext-real V26() Element of REAL
j is V22() ext-real V26() Element of REAL
j is V22() ext-real V26() Element of REAL
|[j,j]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
x is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular Matrix of len n, len f, the carrier of (TOP-REAL 2)
Indices x is set
y is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular FinSequence of K246( 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
width 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
Indices y is set
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 . r is V22() ext-real V26() Element of 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,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
y * (r,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
f . p is V22() ext-real V26() Element of REAL
|[(n . r),(f . p)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
x is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular FinSequence of K246( the carrier of (TOP-REAL 2))
len 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
width 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
Indices x is set
y is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular FinSequence of K246( 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
width 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
Indices y is set
dom x is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (width x) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width x -element Element of bool NAT
[:(dom x),(Seg (width x)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
dom y is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (width y) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width y -element Element of bool NAT
[:(dom y),(Seg (width y)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
p is V17() V21() V22() ext-real non negative V26() V52() cardinal set
r is V17() V21() V22() ext-real non negative V26() V52() cardinal set
Seg (len x) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len x -element Element of bool NAT
Seg (len y) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len y -element Element of bool 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
n . j is V22() ext-real V26() Element of REAL
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
f . j is V22() ext-real V26() Element of REAL
[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
x * (r,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
y * (r,p) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(n,f) is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular FinSequence of K246( 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 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
dom n is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
width (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 f 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
Indices (n,f) is set
Seg (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
[:(dom n),(Seg (len f)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() 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
Line ((n,f),y) 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 (n,f)), the carrier of (TOP-REAL 2)))
K247((width (n,f)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
X_axis (Line ((n,f),y)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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)
X_axis r is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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
dom (X_axis r) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (X_axis 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
Seg (len (X_axis r)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (X_axis r) -element Element of bool NAT
dom r is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool 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 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 . y is V22() ext-real V26() Element of REAL
f . j is V22() ext-real V26() Element of REAL
f . j is V22() ext-real V26() Element of REAL
[y,j] is set
{y,j} 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,j},{y}} is V52() V56() set
(n,f) * (y,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (y,j)) `1 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(X_axis r) . j is V22() ext-real V26() Element of REAL
[y,j] is set
{y,j} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{y,j},{y}} is V52() V56() set
(n,f) * (y,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
s2 is V22() ext-real V26() Element of REAL
|[i,s2]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (y,j)) `1 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(X_axis r) . j is V22() ext-real V26() Element of REAL
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
Seg (width (n,f)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width (n,f) -element Element of bool NAT
Col ((n,f),y) 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 (n,f)), the carrier of (TOP-REAL 2)))
K247((len (n,f)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
Y_axis (Col ((n,f),y)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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)
Y_axis r is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
len (Y_axis 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
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
dom (Y_axis r) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
dom r is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool 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 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 is V22() ext-real V26() Element of REAL
n . j is V22() ext-real V26() Element of REAL
n . j is V22() ext-real V26() Element of REAL
[j,y] is set
{j,y} 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,y},{j}} is V52() V56() set
(n,f) * (j,y) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (j,y)) `2 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(Y_axis r) . j is V22() ext-real V26() Element of REAL
[j,y] is set
{j,y} 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,y},{j}} is V52() V56() set
(n,f) * (j,y) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
s2 is V22() ext-real V26() Element of REAL
|[s2,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (j,y)) `2 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(Y_axis r) . j is V22() ext-real V26() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(n,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 FinSequence of K246( the carrier of (TOP-REAL 2))
width (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 f 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
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
dom (n,f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
dom n is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
Indices (n,f) is set
Seg (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
[:(dom n),(Seg (len f)):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
dom f is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool 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
Line ((n,f),y) 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 (n,f)), the carrier of (TOP-REAL 2)))
K247((width (n,f)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
Y_axis (Line ((n,f),y)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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)
Y_axis r is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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
dom (Y_axis r) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
len (Y_axis 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
Seg (len (Y_axis r)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (Y_axis r) -element Element of bool NAT
dom r is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool 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 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 . y is V22() ext-real V26() Element of REAL
f . j is V22() ext-real V26() Element of REAL
f . j is V22() ext-real V26() Element of REAL
[y,j] is set
{y,j} 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,j},{y}} is V52() V56() set
(n,f) * (y,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
s2 is V22() ext-real V26() Element of REAL
|[i,s2]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (y,j)) `2 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(Y_axis r) . j is V22() ext-real V26() Element of REAL
[y,j] is set
{y,j} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{y,j},{y}} is V52() V56() set
(n,f) * (y,j) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (y,j)) `2 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(Y_axis r) . j is V22() ext-real V26() Element of REAL
Seg (len n) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len n -element Element of bool 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
Seg (width (n,f)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width (n,f) -element Element of bool NAT
Col ((n,f),y) 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 (n,f)), the carrier of (TOP-REAL 2)))
K247((len (n,f)), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M12( the carrier of (TOP-REAL 2))
X_axis (Col ((n,f),y)) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
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)
X_axis r is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
len (X_axis 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
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
dom (X_axis r) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
dom r is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
Seg (len (X_axis r)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() len (X_axis r) -element Element of bool 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 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 is V22() ext-real V26() Element of REAL
n . j is V22() ext-real V26() Element of REAL
n . j is V22() ext-real V26() Element of REAL
[j,y] is set
{j,y} 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,y},{j}} is V52() V56() set
(n,f) * (j,y) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
s2 is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
|[s2,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (j,y)) `1 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(X_axis r) . j is V22() ext-real V26() Element of REAL
[j,y] is set
{j,y} 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,y},{j}} is V52() V56() set
(n,f) * (j,y) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
i is V22() ext-real V26() Element of REAL
|[i,i]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
((n,f) * (j,y)) `1 is V22() ext-real V26() Element of REAL
r /. j is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r . j is set
(X_axis r) . j is V22() ext-real V26() Element of REAL
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 non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis n)),(Incr (Y_axis n))) 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))
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)
(n) is Relation-like NAT -defined K246( the carrier of (TOP-REAL 2)) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular FinSequence of K246( the carrier of (TOP-REAL 2))
X_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis n)),(Incr (Y_axis n))) 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))
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)
(n) 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))
X_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis n)),(Incr (Y_axis n))) 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))
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
rng (X_axis n) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
card (rng (X_axis 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
width (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
rng (Y_axis n) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
card (rng (Y_axis 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 (Incr (X_axis 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 (Incr (Y_axis 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
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)
dom n is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
(n) 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))
X_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis n is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis n) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis n)),(Incr (Y_axis n))) 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 (n) is 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 /. y is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
rng (Incr (Y_axis n)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (Y_axis n) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
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
Seg (len n) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len n -element Element of bool NAT
dom (Y_axis n) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (Y_axis 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
Seg (len (Y_axis n)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (Y_axis n) -element Element of bool NAT
(Y_axis n) . y is V22() ext-real V26() Element of REAL
r is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
r `2 is V22() ext-real V26() Element of REAL
dom (Incr (Y_axis n)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
p is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (Y_axis n)) . p is V22() ext-real V26() Element of REAL
rng (Incr (X_axis n)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (X_axis n) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (X_axis n) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (X_axis 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
Seg (len (X_axis n)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (X_axis n) -element Element of bool NAT
(X_axis n) . y is V22() ext-real V26() Element of REAL
r `1 is V22() ext-real V26() Element of REAL
dom (Incr (X_axis n)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
j is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (X_axis n)) . j is V22() ext-real V26() Element of REAL
width (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
card (rng (Y_axis 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 (Incr (Y_axis 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
Seg (width (n)) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() width (n) -element Element of bool 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
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
[j,i] is set
{j,i} 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,i},{j}} is V52() V56() set
(n) * (j,i) 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
card (rng (X_axis 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 (Incr (X_axis 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
dom (n) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
[:(dom (n)),(Seg (width (n))):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
|[(r `1),(r `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
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 non empty V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom f is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(X_axis f) . n is V22() ext-real V26() Element of REAL
f /. 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))
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis f)),(Incr (Y_axis 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))
Line ((f),1) 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))
rng (Line ((f),1)) is V52() set
len f 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 (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
dom (X_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (X_axis f) 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 (len (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (X_axis f) -element Element of bool NAT
p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V22() ext-real V26() Element of REAL
rng (Incr (X_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (X_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Incr (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
j is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (X_axis f)) . j is V22() ext-real V26() Element of REAL
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 V22() ext-real V26() set
len (Incr (X_axis f)) 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
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
(Incr (X_axis f)) . i is V22() ext-real V26() Element of REAL
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
i is V22() ext-real V26() Element of REAL
s2 is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(X_axis f) . s2 is V22() ext-real V26() Element of REAL
rng (Incr (Y_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (Y_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Y_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (Y_axis f) 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 (len (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (Y_axis f) -element Element of bool NAT
(Y_axis f) . n is V22() ext-real V26() Element of REAL
p `2 is V22() ext-real V26() Element of REAL
dom (Incr (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (Y_axis f)) . i is V22() ext-real V26() Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
len (Line ((f),1)) 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 (Line ((f),1)) 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
card (rng (Y_axis f)) 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 (Incr (Y_axis f)) 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
card (rng (X_axis f)) 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
Indices (f) is set
dom (f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
[:(dom (f)),(Seg (width (f))):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
[1,i] is set
{1,i} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{{1,i},{1}} is V52() V56() set
(f) * (1,i) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(Line ((f),1)) . i is set
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 non empty V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom f is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(X_axis f) . n is V22() ext-real V26() Element of REAL
f /. 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))
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis f)),(Incr (Y_axis 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))
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
Line ((f),(len (f))) 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))
rng (Line ((f),(len (f)))) is V52() set
len f 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 (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
dom (X_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (X_axis f) 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 (len (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (X_axis f) -element Element of bool NAT
p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p `1 is V22() ext-real V26() Element of REAL
rng (Incr (X_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (X_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Incr (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
j is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (X_axis f)) . j is V22() ext-real V26() Element of REAL
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 (Incr (X_axis f)) 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 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
(Incr (X_axis f)) . (j + 1) is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(X_axis f) . i is V22() ext-real V26() Element of REAL
rng (Incr (Y_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (Y_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Y_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (Y_axis f) 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 (len (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (Y_axis f) -element Element of bool NAT
(Y_axis f) . n is V22() ext-real V26() Element of REAL
p `2 is V22() ext-real V26() Element of REAL
dom (Incr (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (Y_axis f)) . i is V22() ext-real V26() Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
len (Line ((f),(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 (Line ((f),(len (f)))) 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
card (rng (Y_axis f)) 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 (Incr (Y_axis f)) 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
card (rng (X_axis f)) 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
Indices (f) is set
dom (f) is V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() Element of bool NAT
[:(dom (f)),(Seg (width (f))):] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() V52() set
[(len (f)),i] is set
{(len (f)),i} is V45() V46() V47() V48() V49() V50() V52() V56() V63() V64() V65() set
{(len (f))} is non empty trivial V45() V46() V47() V48() V49() V50() V52() V56() V61() V62() V63() V64() V65() 1 -element set
{{(len (f)),i},{(len (f))}} is V52() V56() set
(f) * ((len (f)),i) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(Line ((f),(len (f)))) . i is set
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 non empty V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom f is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(Y_axis f) . n is V22() ext-real V26() Element of REAL
f /. 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))
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis f)),(Incr (Y_axis 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))
Col ((f),1) 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))
rng (Col ((f),1)) is V52() set
len f 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 (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
dom (Y_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (Y_axis f) 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 (len (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (Y_axis f) -element Element of bool NAT
p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p `2 is V22() ext-real V26() Element of REAL
rng (Incr (Y_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (Y_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Incr (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
j is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (Y_axis f)) . j is V22() ext-real V26() Element of REAL
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 V22() ext-real V26() set
len (Incr (Y_axis f)) 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
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
(Incr (Y_axis f)) . i is V22() ext-real V26() Element of REAL
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
i is V22() ext-real V26() Element of REAL
s2 is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Y_axis f) . s2 is V22() ext-real V26() Element of REAL
rng (Incr (X_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (X_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (X_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (X_axis f) 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 (len (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (X_axis f) -element Element of bool NAT
(X_axis f) . n is V22() ext-real V26() Element of REAL
p `1 is V22() ext-real V26() Element of REAL
dom (Incr (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (X_axis f)) . i is V22() ext-real V26() Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
len (Col ((f),1)) 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 (Col ((f),1)) 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
card (rng (X_axis f)) 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 (Incr (X_axis f)) 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
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
card (rng (Y_axis f)) 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
Indices (f) is set
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
[i,1] is set
{i,1} 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,1},{i}} is V52() V56() set
(f) * (i,1) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(Col ((f),1)) . i is set
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 non empty V52() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom f is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
Y_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
(Y_axis f) . n is V22() ext-real V26() Element of REAL
f /. 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))
X_axis f is Relation-like NAT -defined REAL -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis f) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like FinSequence of REAL
((Incr (X_axis f)),(Incr (Y_axis 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))
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
Col ((f),(width (f))) 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))
rng (Col ((f),(width (f)))) is V52() set
len f 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 (len f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len f -element Element of bool NAT
dom (Y_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (Y_axis f) 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 (len (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (Y_axis f) -element Element of bool NAT
p is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
p `2 is V22() ext-real V26() Element of REAL
rng (Incr (Y_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (Y_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (Incr (Y_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
j is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (Y_axis f)) . j is V22() ext-real V26() Element of REAL
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 (Incr (Y_axis f)) 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 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
(Incr (Y_axis f)) . (j + 1) is V22() ext-real V26() Element of REAL
i is V22() ext-real V26() Element of REAL
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Y_axis f) . i is V22() ext-real V26() Element of REAL
rng (Incr (X_axis f)) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
rng (X_axis f) is non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() set
dom (X_axis f) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
len (X_axis f) 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 (len (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() len (X_axis f) -element Element of bool NAT
(X_axis f) . n is V22() ext-real V26() Element of REAL
p `1 is V22() ext-real V26() Element of REAL
dom (Incr (X_axis f)) is non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() Element of bool NAT
i is V17() V21() V22() ext-real non negative V26() V52() cardinal set
(Incr (X_axis f)) . i is V22() ext-real V26() Element of REAL
|[(p `1),(p `2)]| is Relation-like NAT -defined Function-like non empty V33() V34() V35() V52() 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
len (Col ((f),(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
dom (Col ((f),(width (f)))) 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
card (rng (X_axis f)) 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 (Incr (X_axis f)) 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
card (rng (Y_axis f)) 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
Indices (f) is set
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
[i,(width (f))] is set
{i,(width (f))} 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,(width (f))},{i}} is V52() V56() set
(f) * (i,(width (f))) is V35() 2 -element FinSequence-like Element of the carrier of (TOP-REAL 2)
(Col ((f),(width (f)))) . i is set