:: 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

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

(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

[:[: 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

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

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

{ (((1 - b

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