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