:: TOPALG_4 semantic presentation

K28() is V126() V127() V128() V132() set

K32() is V126() V127() V128() V129() V130() V131() V132() M2( bool K28())

bool K28() is set

K554() is non empty strict TopSpace-like V227() pathwise_connected SubSpace of K552()

K552() is non empty strict TopSpace-like V227() TopStruct

the carrier of K554() is non empty V126() V127() V128() set

[:K554(),K554():] is non empty strict TopSpace-like TopStruct

the carrier of [:K554(),K554():] is non empty set

K27() is V126() V127() V128() V129() V130() V131() V132() set

bool K27() is set

bool K32() is set

K29() is V126() V132() set

K30() is V126() V127() V128() V129() V132() set

K31() is V126() V127() V128() V129() V130() V132() set

[:K28(),K28():] is Relation-like set

bool [:K28(),K28():] is set

K291() is non empty strict multMagma

the carrier of K291() is non empty set

K296() is non empty strict unital Group-like V96() V98() V148() V149() V150() V151() V152() V153() multMagma

K297() is non empty strict V96() V98() V151() V152() V153() M13(K296())

K298() is non empty strict unital V96() V98() V151() V152() V153() V154() M16(K296(),K297())

K300() is non empty strict unital V96() V98() multMagma

K301() is non empty strict unital V96() V98() V154() M13(K300())

K360() is set

{} is set

the empty Relation-like non-empty empty-yielding functional FinSequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() set is empty Relation-like non-empty empty-yielding functional FinSequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() set

{{}} is set

K262({{}}) is non empty functional FinSequence-membered M10({{}})

[:K262({{}}),{{}}:] is Relation-like set

bool [:K262({{}}),{{}}:] is set

PFuncs (K262({{}}),{{}}) is set

1 is non empty V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())

{1} is V126() V127() V128() V129() V130() V131() set

2 is non empty V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())

{1,2} is V126() V127() V128() V129() V130() V131() set

3 is non empty V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())

K396(1,2,3) is V126() V127() V128() V129() V130() V131() set

{{},1} is set

I[01] is non empty strict TopSpace-like V227() pathwise_connected TopStruct

the carrier of I[01] is non empty V126() V127() V128() set

[:1,1:] is Relation-like set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like set

bool [:[:1,1:],1:] is set

[:[:1,1:],K28():] is Relation-like set

bool [:[:1,1:],K28():] is set

[:[:K28(),K28():],K28():] is Relation-like set

bool [:[:K28(),K28():],K28():] is set

[:2,2:] is Relation-like set

[:[:2,2:],K28():] is Relation-like set

bool [:[:2,2:],K28():] is set

K542() is V213() V227() L15()

[: the carrier of K554(), the carrier of K554():] is Relation-like set

bool [: the carrier of K554(), the carrier of K554():] is set

bool the carrier of [:K554(),K554():] is set

K588(2) is V242() L17()

the carrier of K588(2) is set

[:I[01],I[01]:] is non empty strict TopSpace-like TopStruct

the carrier of [:I[01],I[01]:] is non empty set

0[01] is V11() V12() ext-real M2( the carrier of I[01])

0 is V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())

1[01] is V11() V12() ext-real M2( the carrier of I[01])

K52(1,2) is V11() V12() ext-real M2(K28())

Seg 1 is non empty V32() V39(1) V126() V127() V128() V129() V130() V131() M2( bool K32())

Seg 2 is non empty V32() V39(2) V126() V127() V128() V129() V130() V131() M2( bool K32())

I is non empty multMagma

j0 is non empty multMagma

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*I,j0*> is non empty strict V138() multMagma

the carrier of (product <*I,j0*>) is non empty set

the carrier of I is non empty set

the carrier of j0 is non empty set

j1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

Carrier <*I,j0*> is Relation-like non-empty {1,2} -defined Function-like total set

product (Carrier <*I,j0*>) is set

dom (Carrier <*I,j0*>) is V126() V127() V128() V129() V130() V131() M2( bool {1,2})

bool {1,2} is set

S is Relation-like Function-like set

proj1 S is set

<*I,j0*> . 2 is set

(Carrier <*I,j0*>) . 2 is set

T is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like set

T . 2 is set

s2 is 1-sorted

the carrier of s2 is set

<*I,j0*> . 1 is set

(Carrier <*I,j0*>) . 1 is set

T . 1 is set

t1 is 1-sorted

the carrier of t1 is set

s2 is M2( the carrier of I)

s1 is M2( the carrier of j0)

<*s2,s1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

len T is V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())

I is non empty multMagma

the carrier of I is non empty set

j1 is non empty multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty multMagma

the carrier of j0 is non empty set

S is non empty multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*I,j0*> is non empty strict V138() multMagma

the carrier of (product <*I,j0*>) is non empty set

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*j1,S*> is non empty strict V138() multMagma

the carrier of (product <*j1,S*>) is non empty set

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of j0, the carrier of S:])

s2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

t1 is M2( the carrier of I)

t2 is M2( the carrier of j0)

<*t1,t2*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . t1 is M2( the carrier of j1)

s1 . t2 is M2( the carrier of S)

<*(T . t1),(s1 . t2)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

s2 is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

s2 is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

t1 is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

s2 . t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

f is M2( the carrier of I)

g is M2( the carrier of j0)

<*f,g*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . f is M2( the carrier of j1)

s1 . g is M2( the carrier of S)

<*(T . f),(s1 . g)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

t1 . t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

lb is M2( the carrier of I)

B1 is M2( the carrier of j0)

<*lb,B1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . lb is M2( the carrier of j1)

s1 . B1 is M2( the carrier of S)

<*(T . lb),(s1 . B1)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

I is non empty multMagma

the carrier of I is non empty set

j1 is non empty multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty multMagma

the carrier of j0 is non empty set

S is non empty multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*I,j0*> is non empty strict V138() multMagma

the carrier of (product <*I,j0*>) is non empty set

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*j1,S*> is non empty strict V138() multMagma

the carrier of (product <*j1,S*>) is non empty set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

s2 is M2( the carrier of I)

T . s2 is M2( the carrier of j1)

t1 is M2( the carrier of j0)

<*s2,t1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

(I,j0,j1,S,T,s1) . <*s2,t1*> is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

s1 . t1 is M2( the carrier of S)

<*(T . s2),(s1 . t1)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

t2 is M2( the carrier of I)

f is M2( the carrier of j0)

<*t2,f*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . t2 is M2( the carrier of j1)

s1 . f is M2( the carrier of S)

<*(T . t2),(s1 . f)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

I is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of I is non empty set

j1 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of j0 is non empty set

S is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*I,j0*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*j1,S*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total multiplicative M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total multiplicative M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

the carrier of (product <*I,j0*>) is non empty set

the carrier of (product <*j1,S*>) is non empty set

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

t1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

t1 * t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

(I,j0,j1,S,T,s1) . (t1 * t2) is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

(I,j0,j1,S,T,s1) . t1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

(I,j0,j1,S,T,s1) . t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

((I,j0,j1,S,T,s1) . t1) * ((I,j0,j1,S,T,s1) . t2) is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

f is M2( the carrier of I)

g is M2( the carrier of j0)

<*f,g*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . f is M2( the carrier of j1)

s1 . g is M2( the carrier of S)

<*(T . f),(s1 . g)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

lb is M2( the carrier of I)

B1 is M2( the carrier of j0)

<*lb,B1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . lb is M2( the carrier of j1)

s1 . B1 is M2( the carrier of S)

<*(T . lb),(s1 . B1)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

t2 . 2 is set

B2 is M2( the carrier of I)

A1 is M2( the carrier of j0)

<*B2,A1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . B2 is M2( the carrier of j1)

s1 . A1 is M2( the carrier of S)

<*(T . B2),(s1 . A1)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

<*I,j0*> . 2 is set

t1 . 2 is set

g * B1 is M2( the carrier of j0)

<*B2,A1*> . 2 is set

s1 . (g * B1) is M2( the carrier of S)

(s1 . g) * (s1 . B1) is M2( the carrier of S)

t2 . 1 is set

<*I,j0*> . 1 is set

t1 . 1 is set

f * lb is M2( the carrier of I)

<*B2,A1*> . 1 is set

T . (f * lb) is M2( the carrier of j1)

(T . f) * (T . lb) is M2( the carrier of j1)

I is non empty multMagma

the carrier of I is non empty set

j1 is non empty multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty multMagma

the carrier of j0 is non empty set

S is non empty multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*I,j0*> is non empty strict V138() multMagma

the carrier of (product <*I,j0*>) is non empty set

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*j1,S*> is non empty strict V138() multMagma

the carrier of (product <*j1,S*>) is non empty set

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

s2 is set

proj1 (I,j0,j1,S,T,s1) is set

t1 is set

(I,j0,j1,S,T,s1) . s2 is set

(I,j0,j1,S,T,s1) . t1 is set

dom (I,j0,j1,S,T,s1) is M2( bool the carrier of (product <*I,j0*>))

bool the carrier of (product <*I,j0*>) is set

f is M2( the carrier of I)

g is M2( the carrier of j0)

<*f,g*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . f is M2( the carrier of j1)

s1 . g is M2( the carrier of S)

<*(T . f),(s1 . g)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

lb is M2( the carrier of I)

B1 is M2( the carrier of j0)

<*lb,B1*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . lb is M2( the carrier of j1)

s1 . B1 is M2( the carrier of S)

<*(T . lb),(s1 . B1)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

dom T is M2( bool the carrier of I)

bool the carrier of I is set

dom s1 is M2( bool the carrier of j0)

bool the carrier of j0 is set

I is non empty multMagma

the carrier of I is non empty set

j1 is non empty multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty multMagma

the carrier of j0 is non empty set

S is non empty multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*j1,S*> is non empty strict V138() multMagma

the carrier of (product <*j1,S*>) is non empty set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() set

product <*I,j0*> is non empty strict V138() multMagma

the carrier of (product <*I,j0*>) is non empty set

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

rng T is M2( bool the carrier of j1)

bool the carrier of j1 is set

rng s1 is M2( bool the carrier of S)

bool the carrier of S is set

rng (I,j0,j1,S,T,s1) is M2( bool the carrier of (product <*j1,S*>))

bool the carrier of (product <*j1,S*>) is set

t1 is set

t2 is M2( the carrier of j1)

f is M2( the carrier of S)

<*t2,f*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

dom s1 is M2( bool the carrier of j0)

bool the carrier of j0 is set

g is set

s1 . g is set

dom T is M2( bool the carrier of I)

bool the carrier of I is set

lb is set

T . lb is set

dom (I,j0,j1,S,T,s1) is M2( bool the carrier of (product <*I,j0*>))

bool the carrier of (product <*I,j0*>) is set

B1 is M2( the carrier of I)

B2 is M2( the carrier of j0)

<*B1,B2*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

<*lb,g*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set

(I,j0,j1,S,T,s1) . <*lb,g*> is set

B1 is M2( the carrier of I)

B2 is M2( the carrier of j0)

<*B1,B2*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*I,j0*>))

T . B1 is M2( the carrier of j1)

s1 . B2 is M2( the carrier of S)

<*(T . B1),(s1 . B2)*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like M2( the carrier of (product <*j1,S*>))

I is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of I is non empty set

j1 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

j0 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of j0 is non empty set

S is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*I,j0*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

the carrier of (product <*I,j0*>) is non empty set

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*j1,S*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

the carrier of (product <*j1,S*>) is non empty set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total multiplicative M2( bool [: the carrier of I, the carrier of j1:])

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total multiplicative M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total multiplicative M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

rng s1 is M2( bool the carrier of S)

bool the carrier of S is set

rng T is M2( bool the carrier of j1)

bool the carrier of j1 is set

rng (I,j0,j1,S,T,s1) is M2( bool the carrier of (product <*j1,S*>))

bool the carrier of (product <*j1,S*>) is set

I is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

j1 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

j0 is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

S is non empty unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma

<*I,j0*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*I,j0*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

<*j1,S*> is non empty Relation-like K32() -defined {1,2} -defined Function-like total V32() V39(2) FinSequence-like FinSubsequence-like V173() V176() Group-like V178({1,2}) set

product <*j1,S*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma

the carrier of I is non empty set

the carrier of j1 is non empty set

[: the carrier of I, the carrier of j1:] is Relation-like set

bool [: the carrier of I, the carrier of j1:] is set

T is Relation-like the carrier of I -defined the carrier of j1 -valued Function-like quasi_total multiplicative M2( bool [: the carrier of I, the carrier of j1:])

the carrier of j0 is non empty set

the carrier of S is non empty set

[: the carrier of j0, the carrier of S:] is Relation-like set

bool [: the carrier of j0, the carrier of S:] is set

s1 is Relation-like the carrier of j0 -defined the carrier of S -valued Function-like quasi_total multiplicative M2( bool [: the carrier of j0, the carrier of S:])

(I,j0,j1,S,T,s1) is Relation-like the carrier of (product <*I,j0*>) -defined the carrier of (product <*j1,S*>) -valued Function-like quasi_total multiplicative M2( bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):])

the carrier of (product <*I,j0*>) is non empty set

the carrier of (product <*j1,S*>) is non empty set

[: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is Relation-like set

bool [: the carrier of (product <*I,j0*>), the carrier of (product <*j1,S*>):] is set

S is Relation-like Function-like set

proj1 S is set

T is Relation-like Function-like set

proj1 T is set

<:S,T:> is Relation-like Function-like set

pr1 <:S,T:> is Relation-like Function-like set

proj1 (pr1 <:S,T:>) is set

proj1 <:S,T:> is set

s1 is set

(pr1 <:S,T:>) . s1 is set

S . s1 is set

<:S,T:> . s1 is set

(<:S,T:> . s1) `1 is set

T . s1 is set

[(S . s1),(T . s1)] is V24() set

{(S . s1),(T . s1)} is set

{(S . s1)} is set

{{(S . s1),(T . s1)},{(S . s1)}} is set

[(S . s1),(T . s1)] `1 is set

(proj1 S) /\ (proj1 T) is set

S is Relation-like Function-like set

proj1 S is set

T is Relation-like Function-like set

proj1 T is set

<:S,T:> is Relation-like Function-like set

pr2 <:S,T:> is Relation-like Function-like set

proj1 (pr2 <:S,T:>) is set

proj1 <:S,T:> is set

s1 is set

(pr2 <:S,T:>) . s1 is set

T . s1 is set

<:S,T:> . s1 is set

(<:S,T:> . s1) `2 is set

S . s1 is set

[(S . s1),(T . s1)] is V24() set

{(S . s1),(T . s1)} is set

{(S . s1)} is set

{{(S . s1),(T . s1)},{(S . s1)}} is set

[(S . s1),(T . s1)] `2 is set

(proj1 S) /\ (proj1 T) is set

s1 is non empty TopSpace-like TopStruct

the carrier of s1 is non empty set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

[: the carrier of s1, the carrier of S:] is Relation-like set

bool [: the carrier of s1, the carrier of S:] is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[: the carrier of s1, the carrier of T:] is Relation-like set

bool [: the carrier of s1, the carrier of T:] is set

s2 is Relation-like the carrier of s1 -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of s1, the carrier of S:])

t1 is Relation-like the carrier of s1 -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of s1, the carrier of T:])

<:s2,t1:> is Relation-like Function-like set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

[: the carrier of s1, the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of s1, the carrier of [:S,T:]:] is set

dom s2 is M2( bool the carrier of s1)

bool the carrier of s1 is set

dom t1 is M2( bool the carrier of s1)

<:s2,t1:> is Relation-like the carrier of s1 -defined [: the carrier of S, the carrier of T:] -valued Function-like quasi_total M2( bool [: the carrier of s1,[: the carrier of S, the carrier of T:]:])

[: the carrier of S, the carrier of T:] is Relation-like set

[: the carrier of s1,[: the carrier of S, the carrier of T:]:] is Relation-like set

bool [: the carrier of s1,[: the carrier of S, the carrier of T:]:] is set

dom <:s2,t1:> is M2( bool the carrier of s1)

s1 is non empty TopSpace-like TopStruct

the carrier of s1 is non empty set

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

[: the carrier of s1, the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of s1, the carrier of [:S,T:]:] is set

s2 is Relation-like the carrier of s1 -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of s1, the carrier of [:S,T:]:])

pr1 s2 is Relation-like Function-like set

the carrier of S is non empty set

[: the carrier of s1, the carrier of S:] is Relation-like set

bool [: the carrier of s1, the carrier of S:] is set

proj1 (pr1 s2) is set

dom s2 is M2( bool the carrier of s1)

bool the carrier of s1 is set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is Relation-like set

proj2 (pr1 s2) is set

t1 is set

t2 is set

(pr1 s2) . t2 is set

s2 . t2 is set

(s2 . t2) `1 is set

rng s2 is M2( bool the carrier of [:S,T:])

bool the carrier of [:S,T:] is set

pr2 s2 is Relation-like Function-like set

the carrier of T is non empty set

[: the carrier of s1, the carrier of T:] is Relation-like set

bool [: the carrier of s1, the carrier of T:] is set

proj1 (pr2 s2) is set

dom s2 is M2( bool the carrier of s1)

bool the carrier of s1 is set

[: the carrier of S, the carrier of T:] is Relation-like set

proj2 (pr2 s2) is set

t1 is set

t2 is set

(pr2 s2) . t2 is set

s2 . t2 is set

(s2 . t2) `2 is set

rng s2 is M2( bool the carrier of [:S,T:])

bool the carrier of [:S,T:] is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

s1 is non empty TopSpace-like TopStruct

[:T,s1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,s1:] is non empty set

[: the carrier of S, the carrier of [:T,s1:]:] is Relation-like set

bool [: the carrier of S, the carrier of [:T,s1:]:] is set

s2 is Relation-like the carrier of S -defined the carrier of [:T,s1:] -valued Function-like quasi_total continuous M2( bool [: the carrier of S, the carrier of [:T,s1:]:])

(T,s1,S,s2) is Relation-like the carrier of S -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of S, the carrier of T:])

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is Relation-like set

bool [: the carrier of S, the carrier of T:] is set

bool the carrier of T is set

bool the carrier of S is set

t2 is M2( the carrier of S)

(T,s1,S,s2) . t2 is M2( the carrier of T)

f is M2( bool the carrier of T)

[#] s1 is non empty V3( the carrier of s1) open closed M2( bool the carrier of s1)

the carrier of s1 is non empty set

bool the carrier of s1 is set

[:f,([#] s1):] is Relation-like M2( bool the carrier of [:T,s1:])

bool the carrier of [:T,s1:] is set

[: the carrier of T, the carrier of s1:] is Relation-like set

s2 . t2 is M2( the carrier of [:T,s1:])

g is set

lb is set

[g,lb] is V24() set

{g,lb} is set

{g} is set

{{g,lb},{g}} is set

dom s2 is M2( bool the carrier of S)

[g,lb] `1 is set

B1 is M2( bool the carrier of S)

s2 .: B1 is M2( bool the carrier of [:T,s1:])

(T,s1,S,s2) .: B1 is M2( bool the carrier of T)

B2 is set

A1 is M2( the carrier of S)

(T,s1,S,s2) . A1 is M2( the carrier of T)

s2 . A1 is M2( the carrier of [:T,s1:])

(s2 . A1) `1 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

s1 is non empty TopSpace-like TopStruct

[:T,s1:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,s1:] is non empty set

[: the carrier of S, the carrier of [:T,s1:]:] is Relation-like set

bool [: the carrier of S, the carrier of [:T,s1:]:] is set

s2 is Relation-like the carrier of S -defined the carrier of [:T,s1:] -valued Function-like quasi_total continuous M2( bool [: the carrier of S, the carrier of [:T,s1:]:])

(T,s1,S,s2) is Relation-like the carrier of S -defined the carrier of s1 -valued Function-like quasi_total M2( bool [: the carrier of S, the carrier of s1:])

the carrier of s1 is non empty set

[: the carrier of S, the carrier of s1:] is Relation-like set

bool [: the carrier of S, the carrier of s1:] is set

bool the carrier of s1 is set

bool the carrier of S is set

t2 is M2( the carrier of S)

(T,s1,S,s2) . t2 is M2( the carrier of s1)

f is M2( bool the carrier of s1)

[#] T is non empty V3( the carrier of T) open closed M2( bool the carrier of T)

the carrier of T is non empty set

bool the carrier of T is set

[:([#] T),f:] is Relation-like M2( bool the carrier of [:T,s1:])

bool the carrier of [:T,s1:] is set

[: the carrier of T, the carrier of s1:] is Relation-like set

s2 . t2 is M2( the carrier of [:T,s1:])

g is set

lb is set

[g,lb] is V24() set

{g,lb} is set

{g} is set

{{g,lb},{g}} is set

dom s2 is M2( bool the carrier of S)

[g,lb] `2 is set

B1 is M2( bool the carrier of S)

s2 .: B1 is M2( bool the carrier of [:T,s1:])

(T,s1,S,s2) .: B1 is M2( bool the carrier of s1)

B2 is set

A1 is M2( the carrier of S)

(T,s1,S,s2) . A1 is M2( the carrier of s1)

s2 . A1 is M2( the carrier of [:T,s1:])

(s2 . A1) `2 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

the carrier of [:S,T:] is non empty set

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

[: the carrier of I[01], the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of I[01], the carrier of [:S,T:]:] is set

f is Relation-like the carrier of I[01] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of [:S,T:]:])

f . 0 is set

f . 1 is set

[: the carrier of I[01], the carrier of S:] is Relation-like set

bool [: the carrier of I[01], the carrier of S:] is set

(S,T,I[01],f) is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of S:])

g is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of S:])

g . 0 is set

g . 1 is set

dom g is V126() V127() V128() M2( bool the carrier of I[01])

bool the carrier of I[01] is set

dom f is V126() V127() V128() M2( bool the carrier of I[01])

j0 is V11() V12() ext-real M2( the carrier of I[01])

[s1,t1] `1 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

[s2,t2] `1 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

the carrier of [:S,T:] is non empty set

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

[: the carrier of I[01], the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of I[01], the carrier of [:S,T:]:] is set

f is Relation-like the carrier of I[01] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of [:S,T:]:])

f . 0 is set

f . 1 is set

[: the carrier of I[01], the carrier of T:] is Relation-like set

bool [: the carrier of I[01], the carrier of T:] is set

(S,T,I[01],f) is Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of T:])

g is Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of T:])

g . 0 is set

g . 1 is set

dom g is V126() V127() V128() M2( bool the carrier of I[01])

bool the carrier of I[01] is set

dom f is V126() V127() V128() M2( bool the carrier of I[01])

j0 is V11() V12() ext-real M2( the carrier of I[01])

[s1,t1] `2 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

[s2,t2] `2 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),f) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])

[: the carrier of K554(), the carrier of S:] is Relation-like set

bool [: the carrier of K554(), the carrier of S:] is set

dom (S,T,K554(),f) is V126() V127() V128() M2( bool the carrier of K554())

bool the carrier of K554() is set

dom f is V126() V127() V128() M2( bool the carrier of K554())

j0 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f) . 0 is set

f . 0 is set

(f . 0) `1 is set

[s1,t1] `1 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f) . 1 is set

f . 1 is set

(f . 1) `1 is set

[s2,t2] `1 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),f) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of T:])

[: the carrier of K554(), the carrier of T:] is Relation-like set

bool [: the carrier of K554(), the carrier of T:] is set

dom (S,T,K554(),f) is V126() V127() V128() M2( bool the carrier of K554())

bool the carrier of K554() is set

dom f is V126() V127() V128() M2( bool the carrier of K554())

j0 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f) . 0 is set

f . 0 is set

(f . 0) `2 is set

[s1,t1] `2 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f) . 1 is set

f . 1 is set

(f . 1) `2 is set

[s2,t2] `2 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

the carrier of [:S,T:] is non empty set

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

[: the carrier of I[01], the carrier of S:] is Relation-like set

bool [: the carrier of I[01], the carrier of S:] is set

f is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of S:])

f . 0 is set

f . 1 is set

[: the carrier of I[01], the carrier of T:] is Relation-like set

bool [: the carrier of I[01], the carrier of T:] is set

g is Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of T:])

g . 0 is set

g . 1 is set

(S,T,I[01],f,g) is Relation-like the carrier of I[01] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of I[01], the carrier of [:S,T:]:])

[: the carrier of I[01], the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of I[01], the carrier of [:S,T:]:] is set

(S,T,I[01],f,g) . 0 is set

(S,T,I[01],f,g) . 1 is set

dom f is V126() V127() V128() M2( bool the carrier of I[01])

bool the carrier of I[01] is set

dom g is V126() V127() V128() M2( bool the carrier of I[01])

j0 is V11() V12() ext-real M2( the carrier of I[01])

f . j0 is M2( the carrier of S)

g . j0 is M2( the carrier of T)

[(f . j0),(g . j0)] is V24() M2( the carrier of [:S,T:])

{(f . j0),(g . j0)} is set

{(f . j0)} is set

{{(f . j0),(g . j0)},{(f . j0)}} is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

f . j1 is M2( the carrier of S)

g . j1 is M2( the carrier of T)

[(f . j1),(g . j1)] is V24() M2( the carrier of [:S,T:])

{(f . j1),(g . j1)} is set

{(f . j1)} is set

{{(f . j1),(g . j1)},{(f . j1)}} is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2

g is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2

(S,T,K554(),f,g) is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of [:S,T:]:])

[: the carrier of K554(), the carrier of [:S,T:]:] is Relation-like set

bool [: the carrier of K554(), the carrier of [:S,T:]:] is set

dom f is V126() V127() V128() M2( bool the carrier of K554())

bool the carrier of K554() is set

dom g is V126() V127() V128() M2( bool the carrier of K554())

j1 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f,g) . j1 is M2( the carrier of [:S,T:])

f . j1 is M2( the carrier of S)

g . j1 is M2( the carrier of T)

[(f . j1),(g . j1)] is V24() M2( the carrier of [:S,T:])

{(f . j1),(g . j1)} is set

{(f . j1)} is set

{{(f . j1),(g . j1)},{(f . j1)}} is set

[s2,(g . j1)] is V24() M2( the carrier of [:S,T:])

{s2,(g . j1)} is set

{{s2,(g . j1)},{s2}} is set

j0 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,K554(),f,g) . j0 is M2( the carrier of [:S,T:])

f . j0 is M2( the carrier of S)

g . j0 is M2( the carrier of T)

[(f . j0),(g . j0)] is V24() M2( the carrier of [:S,T:])

{(f . j0),(g . j0)} is set

{(f . j0)} is set

{{(f . j0),(g . j0)},{(f . j0)}} is set

[s1,(g . j0)] is V24() M2( the carrier of [:S,T:])

{s1,(g . j0)} is set

{{s1,(g . j0)},{s1}} is set

S is non empty TopSpace-like pathwise_connected TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like pathwise_connected TopStruct

the carrier of T is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

t2 is M2( the carrier of T)

f is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total continuous Path of s1,s2

g is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total continuous Path of t1,t2

<:f,g:> is Relation-like Function-like set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of T)

t1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1

t2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2

<:t1,t2:> is Relation-like Function-like set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

[s1,s2] is V24() M2( the carrier of [:S,T:])

{s1,s2} is set

{s1} is set

{{s1,s2},{s1}} is set

S is non empty TopSpace-like pathwise_connected TopStruct

T is non empty TopSpace-like pathwise_connected TopStruct

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of [:S,T:])

s2 is M2( the carrier of [:S,T:])

the carrier of S is non empty set

the carrier of T is non empty set

t1 is M2( the carrier of S)

t2 is M2( the carrier of T)

[t1,t2] is V24() M2( the carrier of [:S,T:])

{t1,t2} is set

{t1} is set

{{t1,t2},{t1}} is set

f is M2( the carrier of S)

g is M2( the carrier of T)

[f,g] is V24() M2( the carrier of [:S,T:])

{f,g} is set

{f} is set

{{f,g},{f}} is set

S is non empty TopSpace-like pathwise_connected TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like pathwise_connected TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like pathwise_connected TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

s2 is M2( the carrier of S)

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s1,t1],[s2,t2]

pr1 f is Relation-like Function-like set

pr2 f is Relation-like Function-like set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of T)

[s1,s2] is V24() M2( the carrier of [:S,T:])

{s1,s2} is set

{s1} is set

{{s1,s2},{s1}} is set

t1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]

pr1 t1 is Relation-like Function-like set

pr2 t1 is Relation-like Function-like set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),f) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])

[: the carrier of K554(), the carrier of S:] is Relation-like set

bool [: the carrier of K554(), the carrier of S:] is set

g is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),g) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])

lb is Relation-like the carrier of [:K554(),K554():] -defined the carrier of [:S,T:] -valued Function-like quasi_total Homotopy of f,g

(S,T,[:K554(),K554():],lb) is Relation-like the carrier of [:K554(),K554():] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of [:K554(),K554():], the carrier of S:])

[: the carrier of [:K554(),K554():], the carrier of S:] is Relation-like set

bool [: the carrier of [:K554(),K554():], the carrier of S:] is set

dom f is V126() V127() V128() M2( bool the carrier of K554())

bool the carrier of K554() is set

dom g is V126() V127() V128() M2( bool the carrier of K554())

B1 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,[:K554(),K554():],lb) . (B1,0) is set

[B1,0] is V24() set

{B1,0} is V126() V127() V128() set

{B1} is V126() V127() V128() set

{{B1,0},{B1}} is set

(S,T,[:K554(),K554():],lb) . [B1,0] is set

(S,T,K554(),f) . B1 is M2( the carrier of S)

(S,T,[:K554(),K554():],lb) . (B1,1) is set

[B1,1] is V24() set

{B1,1} is V126() V127() V128() set

{{B1,1},{B1}} is set

(S,T,[:K554(),K554():],lb) . [B1,1] is set

(S,T,K554(),g) . B1 is M2( the carrier of S)

dom lb is M2( bool the carrier of [:K554(),K554():])

j0 is V11() V12() ext-real M2( the carrier of I[01])

[B1,j0] is V24() M2( the carrier of [:I[01],I[01]:])

{B1,j0} is V126() V127() V128() set

{{B1,j0},{B1}} is set

lb . [B1,j0] is M2( the carrier of [:S,T:])

(lb . [B1,j0]) `1 is set

lb . (B1,j0) is set

[B1,j0] is V24() set

lb . [B1,j0] is set

(lb . (B1,j0)) `1 is set

f . B1 is M2( the carrier of [:S,T:])

(f . B1) `1 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

[B1,j1] is V24() M2( the carrier of [:I[01],I[01]:])

{B1,j1} is V126() V127() V128() set

{{B1,j1},{B1}} is set

lb . [B1,j1] is M2( the carrier of [:S,T:])

(lb . [B1,j1]) `1 is set

lb . (B1,j1) is set

[B1,j1] is V24() set

lb . [B1,j1] is set

(lb . (B1,j1)) `1 is set

g . B1 is M2( the carrier of [:S,T:])

(g . B1) `1 is set

B2 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,[:K554(),K554():],lb) . (0,B2) is set

[0,B2] is V24() set

{0,B2} is V126() V127() V128() set

{0} is V126() V127() V128() V129() V130() V131() set

{{0,B2},{0}} is set

(S,T,[:K554(),K554():],lb) . [0,B2] is set

(S,T,[:K554(),K554():],lb) . (1,B2) is set

[1,B2] is V24() set

{1,B2} is V126() V127() V128() set

{{1,B2},{1}} is set

(S,T,[:K554(),K554():],lb) . [1,B2] is set

[j0,B2] is V24() M2( the carrier of [:I[01],I[01]:])

{j0,B2} is V126() V127() V128() set

{j0} is V126() V127() V128() set

{{j0,B2},{j0}} is set

lb . [j0,B2] is M2( the carrier of [:S,T:])

(lb . [j0,B2]) `1 is set

lb . (j0,B2) is set

[j0,B2] is V24() set

lb . [j0,B2] is set

(lb . (j0,B2)) `1 is set

[s1,t1] `1 is set

[j1,B2] is V24() M2( the carrier of [:I[01],I[01]:])

{j1,B2} is V126() V127() V128() set

{j1} is V126() V127() V128() set

{{j1,B2},{j1}} is set

lb . [j1,B2] is M2( the carrier of [:S,T:])

(lb . [j1,B2]) `1 is set

lb . (j1,B2) is set

[j1,B2] is V24() set

lb . [j1,B2] is set

(lb . (j1,B2)) `1 is set

[s2,t2] `1 is set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

[:S,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:S,T:] is non empty set

s1 is M2( the carrier of S)

s2 is M2( the carrier of S)

t1 is M2( the carrier of T)

[s1,t1] is V24() M2( the carrier of [:S,T:])

{s1,t1} is set

{s1} is set

{{s1,t1},{s1}} is set

t2 is M2( the carrier of T)

[s2,t2] is V24() M2( the carrier of [:S,T:])

{s2,t2} is set

{s2} is set

{{s2,t2},{s2}} is set

f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),f) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of T:])

[: the carrier of K554(), the carrier of T:] is Relation-like set

bool [: the carrier of K554(), the carrier of T:] is set

g is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t1],[s2,t2]

(S,T,K554(),g) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of T:])

lb is Relation-like the carrier of [:K554(),K554():] -defined the carrier of [:S,T:] -valued Function-like quasi_total Homotopy of f,g

(S,T,[:K554(),K554():],lb) is Relation-like the carrier of [:K554(),K554():] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of [:K554(),K554():], the carrier of T:])

[: the carrier of [:K554(),K554():], the carrier of T:] is Relation-like set

bool [: the carrier of [:K554(),K554():], the carrier of T:] is set

dom f is V126() V127() V128() M2( bool the carrier of K554())

bool the carrier of K554() is set

dom g is V126() V127() V128() M2( bool the carrier of K554())

B1 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,[:K554(),K554():],lb) . (B1,0) is set

[B1,0] is V24() set

{B1,0} is V126() V127() V128() set

{B1} is V126() V127() V128() set

{{B1,0},{B1}} is set

(S,T,[:K554(),K554():],lb) . [B1,0] is set

(S,T,K554(),f) . B1 is M2( the carrier of T)

(S,T,[:K554(),K554():],lb) . (B1,1) is set

[B1,1] is V24() set

{B1,1} is V126() V127() V128() set

{{B1,1},{B1}} is set

(S,T,[:K554(),K554():],lb) . [B1,1] is set

(S,T,K554(),g) . B1 is M2( the carrier of T)

dom lb is M2( bool the carrier of [:K554(),K554():])

j0 is V11() V12() ext-real M2( the carrier of I[01])

[B1,j0] is V24() M2( the carrier of [:I[01],I[01]:])

{B1,j0} is V126() V127() V128() set

{{B1,j0},{B1}} is set

lb . [B1,j0] is M2( the carrier of [:S,T:])

(lb . [B1,j0]) `2 is set

lb . (B1,j0) is set

[B1,j0] is V24() set

lb . [B1,j0] is set

(lb . (B1,j0)) `2 is set

f . B1 is M2( the carrier of [:S,T:])

(f . B1) `2 is set

j1 is V11() V12() ext-real M2( the carrier of I[01])

[B1,j1] is V24() M2( the carrier of [:I[01],I[01]:])

{B1,j1} is V126() V127() V128() set

{{B1,j1},{B1}} is set

lb . [B1,j1] is M2( the carrier of [:S,T:])

(lb . [B1,j1]) `2 is set

lb . (B1,j1) is set

[B1,j1] is V24() set

lb . [B1,j1] is set

(lb . (B1,j1)) `2 is set

g . B1 is M2( the carrier of [:S,T:])

(g . B1) `2 is set

B2 is V11() V12() ext-real M2( the carrier of I[01])

(S,T,[:K554(),K554():],lb) . (0,B2) is set