:: EUCLIDLP semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set
NAT is V45() V46() V47() V48() V49() V50() V51() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
omega is V45() V46() V47() V48() V49() V50() V51() set
bool omega is non empty set
bool NAT is non empty set
[:COMPLEX,COMPLEX:] is non empty complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty complex-yielding V34() V35() set
bool [:COMPLEX,REAL:] is non empty set
1 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
[:1,1:] is non empty V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty complex-yielding V34() V35() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty complex-yielding V34() V35() set
[:[:REAL,REAL:],REAL:] is non empty complex-yielding V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
[:2,2:] is non empty V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
[:[:2,2:],REAL:] is non empty complex-yielding V34() V35() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is V79() V105() V130() V157() V158() V159() V160() V161() V162() V163() V169() L15()
the U1 of (TOP-REAL 2) is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty V20( RAT ) complex-yielding V34() V35() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V20( RAT ) complex-yielding V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V20( RAT ) V20( INT ) complex-yielding V34() V35() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V20( RAT ) V20( INT ) complex-yielding V34() V35() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty set
0 is empty natural V11() real ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V51() Element of NAT
sqrt 0 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n / x1 is V11() real ext-real Element of REAL
1 / x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
n * x2 is V11() real ext-real Element of REAL
(n * x2) / x1 is V11() real ext-real Element of REAL
x2 / x1 is V11() real ext-real Element of REAL
y1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y1 is non empty FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y1 } is set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x2 * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n / x1) * (x2 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * x2) / x1) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(1 / x1) * (x2 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(x2 / x1) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n / x1) * x2 is V11() real ext-real Element of REAL
((n / x1) * x2) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(1 / x1) * x2 is V11() real ext-real Element of REAL
((1 / x1) * x2) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * x1 is V16() Function-like set
K145(x1,K174(x1)) is V16() Function-like set
- x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + (- x1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is V11() real ext-real Element of REAL
- n is V11() real ext-real Element of REAL
x1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL x1 is non empty FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = x1 } is set
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
- (n * x2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K38(1) is V11() real ext-real non positive set
K38(1) * (n * x2) is V16() Function-like set
(- n) * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
- x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K38(1) * x2 is V16() Function-like set
n * (- x2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
- 1 is V11() real ext-real non positive Element of REAL
(- 1) * n is V11() real ext-real Element of REAL
((- 1) * n) * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * (- 1) is V11() real ext-real Element of REAL
(n * (- 1)) * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x2) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * x2 is V16() Function-like set
K145(x1,K174(x2)) is V16() Function-like set
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y1) is V16() Function-like complex-yielding set
K38(1) * y1 is V16() Function-like set
K145(x2,K174(y1)) is V16() Function-like set
x1 - (x2 - y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174((x2 - y1)) is V16() Function-like complex-yielding set
K38(1) * (x2 - y1) is V16() Function-like set
K145(x1,K174((x2 - y1))) is V16() Function-like set
(x1 - x2) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 - x2) - (- y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174((- y1)) is V16() Function-like complex-yielding set
K38(1) * (- y1) is V16() Function-like set
K145((x1 - x2),K174((- y1))) is V16() Function-like set
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y1 is V16() Function-like set
K145(x2,K174(y1)) is V16() Function-like set
x1 + (x2 - y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K145((x1 + x2),K174(y1)) is V16() Function-like set
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + (- y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y1 is V16() Function-like set
K145(x1,K174(y1)) is V16() Function-like set
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 + (- y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + (y1 + (- y1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
x2 + (0* n) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(- y1) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + ((- y1) + y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
x1 + (0* n) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x2) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * x2 is V16() Function-like set
K145(x1,K174(x2)) is V16() Function-like set
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x2 + y1) + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + (y1 + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + (y1 + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K38(1) is V11() real ext-real non positive set
K38(1) * x1 is V16() Function-like set
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K38(1) * x2 is V16() Function-like set
(- x1) + (- x2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- ((x1 + x2) + y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K38(1) * ((x1 + x2) + y1) is V16() Function-like set
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K38(1) * y1 is V16() Function-like set
((- x1) + (- x2)) + (- y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
(0* n) - ((x1 + x2) + y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(((x1 + x2) + y1)) is V16() Function-like complex-yielding set
K145((0* n),K174(((x1 + x2) + y1))) is V16() Function-like set
(0* n) - (x1 + x2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174((x1 + x2)) is V16() Function-like complex-yielding set
K38(1) * (x1 + x2) is V16() Function-like set
K145((0* n),K174((x1 + x2))) is V16() Function-like set
((0* n) - (x1 + x2)) - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y1) is V16() Function-like complex-yielding set
K145(((0* n) - (x1 + x2)),K174(y1)) is V16() Function-like set
(0* n) - x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x1) is V16() Function-like complex-yielding set
K145((0* n),K174(x1)) is V16() Function-like set
((0* n) - x1) - x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x2) is V16() Function-like complex-yielding set
K145(((0* n) - x1),K174(x2)) is V16() Function-like set
(((0* n) - x1) - x2) - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K145((((0* n) - x1) - x2),K174(y1)) is V16() Function-like set
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x2) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * x2 is V16() Function-like set
K145(x1,K174(x2)) is V16() Function-like set
|.(x1 - x2).| is V11() real ext-real non negative Element of REAL
sqr (x1 - x2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like FinSequence of REAL
mlt ((x1 - x2),(x1 - x2)) is V16() Function-like set
K402((sqr (x1 - x2))) is V11() real ext-real Element of REAL
sqrt K402((sqr (x1 - x2))) is V11() real ext-real Element of REAL
|((x1 - x2),(x1 - x2))| is V11() real ext-real Element of REAL
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
x2 + (0* n) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
0* n is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of n -tuples_on REAL
Seg n is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg n),0) is V16() V19( Seg n) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg n,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg n),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg n),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg n),{0}:] is non empty set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(x2) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * x2 is V16() Function-like set
K145(x1,K174(x2)) is V16() Function-like set
x2 + (0* n) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is V11() real ext-real Element of REAL
x1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL x1 is non empty FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = x1 } is set
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
x2 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K174(y1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y1 is V16() Function-like set
K145(x2,K174(y1)) is V16() Function-like set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
0* x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
x1 |-> 0 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() FinSequence-like Element of x1 -tuples_on REAL
Seg x1 is V45() V46() V47() V48() V49() V50() Element of bool NAT
K277((Seg x1),0) is V16() V19( Seg x1) V20( RAT ) V20( INT ) V20({0}) Function-like V30( Seg x1,{0}) complex-yielding V34() V35() V36() Element of bool [:(Seg x1),{0}:]
{0} is non empty V45() V46() V47() V48() V49() V50() set
[:(Seg x1),{0}:] is V20( RAT ) V20( INT ) complex-yielding V34() V35() V36() set
bool [:(Seg x1),{0}:] is non empty set
n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n - x1 is V11() real ext-real Element of REAL
- x1 is V11() real ext-real Element of REAL
x2 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL x2 is non empty FinSequence-membered FinSequenceSet of REAL
x2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = x2 } is set
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
(n - x1) * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
n * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
(- x1) * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
(n * y1) + ((- x1) * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
x1 * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
- (x1 * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
K38(1) is V11() real ext-real non positive set
K38(1) * (x1 * y1) is V16() Function-like set
(n * y1) + (- (x1 * y1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
(n * y1) - (x1 * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
K174((x1 * y1)) is V16() Function-like complex-yielding set
K145((n * y1),K174((x1 * y1))) is V16() Function-like set
n + (- x1) is V11() real ext-real Element of REAL
(n + (- x1)) * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x2) FinSequence-like Element of REAL x2
n is V11() real ext-real Element of REAL
- n is V11() real ext-real Element of REAL
x1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL x1 is non empty FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = x1 } is set
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
x2 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K174(y1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y1 is V16() Function-like set
K145(x2,K174(y1)) is V16() Function-like set
n * (x2 - y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
- (n * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K38(1) * (n * y1) is V16() Function-like set
(n * x2) + (- (n * y1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(- n) * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(n * x2) + ((- n) * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(n * x2) - (n * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
K174((n * y1)) is V16() Function-like complex-yielding set
K145((n * x2),K174((n * y1))) is V16() Function-like set
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * (- y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(n * x2) + (n * (- y1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n - x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
(n - x1) - x2 is V11() real ext-real Element of REAL
y1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y1 is non empty FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y1 } is set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n - x1) - x2) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x1 * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * y2) - (x1 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((x1 * y2)) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * (x1 * y2) is V16() Function-like set
K145((n * y2),K174((x1 * y2))) is V16() Function-like set
x2 * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * y2) - (x1 * y2)) - (x2 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((x2 * y2)) is V16() Function-like complex-yielding set
K38(1) * (x2 * y2) is V16() Function-like set
K145(((n * y2) - (x1 * y2)),K174((x2 * y2))) is V16() Function-like set
(n - x1) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n - x1) * y2) - (x2 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K145(((n - x1) * y2),K174((x2 * y2))) is V16() Function-like set
n is V11() real ext-real Element of REAL
- n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
- x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
- x2 is V11() real ext-real Element of REAL
y1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y1 is non empty FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y1 } is set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(- n) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x1 * L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * P) + (x1 * L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(- x1) * L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((- n) * P) + ((- x1) * L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
L2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x2 * L2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * P) + (x1 * L1)) + (x2 * L2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 - (((n * P) + (x1 * L1)) + (x2 * L2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((((n * P) + (x1 * L1)) + (x2 * L2))) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * (((n * P) + (x1 * L1)) + (x2 * L2)) is V16() Function-like set
K145(y2,K174((((n * P) + (x1 * L1)) + (x2 * L2)))) is V16() Function-like set
(- x2) * L2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(((- n) * P) + ((- x1) * L1)) + ((- x2) * L2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + ((((- n) * P) + ((- x1) * L1)) + ((- x2) * L2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
- (n * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K38(1) * (n * P) is V16() Function-like set
- (x1 * L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K38(1) * (x1 * L1) is V16() Function-like set
(- (n * P)) + (- (x1 * L1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
- (x2 * L2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K38(1) * (x2 * L2) is V16() Function-like set
((- (n * P)) + (- (x1 * L1))) + (- (x2 * L2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + (((- (n * P)) + (- (x1 * L1))) + (- (x2 * L2))) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((- n) * P) + (- (x1 * L1)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(((- n) * P) + (- (x1 * L1))) + (- (x2 * L2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + ((((- n) * P) + (- (x1 * L1))) + (- (x2 * L2))) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(((- n) * P) + ((- x1) * L1)) + (- (x2 * L2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + ((((- n) * P) + ((- x1) * L1)) + (- (x2 * L2))) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n is V11() real ext-real Element of REAL
- n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n + x1 is V11() real ext-real Element of REAL
- x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
(n + x1) + x2 is V11() real ext-real Element of REAL
- x2 is V11() real ext-real Element of REAL
y1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y1 is non empty FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y1 } is set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n + x1) + x2) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 - (((n + x1) + x2) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((((n + x1) + x2) * P)) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * (((n + x1) + x2) * P) is V16() Function-like set
K145(y2,K174((((n + x1) + x2) * P))) is V16() Function-like set
(- n) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + ((- n) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(- x1) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(y2 + ((- n) * P)) + ((- x1) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(- x2) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((y2 + ((- n) * P)) + ((- x1) * P)) + ((- x2) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n + x1) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x2 * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n + x1) * P) + (x2 * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 - (((n + x1) * P) + (x2 * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((((n + x1) * P) + (x2 * P))) is V16() Function-like complex-yielding set
K38(1) * (((n + x1) * P) + (x2 * P)) is V16() Function-like set
K145(y2,K174((((n + x1) * P) + (x2 * P)))) is V16() Function-like set
n * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x1 * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * P) + (x1 * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * P) + (x1 * P)) + (x2 * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 - (((n * P) + (x1 * P)) + (x2 * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
K174((((n * P) + (x1 * P)) + (x2 * P))) is V16() Function-like complex-yielding set
K38(1) * (((n * P) + (x1 * P)) + (x2 * P)) is V16() Function-like set
K145(y2,K174((((n * P) + (x1 * P)) + (x2 * P)))) is V16() Function-like set
((- n) * P) + ((- x1) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(((- n) * P) + ((- x1) * P)) + ((- x2) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + ((((- n) * P) + ((- x1) * P)) + ((- x2) * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
y2 + (((- n) * P) + ((- x1) * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(y2 + (((- n) * P) + ((- x1) * P))) + ((- x2) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + (y1 + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + y1) + (x2 + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + x2) + y1) + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + y1) + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + y1) + x2) + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 + P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 + P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + y2) + (x2 + P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(y2 + P) + L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + x2) + y1) + ((y2 + P) + L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 + L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + y2) + (x2 + P)) + (y1 + L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + (y2 + P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + x2) + (y2 + P)) + (y1 + L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y1) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y1 is V16() Function-like set
K145(x1,K174(y1)) is V16() Function-like set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) - (y1 + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174((y1 + y2)) is V16() Function-like complex-yielding set
K38(1) * (y1 + y2) is V16() Function-like set
K145((x1 + x2),K174((y1 + y2))) is V16() Function-like set
x2 - y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y2) is V16() Function-like complex-yielding set
K38(1) * y2 is V16() Function-like set
K145(x2,K174(y2)) is V16() Function-like set
(x1 - y1) + (x2 - y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) - y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K145((x1 + x2),K174(y1)) is V16() Function-like set
((x1 + x2) - y1) - y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K145(((x1 + x2) - y1),K174(y2)) is V16() Function-like set
- y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
- y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(- y1) + (- y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + ((- y1) + (- y2)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = n } is set
x1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 + x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x1 - y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(y2) is V16() Function-like complex-yielding set
K38(1) is V11() real ext-real non positive set
K38(1) * y2 is V16() Function-like set
K145(x1,K174(y2)) is V16() Function-like set
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
y2 + P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
x2 - P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(P) is V16() Function-like complex-yielding set
K38(1) * P is V16() Function-like set
K145(x2,K174(P)) is V16() Function-like set
(x1 - y2) + (x2 - P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(y2 + P) + L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
((x1 + x2) + y1) - ((y2 + P) + L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(((y2 + P) + L1)) is V16() Function-like complex-yielding set
K38(1) * ((y2 + P) + L1) is V16() Function-like set
K145(((x1 + x2) + y1),K174(((y2 + P) + L1))) is V16() Function-like set
y1 - L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174(L1) is V16() Function-like complex-yielding set
K38(1) * L1 is V16() Function-like set
K145(y1,K174(L1)) is V16() Function-like set
((x1 - y2) + (x2 - P)) + (y1 - L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
(x1 + x2) - (y2 + P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
K174((y2 + P)) is V16() Function-like complex-yielding set
K38(1) * (y2 + P) is V16() Function-like set
K145((x1 + x2),K174((y2 + P))) is V16() Function-like set
((x1 + x2) - (y2 + P)) + (y1 - L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(n) FinSequence-like Element of REAL n
n is V11() real ext-real Element of REAL
x1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL x1 is non empty FinSequence-membered FinSequenceSet of REAL
x1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = x1 } is set
x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * x2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
x2 + y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * y1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(n * x2) + (n * y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(x2 + y1) + y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * ((x2 + y1) + y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
((n * x2) + (n * y1)) + (n * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n * (x2 + y1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
(n * (x2 + y1)) + (n * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(x1) FinSequence-like Element of REAL x1
n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n * x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
n * x2 is V11() real ext-real Element of REAL
y1 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y1 is non empty FinSequence-membered FinSequenceSet of REAL
y1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y1 } is set
y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x1 * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * x1) * y2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
x2 * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(x1 * y2) + (x2 * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n * ((x1 * y2) + (x2 * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * x2) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * x1) * y2) + ((n * x2) * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n * (x1 * y2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n * (x2 * P) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
(n * (x1 * y2)) + (n * (x2 * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
((n * x1) * y2) + (n * (x2 * P)) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y1) FinSequence-like Element of REAL y1
n is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
n * x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
n * x2 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
n * y1 is V11() real ext-real Element of REAL
y2 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
REAL y2 is non empty FinSequence-membered FinSequenceSet of REAL
y2 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
REAL * is FinSequenceSet of REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like Element of REAL * : len b₁ = y2 } is set
P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
x1 * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
(n * x1) * P is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
x2 * L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
(x1 * P) + (x2 * L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
(n * x2) * L1 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
((n * x1) * P) + ((n * x2) * L1) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
L2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
y1 * L2 is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2) FinSequence-like Element of REAL y2
((x1 * P) + (x2 * L1)) + (y1 * L2) is V16() V19( NAT ) V20( REAL ) Function-like complex-yielding V34() V35() V69(y2)