:: EUCLID_4 semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set
NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)
K6(REAL) is 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
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-yielding V36() V37() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-yielding V36() V37() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) complex-yielding V36() V37() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-yielding V36() V37() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-yielding V36() V37() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-yielding V36() V37() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-yielding V36() V37() V38() set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-yielding V36() V37() V38() set
K6(K7(K7(NAT,NAT),NAT)) is set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,REAL) is complex-yielding V36() V37() set
K6(K7(COMPLEX,REAL)) is set
K419() is non empty V107() L8()
the carrier of K419() is non empty set
K424() is non empty V107() V129() V130() V131() V133() V159() V160() V161() V162() V163() V164() L8()
K425() is non empty V107() V131() V133() V162() V163() V164() M15(K424())
K426() is non empty V107() V129() V131() V133() V162() V163() V164() V165() M18(K424(),K425())
K428() is non empty V107() V129() V131() V133() L8()
K429() is non empty V107() V129() V131() V133() V165() M15(K428())
1 is non empty natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
K7(1,1) is V20( RAT ) V20( INT ) complex-yielding V36() V37() V38() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V20( RAT ) V20( INT ) complex-yielding V36() V37() V38() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V36() V37() set
K6(K7(K7(1,1),REAL)) is set
2 is non empty natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
K7(2,2) is V20( RAT ) V20( INT ) complex-yielding V36() V37() V38() set
K7(K7(2,2),REAL) is complex-yielding V36() V37() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty V105() V149() V150() TopSpace-like V194() V195() V196() V197() V198() V199() V200() V206() L16()
the carrier of (TOP-REAL 2) is non empty set
{} is set
the empty V45() V46() V47() V48() V49() V50() V51() set is empty V45() V46() V47() V48() V49() V50() V51() set
0 is natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
4 is non empty natural V11() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
K150(1,4) is V11() real ext-real V34() Element of RAT
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
0* n is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
0 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(0) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),0,K83(REAL)) is set
K67(R,K397(0)) is V16() complex-yielding V36() V37() set
(0 * R) + R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),(0 * R),R) is set
R + (0* n) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),R,(0* n)) is set
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
0 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K67(p1,K397(0)) is V16() complex-yielding V36() V37() set
1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(p1,K397(1)) is V16() complex-yielding V36() V37() set
(0 * p1) + (1 * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K339(K165(),(0 * p1),(1 * p1)) is set
0 + 1 is V11() real ext-real Element of REAL
(0 + 1) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K397((0 + 1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(0 + 1),K83(REAL)) is set
K67(p1,K397((0 + 1))) is V16() complex-yielding V36() V37() set
n is V11() real ext-real Element of REAL
R is natural V11() real ext-real set
0* R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
REAL R is non empty FinSequence-membered FinSequenceSet of REAL
R -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of R -tuples_on REAL
n * (0* R) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67((0* R),K397(n)) is V16() complex-yielding V36() V37() set
|.(n * (0* R)).| is V11() real ext-real non negative Element of REAL
sqr (n * (0* R)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like FinSequence of REAL
sqrreal is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K67((n * (0* R)),sqrreal) is V16() complex-yielding V36() V37() set
mlt ((n * (0* R)),(n * (0* R))) is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K339(K167(),(n * (0* R)),(n * (0* R))) is set
K412((sqr (n * (0* R)))) is V11() real ext-real Element of REAL
sqrt K412((sqr (n * (0* R)))) is V11() real ext-real Element of REAL
abs n is V11() real ext-real Element of REAL
|.(0* R).| is V11() real ext-real non negative Element of REAL
sqr (0* R) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like FinSequence of REAL
K67((0* R),sqrreal) is V16() complex-yielding V36() V37() set
mlt ((0* R),(0* R)) is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K339(K167(),(0* R),(0* R)) is set
K412((sqr (0* R))) is V11() real ext-real Element of REAL
sqrt K412((sqr (0* R))) is V11() real ext-real Element of REAL
(abs n) * |.(0* R).| is V11() real ext-real Element of REAL
(abs n) * 0 is V11() real ext-real Element of REAL
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
0* n is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
1 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(R,K397(1)) is V16() complex-yielding V36() V37() set
0 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(0) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),0,K83(REAL)) is set
K67(R,K397(0)) is V16() complex-yielding V36() V37() set
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
0 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K67(p1,K397(0)) is V16() complex-yielding V36() V37() set
(0 * p1) + p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),(0 * p1),p1) is set
((0 * p1) + p1) - p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K166() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() Element of K6(K7(K7(REAL,REAL),REAL))
K163() is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K361(REAL,K165(),K83(REAL),K163()) is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() Element of K6(K7(K7(REAL,REAL),REAL))
K339(K166(),((0 * p1) + p1),p1) is set
K240(p1) is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K67(p1,K163()) is V16() complex-yielding V36() V37() set
K38(1) is V11() real ext-real set
K38(1) * p1 is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K397(K38(1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),K38(1),K83(REAL)) is set
K67(p1,K397(K38(1))) is V16() complex-yielding V36() V37() set
K211(((0 * p1) + p1),K240(p1)) is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K339(K165(),((0 * p1) + p1),K240(p1)) is set
p1 - p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
K339(K166(),p1,p1) is set
K211(p1,K240(p1)) is V16() V19( NAT ) V21() complex-yielding V36() V37() FinSequence-like set
K339(K165(),p1,K240(p1)) is set
p1 is natural V11() real ext-real set
REAL p1 is non empty FinSequence-membered FinSequenceSet of REAL
p1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
n is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
n * R is V11() real ext-real Element of REAL
(n * R) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397((n * R)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(n * R),K83(REAL)) is set
K67(p2,K397((n * R))) is V16() complex-yielding V36() V37() set
R * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397(R) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),R,K83(REAL)) is set
K67(p2,K397(R)) is V16() complex-yielding V36() V37() set
n * (R * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67((R * p2),K397(n)) is V16() complex-yielding V36() V37() set
n is V11() real ext-real Element of REAL
R is natural V11() real ext-real set
REAL R is non empty FinSequence-membered FinSequenceSet of REAL
R -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
0* R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
R |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of R -tuples_on REAL
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
n * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67(p1,K397(n)) is V16() complex-yielding V36() V37() set
1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(p1,K397(1)) is V16() complex-yielding V36() V37() set
1 / n is V11() real ext-real Element of REAL
(1 / n) * n is V11() real ext-real Element of REAL
((1 / n) * n) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(((1 / n) * n)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),((1 / n) * n),K83(REAL)) is set
K67(p1,K397(((1 / n) * n))) is V16() complex-yielding V36() V37() set
(1 / n) * (n * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397((1 / n)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 / n),K83(REAL)) is set
K67((n * p1),K397((1 / n))) is V16() complex-yielding V36() V37() set
R is natural V11() real ext-real set
REAL R is non empty FinSequence-membered FinSequenceSet of REAL
R -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
p1 + p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),p1,p2) is set
n is V11() real ext-real Element of REAL
n * (p1 + p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67((p1 + p2),K397(n)) is V16() complex-yielding V36() V37() set
n * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K67(p1,K397(n)) is V16() complex-yielding V36() V37() set
n * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K67(p2,K397(n)) is V16() complex-yielding V36() V37() set
(n * p1) + (n * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K339(K165(),(n * p1),(n * p2)) is set
p1 is natural V11() real ext-real set
REAL p1 is non empty FinSequence-membered FinSequenceSet of REAL
p1 -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
n is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
n + R is V11() real ext-real Element of REAL
(n + R) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397((n + R)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(n + R),K83(REAL)) is set
K67(p2,K397((n + R))) is V16() complex-yielding V36() V37() set
n * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67(p2,K397(n)) is V16() complex-yielding V36() V37() set
R * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K397(R) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),R,K83(REAL)) is set
K67(p2,K397(R)) is V16() complex-yielding V36() V37() set
(n * p2) + (R * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(p1) FinSequence-like Element of REAL p1
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),(n * p2),(R * p2)) is set
n is V11() real ext-real Element of REAL
R is natural V11() real ext-real set
REAL R is non empty FinSequence-membered FinSequenceSet of REAL
R -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
n * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(n) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),n,K83(REAL)) is set
K67(p1,K397(n)) is V16() complex-yielding V36() V37() set
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
n * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K67(p2,K397(n)) is V16() complex-yielding V36() V37() set
1 / n is V11() real ext-real Element of REAL
(1 / n) * n is V11() real ext-real Element of REAL
((1 / n) * n) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(((1 / n) * n)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),((1 / n) * n),K83(REAL)) is set
K67(p1,K397(((1 / n) * n))) is V16() complex-yielding V36() V37() set
(1 / n) * (n * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397((1 / n)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 / n),K83(REAL)) is set
K67((n * p2),K397((1 / n))) is V16() complex-yielding V36() V37() set
((1 / n) * n) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K67(p2,K397(((1 / n) * n))) is V16() complex-yielding V36() V37() set
1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(p1,K397(1)) is V16() complex-yielding V36() V37() set
1 * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(R) FinSequence-like Element of REAL R
K67(p2,K397(1)) is V16() complex-yielding V36() V37() set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
{ (((1 - b₁) * R) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
K6((REAL n)) is set
q1 is set
y1 is V11() real ext-real Element of REAL
1 - y1 is V11() real ext-real Element of REAL
(1 - y1) * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - y1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - y1),K83(REAL)) is set
K67(R,K397((1 - y1))) is V16() complex-yielding V36() V37() set
y1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(y1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),y1,K83(REAL)) is set
K67(p1,K397(y1)) is V16() complex-yielding V36() V37() set
((1 - y1) * R) + (y1 * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),((1 - y1) * R),(y1 * p1)) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,R,p1) is Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * R) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
1 - 0 is V11() real ext-real Element of REAL
1 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(R,K397(1)) is V16() complex-yielding V36() V37() set
0 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(0) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),0,K83(REAL)) is set
K67(p1,K397(0)) is V16() complex-yielding V36() V37() set
0* n is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
R + (0* n) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),R,(0* n)) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,R,p1) is non empty Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * R) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
(n,p1,R) is non empty Element of K6((REAL n))
{ (((1 - b₁) * p1) + (b₁ * R)) where b₁ is V11() real ext-real Element of REAL : verum } is set
p2 is set
q1 is V11() real ext-real Element of REAL
1 - q1 is V11() real ext-real Element of REAL
(1 - q1) * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - q1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - q1),K83(REAL)) is set
K67(R,K397((1 - q1))) is V16() complex-yielding V36() V37() set
q1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(q1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),q1,K83(REAL)) is set
K67(p1,K397(q1)) is V16() complex-yielding V36() V37() set
((1 - q1) * R) + (q1 * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),((1 - q1) * R),(q1 * p1)) is set
1 - (1 - q1) is V11() real ext-real Element of REAL
(1 - (1 - q1)) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - (1 - q1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - (1 - q1)),K83(REAL)) is set
K67(p1,K397((1 - (1 - q1)))) is V16() complex-yielding V36() V37() set
((1 - (1 - q1)) * p1) + ((1 - q1) * R) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - (1 - q1)) * p1),((1 - q1) * R)) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
q1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,p2,q1) is non empty Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * p2) + (b₁ * q1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
(n,q1,p2) is non empty Element of K6((REAL n))
{ (((1 - b₁) * q1) + (b₁ * p2)) where b₁ is V11() real ext-real Element of REAL : verum } is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,R,p1) is non empty Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * R) + (b₁ * p1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
1 - 0 is V11() real ext-real Element of REAL
1 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),1,K83(REAL)) is set
K67(R,K397(1)) is V16() complex-yielding V36() V37() set
1 - 1 is V11() real ext-real Element of REAL
0 * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(0) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),0,K83(REAL)) is set
K67(R,K397(0)) is V16() complex-yielding V36() V37() set
0* n is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
n |-> 0 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() FinSequence-like Element of n -tuples_on REAL
1 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67(p1,K397(1)) is V16() complex-yielding V36() V37() set
(0* n) + p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),(0* n),p1) is set
0 * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67(p1,K397(0)) is V16() complex-yielding V36() V37() set
R + (0* n) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),R,(0* n)) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 + p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),p1,p2) is set
R + (p1 + p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),R,(p1 + p2)) is set
R + p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),R,p1) is set
(R + p1) + p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(R + p1),p2) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,p1,p2) is non empty Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * p1) + (b₁ * p2)) where b₁ is V11() real ext-real Element of REAL : verum } is set
q1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,R,q1) is non empty Element of K6((REAL n))
{ (((1 - b₁) * R) + (b₁ * q1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
y1 is V11() real ext-real Element of REAL
1 - y1 is V11() real ext-real Element of REAL
(1 - y1) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - y1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - y1),K83(REAL)) is set
K67(p1,K397((1 - y1))) is V16() complex-yielding V36() V37() set
y1 * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(y1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),y1,K83(REAL)) is set
K67(p2,K397(y1)) is V16() complex-yielding V36() V37() set
((1 - y1) * p1) + (y1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),((1 - y1) * p1),(y1 * p2)) is set
x1 is V11() real ext-real Element of REAL
1 - x1 is V11() real ext-real Element of REAL
(1 - x1) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - x1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - x1),K83(REAL)) is set
K67(p1,K397((1 - x1))) is V16() complex-yielding V36() V37() set
x1 * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(x1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),x1,K83(REAL)) is set
K67(p2,K397(x1)) is V16() complex-yielding V36() V37() set
((1 - x1) * p1) + (x1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - x1) * p1),(x1 * p2)) is set
x2 is set
y2 is V11() real ext-real Element of REAL
1 - y2 is V11() real ext-real Element of REAL
(1 - y2) * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - y2)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - y2),K83(REAL)) is set
K67(R,K397((1 - y2))) is V16() complex-yielding V36() V37() set
y2 * q1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(y2) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),y2,K83(REAL)) is set
K67(q1,K397(y2)) is V16() complex-yielding V36() V37() set
((1 - y2) * R) + (y2 * q1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - y2) * R),(y2 * q1)) is set
(1 - y2) * ((1 - y1) * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67(((1 - y1) * p1),K397((1 - y2))) is V16() complex-yielding V36() V37() set
(1 - y2) * (y1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67((y1 * p2),K397((1 - y2))) is V16() complex-yielding V36() V37() set
((1 - y2) * ((1 - y1) * p1)) + ((1 - y2) * (y1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - y2) * ((1 - y1) * p1)),((1 - y2) * (y1 * p2))) is set
y2 * (((1 - x1) * p1) + (x1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67((((1 - x1) * p1) + (x1 * p2)),K397(y2)) is V16() complex-yielding V36() V37() set
(((1 - y2) * ((1 - y1) * p1)) + ((1 - y2) * (y1 * p2))) + (y2 * (((1 - x1) * p1) + (x1 * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * ((1 - y1) * p1)) + ((1 - y2) * (y1 * p2))),(y2 * (((1 - x1) * p1) + (x1 * p2)))) is set
y2 * ((1 - x1) * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67(((1 - x1) * p1),K397(y2)) is V16() complex-yielding V36() V37() set
y2 * (x1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67((x1 * p2),K397(y2)) is V16() complex-yielding V36() V37() set
(y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(y2 * ((1 - x1) * p1)),(y2 * (x1 * p2))) is set
(((1 - y2) * ((1 - y1) * p1)) + ((1 - y2) * (y1 * p2))) + ((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * ((1 - y1) * p1)) + ((1 - y2) * (y1 * p2))),((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2)))) is set
(1 - y2) * (1 - y1) is V11() real ext-real Element of REAL
((1 - y2) * (1 - y1)) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(((1 - y2) * (1 - y1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),((1 - y2) * (1 - y1)),K83(REAL)) is set
K67(p1,K397(((1 - y2) * (1 - y1)))) is V16() complex-yielding V36() V37() set
(((1 - y2) * (1 - y1)) * p1) + ((1 - y2) * (y1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * (1 - y1)) * p1),((1 - y2) * (y1 * p2))) is set
((((1 - y2) * (1 - y1)) * p1) + ((1 - y2) * (y1 * p2))) + ((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) * p1) + ((1 - y2) * (y1 * p2))),((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2)))) is set
(1 - y2) * y1 is V11() real ext-real Element of REAL
((1 - y2) * y1) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(((1 - y2) * y1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),((1 - y2) * y1),K83(REAL)) is set
K67(p2,K397(((1 - y2) * y1))) is V16() complex-yielding V36() V37() set
(((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * (1 - y1)) * p1),(((1 - y2) * y1) * p2)) is set
((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)) + ((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)),((y2 * ((1 - x1) * p1)) + (y2 * (x1 * p2)))) is set
y2 * (1 - x1) is V11() real ext-real Element of REAL
(y2 * (1 - x1)) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((y2 * (1 - x1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(y2 * (1 - x1)),K83(REAL)) is set
K67(p1,K397((y2 * (1 - x1)))) is V16() complex-yielding V36() V37() set
((y2 * (1 - x1)) * p1) + (y2 * (x1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((y2 * (1 - x1)) * p1),(y2 * (x1 * p2))) is set
((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)) + (((y2 * (1 - x1)) * p1) + (y2 * (x1 * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)),(((y2 * (1 - x1)) * p1) + (y2 * (x1 * p2)))) is set
y2 * x1 is V11() real ext-real Element of REAL
(y2 * x1) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((y2 * x1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(y2 * x1),K83(REAL)) is set
K67(p2,K397((y2 * x1))) is V16() complex-yielding V36() V37() set
((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((y2 * (1 - x1)) * p1),((y2 * x1) * p2)) is set
((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)) + (((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) * p1) + (((1 - y2) * y1) * p2)),(((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2))) is set
(((1 - y2) * y1) * p2) + (((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * y1) * p2),(((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2))) is set
(((1 - y2) * (1 - y1)) * p1) + ((((1 - y2) * y1) * p2) + (((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * (1 - y1)) * p1),((((1 - y2) * y1) * p2) + (((y2 * (1 - x1)) * p1) + ((y2 * x1) * p2)))) is set
(((1 - y2) * y1) * p2) + ((y2 * x1) * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * y1) * p2),((y2 * x1) * p2)) is set
((y2 * (1 - x1)) * p1) + ((((1 - y2) * y1) * p2) + ((y2 * x1) * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((y2 * (1 - x1)) * p1),((((1 - y2) * y1) * p2) + ((y2 * x1) * p2))) is set
(((1 - y2) * (1 - y1)) * p1) + (((y2 * (1 - x1)) * p1) + ((((1 - y2) * y1) * p2) + ((y2 * x1) * p2))) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * (1 - y1)) * p1),(((y2 * (1 - x1)) * p1) + ((((1 - y2) * y1) * p2) + ((y2 * x1) * p2)))) is set
(((1 - y2) * (1 - y1)) * p1) + ((y2 * (1 - x1)) * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),(((1 - y2) * (1 - y1)) * p1),((y2 * (1 - x1)) * p1)) is set
((((1 - y2) * (1 - y1)) * p1) + ((y2 * (1 - x1)) * p1)) + ((((1 - y2) * y1) * p2) + ((y2 * x1) * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) * p1) + ((y2 * (1 - x1)) * p1)),((((1 - y2) * y1) * p2) + ((y2 * x1) * p2))) is set
((1 - y2) * (1 - y1)) + (y2 * (1 - x1)) is V11() real ext-real Element of REAL
(((1 - y2) * (1 - y1)) + (y2 * (1 - x1))) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((((1 - y2) * (1 - y1)) + (y2 * (1 - x1)))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(((1 - y2) * (1 - y1)) + (y2 * (1 - x1))),K83(REAL)) is set
K67(p1,K397((((1 - y2) * (1 - y1)) + (y2 * (1 - x1))))) is V16() complex-yielding V36() V37() set
((((1 - y2) * (1 - y1)) + (y2 * (1 - x1))) * p1) + ((((1 - y2) * y1) * p2) + ((y2 * x1) * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 - y2) * (1 - y1)) + (y2 * (1 - x1))) * p1),((((1 - y2) * y1) * p2) + ((y2 * x1) * p2))) is set
1 * y1 is V11() real ext-real Element of REAL
y2 * y1 is V11() real ext-real Element of REAL
(1 * y1) - (y2 * y1) is V11() real ext-real Element of REAL
((1 * y1) - (y2 * y1)) + (y2 * x1) is V11() real ext-real Element of REAL
1 - (((1 * y1) - (y2 * y1)) + (y2 * x1)) is V11() real ext-real Element of REAL
(1 - (((1 * y1) - (y2 * y1)) + (y2 * x1))) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - (((1 * y1) - (y2 * y1)) + (y2 * x1)))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - (((1 * y1) - (y2 * y1)) + (y2 * x1))),K83(REAL)) is set
K67(p1,K397((1 - (((1 * y1) - (y2 * y1)) + (y2 * x1))))) is V16() complex-yielding V36() V37() set
(((1 * y1) - (y2 * y1)) + (y2 * x1)) * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((((1 * y1) - (y2 * y1)) + (y2 * x1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(((1 * y1) - (y2 * y1)) + (y2 * x1)),K83(REAL)) is set
K67(p2,K397((((1 * y1) - (y2 * y1)) + (y2 * x1)))) is V16() complex-yielding V36() V37() set
((1 - (((1 * y1) - (y2 * y1)) + (y2 * x1))) * p1) + ((((1 * y1) - (y2 * y1)) + (y2 * x1)) * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - (((1 * y1) - (y2 * y1)) + (y2 * x1))) * p1),((((1 * y1) - (y2 * y1)) + (y2 * x1)) * p2)) is set
n is natural V11() real ext-real set
REAL n is non empty FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is FinSequence-membered FinSequenceSet of REAL
R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,p1,p2) is non empty Element of K6((REAL n))
K6((REAL n)) is set
{ (((1 - b₁) * p1) + (b₁ * p2)) where b₁ is V11() real ext-real Element of REAL : verum } is set
q1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
(n,R,q1) is non empty Element of K6((REAL n))
{ (((1 - b₁) * R) + (b₁ * q1)) where b₁ is V11() real ext-real Element of REAL : verum } is set
y1 is V11() real ext-real Element of REAL
1 - y1 is V11() real ext-real Element of REAL
(1 - y1) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - y1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K167() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K83(REAL) is non empty V16() V19( REAL ) V20( REAL ) V26( REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - y1),K83(REAL)) is set
K67(p1,K397((1 - y1))) is V16() complex-yielding V36() V37() set
y1 * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(y1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),y1,K83(REAL)) is set
K67(p2,K397(y1)) is V16() complex-yielding V36() V37() set
((1 - y1) * p1) + (y1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K165() is V16() V19(K7(REAL,REAL)) V20( REAL ) V21() V30(K7(REAL,REAL), REAL ) complex-yielding V36() V37() V178( REAL ) V179( REAL ) Element of K6(K7(K7(REAL,REAL),REAL))
K339(K165(),((1 - y1) * p1),(y1 * p2)) is set
x1 is V11() real ext-real Element of REAL
1 - x1 is V11() real ext-real Element of REAL
(1 - x1) * p1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - x1)) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - x1),K83(REAL)) is set
K67(p1,K397((1 - x1))) is V16() complex-yielding V36() V37() set
x1 * p2 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(x1) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),x1,K83(REAL)) is set
K67(p2,K397(x1)) is V16() complex-yielding V36() V37() set
((1 - x1) * p1) + (x1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - x1) * p1),(x1 * p2)) is set
y1 - x1 is V11() real ext-real Element of REAL
y1 - 1 is V11() real ext-real Element of REAL
(y1 - 1) / (y1 - x1) is V11() real ext-real Element of REAL
1 - ((y1 - 1) / (y1 - x1)) is V11() real ext-real Element of REAL
(1 - ((y1 - 1) / (y1 - x1))) * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((1 - ((y1 - 1) / (y1 - x1)))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(1 - ((y1 - 1) / (y1 - x1))),K83(REAL)) is set
K67(R,K397((1 - ((y1 - 1) / (y1 - x1))))) is V16() complex-yielding V36() V37() set
((y1 - 1) / (y1 - x1)) * q1 is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397(((y1 - 1) / (y1 - x1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),((y1 - 1) / (y1 - x1)),K83(REAL)) is set
K67(q1,K397(((y1 - 1) / (y1 - x1)))) is V16() complex-yielding V36() V37() set
((1 - ((y1 - 1) / (y1 - x1))) * R) + (((y1 - 1) / (y1 - x1)) * q1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((1 - ((y1 - 1) / (y1 - x1))) * R),(((y1 - 1) / (y1 - x1)) * q1)) is set
1 * (y1 - x1) is V11() real ext-real Element of REAL
(1 * (y1 - x1)) - (y1 - 1) is V11() real ext-real Element of REAL
((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1) is V11() real ext-real Element of REAL
(((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1)) * R is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1)),K83(REAL)) is set
K67(R,K397((((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1)))) is V16() complex-yielding V36() V37() set
((((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1)) * R) + (((y1 - 1) / (y1 - x1)) * q1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((1 * (y1 - x1)) - (y1 - 1)) / (y1 - x1)) * R),(((y1 - 1) / (y1 - x1)) * q1)) is set
- x1 is V11() real ext-real Element of REAL
(- x1) + 1 is V11() real ext-real Element of REAL
((- x1) + 1) / (y1 - x1) is V11() real ext-real Element of REAL
(((- x1) + 1) / (y1 - x1)) * ((1 - y1) * p1) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K397((((- x1) + 1) / (y1 - x1))) is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) complex-yielding V36() V37() Element of K6(K7(REAL,REAL))
K341(K167(),(((- x1) + 1) / (y1 - x1)),K83(REAL)) is set
K67(((1 - y1) * p1),K397((((- x1) + 1) / (y1 - x1)))) is V16() complex-yielding V36() V37() set
(((- x1) + 1) / (y1 - x1)) * (y1 * p2) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67((y1 * p2),K397((((- x1) + 1) / (y1 - x1)))) is V16() complex-yielding V36() V37() set
((((- x1) + 1) / (y1 - x1)) * ((1 - y1) * p1)) + ((((- x1) + 1) / (y1 - x1)) * (y1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K339(K165(),((((- x1) + 1) / (y1 - x1)) * ((1 - y1) * p1)),((((- x1) + 1) / (y1 - x1)) * (y1 * p2))) is set
((y1 - 1) / (y1 - x1)) * (((1 - x1) * p1) + (x1 * p2)) is V16() V19( NAT ) V20( REAL ) V21() complex-yielding V36() V37() V69(n) FinSequence-like Element of REAL n
K67((((1 - x1) * p1) + (x1 * p2)),K397(((y1 - 1) / (y1 - x1)))) is V16() complex-yielding V36() V37() set
(((((- x1) + 1) / (y1 - x1)) * ((1 - y1) * p1)) + ((((- x1)