:: TOPALG_2 semantic presentation

REAL is non empty V40() V166() V167() V168() V172() V259() V260() interval set
NAT is V166() V167() V168() V169() V170() V171() V172() V259() Element of bool REAL
bool REAL is set
I[01] is non empty strict TopSpace-like real-membered pathwise_connected SubSpace of R^1
R^1 is non empty strict TopSpace-like real-membered TopStruct
the carrier of I[01] is non empty V166() V167() V168() set
[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],I[01]:] is non empty set
COMPLEX is non empty V40() V166() V172() set
RAT is non empty V40() V166() V167() V168() V169() V172() set
INT is non empty V40() V166() V167() V168() V169() V170() V172() set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
omega is V166() V167() V168() V169() V170() V171() V172() V259() set
bool omega is set
bool NAT is set
K261() is set
1 is non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set
2 is non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() Element of NAT
[:2,2:] is set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is set
I[01] is non empty strict TopSpace-like real-membered pathwise_connected TopStruct
the carrier of I[01] is non empty V166() V167() V168() set
K358() is V108() real-membered L7()
0 is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
the empty trivial V166() V167() V168() V169() V170() V171() V172() V259() interval set is empty trivial V166() V167() V168() V169() V170() V171() V172() V259() interval set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V166() V167() V168() set
TOP-REAL 1 is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
the carrier of (TOP-REAL 1) is non empty set
{} is set
{{},1} is set
[: the carrier of I[01], the carrier of I[01]:] is set
bool [: the carrier of I[01], the carrier of I[01]:] is set
bool the carrier of [:I[01],I[01]:] is set
[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:I[01],I[01]:] is non empty set
K667() is non empty V134() L10()
the carrier of K667() is non empty set
K672() is non empty V134() V220() V221() V222() V224() V250() V251() V252() V253() V254() V255() L10()
K673() is non empty V134() V222() V224() V253() V254() V255() M33(K672())
K674() is non empty V134() V220() V222() V224() V253() V254() V255() V256() M36(K672(),K673())
K676() is non empty V134() V220() V222() V224() L10()
K677() is non empty V134() V220() V222() V224() V256() M33(K676())
0[01] is V11() real ext-real Element of the carrier of I[01]
1[01] is V11() real ext-real Element of the carrier of I[01]
the carrier of R^1 is non empty V166() V167() V168() set
[: the carrier of (TOP-REAL 1), the carrier of R^1:] is set
bool [: the carrier of (TOP-REAL 1), the carrier of R^1:] is set
(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
I is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL I is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
the carrier of (TOP-REAL I) is non empty set
bool the carrier of (TOP-REAL I) is set
the Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I) is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
LSeg ( the Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I), the Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)) is non empty convex Element of bool the carrier of (TOP-REAL I)
{ (((1 - b₁) * the Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)) + (b₁ * the Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I))) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
I is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL I is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
I is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL I is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
T is non empty TopSpace-like SubSpace of TOP-REAL I
[#] T is non empty non proper V80(T) Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is set
the carrier of (TOP-REAL I) is non empty set
bool the carrier of (TOP-REAL I) is set
a is Element of the carrier of T
b is Element of the carrier of T
P is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
Q is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
LSeg (P,Q) is non empty convex Element of bool the carrier of (TOP-REAL I)
{ (((1 - b₁) * P) + (b₁ * Q)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
(TOP-REAL I) | (LSeg (P,Q)) is non empty strict TopSpace-like SubSpace of TOP-REAL I
[#] ((TOP-REAL I) | (LSeg (P,Q))) is non empty non proper V80((TOP-REAL I) | (LSeg (P,Q))) Element of bool the carrier of ((TOP-REAL I) | (LSeg (P,Q)))
the carrier of ((TOP-REAL I) | (LSeg (P,Q))) is non empty set
bool the carrier of ((TOP-REAL I) | (LSeg (P,Q))) is set
[: the carrier of I[01], the carrier of ((TOP-REAL I) | (LSeg (P,Q))):] is set
bool [: the carrier of I[01], the carrier of ((TOP-REAL I) | (LSeg (P,Q))):] is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL I) | (LSeg (P,Q))) -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL I) | (LSeg (P,Q))):]
Q . 0 is set
Q . 1 is set
[: the carrier of I[01], the carrier of T:] is set
bool [: the carrier of I[01], the carrier of T:] is set
s is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
s . 0 is set
s . 1 is set
P is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
Q is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
P is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
Q is Relation-like REAL -valued Function-like V47(I) FinSequence-like V158() Element of the carrier of (TOP-REAL I)
I is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL I is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
the carrier of (TOP-REAL I) is non empty set
the topology of (TOP-REAL I) is non empty Element of bool (bool the carrier of (TOP-REAL I))
bool the carrier of (TOP-REAL I) is set
bool (bool the carrier of (TOP-REAL I)) is set
TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #) is non empty strict TopSpace-like TopStruct
T is TopSpace-like SubSpace of TOP-REAL I
[#] (TOP-REAL I) is non empty non proper non proper V80( TOP-REAL I) V80( TOP-REAL I) convex Element of bool the carrier of (TOP-REAL I)
[#] TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #) is non empty non proper V80( TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #)) Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #)
the carrier of TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #) is non empty set
bool the carrier of TopStruct(# the carrier of (TOP-REAL I), the topology of (TOP-REAL I) #) is set
[#] T is non proper V80(T) Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is set
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
T is non empty TopSpace-like SubSpace of I
the carrier of T is non empty set
a is Element of the carrier of I
b is Element of the carrier of I
P is Element of the carrier of T
Q is Element of the carrier of T
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Path of P,Q
bool the carrier of I is set
[: the carrier of I[01], the carrier of I:] is set
bool [: the carrier of I[01], the carrier of I:] is set
s is non empty Relation-like the carrier of I[01] -defined the carrier of I -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of I:]
s . 0 is set
s . 1 is set
[:(TOP-REAL 1),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL 1),I[01]:] is non empty set
[: the carrier of (TOP-REAL 1), the carrier of I[01]:] is set
[:R^1,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:R^1,I[01]:] is non empty set
[: the carrier of R^1, the carrier of I[01]:] is set
id I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total continuous V104( I[01] , I[01] ) Element of bool [: the carrier of I[01], the carrier of I[01]:]
id the carrier of I[01] is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued total quasi_total Element of bool [: the carrier of I[01], the carrier of I[01]:]
dom (id I[01]) is set
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
[: the carrier of I[01], the carrier of a:] is set
bool [: the carrier of I[01], the carrier of a:] is set
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
the carrier of (TOP-REAL T) is non empty set
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of a:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of a:]
Q is V11() real ext-real Element of the carrier of I[01]
Q is V11() real ext-real Element of the carrier of I[01]
b . Q is Element of the carrier of a
P . Q is Element of the carrier of a
1 - Q is V11() real ext-real Element of REAL
bool the carrier of (TOP-REAL T) is set
s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(1 - Q) * s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(s,(1 - Q)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
Q * t is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(t,Q) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - Q) * s) + (Q * t) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - Q) * s),(Q * t)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
[#] a is non empty non proper V80(a) Element of bool the carrier of a
bool the carrier of a is set
LSeg (s,t) is non empty convex Element of bool the carrier of (TOP-REAL T)
{ (((1 - b₁) * s) + (b₁ * t)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
[:[: the carrier of I[01], the carrier of I[01]:], the carrier of a:] is set
bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of a:] is set
Q is Relation-like [: the carrier of I[01], the carrier of I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of a:]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
s is V11() real ext-real Element of the carrier of I[01]
b . s is Element of the carrier of a
P . s is Element of the carrier of a
t is V11() real ext-real Element of the carrier of I[01]
Q . (s,t) is set
[s,t] is non empty set
{s,t} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,t},{s}} is set
Q . [s,t] is set
1 - t is V11() real ext-real Element of REAL
P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(1 - t) * P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1,(1 - t)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,t) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - t) * P1) + (t * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - t) * P1),(t * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(1 - t) * P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1,(1 - t)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,t) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - t) * P1) + (t * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - t) * P1),(t * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
s is V11() real ext-real Element of the carrier of I[01]
t is V11() real ext-real Element of the carrier of I[01]
Q . (s,t) is set
[s,t] is non empty set
{s,t} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,t},{s}} is set
Q . [s,t] is set
Q . (s,t) is set
Q . [s,t] is set
b . s is Element of the carrier of a
P . s is Element of the carrier of a
P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
1 - t is V11() real ext-real Element of REAL
(1 - t) * P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1,(1 - t)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
t * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,t) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - t) * P1) + (t * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - t) * P1),(t * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
[: the carrier of I[01], the carrier of a:] is set
bool [: the carrier of I[01], the carrier of a:] is set
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
(T,a,b,P) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
the carrier of (TOP-REAL T) is non empty set
bool the carrier of (TOP-REAL T) is set
[: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):] is set
[: the carrier of I[01], the carrier of (TOP-REAL T):] is set
bool [: the carrier of I[01], the carrier of (TOP-REAL T):] is set
[:b,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:a,I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:]
[:a,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:] is set
[:P,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:a,I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:]
s is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of (TOP-REAL T):]
t is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of (TOP-REAL T):]
Q1 is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL T):]
[:Q1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:(TOP-REAL T),I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL T),I[01]:]:]
[:(TOP-REAL T),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL T),I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL T),I[01]:]:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL T),I[01]:]:] is set
P1I is non empty Relation-like the carrier of I[01] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of (TOP-REAL T):]
[:P1I,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:(TOP-REAL T),I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(TOP-REAL T),I[01]:]:]
[: the carrier of (TOP-REAL T), the carrier of I[01]:] is set
[:[: the carrier of (TOP-REAL T), the carrier of I[01]:], the carrier of (TOP-REAL T):] is set
bool [:[: the carrier of (TOP-REAL T), the carrier of I[01]:], the carrier of (TOP-REAL T):] is set
Pb is Relation-like [: the carrier of (TOP-REAL T), the carrier of I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL T), the carrier of I[01]:], the carrier of (TOP-REAL T):]
Pa is Relation-like [: the carrier of (TOP-REAL T), the carrier of I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL T), the carrier of I[01]:], the carrier of (TOP-REAL T):]
[: the carrier of [:(TOP-REAL T),I[01]:], the carrier of (TOP-REAL T):] is set
bool [: the carrier of [:(TOP-REAL T),I[01]:], the carrier of (TOP-REAL T):] is set
g is non empty Relation-like the carrier of [:(TOP-REAL T),I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL T),I[01]:], the carrier of (TOP-REAL T):]
Pb is non empty Relation-like the carrier of [:(TOP-REAL T),I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL T),I[01]:], the carrier of (TOP-REAL T):]
Pb * [:Q1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
g * [:P1I,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
p is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
dom P is set
dom b is set
s is Element of the carrier of [:I[01],I[01]:]
Q . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(Pb * [:Q1,(id I[01]):]) . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(g * [:P1I,(id I[01]):]) . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
((Pb * [:Q1,(id I[01]):]) . s) + ((g * [:P1I,(id I[01]):]) . s) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((Pb * [:Q1,(id I[01]):]) . s),((g * [:P1I,(id I[01]):]) . s)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t is V11() real ext-real Element of the carrier of I[01]
a1 is V11() real ext-real Element of the carrier of I[01]
[t,a1] is non empty Element of the carrier of [:I[01],I[01]:]
{t,a1} is V166() V167() V168() set
{t} is trivial V166() V167() V168() set
{{t,a1},{t}} is set
b . t is Element of the carrier of a
P . t is Element of the carrier of a
(T,a,b,P) . (t,a1) is set
[t,a1] is non empty set
(T,a,b,P) . [t,a1] is set
b1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
1 - a1 is V11() real ext-real Element of REAL
(1 - a1) * b1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(b1,(1 - a1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
b1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
a1 * b1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(b1,a1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - a1) * b1) + (a1 * b1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - a1) * b1),(a1 * b1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(id I[01]) . a1 is V11() real ext-real Element of the carrier of I[01]
g * [:P,(id I[01]):] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
(g * [:P,(id I[01]):]) . s is set
[:P,(id I[01]):] . (t,a1) is set
[:P,(id I[01]):] . [t,a1] is set
g . ([:P,(id I[01]):] . (t,a1)) is set
g . ((P . t),a1) is set
[(P . t),a1] is non empty set
{(P . t),a1} is set
{(P . t)} is trivial set
{{(P . t),a1},{(P . t)}} is set
g . [(P . t),a1] is set
P1I . t is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
a1 * (P1I . t) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652((P1I . t),a1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Pb * [:b,(id I[01]):] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of (TOP-REAL T) -valued Function-like Element of bool [: the carrier of [:I[01],I[01]:], the carrier of (TOP-REAL T):]
(Pb * [:b,(id I[01]):]) . s is set
[:b,(id I[01]):] . (t,a1) is set
[:b,(id I[01]):] . [t,a1] is set
Pb . ([:b,(id I[01]):] . (t,a1)) is set
Pb . ((b . t),a1) is set
[(b . t),a1] is non empty set
{(b . t),a1} is set
{(b . t)} is trivial set
{{(b . t),a1},{(b . t)}} is set
Pb . [(b . t),a1] is set
Q1 . t is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(1 - a1) * (Q1 . t) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652((Q1 . t),(1 - a1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
s is Element of the carrier of [:I[01],I[01]:]
Q . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
p . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(Pb * [:Q1,(id I[01]):]) . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(g * [:P1I,(id I[01]):]) . s is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
((Pb * [:Q1,(id I[01]):]) . s) + ((g * [:P1I,(id I[01]):]) . s) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((Pb * [:Q1,(id I[01]):]) . s),((g * [:P1I,(id I[01]):]) . s)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
P is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of P is non empty set
Q is Element of the carrier of P
Q is Element of the carrier of P
s is non empty Relation-like the carrier of I[01] -defined the carrier of P -valued Function-like total quasi_total continuous Path of Q,Q
t is non empty Relation-like the carrier of I[01] -defined the carrier of P -valued Function-like total quasi_total continuous Path of Q,Q
(T,P,s,t) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of P -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of P:]
[: the carrier of [:I[01],I[01]:], the carrier of P:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of P:] is set
Q1 is V11() real ext-real Element of the carrier of I[01]
(T,P,s,t) . (Q1,0) is set
[Q1,0] is non empty set
{Q1,0} is V166() V167() V168() set
{Q1} is trivial V166() V167() V168() set
{{Q1,0},{Q1}} is set
(T,P,s,t) . [Q1,0] is set
s . Q1 is Element of the carrier of P
(T,P,s,t) . (Q1,1) is set
[Q1,1] is non empty set
{Q1,1} is V166() V167() V168() set
{{Q1,1},{Q1}} is set
(T,P,s,t) . [Q1,1] is set
t . Q1 is Element of the carrier of P
the carrier of (TOP-REAL T) is non empty set
a is V11() real ext-real Element of the carrier of I[01]
s . a is Element of the carrier of P
(T,P,s,t) . (Q1,a) is set
[Q1,a] is non empty set
{Q1,a} is V166() V167() V168() set
{{Q1,a},{Q1}} is set
(T,P,s,t) . [Q1,a] is set
P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
1 - a is V11() real ext-real Element of REAL
(1 - a) * P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1,(1 - a)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
a * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,a) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - a) * P1) + (a * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - a) * P1),(a * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
0 * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,0) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
P1 + (0 * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(P1,(0 * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
0. (TOP-REAL T) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V70( TOP-REAL T) V158() Element of the carrier of (TOP-REAL T)
the ZeroF of (TOP-REAL T) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
P1 + (0. (TOP-REAL T)) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(P1,(0. (TOP-REAL T))) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
b is V11() real ext-real Element of the carrier of I[01]
(T,P,s,t) . (Q1,b) is set
[Q1,b] is non empty set
{Q1,b} is V166() V167() V168() set
{{Q1,b},{Q1}} is set
(T,P,s,t) . [Q1,b] is set
1 - b is V11() real ext-real Element of REAL
(1 - b) * P1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1,(1 - b)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
b * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,b) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - b) * P1) + (b * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - b) * P1),(b * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
1 * Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(0. (TOP-REAL T)) + (1 * Q1) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646((0. (TOP-REAL T)),(1 * Q1)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(0. (TOP-REAL T)) + Q1 is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646((0. (TOP-REAL T)),Q1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t . a is Element of the carrier of P
Pa is V11() real ext-real Element of the carrier of I[01]
(T,P,s,t) . (0,Pa) is set
[0,Pa] is non empty set
{0,Pa} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,Pa},{0}} is set
(T,P,s,t) . [0,Pa] is set
(T,P,s,t) . (1,Pa) is set
[1,Pa] is non empty set
{1,Pa} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,Pa},{1}} is set
(T,P,s,t) . [1,Pa] is set
P1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
1 - Pa is V11() real ext-real Element of REAL
(1 - Pa) * P1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1I,(1 - Pa)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
Pa * Q1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Q1I,Pa) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - Pa) * P1I) + (Pa * Q1I) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - Pa) * P1I),(Pa * Q1I)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
1 * P1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1I,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Pa * P1I is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(P1I,Pa) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(1 * P1I) - (Pa * P1I) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K650((1 * P1I),(Pa * P1I)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 * P1I) - (Pa * P1I)) + (Pa * P1I) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 * P1I) - (Pa * P1I)),(Pa * P1I)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
t . b is Element of the carrier of P
s . b is Element of the carrier of P
Pb is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
(1 - Pa) * Pb is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Pb,(1 - Pa)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Pa is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
Pa * Pa is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Pa,Pa) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 - Pa) * Pb) + (Pa * Pa) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 - Pa) * Pb),(Pa * Pa)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
1 * Pb is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Pb,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(1 * Pb) - (Pa * Pa) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K650((1 * Pb),(Pa * Pa)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Pa * Pb is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Pb,Pa) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
((1 * Pb) - (Pa * Pa)) + (Pa * Pb) is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K646(((1 * Pb) - (Pa * Pa)),(Pa * Pb)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
1 * Pa is Relation-like REAL -valued Function-like V47(T) FinSequence-like V158() Element of the carrier of (TOP-REAL T)
K652(Pa,1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
b is Element of the carrier of a
P is Element of the carrier of a
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
(T,a,Q,Q) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
s is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
t is V11() real ext-real Element of the carrier of I[01]
s . (t,0) is set
[t,0] is non empty set
{t,0} is V166() V167() V168() set
{t} is trivial V166() V167() V168() set
{{t,0},{t}} is set
s . [t,0] is set
Q . t is Element of the carrier of a
P1 is V11() real ext-real Element of the carrier of I[01]
s . (P1,1) is set
[P1,1] is non empty set
{P1,1} is V166() V167() V168() set
{P1} is trivial V166() V167() V168() set
{{P1,1},{P1}} is set
s . [P1,1] is set
Q . P1 is Element of the carrier of a
Q1 is V11() real ext-real Element of the carrier of I[01]
s . (0,Q1) is set
[0,Q1] is non empty set
{0,Q1} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,Q1},{0}} is set
s . [0,Q1] is set
P1 is V11() real ext-real Element of the carrier of I[01]
s . (1,P1) is set
[1,P1] is non empty set
{1,P1} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,P1},{1}} is set
s . [1,P1] is set
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
b is Element of the carrier of a
P is Element of the carrier of a
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
s is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Homotopy of Q,Q
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
b is Element of the carrier of a
FundamentalGroup (a,b) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the carrier of (FundamentalGroup (a,b)) is non empty set
Loops b is non empty set
Paths (b,b) is non empty set
EqRel (a,b) is non empty Relation-like Loops b -defined Loops b -valued total quasi_total V97() V102() Element of bool [:(Loops b),(Loops b):]
[:(Loops b),(Loops b):] is set
bool [:(Loops b),(Loops b):] is set
EqRel (a,b,b) is Relation-like Paths (b,b) -defined Paths (b,b) -valued Element of bool [:(Paths (b,b)),(Paths (b,b)):]
[:(Paths (b,b)),(Paths (b,b)):] is set
bool [:(Paths (b,b)),(Paths (b,b)):] is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,b
Class ((EqRel (a,b)),P) is Element of bool (Loops b)
bool (Loops b) is set
{(Class ((EqRel (a,b)),P))} is trivial set
Q is set
s is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,b
Class ((EqRel (a,b)),s) is Element of bool (Loops b)
Q is set
Class (EqRel (a,b)) is a_partition of Loops b
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
b is Element of the carrier of a
FundamentalGroup (a,b) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant total quasi_total continuous Path of b,b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant total quasi_total continuous Path of b,b
EqRel (a,b) is non empty Relation-like Loops b -defined Loops b -valued total quasi_total V97() V102() Element of bool [:(Loops b),(Loops b):]
Loops b is non empty set
Paths (b,b) is non empty set
[:(Loops b),(Loops b):] is set
bool [:(Loops b),(Loops b):] is set
EqRel (a,b,b) is Relation-like Paths (b,b) -defined Paths (b,b) -valued Element of bool [:(Paths (b,b)),(Paths (b,b)):]
[:(Paths (b,b)),(Paths (b,b)):] is set
bool [:(Paths (b,b)),(Paths (b,b)):] is set
the carrier of (FundamentalGroup (a,b)) is non empty set
Class (EqRel (a,b)) is a_partition of Loops b
Class ((EqRel (a,b)), the non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant total quasi_total continuous Path of b,b) is Element of bool (Loops b)
bool (Loops b) is set
{(Class ((EqRel (a,b)), the non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like constant total quasi_total continuous Path of b,b))} is trivial set
T is V11() real ext-real set
|[T]| is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
|[T]| /. 1 is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
<*a*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
<*a*> /. 1 is V11() real ext-real Element of REAL
T is V11() real ext-real set
a is V11() real ext-real set
[.T,a.] is V166() V167() V168() interval Element of bool REAL
{ (((1 - b₁) * T) + (b₁ * a)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
P is set
Q is V11() real ext-real Element of REAL
a - T is V11() real ext-real set
a - a is V11() real ext-real set
Q - T is V11() real ext-real Element of REAL
(Q - T) / (a - T) is V11() real ext-real Element of REAL
Q is V11() real ext-real Element of REAL
[.0,1.] is V166() V167() V168() interval Element of bool REAL
1 - Q is V11() real ext-real Element of REAL
(1 - Q) * T is V11() real ext-real Element of REAL
Q * a is V11() real ext-real Element of REAL
((1 - Q) * T) + (Q * a) is V11() real ext-real Element of REAL
Q * (a - T) is V11() real ext-real Element of REAL
T + (Q * (a - T)) is V11() real ext-real Element of REAL
T + (Q - T) is V11() real ext-real Element of REAL
{ (((1 - b₂) * T) + (b₂ * a)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₂ & b₂ <= 1 ) } is set
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) * T is V11() real ext-real Element of REAL
1 * a is V11() real ext-real Element of REAL
((1 - 1) * T) + (1 * a) is V11() real ext-real Element of REAL
{ (((1 - b₂) * T) + (b₂ * a)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₂ & b₂ <= 1 ) } is set
{ (((1 - b₂) * T) + (b₂ * a)) where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₂ & b₂ <= 1 ) } is set
P is set
Q is V11() real ext-real Element of REAL
1 - Q is V11() real ext-real Element of REAL
(1 - Q) * T is V11() real ext-real Element of REAL
Q * a is V11() real ext-real Element of REAL
((1 - Q) * T) + (Q * a) is V11() real ext-real Element of REAL
[: the carrier of [:R^1,I[01]:], the carrier of R^1:] is set
bool [: the carrier of [:R^1,I[01]:], the carrier of R^1:] is set
[:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):] is set
bool [:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):] is set
T is Relation-like [: the carrier of (TOP-REAL 1), the carrier of I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):]
[: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):] is set
bool [: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):] is set
b is non empty Relation-like the carrier of (TOP-REAL 1) -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL 1), the carrier of R^1:]
P is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of R^1:]
b /" is non empty Relation-like the carrier of R^1 -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of R^1, the carrier of (TOP-REAL 1):]
[: the carrier of R^1, the carrier of (TOP-REAL 1):] is set
bool [: the carrier of R^1, the carrier of (TOP-REAL 1):] is set
[:(b /"),(id I[01]):] is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of [:(TOP-REAL 1),I[01]:] -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:]
[: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:] is set
bool [: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:] is set
a is non empty Relation-like the carrier of [:(TOP-REAL 1),I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):]
a * [:(b /"),(id I[01]):] is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):]
[: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):] is set
bool [: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):] is set
b * (a * [:(b /"),(id I[01]):]) is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of R^1:]
Q is Element of the carrier of [:R^1,I[01]:]
P . Q is V11() real ext-real Element of the carrier of R^1
(b * (a * [:(b /"),(id I[01]):])) . Q is V11() real ext-real Element of the carrier of R^1
s is V11() real ext-real Element of the carrier of R^1
t is V11() real ext-real Element of the carrier of I[01]
[s,t] is non empty Element of the carrier of [:R^1,I[01]:]
{s,t} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,t},{s}} is set
dom (b /") is set
rng b is set
[#] R^1 is non empty non proper V80( R^1 ) V166() V167() V168() Element of bool the carrier of R^1
bool the carrier of R^1 is set
dom b is set
Q is Relation-like Function-like set
Q " is Relation-like Function-like set
(b /") . s is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
1 - t is V11() real ext-real Element of REAL
(1 - t) * ((b /") . s) is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
K652(((b /") . s),(1 - t)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q1 is V11() real ext-real Element of REAL
<*Q1*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
<*s*> is Relation-like NAT -defined the carrier of R^1 -valued Function-like FinSequence-like FinSequence of the carrier of R^1
|[s]| is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
REAL 1 is non empty FinSequence-membered M9( REAL )
b . <*s*> is set
|[s]| /. 1 is V11() real ext-real Element of REAL
(Q ") . s is set
P1 is V47(1) Element of REAL 1
(1 - t) * P1 is Relation-like NAT -defined REAL -valued Function-like V47(1) FinSequence-like M10( REAL , REAL 1)
(1 - t) * s is V11() real ext-real Element of REAL
<*((1 - t) * s)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
(a * [:(b /"),(id I[01]):]) . Q is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
b . ((a * [:(b /"),(id I[01]):]) . Q) is V11() real ext-real Element of the carrier of R^1
[:(b /"),(id I[01]):] . (s,t) is set
[s,t] is non empty set
[:(b /"),(id I[01]):] . [s,t] is set
a . ([:(b /"),(id I[01]):] . (s,t)) is set
b . (a . ([:(b /"),(id I[01]):] . (s,t))) is set
(id I[01]) . t is V11() real ext-real Element of the carrier of I[01]
a . (((b /") . s),((id I[01]) . t)) is set
[((b /") . s),((id I[01]) . t)] is non empty set
{((b /") . s),((id I[01]) . t)} is set
{((b /") . s)} is trivial set
{{((b /") . s),((id I[01]) . t)},{((b /") . s)}} is set
a . [((b /") . s),((id I[01]) . t)] is set
b . (a . (((b /") . s),((id I[01]) . t))) is set
a . (((b /") . s),t) is set
[((b /") . s),t] is non empty set
{((b /") . s),t} is set
{{((b /") . s),t},{((b /") . s)}} is set
a . [((b /") . s),t] is set
b . (a . (((b /") . s),t)) is set
b . ((1 - t) * ((b /") . s)) is V11() real ext-real Element of the carrier of R^1
((1 - t) * ((b /") . s)) /. 1 is V11() real ext-real Element of REAL
<*Q1*> /. 1 is V11() real ext-real Element of REAL
P . (s,t) is set
P . [s,t] is set
[:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):] is set
bool [:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):] is set
T is Relation-like [: the carrier of (TOP-REAL 1), the carrier of I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [:[: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1):]
[: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):] is set
bool [: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):] is set
b is non empty Relation-like the carrier of (TOP-REAL 1) -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of (TOP-REAL 1), the carrier of R^1:]
P is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of R^1:]
b /" is non empty Relation-like the carrier of R^1 -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of R^1, the carrier of (TOP-REAL 1):]
[: the carrier of R^1, the carrier of (TOP-REAL 1):] is set
bool [: the carrier of R^1, the carrier of (TOP-REAL 1):] is set
[:(b /"),(id I[01]):] is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of [:(TOP-REAL 1),I[01]:] -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:]
[: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:] is set
bool [: the carrier of [:R^1,I[01]:], the carrier of [:(TOP-REAL 1),I[01]:]:] is set
a is non empty Relation-like the carrier of [:(TOP-REAL 1),I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL 1),I[01]:], the carrier of (TOP-REAL 1):]
a * [:(b /"),(id I[01]):] is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):]
[: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):] is set
bool [: the carrier of [:R^1,I[01]:], the carrier of (TOP-REAL 1):] is set
b * (a * [:(b /"),(id I[01]):]) is non empty Relation-like the carrier of [:R^1,I[01]:] -defined the carrier of R^1 -valued Function-like total quasi_total Element of bool [: the carrier of [:R^1,I[01]:], the carrier of R^1:]
Q is Element of the carrier of [:R^1,I[01]:]
P . Q is V11() real ext-real Element of the carrier of R^1
(b * (a * [:(b /"),(id I[01]):])) . Q is V11() real ext-real Element of the carrier of R^1
s is V11() real ext-real Element of the carrier of R^1
t is V11() real ext-real Element of the carrier of I[01]
[s,t] is non empty Element of the carrier of [:R^1,I[01]:]
{s,t} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,t},{s}} is set
dom (b /") is set
rng b is set
[#] R^1 is non empty non proper V80( R^1 ) V166() V167() V168() Element of bool the carrier of R^1
bool the carrier of R^1 is set
dom b is set
Q is Relation-like Function-like set
Q " is Relation-like Function-like set
(b /") . s is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
t * ((b /") . s) is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
K652(((b /") . s),t) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
Q1 is V11() real ext-real Element of REAL
<*Q1*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
<*s*> is Relation-like NAT -defined the carrier of R^1 -valued Function-like FinSequence-like FinSequence of the carrier of R^1
|[s]| is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
REAL 1 is non empty FinSequence-membered M9( REAL )
b . <*s*> is set
|[s]| /. 1 is V11() real ext-real Element of REAL
(Q ") . s is set
P1 is V47(1) Element of REAL 1
t * P1 is Relation-like NAT -defined REAL -valued Function-like V47(1) FinSequence-like M10( REAL , REAL 1)
t * s is V11() real ext-real set
<*(t * s)*> is Relation-like Function-like set
(a * [:(b /"),(id I[01]):]) . Q is Relation-like REAL -valued Function-like V47(1) FinSequence-like V158() Element of the carrier of (TOP-REAL 1)
b . ((a * [:(b /"),(id I[01]):]) . Q) is V11() real ext-real Element of the carrier of R^1
[:(b /"),(id I[01]):] . (s,t) is set
[s,t] is non empty set
[:(b /"),(id I[01]):] . [s,t] is set
a . ([:(b /"),(id I[01]):] . (s,t)) is set
b . (a . ([:(b /"),(id I[01]):] . (s,t))) is set
(id I[01]) . t is V11() real ext-real Element of the carrier of I[01]
a . (((b /") . s),((id I[01]) . t)) is set
[((b /") . s),((id I[01]) . t)] is non empty set
{((b /") . s),((id I[01]) . t)} is set
{((b /") . s)} is trivial set
{{((b /") . s),((id I[01]) . t)},{((b /") . s)}} is set
a . [((b /") . s),((id I[01]) . t)] is set
b . (a . (((b /") . s),((id I[01]) . t))) is set
a . (((b /") . s),t) is set
[((b /") . s),t] is non empty set
{((b /") . s),t} is set
{{((b /") . s),t},{((b /") . s)}} is set
a . [((b /") . s),t] is set
b . (a . (((b /") . s),t)) is set
b . (t * ((b /") . s)) is V11() real ext-real Element of the carrier of R^1
(t * ((b /") . s)) /. 1 is V11() real ext-real Element of REAL
<*Q1*> /. 1 is V11() real ext-real Element of REAL
P . (s,t) is set
P . [s,t] is set
bool the carrier of R^1 is set
T is non empty V166() V167() V168() Element of bool the carrier of R^1
a is ext-real set
b is ext-real set
K58(a,b) is interval set
P is V11() real ext-real Element of REAL
Q is V11() real ext-real Element of REAL
[.P,Q.] is V166() V167() V168() interval Element of bool REAL
T is real-membered TopStruct
the carrier of T is V166() V167() V168() set
bool the carrier of T is set
{} T is empty trivial V166() V167() V168() V169() V170() V171() V172() V259() interval Element of bool the carrier of T
T is TopSpace-like real-membered SubSpace of R^1
[#] T is non proper V80(T) V166() V167() V168() Element of bool the carrier of T
the carrier of T is V166() V167() V168() set
bool the carrier of T is set
a is V166() V167() V168() Element of bool REAL
T is non empty strict TopSpace-like real-membered SubSpace of R^1
() is non empty strict TopSpace-like real-membered () SubSpace of R^1
T is non empty TopSpace-like real-membered () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
[.a,b.] is V166() V167() V168() interval Element of bool REAL
the carrier of () is non empty V166() V167() V168() set
[#] T is non empty non proper V80(T) V166() V167() V168() Element of bool the carrier of T
bool the carrier of T is set
P is V11() real ext-real Element of the carrier of ()
Q is V11() real ext-real Element of the carrier of ()
[.P,Q.] is V166() V167() V168() interval Element of bool REAL
T is non empty TopSpace-like real-membered SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
(#) (a,b) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
Closed-Interval-TSpace (a,b) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (a,b)) is non empty V166() V167() V168() set
(a,b) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (a,b))
L[01] (((#) (a,b)),((a,b) (#))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (a,b)) -valued Function-like total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):] is set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (a,b)):] is set
[.a,b.] is V166() V167() V168() interval Element of bool REAL
[: the carrier of I[01], the carrier of T:] is set
bool [: the carrier of I[01], the carrier of T:] is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
Q . 0 is set
Q . 1 is set
the carrier of () is non empty V166() V167() V168() set
bool the carrier of () is set
[: the carrier of I[01], the carrier of ():] is set
bool [: the carrier of I[01], the carrier of ():] is set
s is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of ():]
Q . ((#) (0,1)) is set
Q . ((0,1) (#)) is set
(b,a) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,a))
Closed-Interval-TSpace (b,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (b,a)) is non empty V166() V167() V168() set
(#) (b,a) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (b,a))
L[01] (((b,a) (#)),((#) (b,a))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (b,a)) -valued Function-like total quasi_total Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):]
[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):] is set
bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (b,a)):] is set
[.b,a.] is V166() V167() V168() interval Element of bool REAL
[: the carrier of I[01], the carrier of T:] is set
bool [: the carrier of I[01], the carrier of T:] is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
Q . 0 is set
Q . 1 is set
the carrier of () is non empty V166() V167() V168() set
bool the carrier of () is set
[: the carrier of I[01], the carrier of ():] is set
bool [: the carrier of I[01], the carrier of ():] is set
s is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of ():]
Q . ((#) (0,1)) is set
Q . ((0,1) (#)) is set
T is V11() real ext-real set
a is V11() real ext-real set
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
[.T,a.] is V166() V167() V168() interval Element of bool REAL
[#] (Closed-Interval-TSpace (T,a)) is non empty non proper V80( Closed-Interval-TSpace (T,a)) V166() V167() V168() Element of bool the carrier of (Closed-Interval-TSpace (T,a))
the carrier of (Closed-Interval-TSpace (T,a)) is non empty V166() V167() V168() set
bool the carrier of (Closed-Interval-TSpace (T,a)) is set
T is V11() real ext-real set
a is V11() real ext-real set
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
b is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
[: the carrier of I[01], the carrier of T:] is set
bool [: the carrier of I[01], the carrier of T:] is set
[: the carrier of [:I[01],I[01]:], the carrier of T:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
a is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
b is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
P is V11() real ext-real Element of the carrier of I[01]
Q is V11() real ext-real Element of the carrier of I[01]
1 - Q is V11() real ext-real Element of REAL
a . P is V11() real ext-real Element of the carrier of T
(1 - Q) * (a . P) is V11() real ext-real Element of REAL
b . P is V11() real ext-real Element of the carrier of T
Q * (b . P) is V11() real ext-real set
((1 - Q) * (a . P)) + (Q * (b . P)) is V11() real ext-real Element of REAL
[.(a . P),(b . P).] is V166() V167() V168() interval Element of bool REAL
1 - 1 is V11() real ext-real Element of REAL
(1 - Q) * (b . P) is V11() real ext-real Element of REAL
((1 - Q) * (b . P)) + (Q * (b . P)) is V11() real ext-real Element of REAL
[.(b . P),(a . P).] is V166() V167() V168() interval Element of bool REAL
(b . P) - (b . P) is V11() real ext-real set
(b . P) - (a . P) is V11() real ext-real set
Q * ((b . P) - (a . P)) is V11() real ext-real set
Q * 0 is V11() real ext-real Element of REAL
(a . P) + (Q * ((b . P) - (a . P))) is V11() real ext-real set
(a . P) + 0 is V11() real ext-real Element of REAL
[:[: the carrier of I[01], the carrier of I[01]:], the carrier of T:] is set
bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of T:] is set
P is Relation-like [: the carrier of I[01], the carrier of I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [:[: the carrier of I[01], the carrier of I[01]:], the carrier of T:]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
Q is V11() real ext-real Element of the carrier of I[01]
s is V11() real ext-real Element of the carrier of I[01]
Q . (Q,s) is set
[Q,s] is non empty set
{Q,s} is V166() V167() V168() set
{Q} is trivial V166() V167() V168() set
{{Q,s},{Q}} is set
Q . [Q,s] is set
1 - s is V11() real ext-real Element of REAL
a . Q is V11() real ext-real Element of the carrier of T
(1 - s) * (a . Q) is V11() real ext-real Element of REAL
b . Q is V11() real ext-real Element of the carrier of T
s * (b . Q) is V11() real ext-real set
((1 - s) * (a . Q)) + (s * (b . Q)) is V11() real ext-real Element of REAL
P is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
Q is V11() real ext-real Element of the carrier of I[01]
s is V11() real ext-real Element of the carrier of I[01]
P . (Q,s) is set
[Q,s] is non empty set
{Q,s} is V166() V167() V168() set
{Q} is trivial V166() V167() V168() set
{{Q,s},{Q}} is set
P . [Q,s] is set
Q . (Q,s) is set
Q . [Q,s] is set
1 - s is V11() real ext-real Element of REAL
a . Q is V11() real ext-real Element of the carrier of T
(1 - s) * (a . Q) is V11() real ext-real Element of REAL
b . Q is V11() real ext-real Element of the carrier of T
s * (b . Q) is V11() real ext-real set
((1 - s) * (a . Q)) + (s * (b . Q)) is V11() real ext-real Element of REAL
the carrier of () is non empty V166() V167() V168() set
a is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of a is non empty V166() V167() V168() set
[: the carrier of I[01], the carrier of a:] is set
bool [: the carrier of I[01], the carrier of a:] is set
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
(a,b,P) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
[:b,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:a,I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:]
[:a,I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:a,I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:] is set
[:P,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:a,I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:a,I[01]:]:]
bool the carrier of () is set
[: the carrier of [:I[01],I[01]:], the carrier of ():] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of ():] is set
[: the carrier of I[01], the carrier of ():] is set
bool [: the carrier of I[01], the carrier of ():] is set
P1 is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of ():]
Q1 is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of ():]
P1 is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of ():]
[:P1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:(),I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(),I[01]:]:]
[:(),I[01]:] is non empty strict TopSpace-like TopStruct
the carrier of [:(),I[01]:] is non empty set
[: the carrier of [:I[01],I[01]:], the carrier of [:(),I[01]:]:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:(),I[01]:]:] is set
Q1 is non empty Relation-like the carrier of I[01] -defined the carrier of () -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of ():]
[:Q1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:(),I[01]:] -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of [:(),I[01]:]:]
Pb is V11() real ext-real Element of the carrier of I[01]
1 - Pb is V11() real ext-real Element of REAL
Pa is V11() real ext-real Element of the carrier of ()
(1 - Pb) * Pa is V11() real ext-real Element of REAL
[: the carrier of (), the carrier of I[01]:] is set
[:[: the carrier of (), the carrier of I[01]:], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of I[01]:], the carrier of ():] is set
Pa is Relation-like [: the carrier of (), the carrier of I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [:[: the carrier of (), the carrier of I[01]:], the carrier of ():]
Pb is V11() real ext-real Element of the carrier of ()
Pa is V11() real ext-real Element of the carrier of I[01]
Pa * Pb is V11() real ext-real set
Pb is Relation-like [: the carrier of (), the carrier of I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [:[: the carrier of (), the carrier of I[01]:], the carrier of ():]
[: the carrier of [:(),I[01]:], the carrier of ():] is set
bool [: the carrier of [:(),I[01]:], the carrier of ():] is set
Pb is non empty Relation-like the carrier of [:(),I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:(),I[01]:], the carrier of ():]
Pa is non empty Relation-like the carrier of [:(),I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:(),I[01]:], the carrier of ():]
Pa * [:P1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
Pb * [:Q1,(id I[01]):] is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
g is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
t is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
dom P is set
dom b is set
p is Element of the carrier of [:I[01],I[01]:]
t . p is V11() real ext-real Element of the carrier of ()
(Pa * [:P1,(id I[01]):]) . p is V11() real ext-real Element of the carrier of ()
(Pb * [:Q1,(id I[01]):]) . p is V11() real ext-real Element of the carrier of ()
((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) is V11() real ext-real set
s is V11() real ext-real Element of the carrier of I[01]
t is V11() real ext-real Element of the carrier of I[01]
[s,t] is non empty Element of the carrier of [:I[01],I[01]:]
{s,t} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,t},{s}} is set
b . s is V11() real ext-real Element of the carrier of a
P . s is V11() real ext-real Element of the carrier of a
(a,b,P) . (s,t) is set
[s,t] is non empty set
(a,b,P) . [s,t] is set
1 - t is V11() real ext-real Element of REAL
a1 is V11() real ext-real Element of the carrier of ()
(1 - t) * a1 is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of the carrier of ()
t * b1 is V11() real ext-real set
((1 - t) * a1) + (t * b1) is V11() real ext-real Element of REAL
(id I[01]) . t is V11() real ext-real Element of the carrier of I[01]
Pb * [:P,(id I[01]):] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
(Pb * [:P,(id I[01]):]) . p is set
[:P,(id I[01]):] . (s,t) is set
[:P,(id I[01]):] . [s,t] is set
Pb . ([:P,(id I[01]):] . (s,t)) is set
Pb . ((P . s),t) is set
[(P . s),t] is non empty set
{(P . s),t} is V166() V167() V168() set
{(P . s)} is trivial V166() V167() V168() set
{{(P . s),t},{(P . s)}} is set
Pb . [(P . s),t] is set
t * (P . s) is V11() real ext-real set
Pa * [:b,(id I[01]):] is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of () -valued Function-like Element of bool [: the carrier of [:I[01],I[01]:], the carrier of ():]
(Pa * [:b,(id I[01]):]) . p is set
[:b,(id I[01]):] . (s,t) is set
[:b,(id I[01]):] . [s,t] is set
Pa . ([:b,(id I[01]):] . (s,t)) is set
Pa . ((b . s),t) is set
[(b . s),t] is non empty set
{(b . s),t} is V166() V167() V168() set
{(b . s)} is trivial V166() V167() V168() set
{{(b . s),t},{(b . s)}} is set
Pa . [(b . s),t] is set
(1 - t) * (b . s) is V11() real ext-real Element of REAL
p is Element of the carrier of [:I[01],I[01]:]
t . p is V11() real ext-real Element of the carrier of ()
g . p is V11() real ext-real Element of the carrier of ()
(Pa * [:P1,(id I[01]):]) . p is V11() real ext-real Element of the carrier of ()
(Pb * [:Q1,(id I[01]):]) . p is V11() real ext-real Element of the carrier of ()
((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) is V11() real ext-real set
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
(T,P,Q) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
[: the carrier of [:I[01],I[01]:], the carrier of T:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
s is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (s,0) is set
[s,0] is non empty set
{s,0} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,0},{s}} is set
(T,P,Q) . [s,0] is set
P . s is V11() real ext-real Element of the carrier of T
(T,P,Q) . (s,1) is set
[s,1] is non empty set
{s,1} is V166() V167() V168() set
{{s,1},{s}} is set
(T,P,Q) . [s,1] is set
Q . s is V11() real ext-real Element of the carrier of T
P . 0[01] is V11() real ext-real Element of the carrier of T
Q . 0[01] is V11() real ext-real Element of the carrier of T
1 - 0 is V11() real ext-real Element of REAL
(1 - 0) * (P . s) is V11() real ext-real Element of REAL
0 * (Q . s) is V11() real ext-real Element of REAL
((1 - 0) * (P . s)) + (0 * (Q . s)) is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real Element of REAL
(1 - 1) * (P . s) is V11() real ext-real Element of REAL
1 * (Q . s) is V11() real ext-real Element of REAL
((1 - 1) * (P . s)) + (1 * (Q . s)) is V11() real ext-real Element of REAL
t is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (0,t) is set
[0,t] is non empty set
{0,t} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,t},{0}} is set
(T,P,Q) . [0,t] is set
(T,P,Q) . (1,t) is set
[1,t] is non empty set
{1,t} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,t},{1}} is set
(T,P,Q) . [1,t] is set
1 - t is V11() real ext-real Element of REAL
(1 - t) * (P . 0[01]) is V11() real ext-real Element of REAL
t * (Q . 0[01]) is V11() real ext-real set
((1 - t) * (P . 0[01])) + (t * (Q . 0[01])) is V11() real ext-real Element of REAL
P . 1[01] is V11() real ext-real Element of the carrier of T
Q . 1[01] is V11() real ext-real Element of the carrier of T
(1 - t) * (P . 1[01]) is V11() real ext-real Element of REAL
t * (Q . 1[01]) is V11() real ext-real set
((1 - t) * (P . 1[01])) + (t * (Q . 1[01])) is V11() real ext-real Element of REAL
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
[: the carrier of [:I[01],I[01]:], the carrier of T:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
(T,P,Q) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
s is V11() real ext-real Element of the carrier of I[01]
Q . (s,0) is set
[s,0] is non empty set
{s,0} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,0},{s}} is set
Q . [s,0] is set
P . s is V11() real ext-real Element of the carrier of T
t is V11() real ext-real Element of the carrier of I[01]
Q . (t,1) is set
[t,1] is non empty set
{t,1} is V166() V167() V168() set
{t} is trivial V166() V167() V168() set
{{t,1},{t}} is set
Q . [t,1] is set
Q . t is V11() real ext-real Element of the carrier of T
P1 is V11() real ext-real Element of the carrier of I[01]
Q . (0,P1) is set
[0,P1] is non empty set
{0,P1} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,P1},{0}} is set
Q . [0,P1] is set
Q1 is V11() real ext-real Element of the carrier of I[01]
Q . (1,Q1) is set
[1,Q1] is non empty set
{1,Q1} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,Q1},{1}} is set
Q . [1,Q1] is set
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
Q is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Homotopy of P,Q
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
FundamentalGroup (T,a) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the carrier of (FundamentalGroup (T,a)) is non empty set
Loops a is non empty set
Paths (a,a) is non empty set
EqRel (T,a) is non empty Relation-like Loops a -defined Loops a -valued total quasi_total V97() V102() Element of bool [:(Loops a),(Loops a):]
[:(Loops a),(Loops a):] is set
bool [:(Loops a),(Loops a):] is set
EqRel (T,a,a) is Relation-like Paths (a,a) -defined Paths (a,a) -valued Element of bool [:(Paths (a,a)),(Paths (a,a)):]
[:(Paths (a,a)),(Paths (a,a)):] is set
bool [:(Paths (a,a)),(Paths (a,a)):] is set
b is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,a
Class ((EqRel (T,a)),b) is Element of bool (Loops a)
bool (Loops a) is set
{(Class ((EqRel (T,a)),b))} is trivial set
Q is set
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,a
Class ((EqRel (T,a)),Q) is Element of bool (Loops a)
Q is set
Class (EqRel (T,a)) is a_partition of Loops a
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
FundamentalGroup (T,a) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant total quasi_total continuous Path of a,a is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant total quasi_total continuous Path of a,a
EqRel (T,a) is non empty Relation-like Loops a -defined Loops a -valued total quasi_total V97() V102() Element of bool [:(Loops a),(Loops a):]
Loops a is non empty set
Paths (a,a) is non empty set
[:(Loops a),(Loops a):] is set
bool [:(Loops a),(Loops a):] is set
EqRel (T,a,a) is Relation-like Paths (a,a) -defined Paths (a,a) -valued Element of bool [:(Paths (a,a)),(Paths (a,a)):]
[:(Paths (a,a)),(Paths (a,a)):] is set
bool [:(Paths (a,a)),(Paths (a,a)):] is set
the carrier of (FundamentalGroup (T,a)) is non empty set
Class (EqRel (T,a)) is a_partition of Loops a
Class ((EqRel (T,a)), the non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant total quasi_total continuous Path of a,a) is Element of bool (Loops a)
bool (Loops a) is set
{(Class ((EqRel (T,a)), the non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant total quasi_total continuous Path of a,a))} is trivial set
T is V11() real ext-real set
a is V11() real ext-real set
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,a)) is non empty V166() V167() V168() set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,a))
P is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,a))
Q is non empty Relation-like the carrier of I[01] -defined the carrier of (Closed-Interval-TSpace (T,a)) -valued Function-like total quasi_total Path of b,P
Q is non empty Relation-like the carrier of I[01] -defined the carrier of (Closed-Interval-TSpace (T,a)) -valued Function-like total quasi_total Path of b,P
T is V11() real ext-real set
a is V11() real ext-real set
Closed-Interval-TSpace (T,a) is non empty strict TopSpace-like real-membered SubSpace of R^1
the carrier of (Closed-Interval-TSpace (T,a)) is non empty V166() V167() V168() set
b is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (T,a))
FundamentalGroup ((Closed-Interval-TSpace (T,a)),b) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the carrier of (FundamentalGroup ((Closed-Interval-TSpace (T,a)),b)) is non empty set
Loops b is non empty set
Paths (b,b) is non empty set
EqRel ((Closed-Interval-TSpace (T,a)),b) is non empty Relation-like Loops b -defined Loops b -valued total quasi_total V97() V102() Element of bool [:(Loops b),(Loops b):]
[:(Loops b),(Loops b):] is set
bool [:(Loops b),(Loops b):] is set
EqRel ((Closed-Interval-TSpace (T,a)),b,b) is Relation-like Paths (b,b) -defined Paths (b,b) -valued Element of bool [:(Paths (b,b)),(Paths (b,b)):]
[:(Paths (b,b)),(Paths (b,b)):] is set
bool [:(Paths (b,b)),(Paths (b,b)):] is set
P is non empty Relation-like the carrier of I[01] -defined the carrier of (Closed-Interval-TSpace (T,a)) -valued Function-like total quasi_total Path of b,b
Class ((EqRel ((Closed-Interval-TSpace (T,a)),b)),P) is Element of bool (Loops b)
bool (Loops b) is set
{(Class ((EqRel ((Closed-Interval-TSpace (T,a)),b)),P))} is trivial set
T is V11() real ext-real Element of the carrier of I[01]
a is V11() real ext-real Element of the carrier of I[01]
b is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total continuous Path of T,a
P is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total continuous Path of T,a
T is V11() real ext-real Element of the carrier of I[01]
FundamentalGroup (I[01],T) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
the carrier of (FundamentalGroup (I[01],T)) is non empty set
Loops T is non empty set
Paths (T,T) is non empty set
EqRel (I[01],T) is non empty Relation-like Loops T -defined Loops T -valued total quasi_total V97() V102() Element of bool [:(Loops T),(Loops T):]
[:(Loops T),(Loops T):] is set
bool [:(Loops T),(Loops T):] is set
EqRel (I[01],T,T) is Relation-like Paths (T,T) -defined Paths (T,T) -valued Element of bool [:(Paths (T,T)),(Paths (T,T)):]
[:(Paths (T,T)),(Paths (T,T)):] is set
bool [:(Paths (T,T)),(Paths (T,T)):] is set
a is non empty Relation-like the carrier of I[01] -defined the carrier of I[01] -valued Function-like total quasi_total continuous Path of T,T
Class ((EqRel (I[01],T)),a) is Element of bool (Loops T)
bool (Loops T) is set
{(Class ((EqRel (I[01],T)),a))} is trivial set
T is V11() real ext-real Element of the carrier of I[01]
FundamentalGroup (I[01],T) is non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() L10()
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
[: the carrier of I[01], the carrier of a:] is set
bool [: the carrier of I[01], the carrier of a:] is set
b is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of a:]
(T,a,b,P) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
T is natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() Element of NAT
TOP-REAL T is non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() RLTopStruct
a is non empty TopSpace-like pathwise_connected (T) SubSpace of TOP-REAL T
the carrier of a is non empty set
b is Element of the carrier of a
P is Element of the carrier of a
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
Q is non empty Relation-like the carrier of I[01] -defined the carrier of a -valued Function-like total quasi_total continuous Path of b,P
(T,a,Q,Q) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of a -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of a:]
[: the carrier of [:I[01],I[01]:], the carrier of a:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of a:] is set
s is V11() real ext-real Element of the carrier of I[01]
(T,a,Q,Q) . (s,0) is set
[s,0] is non empty set
{s,0} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,0},{s}} is set
(T,a,Q,Q) . [s,0] is set
Q . s is Element of the carrier of a
t is V11() real ext-real Element of the carrier of I[01]
(T,a,Q,Q) . (t,1) is set
[t,1] is non empty set
{t,1} is V166() V167() V168() set
{t} is trivial V166() V167() V168() set
{{t,1},{t}} is set
(T,a,Q,Q) . [t,1] is set
Q . t is Element of the carrier of a
P1 is V11() real ext-real Element of the carrier of I[01]
(T,a,Q,Q) . (0,P1) is set
[0,P1] is non empty set
{0,P1} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,P1},{0}} is set
(T,a,Q,Q) . [0,P1] is set
Q1 is V11() real ext-real Element of the carrier of I[01]
(T,a,Q,Q) . (1,Q1) is set
[1,Q1] is non empty set
{1,Q1} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,Q1},{1}} is set
(T,a,Q,Q) . [1,Q1] is set
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
[: the carrier of I[01], the carrier of T:] is set
bool [: the carrier of I[01], the carrier of T:] is set
a is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of T:]
b is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of T:]
(T,a,b) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
[: the carrier of [:I[01],I[01]:], the carrier of T:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
T is non empty TopSpace-like real-membered pathwise_connected () SubSpace of ()
the carrier of T is non empty V166() V167() V168() set
a is V11() real ext-real Element of the carrier of T
b is V11() real ext-real Element of the carrier of T
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
Q is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like total quasi_total continuous Path of a,b
(T,P,Q) is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like total quasi_total continuous Element of bool [: the carrier of [:I[01],I[01]:], the carrier of T:]
[: the carrier of [:I[01],I[01]:], the carrier of T:] is set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
Q is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (Q,0) is set
[Q,0] is non empty set
{Q,0} is V166() V167() V168() set
{Q} is trivial V166() V167() V168() set
{{Q,0},{Q}} is set
(T,P,Q) . [Q,0] is set
P . Q is V11() real ext-real Element of the carrier of T
s is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (s,1) is set
[s,1] is non empty set
{s,1} is V166() V167() V168() set
{s} is trivial V166() V167() V168() set
{{s,1},{s}} is set
(T,P,Q) . [s,1] is set
Q . s is V11() real ext-real Element of the carrier of T
t is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (0,t) is set
[0,t] is non empty set
{0,t} is V166() V167() V168() set
{0} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{0,t},{0}} is set
(T,P,Q) . [0,t] is set
P1 is V11() real ext-real Element of the carrier of I[01]
(T,P,Q) . (1,P1) is set
[1,P1] is non empty set
{1,P1} is V166() V167() V168() set
{1} is trivial V166() V167() V168() V169() V170() V171() V259() set
{{1,P1},{1}} is set
(T,P,Q) . [1,P1] is set