REAL is non empty V40() V65() V66() V67() V71() set
NAT is ordinal V40() V45() V46() V65() V66() V67() V68() V69() V70() V71() Element of K19(REAL)
K19(REAL) is V40() set
COMPLEX is non empty V40() V65() V71() set
RAT is non empty V40() V65() V66() V67() V68() V71() set
INT is non empty V40() V65() V66() V67() V68() V69() V71() set
K20(COMPLEX,COMPLEX) is V40() complex-yielding set
K19(K20(COMPLEX,COMPLEX)) is V40() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V40() complex-yielding set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V40() set
K20(REAL,REAL) is V40() complex-yielding V56() V57() set
K19(K20(REAL,REAL)) is V40() set
K20(K20(REAL,REAL),REAL) is V40() complex-yielding V56() V57() set
K19(K20(K20(REAL,REAL),REAL)) is V40() set
K20(RAT,RAT) is RAT -valued V40() complex-yielding V56() V57() set
K19(K20(RAT,RAT)) is V40() set
K20(K20(RAT,RAT),RAT) is RAT -valued V40() complex-yielding V56() V57() set
K19(K20(K20(RAT,RAT),RAT)) is V40() set
K20(INT,INT) is RAT -valued INT -valued V40() complex-yielding V56() V57() set
K19(K20(INT,INT)) is V40() set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V40() complex-yielding V56() V57() set
K19(K20(K20(INT,INT),INT)) is V40() set
K20(NAT,NAT) is RAT -valued INT -valued complex-yielding V56() V57() V58() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V56() V57() V58() set
K19(K20(K20(NAT,NAT),NAT)) is set
omega is ordinal V40() V45() V46() V65() V66() V67() V68() V69() V70() V71() set
K19(omega) is V40() set
K19(NAT) is V40() set
{} is functional empty ordinal V45() V47( {} ) FinSequence-membered V65() V66() V67() V68() V69() V70() V71() set
1 is non empty ordinal natural V31() real ext-real positive non negative V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
{{},1} is non empty set
ExtREAL is non empty V66() set
0 is functional empty ordinal natural V31() real ext-real non positive non negative V36() V37() V40() V45() V47( {} ) FinSequence-membered V65() V66() V67() V68() V69() V70() V71() Element of NAT
2 is non empty ordinal natural V31() real ext-real positive non negative V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
3 is non empty ordinal natural V31() real ext-real positive non negative V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg 1 is non empty V12() V40() V47(1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
{1} is non empty V12() V47(1) V65() V66() V67() V68() V69() V70() set
Seg 2 is non empty V40() V47(2) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
{1,2} is non empty V65() V66() V67() V68() V69() V70() set
0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 0 } is set
X is V31() real ext-real set
f is V31() real ext-real set
min (X,f) is V31() real ext-real set
max (X,f) is V31() real ext-real set
X is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = X } is set
f is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
mlt (f,p) is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,f,p) is set
r is V31() real ext-real Element of REAL
<*r*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
f ^ <*r*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(X + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
X + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
s is V31() real ext-real Element of REAL
<*s*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
p ^ <*s*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(X + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
mlt ((f ^ <*r*>),(p ^ <*s*>)) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
K209(multreal,(f ^ <*r*>),(p ^ <*s*>)) is set
r * s is V31() real ext-real Element of REAL
<*(r * s)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
(mlt (f,p)) ^ <*(r * s)*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(X + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
len (f ^ <*r*>) is non empty ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len f) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len p is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len p) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len (p ^ <*s*>) is non empty ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len (mlt ((f ^ <*r*>),(p ^ <*s*>))) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (X + 1) is V40() V47(X + 1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is ordinal natural V31() real ext-real V40() V45() set
(mlt ((f ^ <*r*>),(p ^ <*s*>))) . s is V31() real ext-real Element of REAL
((mlt (f,p)) ^ <*(r * s)*>) . s is V31() real ext-real Element of REAL
Seg X is V40() V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
Seg (len f) is V40() V47( len f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom f is V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(f ^ <*r*>) . s is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
Seg (len p) is V40() V47( len p) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom p is V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(p ^ <*s*>) . s is V31() real ext-real Element of REAL
p . s is V31() real ext-real Element of REAL
(f . s) * (p . s) is V31() real ext-real Element of REAL
len (mlt (f,p)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
dom (mlt (f,p)) is V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(mlt (f,p)) . s is V31() real ext-real Element of REAL
(f ^ <*r*>) . s is V31() real ext-real Element of REAL
len (mlt (f,p)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len (mlt (f,p))) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(p ^ <*s*>) . s is V31() real ext-real Element of REAL
(X + 1) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = X + 1 } is set
X is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = X } is set
f is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
Sum f is V31() real ext-real Element of REAL
dom f is V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
p is ordinal natural V31() real ext-real V40() V45() set
f . p is V31() real ext-real Element of REAL
p is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
f . p is V31() real ext-real Element of REAL
X is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = X } is set
X |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
Seg X is V40() V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K213((Seg X),0) is Relation-like Seg X -defined RAT -valued INT -valued {0} -valued Function-like V18( Seg X,{0}) V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() V58() Element of K19(K20((Seg X),{0}))
{0} is non empty V12() V47(1) V65() V66() V67() V68() V69() V70() set
K20((Seg X),{0}) is RAT -valued INT -valued complex-yielding V56() V57() V58() set
K19(K20((Seg X),{0})) is set
f is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
dom f is V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
len f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
p is ordinal natural V31() real ext-real V40() V45() set
f . p is V31() real ext-real Element of REAL
(X |-> 0) . p is V31() real ext-real Element of REAL
Seg (len f) is V40() V47( len f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
len (X |-> 0) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = X } is set
X |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
Seg X is V40() V47(X) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K213((Seg X),0) is Relation-like Seg X -defined RAT -valued INT -valued {0} -valued Function-like V18( Seg X,{0}) V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() V58() Element of K19(K20((Seg X),{0}))
{0} is non empty V12() V47(1) V65() V66() V67() V68() V69() V70() set
K20((Seg X),{0}) is RAT -valued INT -valued complex-yielding V56() V57() V58() set
K19(K20((Seg X),{0})) is set
f is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
mlt ((X |-> 0),f) is Relation-like NAT -defined REAL -valued Function-like V40() V47(X) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of X -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,(X |-> 0),f) is set
len (mlt ((X |-> 0),f)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
p is ordinal natural V31() real ext-real V40() V45() set
(mlt ((X |-> 0),f)) . p is V31() real ext-real Element of REAL
(X |-> 0) . p is V31() real ext-real Element of REAL
Seg (len (mlt ((X |-> 0),f))) is V40() V47( len (mlt ((X |-> 0),f))) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
f . p is V31() real ext-real Element of REAL
((X |-> 0) . p) * (f . p) is V31() real ext-real Element of REAL
0 * (f . p) is V31() real ext-real Element of REAL
len (X |-> 0) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
dom X is set
X is V31() real ext-real Element of REAL
f is V31() real ext-real Element of REAL
[.X,f.] is V65() V66() V67() Element of K19(REAL)
p is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom p is set
{ b1 where b1 is V31() real ext-real Element of REAL : ( X <= b1 & b1 <= f ) } is set
s is V31() real ext-real Element of REAL
1 - s is V31() real ext-real Element of REAL
s * f is V31() real ext-real Element of REAL
(1 - s) * f is V31() real ext-real Element of REAL
(s * f) + ((1 - s) * f) is V31() real ext-real Element of REAL
s * X is V31() real ext-real Element of REAL
(1 - s) * X is V31() real ext-real Element of REAL
(s * X) + ((1 - s) * X) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
p . s is V31() real ext-real Element of REAL
s * (p . s) is V31() real ext-real Element of REAL
p . c7 is V31() real ext-real Element of REAL
(1 - s) * (p . c7) is V31() real ext-real Element of REAL
(s * (p . s)) + ((1 - s) * (p . c7)) is V31() real ext-real Element of REAL
s * s is V31() real ext-real Element of REAL
(1 - s) * c7 is V31() real ext-real Element of REAL
(s * s) + ((1 - s) * c7) is V31() real ext-real Element of REAL
p . ((s * s) + ((1 - s) * c7)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
1 - s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
s * s is V31() real ext-real Element of REAL
(1 - s) * c7 is V31() real ext-real Element of REAL
(s * s) + ((1 - s) * c7) is V31() real ext-real Element of REAL
p . s is V31() real ext-real Element of REAL
s * (p . s) is V31() real ext-real Element of REAL
p . c7 is V31() real ext-real Element of REAL
(1 - s) * (p . c7) is V31() real ext-real Element of REAL
(s * (p . s)) + ((1 - s) * (p . c7)) is V31() real ext-real Element of REAL
p . ((s * s) + ((1 - s) * c7)) is V31() real ext-real Element of REAL
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
r - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
(1 - p) * (r - s) is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - s is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(((p * r) + ((1 - p) * s)) - s) / (r - s) is V31() real ext-real Element of REAL
(r - ((p * r) + ((1 - p) * s))) / (r - s) is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - r is V31() real ext-real Element of REAL
(1 - p) * (s - r) is V31() real ext-real Element of REAL
(((p * r) + ((1 - p) * s)) - r) / (s - r) is V31() real ext-real Element of REAL
(s - ((p * r) + ((1 - p) * s))) / (s - r) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
((s - r) / (s - p)) + ((r - p) / (s - p)) is V31() real ext-real Element of REAL
(s - r) + (r - p) is V31() real ext-real Element of REAL
((s - r) + (r - p)) / (s - p) is V31() real ext-real Element of REAL
((s - r) / (s - p)) * p is V31() real ext-real Element of REAL
1 - ((s - r) / (s - p)) is V31() real ext-real Element of REAL
(1 - ((s - r) / (s - p))) * s is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * p) + ((1 - ((s - r) / (s - p))) * s) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
(p * (s - r)) / (s - p) is V31() real ext-real Element of REAL
s * ((r - p) / (s - p)) is V31() real ext-real Element of REAL
((p * (s - r)) / (s - p)) + (s * ((r - p) / (s - p))) is V31() real ext-real Element of REAL
s * (r - p) is V31() real ext-real Element of REAL
(s * (r - p)) / (s - p) is V31() real ext-real Element of REAL
((p * (s - r)) / (s - p)) + ((s * (r - p)) / (s - p)) is V31() real ext-real Element of REAL
s * p is V31() real ext-real Element of REAL
r * p is V31() real ext-real Element of REAL
(s * p) - (r * p) is V31() real ext-real Element of REAL
(r - p) * s is V31() real ext-real Element of REAL
((s * p) - (r * p)) + ((r - p) * s) is V31() real ext-real Element of REAL
(((s * p) - (r * p)) + ((r - p) * s)) / (s - p) is V31() real ext-real Element of REAL
r * (s - p) is V31() real ext-real Element of REAL
(r * (s - p)) / (s - p) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
f . c7 is V31() real ext-real Element of REAL
r - c7 is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
(r - c7) / (r - s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - c7) / (r - s)) * (f . s) is V31() real ext-real Element of REAL
c7 - s is V31() real ext-real Element of REAL
(c7 - s) / (r - s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
((c7 - s) / (r - s)) * (f . r) is V31() real ext-real Element of REAL
(((r - c7) / (r - s)) * (f . s)) + (((c7 - s) / (r - s)) * (f . r)) is V31() real ext-real Element of REAL
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
r - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
(1 - p) * (r - s) is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - s is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(((p * r) + ((1 - p) * s)) - s) / (r - s) is V31() real ext-real Element of REAL
(r - ((p * r) + ((1 - p) * s))) / (r - s) is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - r is V31() real ext-real Element of REAL
(1 - p) * (s - r) is V31() real ext-real Element of REAL
(((p * r) + ((1 - p) * s)) - r) / (s - r) is V31() real ext-real Element of REAL
(s - ((p * r) + ((1 - p) * s))) / (s - r) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
((s - r) / (s - p)) + ((r - p) / (s - p)) is V31() real ext-real Element of REAL
(s - r) + (r - p) is V31() real ext-real Element of REAL
((s - r) + (r - p)) / (s - p) is V31() real ext-real Element of REAL
((s - r) / (s - p)) * p is V31() real ext-real Element of REAL
1 - ((s - r) / (s - p)) is V31() real ext-real Element of REAL
(1 - ((s - r) / (s - p))) * s is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * p) + ((1 - ((s - r) / (s - p))) * s) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
(p * (s - r)) / (s - p) is V31() real ext-real Element of REAL
s * ((r - p) / (s - p)) is V31() real ext-real Element of REAL
((p * (s - r)) / (s - p)) + (s * ((r - p) / (s - p))) is V31() real ext-real Element of REAL
s * (r - p) is V31() real ext-real Element of REAL
(s * (r - p)) / (s - p) is V31() real ext-real Element of REAL
((p * (s - r)) / (s - p)) + ((s * (r - p)) / (s - p)) is V31() real ext-real Element of REAL
s * p is V31() real ext-real Element of REAL
r * p is V31() real ext-real Element of REAL
(s * p) - (r * p) is V31() real ext-real Element of REAL
(r - p) * s is V31() real ext-real Element of REAL
((s * p) - (r * p)) + ((r - p) * s) is V31() real ext-real Element of REAL
(((s * p) - (r * p)) + ((r - p) * s)) / (s - p) is V31() real ext-real Element of REAL
r * (s - p) is V31() real ext-real Element of REAL
(r * (s - p)) / (s - p) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
(s - r) / (s - p) is V31() real ext-real Element of REAL
f . p is V31() real ext-real Element of REAL
((s - r) / (s - p)) * (f . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
(r - p) / (s - p) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - p) / (s - p)) * (f . s) is V31() real ext-real Element of REAL
(((s - r) / (s - p)) * (f . p)) + (((r - p) / (s - p)) * (f . s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
r - c7 is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
(r - c7) / (r - s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
((r - c7) / (r - s)) * (f . s) is V31() real ext-real Element of REAL
c7 - s is V31() real ext-real Element of REAL
(c7 - s) / (r - s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
((c7 - s) / (r - s)) * (f . r) is V31() real ext-real Element of REAL
(((r - c7) / (r - s)) * (f . s)) + (((c7 - s) / (r - s)) * (f . r)) is V31() real ext-real Element of REAL
f . c7 is V31() real ext-real Element of REAL
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is set
p is set
dom X is set
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
1 - r is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
r * (X . s) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - r) * (X . s) is V31() real ext-real Element of REAL
(r * (X . s)) + ((1 - r) * (X . s)) is V31() real ext-real Element of REAL
X . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X is V31() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f - X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
dom f is set
r is V31() real ext-real Element of REAL
1 - r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(f - X) . s is V31() real ext-real Element of REAL
r * ((f - X) . s) is V31() real ext-real Element of REAL
(f - X) . s is V31() real ext-real Element of REAL
(1 - r) * ((f - X) . s) is V31() real ext-real Element of REAL
(r * ((f - X) . s)) + ((1 - r) * ((f - X) . s)) is V31() real ext-real Element of REAL
(f - X) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
r * (f . s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - r) * (f . s) is V31() real ext-real Element of REAL
(r * (f . s)) + ((1 - r) * (f . s)) is V31() real ext-real Element of REAL
f . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
((r * (f . s)) + ((1 - r) * (f . s))) - X is V31() real ext-real Element of REAL
(f . ((r * s) + ((1 - r) * s))) - X is V31() real ext-real Element of REAL
(f . s) - X is V31() real ext-real Element of REAL
(f . s) - X is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(f - X) . s is V31() real ext-real Element of REAL
r * ((f - X) . s) is V31() real ext-real Element of REAL
(f - X) . s is V31() real ext-real Element of REAL
(1 - r) * ((f - X) . s) is V31() real ext-real Element of REAL
(r * ((f - X) . s)) + ((1 - r) * ((f - X) . s)) is V31() real ext-real Element of REAL
(f - X) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
dom (f - X) is set
X is V31() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f - X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
dom (f - X) is set
dom f is set
- X is V31() real ext-real Element of REAL
(f - X) - (- X) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
r is V31() real ext-real Element of REAL
((f - X) - (- X)) . r is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
(f - X) . r is V31() real ext-real Element of REAL
((f - X) . r) - (- X) is V31() real ext-real Element of REAL
((f - X) . r) + X is V31() real ext-real Element of REAL
(f . r) - X is V31() real ext-real Element of REAL
((f . r) - X) + X is V31() real ext-real Element of REAL
X - X is V31() real ext-real Element of REAL
(f . r) - (X - X) is V31() real ext-real Element of REAL
dom ((f - X) - (- X)) is set
X is V31() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
X (#) f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
dom f is set
dom (X (#) f) is set
r is V31() real ext-real Element of REAL
1 - r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X (#) f) . s is V31() real ext-real Element of REAL
r * ((X (#) f) . s) is V31() real ext-real Element of REAL
(X (#) f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X (#) f) . s) is V31() real ext-real Element of REAL
(r * ((X (#) f) . s)) + ((1 - r) * ((X (#) f) . s)) is V31() real ext-real Element of REAL
(X (#) f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
r * (f . s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - r) * (f . s) is V31() real ext-real Element of REAL
(r * (f . s)) + ((1 - r) * (f . s)) is V31() real ext-real Element of REAL
f . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X * ((r * (f . s)) + ((1 - r) * (f . s))) is V31() real ext-real Element of REAL
X * (f . ((r * s) + ((1 - r) * s))) is V31() real ext-real Element of REAL
X * (f . s) is V31() real ext-real Element of REAL
r * (X * (f . s)) is V31() real ext-real Element of REAL
X * (f . s) is V31() real ext-real Element of REAL
(1 - r) * (X * (f . s)) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X (#) f) . s is V31() real ext-real Element of REAL
r * ((X (#) f) . s) is V31() real ext-real Element of REAL
(X (#) f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X (#) f) . s) is V31() real ext-real Element of REAL
(r * ((X (#) f) . s)) + ((1 - r) * ((X (#) f) . s)) is V31() real ext-real Element of REAL
(X (#) f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X is V31() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
X (#) f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
1 / X is V31() real ext-real Element of REAL
(1 / X) (#) (X (#) f) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom ((1 / X) (#) (X (#) f)) is set
dom (X (#) f) is set
r is V31() real ext-real Element of REAL
((1 / X) (#) (X (#) f)) . r is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
(X (#) f) . r is V31() real ext-real Element of REAL
(1 / X) * ((X (#) f) . r) is V31() real ext-real Element of REAL
X * (f . r) is V31() real ext-real Element of REAL
(1 / X) * (X * (f . r)) is V31() real ext-real Element of REAL
(1 / X) * X is V31() real ext-real Element of REAL
((1 / X) * X) * (f . r) is V31() real ext-real Element of REAL
1 * (f . r) is V31() real ext-real Element of REAL
dom f is set
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
X + f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
dom X is set
dom f is set
(dom X) /\ (dom f) is set
dom (X + f) is set
r is V31() real ext-real Element of REAL
1 - r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
r * ((X + f) . s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X + f) . s) is V31() real ext-real Element of REAL
(r * ((X + f) . s)) + ((1 - r) * ((X + f) . s)) is V31() real ext-real Element of REAL
(X + f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
f . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
(X . ((r * s) + ((1 - r) * s))) + (f . ((r * s) + ((1 - r) * s))) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(X . s) + (f . s) is V31() real ext-real Element of REAL
r * (X . s) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - r) * (X . s) is V31() real ext-real Element of REAL
(r * (X . s)) + ((1 - r) * (X . s)) is V31() real ext-real Element of REAL
r * (f . s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - r) * (f . s) is V31() real ext-real Element of REAL
(r * (f . s)) + ((1 - r) * (f . s)) is V31() real ext-real Element of REAL
((r * (X . s)) + ((1 - r) * (X . s))) + ((r * (f . s)) + ((1 - r) * (f . s))) is V31() real ext-real Element of REAL
r * ((X . s) + (f . s)) is V31() real ext-real Element of REAL
(X . s) + (f . s) is V31() real ext-real Element of REAL
(1 - r) * ((X . s) + (f . s)) is V31() real ext-real Element of REAL
(r * ((X . s) + (f . s))) + ((1 - r) * ((X . s) + (f . s))) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
r * ((X + f) . s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X + f) . s) is V31() real ext-real Element of REAL
(r * ((X + f) . s)) + ((1 - r) * ((X + f) . s)) is V31() real ext-real Element of REAL
(X + f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
X + f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is set
dom X is set
dom f is set
(dom X) /\ (dom f) is set
dom (X + f) is set
r is V31() real ext-real Element of REAL
1 - r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
r * ((X + f) . s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X + f) . s) is V31() real ext-real Element of REAL
(r * ((X + f) . s)) + ((1 - r) * ((X + f) . s)) is V31() real ext-real Element of REAL
(X + f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
f . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
(X . ((r * s) + ((1 - r) * s))) + (f . ((r * s) + ((1 - r) * s))) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(X . s) + (f . s) is V31() real ext-real Element of REAL
r * (X . s) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - r) * (X . s) is V31() real ext-real Element of REAL
(r * (X . s)) + ((1 - r) * (X . s)) is V31() real ext-real Element of REAL
r * (f . s) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(1 - r) * (f . s) is V31() real ext-real Element of REAL
(r * (f . s)) + ((1 - r) * (f . s)) is V31() real ext-real Element of REAL
((r * (X . s)) + ((1 - r) * (X . s))) + ((r * (f . s)) + ((1 - r) * (f . s))) is V31() real ext-real Element of REAL
r * ((X . s) + (f . s)) is V31() real ext-real Element of REAL
(X . s) + (f . s) is V31() real ext-real Element of REAL
(1 - r) * ((X . s) + (f . s)) is V31() real ext-real Element of REAL
(r * ((X . s) + (f . s))) + ((1 - r) * ((X . s) + (f . s))) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r * s is V31() real ext-real Element of REAL
(1 - r) * s is V31() real ext-real Element of REAL
(r * s) + ((1 - r) * s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
r * ((X + f) . s) is V31() real ext-real Element of REAL
(X + f) . s is V31() real ext-real Element of REAL
(1 - r) * ((X + f) . s) is V31() real ext-real Element of REAL
(r * ((X + f) . s)) + ((1 - r) * ((X + f) . s)) is V31() real ext-real Element of REAL
(X + f) . ((r * s) + ((1 - r) * s)) is V31() real ext-real Element of REAL
X is V31() real ext-real Element of REAL
f is V31() real ext-real Element of REAL
p is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
X (#) p is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
r is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f (#) r is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
(X (#) p) + (f (#) r) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
s is set
dom r is set
dom p is set
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom X is set
f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - r is V31() real ext-real Element of REAL
(1 - p) * (s - r) is V31() real ext-real Element of REAL
(X . ((p * r) + ((1 - p) * s))) - (X . r) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - r) is V31() real ext-real Element of REAL
(((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - r)) * p is V31() real ext-real Element of REAL
(s - r) * (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
p * ((s - r) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(s - r) * (X . r) is V31() real ext-real Element of REAL
p * ((s - r) * (X . r)) is V31() real ext-real Element of REAL
(p * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) - (p * ((s - r) * (X . r))) is V31() real ext-real Element of REAL
(X . s) - (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (s - r) is V31() real ext-real Element of REAL
(((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (s - r)) * (1 - p) is V31() real ext-real Element of REAL
(s - r) * (X . s) is V31() real ext-real Element of REAL
(1 - p) * ((s - r) * (X . s)) is V31() real ext-real Element of REAL
(1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
((1 - p) * ((s - r) * (X . s))) - ((1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
s - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) / (((p * r) + ((1 - p) * s)) - r) is V31() real ext-real Element of REAL
(X . s) - (X . r) is V31() real ext-real Element of REAL
((X . s) - (X . r)) / (s - r) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) / (s - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (((p * r) + ((1 - p) * s)) - r) is V31() real ext-real Element of REAL
(p * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) + ((1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
((1 - p) * ((s - r) * (X . s))) + (p * ((s - r) * (X . r))) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) * (s - r) is V31() real ext-real Element of REAL
(p * (X . r)) * (s - r) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (s - r)) + ((p * (X . r)) * (s - r)) is V31() real ext-real Element of REAL
((((1 - p) * (X . s)) * (s - r)) + ((p * (X . r)) * (s - r))) / (s - r) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (s - r)) / (s - r) is V31() real ext-real Element of REAL
((p * (X . r)) * (s - r)) / (s - r) is V31() real ext-real Element of REAL
((((1 - p) * (X . s)) * (s - r)) / (s - r)) + (((p * (X . r)) * (s - r)) / (s - r)) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) + (((p * (X . r)) * (s - r)) / (s - r)) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - s is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(X . ((p * r) + ((1 - p) * s))) - (X . s) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - s) is V31() real ext-real Element of REAL
(((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - s)) * (1 - p) is V31() real ext-real Element of REAL
(r - s) * (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
(1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(r - s) * (X . s) is V31() real ext-real Element of REAL
(1 - p) * ((r - s) * (X . s)) is V31() real ext-real Element of REAL
((1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) - ((1 - p) * ((r - s) * (X . s))) is V31() real ext-real Element of REAL
(X . r) - (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (r - s) is V31() real ext-real Element of REAL
(((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (r - s)) * p is V31() real ext-real Element of REAL
(r - s) * (X . r) is V31() real ext-real Element of REAL
p * ((r - s) * (X . r)) is V31() real ext-real Element of REAL
p * ((r - s) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(p * ((r - s) * (X . r))) - (p * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
r - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
(1 - p) * (r - s) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) / (((p * r) + ((1 - p) * s)) - s) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) / (r - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (((p * r) + ((1 - p) * s)) - s) is V31() real ext-real Element of REAL
((1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) + (p * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
(p * ((r - s) * (X . r))) + ((1 - p) * ((r - s) * (X . s))) is V31() real ext-real Element of REAL
(p * (X . r)) * (r - s) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) * (r - s) is V31() real ext-real Element of REAL
((p * (X . r)) * (r - s)) + (((1 - p) * (X . s)) * (r - s)) is V31() real ext-real Element of REAL
(((p * (X . r)) * (r - s)) + (((1 - p) * (X . s)) * (r - s))) / (r - s) is V31() real ext-real Element of REAL
((p * (X . r)) * (r - s)) / (r - s) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (r - s)) / (r - s) is V31() real ext-real Element of REAL
(((p * (X . r)) * (r - s)) / (r - s)) + ((((1 - p) * (X . s)) * (r - s)) / (r - s)) is V31() real ext-real Element of REAL
(p * (X . r)) + ((((1 - p) * (X . s)) * (r - s)) / (r - s)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
(r - s) / (r - p) is V31() real ext-real Element of REAL
(s - p) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) + ((s - p) / (r - p)) is V31() real ext-real Element of REAL
(r - s) + (s - p) is V31() real ext-real Element of REAL
((r - s) + (s - p)) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) * p is V31() real ext-real Element of REAL
1 - ((r - s) / (r - p)) is V31() real ext-real Element of REAL
(1 - ((r - s) / (r - p))) * r is V31() real ext-real Element of REAL
(((r - s) / (r - p)) * p) + ((1 - ((r - s) / (r - p))) * r) is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(p * (r - s)) / (r - p) is V31() real ext-real Element of REAL
r * ((s - p) / (r - p)) is V31() real ext-real Element of REAL
((p * (r - s)) / (r - p)) + (r * ((s - p) / (r - p))) is V31() real ext-real Element of REAL
r * (s - p) is V31() real ext-real Element of REAL
(r * (s - p)) / (r - p) is V31() real ext-real Element of REAL
((p * (r - s)) / (r - p)) + ((r * (s - p)) / (r - p)) is V31() real ext-real Element of REAL
r * p is V31() real ext-real Element of REAL
s * p is V31() real ext-real Element of REAL
(r * p) - (s * p) is V31() real ext-real Element of REAL
(s - p) * r is V31() real ext-real Element of REAL
((r * p) - (s * p)) + ((s - p) * r) is V31() real ext-real Element of REAL
(((r * p) - (s * p)) + ((s - p) * r)) / (r - p) is V31() real ext-real Element of REAL
s * (r - p) is V31() real ext-real Element of REAL
(s * (r - p)) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) * (X . p) is V31() real ext-real Element of REAL
((s - p) / (r - p)) * (X . r) is V31() real ext-real Element of REAL
(((r - s) / (r - p)) * (X . p)) + (((s - p) / (r - p)) * (X . r)) is V31() real ext-real Element of REAL
(r - p) * ((((r - s) / (r - p)) * (X . p)) + (((s - p) / (r - p)) * (X . r))) is V31() real ext-real Element of REAL
(r - p) * ((r - s) / (r - p)) is V31() real ext-real Element of REAL
((r - p) * ((r - s) / (r - p))) * (X . p) is V31() real ext-real Element of REAL
(r - p) * (((s - p) / (r - p)) * (X . r)) is V31() real ext-real Element of REAL
(((r - p) * ((r - s) / (r - p))) * (X . p)) + ((r - p) * (((s - p) / (r - p)) * (X . r))) is V31() real ext-real Element of REAL
(r - s) * (X . p) is V31() real ext-real Element of REAL
(r - p) * ((s - p) / (r - p)) is V31() real ext-real Element of REAL
((r - p) * ((s - p) / (r - p))) * (X . r) is V31() real ext-real Element of REAL
((r - s) * (X . p)) + (((r - p) * ((s - p) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
(s - p) * (X . r) is V31() real ext-real Element of REAL
((r - s) * (X . p)) + ((s - p) * (X . r)) is V31() real ext-real Element of REAL
X . ((((r - s) / (r - p)) * p) + ((1 - ((r - s) / (r - p))) * r)) is V31() real ext-real Element of REAL
(1 - ((r - s) / (r - p))) * (X . r) is V31() real ext-real Element of REAL
(((r - s) / (r - p)) * (X . p)) + ((1 - ((r - s) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
(r - p) * (X . s) is V31() real ext-real Element of REAL
(r - p) * (X . p) is V31() real ext-real Element of REAL
(s - p) * (X . p) is V31() real ext-real Element of REAL
((s - p) * (X . r)) - ((s - p) * (X . p)) is V31() real ext-real Element of REAL
((r - p) * (X . p)) + (((s - p) * (X . r)) - ((s - p) * (X . p))) is V31() real ext-real Element of REAL
((r - p) * (X . s)) - ((r - p) * (X . p)) is V31() real ext-real Element of REAL
(r - p) * ((X . s) - (X . p)) is V31() real ext-real Element of REAL
(s - p) * ((X . r) - (X . p)) is V31() real ext-real Element of REAL
(r - p) * (X . r) is V31() real ext-real Element of REAL
(r - s) * (X . r) is V31() real ext-real Element of REAL
((r - s) * (X . r)) - ((r - s) * (X . p)) is V31() real ext-real Element of REAL
((r - p) * (X . r)) - (((r - s) * (X . r)) - ((r - s) * (X . p))) is V31() real ext-real Element of REAL
(((r - s) * (X . r)) - ((r - s) * (X . p))) + ((r - p) * (X . s)) is V31() real ext-real Element of REAL
((r - p) * (X . r)) - ((r - p) * (X . s)) is V31() real ext-real Element of REAL
(r - s) * ((X . r) - (X . p)) is V31() real ext-real Element of REAL
(r - p) * ((X . r) - (X . s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
X . c7 is V31() real ext-real Element of REAL
(X . c7) - (X . s) is V31() real ext-real Element of REAL
c7 - s is V31() real ext-real Element of REAL
((X . c7) - (X . s)) / (c7 - s) is V31() real ext-real Element of REAL
(X . c7) - (X . r) is V31() real ext-real Element of REAL
c7 - r is V31() real ext-real Element of REAL
((X . c7) - (X . r)) / (c7 - r) is V31() real ext-real Element of REAL
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom X is set
f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - r is V31() real ext-real Element of REAL
(1 - p) * (s - r) is V31() real ext-real Element of REAL
(X . ((p * r) + ((1 - p) * s))) - (X . r) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - r) is V31() real ext-real Element of REAL
(((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - r)) * p is V31() real ext-real Element of REAL
(s - r) * (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
p * ((s - r) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(s - r) * (X . r) is V31() real ext-real Element of REAL
p * ((s - r) * (X . r)) is V31() real ext-real Element of REAL
(p * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) - (p * ((s - r) * (X . r))) is V31() real ext-real Element of REAL
(X . s) - (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (s - r) is V31() real ext-real Element of REAL
(((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (s - r)) * (1 - p) is V31() real ext-real Element of REAL
(s - r) * (X . s) is V31() real ext-real Element of REAL
(1 - p) * ((s - r) * (X . s)) is V31() real ext-real Element of REAL
(1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
((1 - p) * ((s - r) * (X . s))) - ((1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
s - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p * (s - r) is V31() real ext-real Element of REAL
(X . s) - (X . r) is V31() real ext-real Element of REAL
((X . s) - (X . r)) / (s - r) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) / (((p * r) + ((1 - p) * s)) - r) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) / (s - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . s) - (X . ((p * r) + ((1 - p) * s)))) * (((p * r) + ((1 - p) * s)) - r) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . r)) * (s - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((1 - p) * ((s - r) * (X . s))) + (p * ((s - r) * (X . r))) is V31() real ext-real Element of REAL
(p * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) + ((1 - p) * ((s - r) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) * (s - r) is V31() real ext-real Element of REAL
(p * (X . r)) * (s - r) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (s - r)) + ((p * (X . r)) * (s - r)) is V31() real ext-real Element of REAL
((((1 - p) * (X . s)) * (s - r)) + ((p * (X . r)) * (s - r))) / (s - r) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (s - r)) / (s - r) is V31() real ext-real Element of REAL
((p * (X . r)) * (s - r)) / (s - r) is V31() real ext-real Element of REAL
((((1 - p) * (X . s)) * (s - r)) / (s - r)) + (((p * (X . r)) * (s - r)) / (s - r)) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) + (((p * (X . r)) * (s - r)) / (s - r)) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((p * r) + ((1 - p) * s)) - s is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(X . ((p * r) + ((1 - p) * s))) - (X . s) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - s) is V31() real ext-real Element of REAL
(((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - s)) * (1 - p) is V31() real ext-real Element of REAL
(r - s) * (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
(1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(r - s) * (X . s) is V31() real ext-real Element of REAL
(1 - p) * ((r - s) * (X . s)) is V31() real ext-real Element of REAL
((1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) - ((1 - p) * ((r - s) * (X . s))) is V31() real ext-real Element of REAL
(X . r) - (X . ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (r - s) is V31() real ext-real Element of REAL
(((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (r - s)) * p is V31() real ext-real Element of REAL
(r - s) * (X . r) is V31() real ext-real Element of REAL
p * ((r - s) * (X . r)) is V31() real ext-real Element of REAL
p * ((r - s) * (X . ((p * r) + ((1 - p) * s)))) is V31() real ext-real Element of REAL
(p * ((r - s) * (X . r))) - (p * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
r - ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
(1 - p) * (r - s) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) / (((p * r) + ((1 - p) * s)) - s) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) / (r - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
((X . r) - (X . ((p * r) + ((1 - p) * s)))) * (((p * r) + ((1 - p) * s)) - s) is V31() real ext-real Element of REAL
((X . ((p * r) + ((1 - p) * s))) - (X . s)) * (r - ((p * r) + ((1 - p) * s))) is V31() real ext-real Element of REAL
(p * ((r - s) * (X . r))) + ((1 - p) * ((r - s) * (X . s))) is V31() real ext-real Element of REAL
((1 - p) * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) + (p * ((r - s) * (X . ((p * r) + ((1 - p) * s))))) is V31() real ext-real Element of REAL
(p * (X . r)) * (r - s) is V31() real ext-real Element of REAL
((1 - p) * (X . s)) * (r - s) is V31() real ext-real Element of REAL
((p * (X . r)) * (r - s)) + (((1 - p) * (X . s)) * (r - s)) is V31() real ext-real Element of REAL
(((p * (X . r)) * (r - s)) + (((1 - p) * (X . s)) * (r - s))) / (r - s) is V31() real ext-real Element of REAL
((p * (X . r)) * (r - s)) / (r - s) is V31() real ext-real Element of REAL
(((1 - p) * (X . s)) * (r - s)) / (r - s) is V31() real ext-real Element of REAL
(((p * (X . r)) * (r - s)) / (r - s)) + ((((1 - p) * (X . s)) * (r - s)) / (r - s)) is V31() real ext-real Element of REAL
(p * (X . r)) + ((((1 - p) * (X . s)) * (r - s)) / (r - s)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
p * (X . r) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(1 - p) * (X . s) is V31() real ext-real Element of REAL
(p * (X . r)) + ((1 - p) * (X . s)) is V31() real ext-real Element of REAL
X . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
(r - s) / (r - p) is V31() real ext-real Element of REAL
(s - p) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) + ((s - p) / (r - p)) is V31() real ext-real Element of REAL
(r - s) + (s - p) is V31() real ext-real Element of REAL
((r - s) + (s - p)) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) * p is V31() real ext-real Element of REAL
1 - ((r - s) / (r - p)) is V31() real ext-real Element of REAL
(1 - ((r - s) / (r - p))) * r is V31() real ext-real Element of REAL
(((r - s) / (r - p)) * p) + ((1 - ((r - s) / (r - p))) * r) is V31() real ext-real Element of REAL
p * (r - s) is V31() real ext-real Element of REAL
(p * (r - s)) / (r - p) is V31() real ext-real Element of REAL
r * ((s - p) / (r - p)) is V31() real ext-real Element of REAL
((p * (r - s)) / (r - p)) + (r * ((s - p) / (r - p))) is V31() real ext-real Element of REAL
r * (s - p) is V31() real ext-real Element of REAL
(r * (s - p)) / (r - p) is V31() real ext-real Element of REAL
((p * (r - s)) / (r - p)) + ((r * (s - p)) / (r - p)) is V31() real ext-real Element of REAL
r * p is V31() real ext-real Element of REAL
s * p is V31() real ext-real Element of REAL
(r * p) - (s * p) is V31() real ext-real Element of REAL
(s - p) * r is V31() real ext-real Element of REAL
((r * p) - (s * p)) + ((s - p) * r) is V31() real ext-real Element of REAL
(((r * p) - (s * p)) + ((s - p) * r)) / (r - p) is V31() real ext-real Element of REAL
s * (r - p) is V31() real ext-real Element of REAL
(s * (r - p)) / (r - p) is V31() real ext-real Element of REAL
((r - s) / (r - p)) * (X . p) is V31() real ext-real Element of REAL
(1 - ((r - s) / (r - p))) * (X . r) is V31() real ext-real Element of REAL
(((r - s) / (r - p)) * (X . p)) + ((1 - ((r - s) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
((((r - s) / (r - p)) * (X . p)) + ((1 - ((r - s) / (r - p))) * (X . r))) * (r - p) is V31() real ext-real Element of REAL
(r - p) * ((r - s) / (r - p)) is V31() real ext-real Element of REAL
((r - p) * ((r - s) / (r - p))) * (X . p) is V31() real ext-real Element of REAL
(r - p) * ((1 - ((r - s) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
(((r - p) * ((r - s) / (r - p))) * (X . p)) + ((r - p) * ((1 - ((r - s) / (r - p))) * (X . r))) is V31() real ext-real Element of REAL
(r - p) * (r - s) is V31() real ext-real Element of REAL
((r - p) * (r - s)) / (r - p) is V31() real ext-real Element of REAL
(((r - p) * (r - s)) / (r - p)) * (X . p) is V31() real ext-real Element of REAL
(r - p) * ((s - p) / (r - p)) is V31() real ext-real Element of REAL
((r - p) * ((s - p) / (r - p))) * (X . r) is V31() real ext-real Element of REAL
((((r - p) * (r - s)) / (r - p)) * (X . p)) + (((r - p) * ((s - p) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
(r - s) * (r - p) is V31() real ext-real Element of REAL
((r - s) * (r - p)) / (r - p) is V31() real ext-real Element of REAL
(((r - s) * (r - p)) / (r - p)) * (X . p) is V31() real ext-real Element of REAL
(r - p) * (s - p) is V31() real ext-real Element of REAL
((r - p) * (s - p)) / (r - p) is V31() real ext-real Element of REAL
(((r - p) * (s - p)) / (r - p)) * (X . r) is V31() real ext-real Element of REAL
((((r - s) * (r - p)) / (r - p)) * (X . p)) + ((((r - p) * (s - p)) / (r - p)) * (X . r)) is V31() real ext-real Element of REAL
(r - p) / (r - p) is V31() real ext-real Element of REAL
(r - s) * ((r - p) / (r - p)) is V31() real ext-real Element of REAL
((r - s) * ((r - p) / (r - p))) * (X . p) is V31() real ext-real Element of REAL
(((r - s) * ((r - p) / (r - p))) * (X . p)) + ((((r - p) * (s - p)) / (r - p)) * (X . r)) is V31() real ext-real Element of REAL
(r - s) * 1 is V31() real ext-real Element of REAL
((r - s) * 1) * (X . p) is V31() real ext-real Element of REAL
(s - p) * (r - p) is V31() real ext-real Element of REAL
((s - p) * (r - p)) / (r - p) is V31() real ext-real Element of REAL
(((s - p) * (r - p)) / (r - p)) * (X . r) is V31() real ext-real Element of REAL
(((r - s) * 1) * (X . p)) + ((((s - p) * (r - p)) / (r - p)) * (X . r)) is V31() real ext-real Element of REAL
(r - s) * (X . p) is V31() real ext-real Element of REAL
(s - p) * ((r - p) / (r - p)) is V31() real ext-real Element of REAL
((s - p) * ((r - p) / (r - p))) * (X . r) is V31() real ext-real Element of REAL
((r - s) * (X . p)) + (((s - p) * ((r - p) / (r - p))) * (X . r)) is V31() real ext-real Element of REAL
(s - p) * 1 is V31() real ext-real Element of REAL
((s - p) * 1) * (X . r) is V31() real ext-real Element of REAL
((r - s) * (X . p)) + (((s - p) * 1) * (X . r)) is V31() real ext-real Element of REAL
(r - p) * (X . p) is V31() real ext-real Element of REAL
(s - p) * (X . r) is V31() real ext-real Element of REAL
(s - p) * (X . p) is V31() real ext-real Element of REAL
((s - p) * (X . r)) - ((s - p) * (X . p)) is V31() real ext-real Element of REAL
((r - p) * (X . p)) + (((s - p) * (X . r)) - ((s - p) * (X . p))) is V31() real ext-real Element of REAL
(X . s) * (r - p) is V31() real ext-real Element of REAL
((X . s) * (r - p)) - ((r - p) * (X . p)) is V31() real ext-real Element of REAL
(s - p) * ((X . r) - (X . p)) is V31() real ext-real Element of REAL
(r - p) * ((X . s) - (X . p)) is V31() real ext-real Element of REAL
s - r is V31() real ext-real Element of REAL
(s - r) * (X . r) is V31() real ext-real Element of REAL
((s - r) * (X . r)) + ((r - s) * (X . p)) is V31() real ext-real Element of REAL
(r - p) * (X . r) is V31() real ext-real Element of REAL
(((s - r) * (X . r)) + ((r - s) * (X . p))) + ((r - p) * (X . r)) is V31() real ext-real Element of REAL
((X . s) * (r - p)) - (((s - r) * (X . r)) + ((r - s) * (X . p))) is V31() real ext-real Element of REAL
- (((s - r) * (X . r)) + ((r - s) * (X . p))) is V31() real ext-real Element of REAL
((X . s) * (r - p)) + (- (((s - r) * (X . r)) + ((r - s) * (X . p)))) is V31() real ext-real Element of REAL
(r - p) * (X . s) is V31() real ext-real Element of REAL
((r - p) * (X . r)) - ((r - p) * (X . s)) is V31() real ext-real Element of REAL
- ((s - r) * (X . r)) is V31() real ext-real Element of REAL
(- ((s - r) * (X . r))) - ((r - s) * (X . p)) is V31() real ext-real Element of REAL
(r - p) * ((X . r) - (X . s)) is V31() real ext-real Element of REAL
(r - s) * ((X . r) - (X . p)) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
c7 is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
X . c7 is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . c7) - (X . s) is V31() real ext-real Element of REAL
c7 - s is V31() real ext-real Element of REAL
((X . c7) - (X . s)) / (c7 - s) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . s) is V31() real ext-real Element of REAL
r - s is V31() real ext-real Element of REAL
((X . r) - (X . s)) / (r - s) is V31() real ext-real Element of REAL
(X . c7) - (X . r) is V31() real ext-real Element of REAL
c7 - r is V31() real ext-real Element of REAL
((X . c7) - (X . r)) / (c7 - r) is V31() real ext-real Element of REAL
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
f -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(f + 1) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f + 1 } is set
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
Sum p is V31() real ext-real Element of REAL
dom p is V47(f + 1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
mlt (p,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,p,r) is set
Sum (mlt (p,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (p,r))) is V31() real ext-real Element of REAL
mlt (p,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
K209(multreal,p,s) is set
Sum (mlt (p,s)) is V31() real ext-real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
c7 is V31() real ext-real Element of REAL
<*c7*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
s ^ <*c7*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
f + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
s is V31() real ext-real Element of REAL
<*s*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
r ^ <*s*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
len r is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len r) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len p is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len p) is V40() V47( len p) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s . ((len r) + 1) is V31() real ext-real Element of REAL
r . ((len r) + 1) is V31() real ext-real Element of REAL
X . (r . ((len r) + 1)) is V31() real ext-real Element of REAL
r . (f + 1) is V31() real ext-real Element of REAL
X . (r . (f + 1)) is V31() real ext-real Element of REAL
len s is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len s) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
r . ((len s) + 1) is V31() real ext-real Element of REAL
X . (r . ((len s) + 1)) is V31() real ext-real Element of REAL
X . c7 is V31() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
p1 is V31() real ext-real Element of REAL
<*p1*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
x ^ <*p1*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
mlt (x,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,x,r) is set
p1 * s is V31() real ext-real Element of REAL
<*(p1 * s)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
(mlt (x,r)) ^ <*(p1 * s)*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
Sum (mlt (x,r)) is V31() real ext-real Element of REAL
1 * (Sum (mlt (x,r))) is V31() real ext-real Element of REAL
(1 * (Sum (mlt (x,r)))) + (p1 * s) is V31() real ext-real Element of REAL
mlt (x,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,x,s) is set
p1 * c7 is V31() real ext-real Element of REAL
<*(p1 * c7)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() V59() V60() V61() V62() FinSequence of REAL
(mlt (x,s)) ^ <*(p1 * c7)*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
Sum (mlt (x,s)) is V31() real ext-real Element of REAL
1 * (Sum (mlt (x,s))) is V31() real ext-real Element of REAL
(1 * (Sum (mlt (x,s)))) + (p1 * c7) is V31() real ext-real Element of REAL
dom x is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
i is ordinal natural V31() real ext-real V40() V45() set
x . i is V31() real ext-real Element of REAL
len x is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len x) is V40() V47( len x) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
Seg (f + 1) is V40() V47(f + 1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
p . i is V31() real ext-real Element of REAL
i is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
x . i is V31() real ext-real Element of REAL
Sum x is V31() real ext-real Element of REAL
i is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
x . i is V31() real ext-real Element of REAL
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
Seg f is V40() V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K213((Seg f),0) is Relation-like Seg f -defined RAT -valued INT -valued {0} -valued Function-like V18( Seg f,{0}) V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() V58() Element of K19(K20((Seg f),{0}))
{0} is non empty V12() V47(1) V65() V66() V67() V68() V69() V70() set
K20((Seg f),{0}) is RAT -valued INT -valued complex-yielding V56() V57() V58() set
K19(K20((Seg f),{0})) is set
f * 0 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
0 + p1 is V31() real ext-real Element of REAL
Sum x is V31() real ext-real Element of REAL
(Sum x) " is V31() real ext-real Element of REAL
((Sum x) ") * x is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
((Sum x) ") multreal is Relation-like REAL -defined REAL -valued Function-like V18( REAL , REAL ) complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
id REAL is Relation-like REAL -defined REAL -valued non empty total complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
K211(multreal,((Sum x) "),(id REAL)) is set
x (#) (((Sum x) ") multreal) is Relation-like complex-yielding V56() V57() set
dom (((Sum x) ") * x) is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
i is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(((Sum x) ") * x) . i is V31() real ext-real Element of REAL
r . i is V31() real ext-real Element of REAL
s . i is V31() real ext-real Element of REAL
X . (s . i) is V31() real ext-real Element of REAL
len (((Sum x) ") * x) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len (((Sum x) ") * x)) is V40() V47( len (((Sum x) ") * x)) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
Seg f is V40() V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
len x is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len x) is V40() V47( len x) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
Seg (f + 1) is V40() V47(f + 1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
x . i is V31() real ext-real Element of REAL
((Sum x) ") * (x . i) is V31() real ext-real Element of REAL
Seg (len s) is V40() V47( len s) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom s is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
r . i is V31() real ext-real Element of REAL
Seg (len r) is V40() V47( len r) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom r is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s . i is V31() real ext-real Element of REAL
(Sum x) * ((Sum x) ") is V31() real ext-real Element of REAL
((Sum x) * ((Sum x) ")) * (Sum (mlt (x,s))) is V31() real ext-real Element of REAL
(((Sum x) * ((Sum x) ")) * (Sum (mlt (x,s)))) + (p1 * c7) is V31() real ext-real Element of REAL
((Sum x) ") * (Sum (mlt (x,s))) is V31() real ext-real Element of REAL
(Sum x) * (((Sum x) ") * (Sum (mlt (x,s)))) is V31() real ext-real Element of REAL
((Sum x) * (((Sum x) ") * (Sum (mlt (x,s))))) + (p1 * c7) is V31() real ext-real Element of REAL
((Sum x) ") * (mlt (x,s)) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
(mlt (x,s)) (#) (((Sum x) ") multreal) is Relation-like complex-yielding V56() V57() set
Sum (((Sum x) ") * (mlt (x,s))) is V31() real ext-real Element of REAL
(Sum x) * (Sum (((Sum x) ") * (mlt (x,s)))) is V31() real ext-real Element of REAL
((Sum x) * (Sum (((Sum x) ") * (mlt (x,s))))) + (p1 * c7) is V31() real ext-real Element of REAL
mlt ((((Sum x) ") * x),s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,(((Sum x) ") * x),s) is set
Sum (mlt ((((Sum x) ") * x),s)) is V31() real ext-real Element of REAL
(Sum x) * (Sum (mlt ((((Sum x) ") * x),s))) is V31() real ext-real Element of REAL
((Sum x) * (Sum (mlt ((((Sum x) ") * x),s)))) + (p1 * c7) is V31() real ext-real Element of REAL
((Sum x) ") * (Sum (mlt (x,r))) is V31() real ext-real Element of REAL
((Sum x) ") * (mlt (x,r)) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
(mlt (x,r)) (#) (((Sum x) ") multreal) is Relation-like complex-yielding V56() V57() set
Sum (((Sum x) ") * (mlt (x,r))) is V31() real ext-real Element of REAL
mlt ((((Sum x) ") * x),r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,(((Sum x) ") * x),r) is set
Sum (mlt ((((Sum x) ") * x),r)) is V31() real ext-real Element of REAL
len x is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(len x) + 1 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(Sum x) + p1 is V31() real ext-real Element of REAL
1 - (Sum x) is V31() real ext-real Element of REAL
Sum (((Sum x) ") * x) is V31() real ext-real Element of REAL
((Sum x) ") * (Sum x) is V31() real ext-real Element of REAL
X . (Sum (mlt ((((Sum x) ") * x),s))) is V31() real ext-real Element of REAL
(Sum x) * (X . (Sum (mlt ((((Sum x) ") * x),s)))) is V31() real ext-real Element of REAL
(Sum x) * (((Sum x) ") * (Sum (mlt (x,r)))) is V31() real ext-real Element of REAL
p1 * (X . c7) is V31() real ext-real Element of REAL
((Sum x) * (X . (Sum (mlt ((((Sum x) ") * x),s))))) + (p1 * (X . c7)) is V31() real ext-real Element of REAL
((Sum x) * (((Sum x) ") * (Sum (mlt (x,r))))) + (p1 * (X . c7)) is V31() real ext-real Element of REAL
p . ((len x) + 1) is V31() real ext-real Element of REAL
((Sum x) * ((Sum x) ")) * (Sum (mlt (x,r))) is V31() real ext-real Element of REAL
(((Sum x) * ((Sum x) ")) * (Sum (mlt (x,r)))) + (p1 * (X . c7)) is V31() real ext-real Element of REAL
Sum x is V31() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
Sum p is V31() real ext-real Element of REAL
dom p is V47(f + 1) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
mlt (p,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,p,r) is set
Sum (mlt (p,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (p,r))) is V31() real ext-real Element of REAL
mlt (p,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f + 1) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of (f + 1) -tuples_on REAL
K209(multreal,p,s) is set
Sum (mlt (p,s)) is V31() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like functional empty ordinal natural V31() real ext-real non positive non negative V40() V45() V47( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of 0 -tuples_on REAL
Sum f is V31() real ext-real Element of REAL
dom f is functional empty ordinal V45() V47( 0 ) FinSequence-membered V65() V66() V67() V68() V69() V70() V71() Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like functional empty ordinal natural V31() real ext-real non positive non negative V40() V45() V47( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of 0 -tuples_on REAL
p is Relation-like NAT -defined REAL -valued Function-like functional empty ordinal natural V31() real ext-real non positive non negative V40() V45() V47( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of 0 -tuples_on REAL
mlt (f,p) is Relation-like NAT -defined REAL -valued Function-like functional empty ordinal natural V31() real ext-real non positive non negative V40() V45() V47( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of 0 -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,f,p) is set
Sum (mlt (f,p)) is V31() real ext-real Element of REAL
X . (Sum (mlt (f,p))) is V31() real ext-real Element of REAL
mlt (f,r) is Relation-like NAT -defined REAL -valued Function-like functional empty ordinal natural V31() real ext-real non positive non negative V40() V45() V47( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of 0 -tuples_on REAL
K209(multreal,f,r) is set
Sum (mlt (f,r)) is V31() real ext-real Element of REAL
f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
f -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
Sum p is V31() real ext-real Element of REAL
dom p is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
mlt (p,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,p,r) is set
Sum (mlt (p,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (p,r))) is V31() real ext-real Element of REAL
mlt (p,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,p,s) is set
Sum (mlt (p,s)) is V31() real ext-real Element of REAL
f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
f -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
Sum p is V31() real ext-real Element of REAL
dom p is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
mlt (p,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,p,r) is set
Sum (mlt (p,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (p,r))) is V31() real ext-real Element of REAL
mlt (p,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,p,s) is set
Sum (mlt (p,s)) is V31() real ext-real Element of REAL
dom X is set
f is V31() real ext-real Element of REAL
1 - f is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
f * p is V31() real ext-real Element of REAL
(1 - f) * r is V31() real ext-real Element of REAL
(f * p) + ((1 - f) * r) is V31() real ext-real Element of REAL
X . ((f * p) + ((1 - f) * r)) is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
f * (X . p) is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(1 - f) * (X . r) is V31() real ext-real Element of REAL
(f * (X . p)) + ((1 - f) * (X . r)) is V31() real ext-real Element of REAL
2 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 2 } is set
<*f,(1 - f)*> is Relation-like NAT -defined Function-like non empty V40() V47(2) FinSequence-like FinSubsequence-like set
<*p,r*> is Relation-like NAT -defined Function-like non empty V40() V47(2) FinSequence-like FinSubsequence-like set
<*(X . p),(X . r)*> is Relation-like NAT -defined Function-like non empty V40() V47(2) FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(2) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of 2 -tuples_on REAL
dom s is V47(2) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
c7 is Relation-like NAT -defined REAL -valued Function-like V40() V47(2) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of 2 -tuples_on REAL
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(2) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of 2 -tuples_on REAL
len s is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len s) is V40() V47( len s) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
r is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
s . r is V31() real ext-real Element of REAL
c7 . r is V31() real ext-real Element of REAL
s . r is V31() real ext-real Element of REAL
X . (s . r) is V31() real ext-real Element of REAL
Sum s is V31() real ext-real Element of REAL
f + (1 - f) is V31() real ext-real Element of REAL
mlt (s,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(2) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of 2 -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,s,s) is set
Sum (mlt (s,s)) is V31() real ext-real Element of REAL
X . (Sum (mlt (s,s))) is V31() real ext-real Element of REAL
mlt (s,c7) is Relation-like NAT -defined REAL -valued Function-like V40() V47(2) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of 2 -tuples_on REAL
K209(multreal,s,c7) is set
Sum (mlt (s,c7)) is V31() real ext-real Element of REAL
s . 1 is V31() real ext-real Element of REAL
s . 2 is V31() real ext-real Element of REAL
len s is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len s is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
multreal .: (s,s) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
len (multreal .: (s,s)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len (mlt (s,s)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
(mlt (s,s)) . 1 is V31() real ext-real Element of REAL
s . 1 is V31() real ext-real Element of REAL
(s . 1) * (s . 1) is V31() real ext-real Element of REAL
(mlt (s,s)) . 2 is V31() real ext-real Element of REAL
s . 2 is V31() real ext-real Element of REAL
(s . 2) * (s . 2) is V31() real ext-real Element of REAL
<*(f * p),((1 - f) * r)*> is Relation-like NAT -defined Function-like non empty V40() V47(2) FinSequence-like FinSubsequence-like set
(mlt (s,c7)) . 1 is V31() real ext-real Element of REAL
c7 . 1 is V31() real ext-real Element of REAL
(s . 1) * (c7 . 1) is V31() real ext-real Element of REAL
(mlt (s,c7)) . 2 is V31() real ext-real Element of REAL
c7 . 2 is V31() real ext-real Element of REAL
(s . 2) * (c7 . 2) is V31() real ext-real Element of REAL
len c7 is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
multreal .: (s,c7) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-yielding V56() V57() FinSequence of REAL
len (multreal .: (s,c7)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
len (mlt (s,c7)) is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
<*(f * (X . p)),((1 - f) * (X . r))*> is Relation-like NAT -defined Function-like non empty V40() V47(2) FinSequence-like FinSubsequence-like set
f is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
f -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
s is ordinal natural V31() real ext-real V36() V37() V40() V45() V65() V66() V67() V68() V69() V70() Element of NAT
s -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = s } is set
p is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
Sum p is V31() real ext-real Element of REAL
dom p is V47(f) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
mlt (p,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
multreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) V21( REAL ) V22( REAL ) complex-yielding V56() V57() Element of K19(K20(K20(REAL,REAL),REAL))
K209(multreal,p,r) is set
Sum (mlt (p,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (p,r))) is V31() real ext-real Element of REAL
mlt (p,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(f) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of f -tuples_on REAL
K209(multreal,p,s) is set
Sum (mlt (p,s)) is V31() real ext-real Element of REAL
c7 is Relation-like NAT -defined REAL -valued Function-like V40() V47(s) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of s -tuples_on REAL
Sum c7 is V31() real ext-real Element of REAL
dom c7 is V47(s) V65() V66() V67() V68() V69() V70() Element of K19(NAT)
s is Relation-like NAT -defined REAL -valued Function-like V40() V47(s) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of s -tuples_on REAL
r is Relation-like NAT -defined REAL -valued Function-like V40() V47(s) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of s -tuples_on REAL
mlt (c7,r) is Relation-like NAT -defined REAL -valued Function-like V40() V47(s) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of s -tuples_on REAL
K209(multreal,c7,r) is set
Sum (mlt (c7,r)) is V31() real ext-real Element of REAL
X . (Sum (mlt (c7,r))) is V31() real ext-real Element of REAL
mlt (c7,s) is Relation-like NAT -defined REAL -valued Function-like V40() V47(s) FinSequence-like FinSubsequence-like complex-yielding V56() V57() Element of s -tuples_on REAL
K209(multreal,c7,s) is set
Sum (mlt (c7,s)) is V31() real ext-real Element of REAL
X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
f is V65() V66() V67() V87() Element of K19(REAL)
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
X . p is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
abs (((X . r) - (X . p)) / (r - p)) is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
(X . s) - (X . p) is V31() real ext-real Element of REAL
s - p is V31() real ext-real Element of REAL
((X . s) - (X . p)) / (s - p) is V31() real ext-real Element of REAL
abs (((X . s) - (X . p)) / (s - p)) is V31() real ext-real Element of REAL
max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))) is V31() real ext-real set
c7 is V31() real ext-real Element of REAL
X . c7 is V31() real ext-real Element of REAL
(X . c7) - (X . p) is V31() real ext-real Element of REAL
c7 - p is V31() real ext-real Element of REAL
((X . c7) - (X . p)) / (c7 - p) is V31() real ext-real Element of REAL
(X . p) - (X . r) is V31() real ext-real Element of REAL
p - r is V31() real ext-real Element of REAL
((X . p) - (X . r)) / (p - r) is V31() real ext-real Element of REAL
- ((X . p) - (X . r)) is V31() real ext-real Element of REAL
- (p - r) is V31() real ext-real Element of REAL
(- ((X . p) - (X . r))) / (- (p - r)) is V31() real ext-real Element of REAL
(X . p) - (X . c7) is V31() real ext-real Element of REAL
p - c7 is V31() real ext-real Element of REAL
((X . p) - (X . c7)) / (p - c7) is V31() real ext-real Element of REAL
- ((X . p) - (X . c7)) is V31() real ext-real Element of REAL
- (p - c7) is V31() real ext-real Element of REAL
(- ((X . p) - (X . c7))) / (- (p - c7)) is V31() real ext-real Element of REAL
(X . p) - (X . c7) is V31() real ext-real Element of REAL
p - c7 is V31() real ext-real Element of REAL
((X . p) - (X . c7)) / (p - c7) is V31() real ext-real Element of REAL
(X . s) - (X . c7) is V31() real ext-real Element of REAL
s - c7 is V31() real ext-real Element of REAL
((X . s) - (X . c7)) / (s - c7) is V31() real ext-real Element of REAL
- ((X . p) - (X . c7)) is V31() real ext-real Element of REAL
- (p - c7) is V31() real ext-real Element of REAL
(- ((X . p) - (X . c7))) / (- (p - c7)) is V31() real ext-real Element of REAL
(X . p) - (X . r) is V31() real ext-real Element of REAL
p - r is V31() real ext-real Element of REAL
((X . p) - (X . r)) / (p - r) is V31() real ext-real Element of REAL
- ((X . p) - (X . r)) is V31() real ext-real Element of REAL
- (p - r) is V31() real ext-real Element of REAL
(- ((X . p) - (X . r))) / (- (p - r)) is V31() real ext-real Element of REAL
(X . c7) - (X . r) is V31() real ext-real Element of REAL
c7 - r is V31() real ext-real Element of REAL
((X . c7) - (X . r)) / (c7 - r) is V31() real ext-real Element of REAL
- (abs (((X . r) - (X . p)) / (r - p))) is V31() real ext-real Element of REAL
c7 is V31() real ext-real set
X . c7 is V31() real ext-real Element of REAL
(X . c7) - (X . p) is V31() real ext-real Element of REAL
abs ((X . c7) - (X . p)) is V31() real ext-real Element of REAL
c7 - p is V31() real ext-real Element of REAL
abs (c7 - p) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) * (abs (c7 - p)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
X . r is V31() real ext-real Element of REAL
(X . r) - (X . p) is V31() real ext-real Element of REAL
r - p is V31() real ext-real Element of REAL
((X . r) - (X . p)) / (r - p) is V31() real ext-real Element of REAL
abs (r - p) is V31() real ext-real Element of REAL
- (abs (((X . s) - (X . p)) / (s - p))) is V31() real ext-real Element of REAL
abs (((X . r) - (X . p)) / (r - p)) is V31() real ext-real Element of REAL
abs ((X . r) - (X . p)) is V31() real ext-real Element of REAL
(abs ((X . r) - (X . p))) / (abs (r - p)) is V31() real ext-real Element of REAL
abs (((X . r) - (X . p)) / (r - p)) is V31() real ext-real Element of REAL
abs ((X . r) - (X . p)) is V31() real ext-real Element of REAL
(abs ((X . r) - (X . p))) / (abs (r - p)) is V31() real ext-real Element of REAL
min ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))) is V31() real ext-real set
dom X is set
c7 is V31() real ext-real set
r is V31() real ext-real Element of REAL
r / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) is V31() real ext-real Element of REAL
p - r is V31() real ext-real Element of REAL
min ((p - r),(s - p)) is V31() real ext-real set
min ((r / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))))),(min ((p - r),(s - p)))) is V31() real ext-real set
x is V31() real ext-real set
x - p is V31() real ext-real Element of REAL
abs (x - p) is V31() real ext-real Element of REAL
X . x is V31() real ext-real Element of REAL
(X . x) - (X . p) is V31() real ext-real Element of REAL
abs ((X . x) - (X . p)) is V31() real ext-real Element of REAL
- (p - r) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) * (abs (x - p)) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) * (min ((r / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))))),(min ((p - r),(s - p))))) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) * (r / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))))) is V31() real ext-real Element of REAL
r * (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) is V31() real ext-real Element of REAL
(r * (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))))) / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) is V31() real ext-real Element of REAL
r * ((max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) / (max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p)))))) is V31() real ext-real Element of REAL
r * 1 is V31() real ext-real Element of REAL
p - r is V31() real ext-real Element of REAL
min ((p - r),(s - p)) is V31() real ext-real set
x is V31() real ext-real set
X . x is V31() real ext-real Element of REAL
(X . x) - (X . p) is V31() real ext-real Element of REAL
abs ((X . x) - (X . p)) is V31() real ext-real Element of REAL
x - p is V31() real ext-real Element of REAL
abs (x - p) is V31() real ext-real Element of REAL
(max ((abs (((X . r) - (X . p)) / (r - p))),(abs (((X . s) - (X . p)) / (s - p))))) * (abs (x - p)) is V31() real ext-real Element of REAL
x is V31() real ext-real set
x - p is V31() real ext-real Element of REAL
abs (x - p) is V31() real ext-real Element of REAL
X . x is V31() real ext-real Element of REAL
(X . x) - (X . p) is V31() real ext-real Element of REAL
abs ((X . x) - (X . p)) is V31() real ext-real Element of REAL
- (p - r) is V31() real ext-real Element of REAL
s is V31() real ext-real set
s is V31() real ext-real set
X is V31() real ext-real set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
f . X is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real set
s is V31() real ext-real Element of REAL
s - X is V31() real ext-real Element of REAL
abs (s - X) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(f . X) - (f . s) is V31() real ext-real Element of REAL
(f . s) - (f . X) is V31() real ext-real Element of REAL
abs ((f . s) - (f . X)) is V31() real ext-real Element of REAL
- (abs ((f . s) - (f . X))) is V31() real ext-real Element of REAL
- ((f . s) - (f . X)) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s - X is V31() real ext-real Element of REAL
abs (s - X) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(f . X) - (f . s) is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
r is V31() real ext-real set
s is V31() real ext-real Element of REAL
s - X is V31() real ext-real Element of REAL
abs (s - X) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(f . s) - (f . X) is V31() real ext-real Element of REAL
abs ((f . s) - (f . X)) is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
s - X is V31() real ext-real Element of REAL
abs (s - X) is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
(f . s) - (f . X) is V31() real ext-real Element of REAL
f . X is V31() real ext-real Element of REAL
p is V31() real ext-real set
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
min (r,s) is V31() real ext-real set
c7 is V31() real ext-real set
c7 - X is V31() real ext-real Element of REAL
abs (c7 - X) is V31() real ext-real Element of REAL
f . c7 is V31() real ext-real Element of REAL
(f . c7) - (f . X) is V31() real ext-real Element of REAL
abs ((f . c7) - (f . X)) is V31() real ext-real Element of REAL
(f . X) - (f . c7) is V31() real ext-real Element of REAL
- ((f . c7) - (f . X)) is V31() real ext-real Element of REAL
- ((f . X) - (f . c7)) is V31() real ext-real Element of REAL
- p is V31() real ext-real Element of REAL
c7 is V31() real ext-real set
c7 - X is V31() real ext-real Element of REAL
abs (c7 - X) is V31() real ext-real Element of REAL
f . c7 is V31() real ext-real Element of REAL
(f . c7) - (f . X) is V31() real ext-real Element of REAL
abs ((f . c7) - (f . X)) is V31() real ext-real Element of REAL
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
f | X is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is V31() real ext-real Element of REAL
dom (f | X) is set
p is V31() real ext-real Element of REAL
dom (f | X) is set
dom (f | X) is set
p is V31() real ext-real set
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(1 - p) * (max ((f . r),(f . s))) is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
p * (max ((f . r),(f . s))) is V31() real ext-real Element of REAL
(p * (max ((f . r),(f . s)))) + ((1 - p) * (max ((f . r),(f . s)))) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
dom f is set
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
dom f is set
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
p * (f . r) is V31() real ext-real Element of REAL
(1 - p) * (f . s) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
p * (f . s) is V31() real ext-real Element of REAL
(p * (f . s)) + ((1 - p) * (f . s)) is V31() real ext-real Element of REAL
(1 - p) * (f . r) is V31() real ext-real Element of REAL
(p * (f . r)) + ((1 - p) * (f . r)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
dom f is set
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
X is set
f is Relation-like REAL -defined REAL -valued Function-like complex-yielding V56() V57() Element of K19(K20(REAL,REAL))
dom f is set
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL
r is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
p * r is V31() real ext-real Element of REAL
(1 - p) * s is V31() real ext-real Element of REAL
(p * r) + ((1 - p) * s) is V31() real ext-real Element of REAL
f . r is V31() real ext-real Element of REAL
f . s is V31() real ext-real Element of REAL
max ((f . r),(f . s)) is V31() real ext-real set
f . ((p * r) + ((1 - p) * s)) is V31() real ext-real Element of REAL