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 REA