REAL is non empty non trivial V48() V49() V50() V54() non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty non trivial V48() V54() non finite set
RAT is non empty non trivial V48() V49() V50() V51() V54() non finite set
INT is non empty non trivial V48() V49() V50() V51() V52() V54() non finite set
omega is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() set
bool omega is non empty set
bool NAT is non empty set
[:COMPLEX,COMPLEX:] is non empty V36() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty V36() V37() V38() set
bool [:COMPLEX,REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
[:2,2:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
[:[:2,2:],2:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
bool [:[:2,2:],2:] is non empty set
[:REAL,REAL:] is non empty V36() V37() V38() set
bool [:REAL,REAL:] is non empty set
K409() is non empty V124() L9()
the carrier of K409() is non empty set
K414() is non empty L9()
K415() is non empty V124() M20(K414())
K416() is non empty V124() V155() V201() M23(K414(),K415())
K418() is non empty V124() V155() V157() V159() L9()
K419() is non empty V124() V155() V201() M20(K418())
I[01] is TopStruct
the carrier of I[01] is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
[:1,1:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V36() V37() V38() set
bool [:[:1,1:],REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V36() V37() V38() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:[:2,2:],REAL:] is non empty V36() V37() V38() set
bool [:[:2,2:],REAL:] is non empty set
RealSpace is strict MetrStruct
K506() is TopSpace-like TopStruct
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V122() V147() V148() V149() V150() V151() V152() V153() V186() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty functional set
bool the carrier of (TOP-REAL 2) is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V36() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty V23( RAT ) V36() V37() V38() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V23( RAT ) V36() V37() V38() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
[:[:NAT,NAT:],NAT:] is non empty V23( RAT ) V23( INT ) V36() V37() V38() V39() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real ext-real non positive non negative Function-like functional V46() V48() V49() V50() V51() V52() V53() V54() finite V59() FinSequence-membered set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V14() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V53() V54() finite V59() FinSequence-membered Element of NAT
K507(0,1) is non empty strict TopSpace-like SubSpace of K506()
K508() is TopSpace-like SubSpace of K506()
the carrier of K508() is set
q is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() set
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() set
q - 1 is V14() real ext-real V46() Element of REAL
c1 + 1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(c1 + 1) - 1 is V14() real ext-real V46() Element of REAL
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
c1 - q is V14() real ext-real V46() Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
Seg r is V48() V49() V50() V51() V52() V53() finite V72(r) Element of bool NAT
F1() is non empty set
F2() is V19() V22( NAT ) V23(F1()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of F1()
dom F2() is V48() V49() V50() V51() V52() V53() finite Element of bool NAT
{ F3(F2(),b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : ( b1 in dom F2() & P1[b1] ) } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : ( b1 in dom F2() & P1[b1] ) } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : b1 in dom F2() } is set
r is set
t is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
F3(F2(),t) is set
F1() is non empty set
F2() is V19() V22( NAT ) V23(F1()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of F1()
len F2() is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
{ F3(F2(),b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : ( 1 <= b1 & b1 <= len F2() & P1[b1] ) } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : ( 1 <= b1 & b1 <= len F2() & P1[b1] ) } is set
dom F2() is V48() V49() V50() V51() V52() V53() finite Element of bool NAT
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT : b1 in dom F2() } is set
r is set
t is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
F3(F2(),t) is set
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
REAL c1 is non empty functional FinSequence-membered M13( REAL )
K266(c1,REAL) is functional FinSequence-membered M13( REAL )
q is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
q - r is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(q - r).| is V14() real ext-real non negative Element of REAL
K396((q - r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((q - r),(q - r)) is V19() Function-like set
K402(K396((q - r))) is V14() real ext-real Element of REAL
K73(K402(K396((q - r)))) is V14() real ext-real Element of REAL
t is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r - t is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(r - t).| is V14() real ext-real non negative Element of REAL
K396((r - t)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((r - t),(r - t)) is V19() Function-like set
K402(K396((r - t))) is V14() real ext-real Element of REAL
K73(K402(K396((r - t)))) is V14() real ext-real Element of REAL
|.(q - r).| - |.(r - t).| is V14() real ext-real Element of REAL
q - t is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(q - t).| is V14() real ext-real non negative Element of REAL
K396((q - t)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((q - t),(q - t)) is V19() Function-like set
K402(K396((q - t))) is V14() real ext-real Element of REAL
K73(K402(K396((q - t)))) is V14() real ext-real Element of REAL
t - r is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(t - r).| is V14() real ext-real non negative Element of REAL
K396((t - r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((t - r),(t - r)) is V19() Function-like set
K402(K396((t - r))) is V14() real ext-real Element of REAL
K73(K402(K396((t - r)))) is V14() real ext-real Element of REAL
|.(q - t).| + |.(t - r).| is V14() real ext-real non negative Element of REAL
|.(q - t).| + |.(r - t).| is V14() real ext-real non negative Element of REAL
(|.(q - t).| + |.(r - t).|) - |.(r - t).| is V14() real ext-real Element of REAL
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
REAL c1 is non empty functional FinSequence-membered M13( REAL )
K266(c1,REAL) is functional FinSequence-membered M13( REAL )
r is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
q is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r - q is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(r - q).| is V14() real ext-real non negative Element of REAL
K396((r - q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((r - q),(r - q)) is V19() Function-like set
K402(K396((r - q))) is V14() real ext-real Element of REAL
K73(K402(K396((r - q)))) is V14() real ext-real Element of REAL
t is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r - t is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(r - t).| is V14() real ext-real non negative Element of REAL
K396((r - t)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((r - t),(r - t)) is V19() Function-like set
K402(K396((r - t))) is V14() real ext-real Element of REAL
K73(K402(K396((r - t)))) is V14() real ext-real Element of REAL
|.(r - q).| - |.(r - t).| is V14() real ext-real Element of REAL
t - q is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(t - q).| is V14() real ext-real non negative Element of REAL
K396((t - q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((t - q),(t - q)) is V19() Function-like set
K402(K396((t - q))) is V14() real ext-real Element of REAL
K73(K402(K396((t - q)))) is V14() real ext-real Element of REAL
q - r is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(q - r).| is V14() real ext-real non negative Element of REAL
K396((q - r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((q - r),(q - r)) is V19() Function-like set
K402(K396((q - r))) is V14() real ext-real Element of REAL
K73(K402(K396((q - r)))) is V14() real ext-real Element of REAL
q - t is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(q - t).| is V14() real ext-real non negative Element of REAL
K396((q - t)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((q - t),(q - t)) is V19() Function-like set
K402(K396((q - t))) is V14() real ext-real Element of REAL
K73(K402(K396((q - t)))) is V14() real ext-real Element of REAL
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
Euclid c1 is non empty strict Reflexive discerning V226() triangle MetrStruct
REAL c1 is non empty functional FinSequence-membered M13( REAL )
K266(c1,REAL) is functional FinSequence-membered M13( REAL )
Pitag_dist c1 is V19() V22([:(REAL c1),(REAL c1):]) V23( REAL ) Function-like V33([:(REAL c1),(REAL c1):], REAL ) V36() V37() V38() Element of bool [:[:(REAL c1),(REAL c1):],REAL:]
[:(REAL c1),(REAL c1):] is non empty set
[:[:(REAL c1),(REAL c1):],REAL:] is non empty V36() V37() V38() set
bool [:[:(REAL c1),(REAL c1):],REAL:] is non empty set
MetrStruct(# (REAL c1),(Pitag_dist c1) #) is strict MetrStruct
the carrier of (Euclid c1) is non empty set
q is Element of the carrier of (Euclid c1)
r is Element of the carrier of (Euclid c1)
dist (q,r) is V14() real ext-real Element of REAL
t is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
p0 is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
t - p0 is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(t - p0).| is V14() real ext-real non negative Element of REAL
K396((t - p0)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((t - p0),(t - p0)) is V19() Function-like set
K402(K396((t - p0))) is V14() real ext-real Element of REAL
K73(K402(K396((t - p0)))) is V14() real ext-real Element of REAL
(Pitag_dist c1) . (t,p0) is V14() real ext-real Element of REAL
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
TOP-REAL c1 is non empty TopSpace-like T_0 T_1 T_2 V122() V147() V148() V149() V150() V151() V152() V153() V186() strict RLTopStruct
the carrier of (TOP-REAL c1) is non empty functional set
bool the carrier of (TOP-REAL c1) is non empty set
q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
LSeg (q,r) is non empty functional V269( TOP-REAL c1) Element of bool the carrier of (TOP-REAL c1)
{ (((1 - b1) * q) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
t is non empty functional Element of bool the carrier of (TOP-REAL c1)
{ b1 where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 & ((1 - b1) * q) + (b1 * r) in t ) } is set
q1 is set
q2 is V14() real ext-real Element of REAL
1 - q2 is V14() real ext-real Element of REAL
(1 - q2) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,q2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q2) * q) + (q2 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
the U6 of (TOP-REAL c1) is V19() V22([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):]) V23( the carrier of (TOP-REAL c1)) Function-like V33([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1)) Element of bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):]
[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):] is non empty set
[:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q2) * q),(q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q2) * q),(q2 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q1 is V48() V49() V50() Element of bool REAL
lower_bound q1 is V14() real ext-real Element of REAL
q2 is V14() real ext-real Element of REAL
1 - q2 is V14() real ext-real Element of REAL
(1 - q2) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,q2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q2) * q) + (q2 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
the U6 of (TOP-REAL c1) is V19() V22([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):]) V23( the carrier of (TOP-REAL c1)) Function-like V33([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1)) Element of bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):]
[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):] is non empty set
[:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q2) * q),(q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q2) * q),(q2 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
F1 is ext-real set
PP is V14() real ext-real Element of REAL
1 - PP is V14() real ext-real Element of REAL
(1 - PP) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - PP)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
PP * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,PP) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - PP) * q) + (PP * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - PP) * q),(PP * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - PP) * q),(PP * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Euclid c1 is non empty strict Reflexive discerning V226() triangle MetrStruct
REAL c1 is non empty functional FinSequence-membered M13( REAL )
K266(c1,REAL) is functional FinSequence-membered M13( REAL )
Pitag_dist c1 is V19() V22([:(REAL c1),(REAL c1):]) V23( REAL ) Function-like V33([:(REAL c1),(REAL c1):], REAL ) V36() V37() V38() Element of bool [:[:(REAL c1),(REAL c1):],REAL:]
[:(REAL c1),(REAL c1):] is non empty set
[:[:(REAL c1),(REAL c1):],REAL:] is non empty V36() V37() V38() set
bool [:[:(REAL c1),(REAL c1):],REAL:] is non empty set
MetrStruct(# (REAL c1),(Pitag_dist c1) #) is strict MetrStruct
the carrier of (Euclid c1) is non empty set
the topology of (TOP-REAL c1) is non empty Element of bool (bool the carrier of (TOP-REAL c1))
bool (bool the carrier of (TOP-REAL c1)) is non empty set
TopStruct(# the carrier of (TOP-REAL c1), the topology of (TOP-REAL c1) #) is non empty strict TopSpace-like TopStruct
TopSpaceMetr (Euclid c1) is TopStruct
the carrier of (TopSpaceMetr (Euclid c1)) is set
bool the carrier of (TopSpaceMetr (Euclid c1)) is non empty set
t ` is functional Element of bool the carrier of (TOP-REAL c1)
the carrier of (TOP-REAL c1) \ t is set
u0 is Element of bool the carrier of (TopSpaceMetr (Euclid c1))
F2 is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
P2 is V14() real ext-real Element of REAL
1 - P2 is V14() real ext-real Element of REAL
(1 - P2) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - P2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
P2 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,P2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - P2) * q) + (P2 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - P2) * q),(P2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - P2) * q),(P2 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
the carrier of (TOP-REAL c1) \ t is functional Element of bool the carrier of (TOP-REAL c1)
PP is Element of the carrier of (Euclid c1)
F2 is V14() real ext-real set
Ball (PP,F2) is Element of bool the carrier of (Euclid c1)
bool the carrier of (Euclid c1) is non empty set
P2 is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
j is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
P2 - j is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(P2 - j).| is V14() real ext-real non negative Element of REAL
K396((P2 - j)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((P2 - j),(P2 - j)) is V19() Function-like set
K402(K396((P2 - j))) is V14() real ext-real Element of REAL
K73(K402(K396((P2 - j)))) is V14() real ext-real Element of REAL
F2 / |.(P2 - j).| is V14() real ext-real Element of REAL
q2 + (F2 / |.(P2 - j).|) is V14() real ext-real Element of REAL
F is V14() real ext-real Element of REAL
F is V14() real ext-real set
P1 is V14() real ext-real Element of REAL
P1 + 0 is V14() real ext-real Element of REAL
(F2 / |.(P2 - j).|) - 0 is V14() real ext-real Element of REAL
P1 - q2 is V14() real ext-real Element of REAL
1 - P1 is V14() real ext-real Element of REAL
(1 - P1) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - P1)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
P1 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,P1) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - P1) * q) + (P1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - P1) * q),(P1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - P1) * q),(P1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
- (((1 - q2) * q) + (q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K390((((1 - q2) * q) + (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K47(1) is V14() real ext-real non positive V46() set
K47(1) * (((1 - q2) * q) + (q2 * r)) is V19() Function-like set
K321((TOP-REAL c1),(((1 - P1) * q) + (P1 * r)),(- (((1 - q2) * q) + (q2 * r)))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + (P1 * r)),(- (((1 - q2) * q) + (q2 * r)))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + (P1 * r)),(- (((1 - q2) * q) + (q2 * r)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K392((((1 - P1) * q) + (P1 * r)),(((1 - q2) * q) + (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K201((((1 - q2) * q) + (q2 * r))) is V19() Function-like V36() set
K172((((1 - P1) * q) + (P1 * r)),K201((((1 - q2) * q) + (q2 * r)))) is V19() Function-like set
- ((1 - q2) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K390(((1 - q2) * q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K47(1) * ((1 - q2) * q) is V19() Function-like set
(- ((1 - q2) * q)) - (q2 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
- (q2 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K390((q2 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K47(1) * (q2 * r) is V19() Function-like set
K321((TOP-REAL c1),(- ((1 - q2) * q)),(- (q2 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(- ((1 - q2) * q)),(- (q2 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((- ((1 - q2) * q)),(- (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K392((- ((1 - q2) * q)),(q2 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K201((q2 * r)) is V19() Function-like V36() set
K172((- ((1 - q2) * q)),K201((q2 * r))) is V19() Function-like set
(((1 - P1) * q) + (P1 * r)) + ((- ((1 - q2) * q)) - (q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + (P1 * r)),((- ((1 - q2) * q)) - (q2 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + (P1 * r)),((- ((1 - q2) * q)) - (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + (P1 * r)) + (- ((1 - q2) * q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + (P1 * r)),(- ((1 - q2) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + (P1 * r)),(- ((1 - q2) * q))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((((1 - P1) * q) + (P1 * r)) + (- ((1 - q2) * q))) + (- (q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((((1 - P1) * q) + (P1 * r)) + (- ((1 - q2) * q))),(- (q2 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((((1 - P1) * q) + (P1 * r)) + (- ((1 - q2) * q))),(- (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - P1) * q) + (- ((1 - q2) * q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - P1) * q),(- ((1 - q2) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - P1) * q),(- ((1 - q2) * q))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P1 * r) + (((1 - P1) * q) + (- ((1 - q2) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(P1 * r),(((1 - P1) * q) + (- ((1 - q2) * q)))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((P1 * r),(((1 - P1) * q) + (- ((1 - q2) * q)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((P1 * r) + (((1 - P1) * q) + (- ((1 - q2) * q)))) + (- (q2 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((P1 * r) + (((1 - P1) * q) + (- ((1 - q2) * q)))),(- (q2 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((P1 * r) + (((1 - P1) * q) + (- ((1 - q2) * q)))),(- (q2 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + (- ((1 - q2) * q))) + (P1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + (- ((1 - q2) * q))),(P1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + (- ((1 - q2) * q))),(P1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
- q2 is V14() real ext-real Element of REAL
(- q2) * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,(- q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((((1 - P1) * q) + (- ((1 - q2) * q))) + (P1 * r)) + ((- q2) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((((1 - P1) * q) + (- ((1 - q2) * q))) + (P1 * r)),((- q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((((1 - P1) * q) + (- ((1 - q2) * q))) + (P1 * r)),((- q2) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
- (1 - q2) is V14() real ext-real Element of REAL
(- (1 - q2)) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(- (1 - q2))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - P1) * q) + ((- (1 - q2)) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - P1) * q),((- (1 - q2)) * q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - P1) * q),((- (1 - q2)) * q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + ((- (1 - q2)) * q)) + (P1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + ((- (1 - q2)) * q)),(P1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + ((- (1 - q2)) * q)),(P1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((((1 - P1) * q) + ((- (1 - q2)) * q)) + (P1 * r)) + ((- q2) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((((1 - P1) * q) + ((- (1 - q2)) * q)) + (P1 * r)),((- q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((((1 - P1) * q) + ((- (1 - q2)) * q)) + (P1 * r)),((- q2) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P1 * r) + ((- q2) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(P1 * r),((- q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((P1 * r),((- q2) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + ((- (1 - q2)) * q)) + ((P1 * r) + ((- q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + ((- (1 - q2)) * q)),((P1 * r) + ((- q2) * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + ((- (1 - q2)) * q)),((P1 * r) + ((- q2) * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
P1 + (- q2) is V14() real ext-real Element of REAL
(P1 + (- q2)) * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,(P1 + (- q2))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) * q) + ((- (1 - q2)) * q)) + ((P1 + (- q2)) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) * q) + ((- (1 - q2)) * q)),((P1 + (- q2)) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) * q) + ((- (1 - q2)) * q)),((P1 + (- q2)) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(1 - P1) + (- (1 - q2)) is V14() real ext-real Element of REAL
((1 - P1) + (- (1 - q2))) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,((1 - P1) + (- (1 - q2)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P1 - q2) * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,(P1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - P1) + (- (1 - q2))) * q) + ((P1 - q2) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - P1) + (- (1 - q2))) * q),((P1 - q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - P1) + (- (1 - q2))) * q),((P1 - q2) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
- (P1 - q2) is V14() real ext-real Element of REAL
(- (P1 - q2)) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(- (P1 - q2))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((- (P1 - q2)) * q) + ((P1 - q2) * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((- (P1 - q2)) * q),((P1 - q2) * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((- (P1 - q2)) * q),((P1 - q2) * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P1 - q2) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(P1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((P1 - q2) * r) - ((P1 - q2) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
- ((P1 - q2) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K390(((P1 - q2) * q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K47(1) * ((P1 - q2) * q) is V19() Function-like set
K321((TOP-REAL c1),((P1 - q2) * r),(- ((P1 - q2) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((P1 - q2) * r),(- ((P1 - q2) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((P1 - q2) * r),(- ((P1 - q2) * q))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K392(((P1 - q2) * r),((P1 - q2) * q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K201(((P1 - q2) * q)) is V19() Function-like V36() set
K172(((P1 - q2) * r),K201(((P1 - q2) * q))) is V19() Function-like set
r - q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
- q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K390(q) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K47(1) * q is V19() Function-like set
K321((TOP-REAL c1),r,(- q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),r,(- q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(r,(- q)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K392(r,q) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K201(q) is V19() Function-like V36() set
K172(r,K201(q)) is V19() Function-like set
(P1 - q2) * (r - q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394((r - q),(P1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P1 - q2) * (P2 - j) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
QQ is Element of the carrier of (Euclid c1)
dist (QQ,PP) is V14() real ext-real Element of REAL
r0 is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r0 is V19() V22( NAT ) Function-like finite V72(c1) FinSequence-like FinSubsequence-like Element of REAL c1
r0 - r0 is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like M14( REAL , REAL c1)
|.(r0 - r0).| is V14() real ext-real non negative Element of REAL
K396((r0 - r0)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189((r0 - r0),(r0 - r0)) is V19() Function-like set
K402(K396((r0 - r0))) is V14() real ext-real Element of REAL
K73(K402(K396((r0 - r0)))) is V14() real ext-real Element of REAL
|.((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r))).| is V14() real ext-real non negative Element of REAL
K396(((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189(((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r))),((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r)))) is V19() Function-like set
K402(K396(((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r))))) is V14() real ext-real Element of REAL
K73(K402(K396(((((1 - P1) * q) + (P1 * r)) - (((1 - q2) * q) + (q2 * r)))))) is V14() real ext-real Element of REAL
|.((P1 - q2) * (P2 - j)).| is V14() real ext-real non negative Element of REAL
K396(((P1 - q2) * (P2 - j))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
K189(((P1 - q2) * (P2 - j)),((P1 - q2) * (P2 - j))) is V19() Function-like set
K402(K396(((P1 - q2) * (P2 - j)))) is V14() real ext-real Element of REAL
K73(K402(K396(((P1 - q2) * (P2 - j))))) is V14() real ext-real Element of REAL
abs (P1 - q2) is V14() real ext-real Element of REAL
(abs (P1 - q2)) * |.(P2 - j).| is V14() real ext-real Element of REAL
(P1 - q2) * |.(P2 - j).| is V14() real ext-real Element of REAL
(F2 / |.(P2 - j).|) * |.(P2 - j).| is V14() real ext-real Element of REAL
dist (PP,QQ) is V14() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of (Euclid c1) : not F2 <= dist (PP,b1) } is set
p is V14() real ext-real Element of REAL
1 - p is V14() real ext-real Element of REAL
(1 - p) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - p)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
p * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,p) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - p) * q) + (p * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - p) * q),(p * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - p) * q),(p * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
{q} is non empty functional finite V59() Element of bool the carrier of (TOP-REAL c1)
(1 - q2) + q2 is V14() real ext-real Element of REAL
((1 - q2) + q2) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,((1 - q2) + q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
P2 is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
F1 is V14() real ext-real Element of REAL
1 - F1 is V14() real ext-real Element of REAL
(1 - F1) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - F1)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
F1 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,F1) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - F1) * q) + (F1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - F1) * q),(F1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - F1) * q),(F1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
c1 is epsilon-transitive epsilon-connected ordinal natural V14() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
TOP-REAL c1 is non empty TopSpace-like T_0 T_1 T_2 V122() V147() V148() V149() V150() V151() V152() V153() V186() strict RLTopStruct
the carrier of (TOP-REAL c1) is non empty functional set
q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
LSeg (q,r) is non empty functional V269( TOP-REAL c1) Element of bool the carrier of (TOP-REAL c1)
bool the carrier of (TOP-REAL c1) is non empty set
{ (((1 - b1) * q) + (b1 * r)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
t is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
p0 is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
LSeg (t,p0) is non empty functional V269( TOP-REAL c1) Element of bool the carrier of (TOP-REAL c1)
{ (((1 - b1) * t) + (b1 * p0)) where b1 is V14() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
q1 is V14() real ext-real Element of REAL
1 - q1 is V14() real ext-real Element of REAL
(1 - q1) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - q1)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q1 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,q1) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q1) * q) + (q1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
the U6 of (TOP-REAL c1) is V19() V22([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):]) V23( the carrier of (TOP-REAL c1)) Function-like V33([: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1)) Element of bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):]
[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):] is non empty set
[:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
bool [:[: the carrier of (TOP-REAL c1), the carrier of (TOP-REAL c1):], the carrier of (TOP-REAL c1):] is non empty set
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q1) * q),(q1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q1) * q),(q1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 is V14() real ext-real Element of REAL
1 - q2 is V14() real ext-real Element of REAL
(1 - q2) * t is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(t,(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 * p0 is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(p0,q2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q2) * t) + (q2 * p0) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q2) * t),(q2 * p0)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q2) * t),(q2 * p0)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
F1 is V14() real ext-real Element of REAL
1 - F1 is V14() real ext-real Element of REAL
(1 - F1) * q is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(q,(1 - F1)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
F1 * r is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(r,F1) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - F1) * q) + (F1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - F1) * q),(F1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - F1) * q),(F1 * r)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(1 - q2) * (((1 - F1) * q) + (F1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394((((1 - F1) * q) + (F1 * r)),(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 * ((1 - q1) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(((1 - q1) * q),q2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
q2 * (q1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394((q1 * r),q2) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(q2 * ((1 - q1) * q)) + (q2 * (q1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(q2 * ((1 - q1) * q)),(q2 * (q1 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((q2 * ((1 - q1) * q)),(q2 * (q1 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q2) * (((1 - F1) * q) + (F1 * r))) + ((q2 * ((1 - q1) * q)) + (q2 * (q1 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q2) * (((1 - F1) * q) + (F1 * r))),((q2 * ((1 - q1) * q)) + (q2 * (q1 * r)))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q2) * (((1 - F1) * q) + (F1 * r))),((q2 * ((1 - q1) * q)) + (q2 * (q1 * r)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(1 - q2) * ((1 - F1) * q) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394(((1 - F1) * q),(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(1 - q2) * (F1 * r) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K394((F1 * r),(1 - q2)) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),((1 - q2) * ((1 - F1) * q)),((1 - q2) * (F1 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388(((1 - q2) * ((1 - F1) * q)),((1 - q2) * (F1 * r))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))) + ((q2 * ((1 - q1) * q)) + (q2 * (q1 * r))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))),((q2 * ((1 - q1) * q)) + (q2 * (q1 * r)))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))),((q2 * ((1 - q1) * q)) + (q2 * (q1 * r)))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))) + (q2 * ((1 - q1) * q)) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K475( the carrier of (TOP-REAL c1), the U6 of (TOP-REAL c1),(((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))),(q2 * ((1 - q1) * q))) is V19() V22( NAT ) Function-like V36() V37() V38() finite V72(c1) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL c1)
K388((((1 - q2) * ((1 - F1) * q)) + ((1 - q2) * (F1 * r))),(q2 * ((1 - q1) * q))) is V19() V22( NAT ) V23( REAL ) Function-like V36() V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL
((