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
[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]) `2 is set
lb . (j0,B2) is set
[j0,B2] is V24() set
lb . [j0,B2] is set
(lb . (j0,B2)) `2 is set
[s1,t1] `2 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]) `2 is set
lb . (j1,B2) is set
[j1,B2] is V24() set
lb . [j1,B2] is set
(lb . (j1,B2)) `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
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
B1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B2 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:K554(),K554():],lb) . [A1,0] is set
B1 . A1 is M2( the carrier of S)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:K554(),K554():],lb) . [A2,1] is set
B2 . A2 is M2( the carrier of S)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:K554(),K554():],lb) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:K554(),K554():],lb) . [1,c18] is set
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:K554(),K554():],lb) . [A1,0] is set
B1 . A1 is M2( the carrier of S)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:K554(),K554():],lb) . [A2,1] is set
B2 . A2 is M2( the carrier of S)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:K554(),K554():],lb) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:K554(),K554():],lb) . [1,c18] 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
B1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
B2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:K554(),K554():],lb) . [A1,0] is set
B1 . A1 is M2( the carrier of T)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:K554(),K554():],lb) . [A2,1] is set
B2 . A2 is M2( the carrier of T)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:K554(),K554():],lb) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:K554(),K554():],lb) . [1,c18] is set
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:K554(),K554():],lb) . [A1,0] is set
B1 . A1 is M2( the carrier of T)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:K554(),K554():],lb) . [A2,1] is set
B2 . A2 is M2( the carrier of T)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:K554(),K554():],lb) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],lb) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:K554(),K554():],lb) . [1,c18] 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
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() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
[: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is set
B2 is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:])
(S,T,[:I[01],I[01]:],B2) is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of S:])
[: the carrier of [:I[01],I[01]:], the carrier of S:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of S:] is set
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:I[01],I[01]:],B2) . [A1,0] is set
lb . A1 is M2( the carrier of S)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:I[01],I[01]:],B2) . [A2,1] is set
B1 . A2 is M2( the carrier of S)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:I[01],I[01]:],B2) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:I[01],I[01]:],B2) . [1,c18] 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() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
B1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
[: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is set
B2 is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:])
(S,T,[:I[01],I[01]:],B2) is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of T:])
[: the carrier of [:I[01],I[01]:], the carrier of T:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
A1 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (A1,0) is set
[A1,0] is V24() set
{A1,0} is V126() V127() V128() set
{A1} is V126() V127() V128() set
{{A1,0},{A1}} is set
(S,T,[:I[01],I[01]:],B2) . [A1,0] is set
lb . A1 is M2( the carrier of T)
A2 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (A2,1) is set
[A2,1] is V24() set
{A2,1} is V126() V127() V128() set
{A2} is V126() V127() V128() set
{{A2,1},{A2}} is set
(S,T,[:I[01],I[01]:],B2) . [A2,1] is set
B1 . A2 is M2( the carrier of T)
lab is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (0,lab) is set
[0,lab] is V24() set
{0,lab} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,lab},{0}} is set
(S,T,[:I[01],I[01]:],B2) . [0,lab] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],B2) . (1,c18) is set
[1,c18] is V24() set
{1,c18} is V126() V127() V128() set
{{1,c18},{1}} is set
(S,T,[:I[01],I[01]:],B2) . [1,c18] 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
(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 S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])
(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() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A2 is Relation-like the carrier of [:K554(),K554():] -defined the carrier of S -valued Function-like quasi_total Homotopy of lb,B1
lab is Relation-like the carrier of [:K554(),K554():] -defined the carrier of T -valued Function-like quasi_total Homotopy of B2,A1
(S,T,[:K554(),K554():],A2,lab) is Relation-like the carrier of [:K554(),K554():] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of [:K554(),K554():], the carrier of [:S,T:]:])
[: the carrier of [:K554(),K554():], the carrier of [:S,T:]:] is Relation-like set
bool [: the carrier of [:K554(),K554():], the carrier of [:S,T:]:] is set
a is V11() V12() ext-real M2( the carrier of I[01])
(S,T,[:K554(),K554():],A2,lab) . (a,0) is set
[a,0] is V24() set
{a,0} is V126() V127() V128() set
{a} is V126() V127() V128() set
{{a,0},{a}} is set
(S,T,[:K554(),K554():],A2,lab) . [a,0] is set
f . a is M2( the carrier of [:S,T:])
(S,T,[:K554(),K554():],A2,lab) . (a,1) is set
[a,1] is V24() set
{a,1} is V126() V127() V128() set
{{a,1},{a}} is set
(S,T,[:K554(),K554():],A2,lab) . [a,1] is set
g . a is M2( the carrier of [:S,T:])
dom f is V126() V127() V128() M2( bool the carrier of K554())
bool the carrier of K554() is set
[: the carrier of S, the carrier of T:] is Relation-like set
dom A2 is M2( bool the carrier of [:K554(),K554():])
dom lab is M2( bool the carrier of [:K554(),K554():])
j0 is V11() V12() ext-real M2( the carrier of I[01])
[a,j0] is V24() M2( the carrier of [:I[01],I[01]:])
{a,j0} is V126() V127() V128() set
{{a,j0},{a}} is set
A2 . [a,j0] is M2( the carrier of S)
lab . [a,j0] is M2( the carrier of T)
[(A2 . [a,j0]),(lab . [a,j0])] is V24() M2( the carrier of [:S,T:])
{(A2 . [a,j0]),(lab . [a,j0])} is set
{(A2 . [a,j0])} is set
{{(A2 . [a,j0]),(lab . [a,j0])},{(A2 . [a,j0])}} is set
A2 . (a,j0) is set
[a,j0] is V24() set
A2 . [a,j0] is set
lab . (a,j0) is set
lab . [a,j0] is set
[(A2 . (a,j0)),(lab . (a,j0))] is V24() set
{(A2 . (a,j0)),(lab . (a,j0))} is set
{(A2 . (a,j0))} is set
{{(A2 . (a,j0)),(lab . (a,j0))},{(A2 . (a,j0))}} is set
(S,T,K554(),f) . a is M2( the carrier of S)
[((S,T,K554(),f) . a),(lab . (a,j0))] is V24() set
{((S,T,K554(),f) . a),(lab . (a,j0))} is set
{((S,T,K554(),f) . a)} is set
{{((S,T,K554(),f) . a),(lab . (a,j0))},{((S,T,K554(),f) . a)}} is set
(S,T,K554(),f) . a is M2( the carrier of T)
[((S,T,K554(),f) . a),((S,T,K554(),f) . a)] is V24() M2( the carrier of [:S,T:])
{((S,T,K554(),f) . a),((S,T,K554(),f) . a)} is set
{{((S,T,K554(),f) . a),((S,T,K554(),f) . a)},{((S,T,K554(),f) . a)}} is set
(f . a) `1 is set
[((f . a) `1),((S,T,K554(),f) . a)] is V24() set
{((f . a) `1),((S,T,K554(),f) . a)} is set
{((f . a) `1)} is set
{{((f . a) `1),((S,T,K554(),f) . a)},{((f . a) `1)}} is set
(f . a) `2 is set
[((f . a) `1),((f . a) `2)] is V24() set
{((f . a) `1),((f . a) `2)} is set
{{((f . a) `1),((f . a) `2)},{((f . a) `1)}} 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])
[a,j1] is V24() M2( the carrier of [:I[01],I[01]:])
{a,j1} is V126() V127() V128() set
{{a,j1},{a}} is set
A2 . [a,j1] is M2( the carrier of S)
lab . [a,j1] is M2( the carrier of T)
[(A2 . [a,j1]),(lab . [a,j1])] is V24() M2( the carrier of [:S,T:])
{(A2 . [a,j1]),(lab . [a,j1])} is set
{(A2 . [a,j1])} is set
{{(A2 . [a,j1]),(lab . [a,j1])},{(A2 . [a,j1])}} is set
A2 . (a,j1) is set
[a,j1] is V24() set
A2 . [a,j1] is set
lab . (a,j1) is set
lab . [a,j1] is set
[(A2 . (a,j1)),(lab . (a,j1))] is V24() set
{(A2 . (a,j1)),(lab . (a,j1))} is set
{(A2 . (a,j1))} is set
{{(A2 . (a,j1)),(lab . (a,j1))},{(A2 . (a,j1))}} is set
(S,T,K554(),g) . a is M2( the carrier of S)
[((S,T,K554(),g) . a),(lab . (a,j1))] is V24() set
{((S,T,K554(),g) . a),(lab . (a,j1))} is set
{((S,T,K554(),g) . a)} is set
{{((S,T,K554(),g) . a),(lab . (a,j1))},{((S,T,K554(),g) . a)}} is set
(S,T,K554(),g) . a is M2( the carrier of T)
[((S,T,K554(),g) . a),((S,T,K554(),g) . a)] is V24() M2( the carrier of [:S,T:])
{((S,T,K554(),g) . a),((S,T,K554(),g) . a)} is set
{{((S,T,K554(),g) . a),((S,T,K554(),g) . a)},{((S,T,K554(),g) . a)}} is set
(g . a) `1 is set
[((g . a) `1),((S,T,K554(),g) . a)] is V24() set
{((g . a) `1),((S,T,K554(),g) . a)} is set
{((g . a) `1)} is set
{{((g . a) `1),((S,T,K554(),g) . a)},{((g . a) `1)}} is set
(g . a) `2 is set
[((g . a) `1),((g . a) `2)] is V24() set
{((g . a) `1),((g . a) `2)} is set
{{((g . a) `1),((g . a) `2)},{((g . a) `1)}} is set
b is V11() V12() ext-real M2( the carrier of I[01])
(S,T,[:K554(),K554():],A2,lab) . (0,b) is set
[0,b] is V24() set
{0,b} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,b},{0}} is set
(S,T,[:K554(),K554():],A2,lab) . [0,b] is set
(S,T,[:K554(),K554():],A2,lab) . (1,b) is set
[1,b] is V24() set
{1,b} is V126() V127() V128() set
{{1,b},{1}} is set
(S,T,[:K554(),K554():],A2,lab) . [1,b] is set
[j0,b] is V24() M2( the carrier of [:I[01],I[01]:])
{j0,b} is V126() V127() V128() set
{j0} is V126() V127() V128() set
{{j0,b},{j0}} is set
A2 . [j0,b] is M2( the carrier of S)
lab . [j0,b] is M2( the carrier of T)
[(A2 . [j0,b]),(lab . [j0,b])] is V24() M2( the carrier of [:S,T:])
{(A2 . [j0,b]),(lab . [j0,b])} is set
{(A2 . [j0,b])} is set
{{(A2 . [j0,b]),(lab . [j0,b])},{(A2 . [j0,b])}} is set
A2 . (j0,b) is set
[j0,b] is V24() set
A2 . [j0,b] is set
lab . (j0,b) is set
lab . [j0,b] is set
[(A2 . (j0,b)),(lab . (j0,b))] is V24() set
{(A2 . (j0,b)),(lab . (j0,b))} is set
{(A2 . (j0,b))} is set
{{(A2 . (j0,b)),(lab . (j0,b))},{(A2 . (j0,b))}} is set
[s1,(lab . (j0,b))] is V24() set
{s1,(lab . (j0,b))} is set
{{s1,(lab . (j0,b))},{s1}} is set
[j1,b] is V24() M2( the carrier of [:I[01],I[01]:])
{j1,b} is V126() V127() V128() set
{j1} is V126() V127() V128() set
{{j1,b},{j1}} is set
A2 . [j1,b] is M2( the carrier of S)
lab . [j1,b] is M2( the carrier of T)
[(A2 . [j1,b]),(lab . [j1,b])] is V24() M2( the carrier of [:S,T:])
{(A2 . [j1,b]),(lab . [j1,b])} is set
{(A2 . [j1,b])} is set
{{(A2 . [j1,b]),(lab . [j1,b])},{(A2 . [j1,b])}} is set
A2 . (j1,b) is set
[j1,b] is V24() set
A2 . [j1,b] is set
lab . (j1,b) is set
lab . [j1,b] is set
[(A2 . (j1,b)),(lab . (j1,b))] is V24() set
{(A2 . (j1,b)),(lab . (j1,b))} is set
{(A2 . (j1,b))} is set
{{(A2 . (j1,b)),(lab . (j1,b))},{(A2 . (j1,b))}} is set
[s2,(lab . (j1,b))] is V24() set
{s2,(lab . (j1,b))} is set
{{s2,(lab . (j1,b))},{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
[: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
(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 S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])
(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() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A2 is Relation-like the carrier of [:K554(),K554():] -defined the carrier of S -valued Function-like quasi_total Homotopy of lb,B1
lab is Relation-like the carrier of [:K554(),K554():] -defined the carrier of T -valued Function-like quasi_total Homotopy of B2,A1
(S,T,[:K554(),K554():],A2,lab) is Relation-like the carrier of [:K554(),K554():] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of [:K554(),K554():], the carrier of [:S,T:]:])
[: the carrier of [:K554(),K554():], the carrier of [:S,T:]:] is Relation-like set
bool [: the carrier of [:K554(),K554():], the carrier of [:S,T:]:] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (c18,0) is set
[c18,0] is V24() set
{c18,0} is V126() V127() V128() set
{c18} is V126() V127() V128() set
{{c18,0},{c18}} is set
(S,T,[:K554(),K554():],A2,lab) . [c18,0] is set
f . c18 is M2( the carrier of [:S,T:])
a is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (a,1) is set
[a,1] is V24() set
{a,1} is V126() V127() V128() set
{a} is V126() V127() V128() set
{{a,1},{a}} is set
(S,T,[:K554(),K554():],A2,lab) . [a,1] is set
g . a is M2( the carrier of [:S,T:])
b is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (0,b) is set
[0,b] is V24() set
{0,b} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,b},{0}} is set
(S,T,[:K554(),K554():],A2,lab) . [0,b] is set
c21 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (1,c21) is set
[1,c21] is V24() set
{1,c21} is V126() V127() V128() set
{{1,c21},{1}} is set
(S,T,[:K554(),K554():],A2,lab) . [1,c21] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (c18,0) is set
[c18,0] is V24() set
{c18,0} is V126() V127() V128() set
{c18} is V126() V127() V128() set
{{c18,0},{c18}} is set
(S,T,[:K554(),K554():],A2,lab) . [c18,0] is set
f . c18 is M2( the carrier of [:S,T:])
a is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (a,1) is set
[a,1] is V24() set
{a,1} is V126() V127() V128() set
{a} is V126() V127() V128() set
{{a,1},{a}} is set
(S,T,[:K554(),K554():],A2,lab) . [a,1] is set
g . a is M2( the carrier of [:S,T:])
b is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (0,b) is set
[0,b] is V24() set
{0,b} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,b},{0}} is set
(S,T,[:K554(),K554():],A2,lab) . [0,b] is set
c21 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:K554(),K554():],A2,lab) . (1,c21) is set
[1,c21] is V24() set
{1,c21} is V126() V127() V128() set
{{1,c21},{1}} is set
(S,T,[:K554(),K554():],A2,lab) . [1,c21] 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
(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 S -valued Function-like quasi_total M2( bool [: the carrier of K554(), the carrier of S:])
(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() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
B2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t1,t2
[: the carrier of [:I[01],I[01]:], the carrier of T:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of T:] is set
A2 is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of T -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of T:])
[: the carrier of [:I[01],I[01]:], the carrier of S:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of S:] is set
lab is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of S -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of S:])
(S,T,[:I[01],I[01]:],lab,A2) is Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of [:S,T:] -valued Function-like quasi_total M2( bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:])
[: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is Relation-like set
bool [: the carrier of [:I[01],I[01]:], the carrier of [:S,T:]:] is set
c18 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],lab,A2) . (c18,0) is set
[c18,0] is V24() set
{c18,0} is V126() V127() V128() set
{c18} is V126() V127() V128() set
{{c18,0},{c18}} is set
(S,T,[:I[01],I[01]:],lab,A2) . [c18,0] is set
f . c18 is M2( the carrier of [:S,T:])
a is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],lab,A2) . (a,1) is set
[a,1] is V24() set
{a,1} is V126() V127() V128() set
{a} is V126() V127() V128() set
{{a,1},{a}} is set
(S,T,[:I[01],I[01]:],lab,A2) . [a,1] is set
g . a is M2( the carrier of [:S,T:])
b is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],lab,A2) . (0,b) is set
[0,b] is V24() set
{0,b} is V126() V127() V128() set
{0} is V126() V127() V128() V129() V130() V131() set
{{0,b},{0}} is set
(S,T,[:I[01],I[01]:],lab,A2) . [0,b] is set
c21 is V11() V12() ext-real M2( the carrier of K554())
(S,T,[:I[01],I[01]:],lab,A2) . (1,c21) is set
[1,c21] is V24() set
{1,c21} is V126() V127() V128() set
{{1,c21},{1}} is set
(S,T,[:I[01],I[01]:],lab,A2) . [1,c21] 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 S)
t2 is M2( the carrier of T)
[s1,t2] is V24() M2( the carrier of [:S,T:])
{s1,t2} is set
{s1} is set
{{s1,t2},{s1}} is set
f is M2( the carrier of T)
[s2,f] is V24() M2( the carrier of [:S,T:])
{s2,f} is set
{s2} is set
{{s2,f},{s2}} is set
g is M2( the carrier of T)
[t1,g] is V24() M2( the carrier of [:S,T:])
{t1,g} is set
{t1} is set
{{t1,g},{t1}} is set
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t2],[s2,f]
(S,T,K554(),lb) 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
B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s2,f],[t1,g]
(S,T,K554(),B1) 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 + B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t2],[t1,g]
(S,T,K554(),(lb + B1)) 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:])
B2 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s2
A1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s2,t1
B2 + A1 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,t1
dom B1 is V126() V127() V128() M2( bool the carrier of K554())
bool the carrier of K554() is set
dom lb is V126() V127() V128() M2( bool the carrier of K554())
dom (lb + B1) is V126() V127() V128() M2( bool the carrier of K554())
A2 is V11() V12() ext-real M2( the carrier of I[01])
1 / 2 is V11() V12() ext-real set
2 * A2 is V11() V12() ext-real set
(S,T,K554(),(lb + B1)) . A2 is M2( the carrier of S)
(lb + B1) . A2 is M2( the carrier of [:S,T:])
((lb + B1) . A2) `1 is set
lb . (2 * A2) is set
(lb . (2 * A2)) `1 is set
B2 . (2 * A2) is set
(B2 + A1) . A2 is M2( the carrier of S)
1 / 2 is V11() V12() ext-real set
A2 is V11() V12() ext-real M2( the carrier of I[01])
2 * A2 is V11() V12() ext-real set
(2 * A2) - 1 is V11() V12() ext-real set
(S,T,K554(),(lb + B1)) . A2 is M2( the carrier of S)
(lb + B1) . A2 is M2( the carrier of [:S,T:])
((lb + B1) . A2) `1 is set
B1 . ((2 * A2) - 1) is set
(B1 . ((2 * A2) - 1)) `1 is set
A1 . ((2 * A2) - 1) is set
(B2 + A1) . A2 is M2( the carrier of S)
A2 is V11() V12() ext-real M2( the carrier of I[01])
1 / 2 is V11() V12() ext-real 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)
s2 is M2( the carrier of S)
t1 is M2( the carrier of S)
t2 is M2( the carrier of T)
[s1,t2] is V24() M2( the carrier of [:S,T:])
{s1,t2} is set
{s1} is set
{{s1,t2},{s1}} is set
f is M2( the carrier of T)
[s2,f] is V24() M2( the carrier of [:S,T:])
{s2,f} is set
{s2} is set
{{s2,f},{s2}} is set
g is M2( the carrier of T)
[t1,g] is V24() M2( the carrier of [:S,T:])
{t1,g} is set
{t1} is set
{{t1,g},{t1}} is set
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s1,t2],[s2,f]
(S,T,s1,s2,t2,f,lb) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total continuous Path of s1,s2
B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s2,f],[t1,g]
lb + B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s1,t2],[t1,g]
(S,T,s1,t1,t2,g,(lb + B1)) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total continuous Path of s1,t1
(S,T,s2,t1,f,g,B1) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total continuous Path of s2,t1
(S,T,s1,s2,t2,f,lb) + (S,T,s2,t1,f,g,B1) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total continuous Path of s1,t1
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 S)
t2 is M2( the carrier of T)
[s1,t2] is V24() M2( the carrier of [:S,T:])
{s1,t2} is set
{s1} is set
{{s1,t2},{s1}} is set
f is M2( the carrier of T)
[s2,f] is V24() M2( the carrier of [:S,T:])
{s2,f} is set
{s2} is set
{{s2,f},{s2}} is set
g is M2( the carrier of T)
[t1,g] is V24() M2( the carrier of [:S,T:])
{t1,g} is set
{t1} is set
{{t1,g},{t1}} is set
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t2],[s2,f]
(S,T,K554(),lb) 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
B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s2,f],[t1,g]
(S,T,K554(),B1) 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 + B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,t2],[t1,g]
(S,T,K554(),(lb + B1)) 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:])
B2 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t2,f
A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of f,g
B2 + A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of t2,g
dom B1 is V126() V127() V128() M2( bool the carrier of K554())
bool the carrier of K554() is set
dom lb is V126() V127() V128() M2( bool the carrier of K554())
dom (lb + B1) is V126() V127() V128() M2( bool the carrier of K554())
A2 is V11() V12() ext-real M2( the carrier of I[01])
1 / 2 is V11() V12() ext-real set
2 * A2 is V11() V12() ext-real set
(S,T,K554(),(lb + B1)) . A2 is M2( the carrier of T)
(lb + B1) . A2 is M2( the carrier of [:S,T:])
((lb + B1) . A2) `2 is set
lb . (2 * A2) is set
(lb . (2 * A2)) `2 is set
B2 . (2 * A2) is set
(B2 + A1) . A2 is M2( the carrier of T)
1 / 2 is V11() V12() ext-real set
A2 is V11() V12() ext-real M2( the carrier of I[01])
2 * A2 is V11() V12() ext-real set
(2 * A2) - 1 is V11() V12() ext-real set
(S,T,K554(),(lb + B1)) . A2 is M2( the carrier of T)
(lb + B1) . A2 is M2( the carrier of [:S,T:])
((lb + B1) . A2) `2 is set
B1 . ((2 * A2) - 1) is set
(B1 . ((2 * A2) - 1)) `2 is set
A1 . ((2 * A2) - 1) is set
(B2 + A1) . A2 is M2( the carrier of T)
A2 is V11() V12() ext-real M2( the carrier of I[01])
1 / 2 is V11() V12() ext-real 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)
s2 is M2( the carrier of S)
t1 is M2( the carrier of S)
t2 is M2( the carrier of T)
[s1,t2] is V24() M2( the carrier of [:S,T:])
{s1,t2} is set
{s1} is set
{{s1,t2},{s1}} is set
f is M2( the carrier of T)
[s2,f] is V24() M2( the carrier of [:S,T:])
{s2,f} is set
{s2} is set
{{s2,f},{s2}} is set
g is M2( the carrier of T)
[t1,g] is V24() M2( the carrier of [:S,T:])
{t1,g} is set
{t1} is set
{{t1,g},{t1}} is set
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s1,t2],[s2,f]
(S,T,s1,s2,t2,f,lb) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total continuous Path of t2,f
B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s2,f],[t1,g]
lb + B1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total continuous Path of [s1,t2],[t1,g]
(S,T,s1,t1,t2,g,(lb + B1)) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total continuous Path of t2,g
(S,T,s2,t1,f,g,B1) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total continuous Path of f,g
(S,T,s1,s2,t2,f,lb) + (S,T,s2,t1,f,g,B1) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total continuous Path of t2,g
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 T)
[s1,s2] is V24() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] is set
g is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),lb) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,lb)) is M2( bool (Loops s2))
bool (Loops s2) is set
(S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,lb)) is M2( bool (Loops s1))
bool (Loops s1) is set
Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is Relation-like non-empty {1,2} -defined Function-like total set
dom (Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is V126() V127() V128() V129() V130() V131() M2( bool {1,2})
bool {1,2} is set
A1 is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> . 1 is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> . 2 is set
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> . 1 is set
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> . 2 is set
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> . A1 is set
(Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) . A1 is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> . A1 is set
A2 is 1-sorted
the carrier of A2 is set
product (Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is set
dom <*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> is non empty V126() V127() V128() V129() V130() V131() M2( bool K32())
A1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
g is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
g is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
lb is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
B1 is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
g . B1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
B2 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),B2) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2,B2) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,B2)) is M2( bool (Loops s1))
bool (Loops s1) is set
(S,T,s1,s2,B2) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,B2)) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,B2))),(Class ((EqRel (T,s2)),(S,T,s1,s2,B2)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
lb . B1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
A1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),A1) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,A1) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,A1)) is M2( bool (Loops s1))
(S,T,s1,s2,A1) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,A1)) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,A1))),(Class ((EqRel (T,s2)),(S,T,s1,s2,A1)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-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)
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
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
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] is set
t1 is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
(S,T,s1,s2) . t1 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
t2 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),t2) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2,t2) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,t2)) is M2( bool (Loops s1))
bool (Loops s1) is set
(S,T,s1,s2,t2) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,t2)) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,t2))),(Class ((EqRel (T,s2)),(S,T,s1,s2,t2)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
f is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),f) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,f) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,f)) is M2( bool (Loops s1))
(S,T,s1,s2,f) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,f)) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,f))),(Class ((EqRel (T,s2)),(S,T,s1,s2,f)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-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)
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
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
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] 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]
Class ((EqRel ([:S,T:],[s1,s2])),t1) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2) . (Class ((EqRel ([:S,T:],[s1,s2])),t1)) is set
(S,T,s1,s2,t1) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,t1)) is M2( bool (Loops s1))
bool (Loops s1) is set
(S,T,s1,s2,t1) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,t1)) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,t1))),(Class ((EqRel (T,s2)),(S,T,s1,s2,t1)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-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
s1 is M2( the carrier of S)
s2 is M2( the carrier of T)
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like quasi_total M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
[:S,T:] is non empty strict TopSpace-like TopStruct
[s1,s2] is V24() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is Relation-like non-empty {1,2} -defined Function-like total set
product (Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is set
lb is set
proj1 (S,T,s1,s2) is set
B1 is set
(S,T,s1,s2) . lb is set
(S,T,s1,s2) . B1 is set
dom (S,T,s1,s2) is M2( bool the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
bool the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is set
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] is set
B2 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),B2) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2,B2) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,B2)) is M2( bool (Loops s1))
bool (Loops s1) is set
(S,T,s1,s2,B2) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,B2)) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,B2))),(Class ((EqRel (T,s2)),(S,T,s1,s2,B2)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
A1 is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),A1) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,A1) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,A1)) is M2( bool (Loops s1))
(S,T,s1,s2,A1) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,A1)) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,A1))),(Class ((EqRel (T,s2)),(S,T,s1,s2,A1)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
rng (S,T,s1,s2) is M2( bool the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
bool the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is set
lb is set
dom (Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is V126() V127() V128() V129() V130() V131() M2( bool {1,2})
bool {1,2} is set
B1 is Relation-like Function-like set
proj1 B1 is set
B2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like set
len B2 is V10() V11() V12() V30() V31() ext-real V126() V127() V128() V129() V130() V131() M3(K28(),K32())
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> . 2 is set
(Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) . 2 is set
B2 . 2 is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] is set
A1 is 1-sorted
the carrier of A1 is set
A1 is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),A1) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> . 1 is set
(Carrier <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) . 1 is set
B2 . 1 is set
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
A2 is 1-sorted
the carrier of A2 is set
A2 is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),A2) is M2( bool (Loops s1))
bool (Loops s1) is set
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
(S,T,s1,s2,A2,A1) is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),(S,T,s1,s2,A2,A1)) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
dom A2 is V126() V127() V128() M2( bool the carrier of K554())
bool the carrier of K554() is set
dom A1 is V126() V127() V128() M2( bool the carrier of K554())
dom (S,T,s1,s2) is M2( bool the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
bool the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is set
(S,T,s1,s2) . (Class ((EqRel ([:S,T:],[s1,s2])),(S,T,s1,s2,A2,A1))) is set
(S,T,s1,s2,(S,T,s1,s2,A2,A1)) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,(S,T,s1,s2,A2,A1))) is M2( bool (Loops s1))
(S,T,s1,s2,(S,T,s1,s2,A2,A1)) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,(S,T,s1,s2,A2,A1))) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,(S,T,s1,s2,A2,A1)))),(Class ((EqRel (T,s2)),(S,T,s1,s2,(S,T,s1,s2,A2,A1))))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
<*(Class ((EqRel (S,s1)),A2)),(Class ((EqRel (T,s2)),(S,T,s1,s2,(S,T,s1,s2,A2,A1))))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
<*(Class ((EqRel (S,s1)),A2)),(Class ((EqRel (T,s2)),A1))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-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
s1 is M2( the carrier of S)
s2 is M2( the carrier of T)
[s1,s2] is V24() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like one-to-one quasi_total onto M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
t2 is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
f is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
t2 * f is M2( the carrier of (FundamentalGroup ([:S,T:],[s1,s2])))
(S,T,s1,s2) . (t2 * f) is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
(S,T,s1,s2) . t2 is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
(S,T,s1,s2) . f is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
((S,T,s1,s2) . t2) * ((S,T,s1,s2) . f) is Relation-like K32() -defined Function-like V32() FinSequence-like FinSubsequence-like M2( the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
Loops [s1,s2] is non empty set
Paths ([s1,s2],[s1,s2]) is non empty set
EqRel ([:S,T:],[s1,s2]) is non empty Relation-like Loops [s1,s2] -defined Loops [s1,s2] -valued total V197() V202() M2( bool [:(Loops [s1,s2]),(Loops [s1,s2]):])
[:(Loops [s1,s2]),(Loops [s1,s2]):] is Relation-like set
bool [:(Loops [s1,s2]),(Loops [s1,s2]):] is set
EqRel ([:S,T:],[s1,s2],[s1,s2]) is Relation-like Paths ([s1,s2],[s1,s2]) -defined Paths ([s1,s2],[s1,s2]) -valued M2( bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):])
[:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is Relation-like set
bool [:(Paths ([s1,s2],[s1,s2])),(Paths ([s1,s2],[s1,s2])):] is set
Loops s1 is non empty set
Paths (s1,s1) is non empty set
EqRel (S,s1) is non empty Relation-like Loops s1 -defined Loops s1 -valued total V197() V202() M2( bool [:(Loops s1),(Loops s1):])
[:(Loops s1),(Loops s1):] is Relation-like set
bool [:(Loops s1),(Loops s1):] is set
EqRel (S,s1,s1) is Relation-like Paths (s1,s1) -defined Paths (s1,s1) -valued M2( bool [:(Paths (s1,s1)),(Paths (s1,s1)):])
[:(Paths (s1,s1)),(Paths (s1,s1)):] is Relation-like set
bool [:(Paths (s1,s1)),(Paths (s1,s1)):] is set
Loops s2 is non empty set
Paths (s2,s2) is non empty set
EqRel (T,s2) is non empty Relation-like Loops s2 -defined Loops s2 -valued total V197() V202() M2( bool [:(Loops s2),(Loops s2):])
[:(Loops s2),(Loops s2):] is Relation-like set
bool [:(Loops s2),(Loops s2):] is set
EqRel (T,s2,s2) is Relation-like Paths (s2,s2) -defined Paths (s2,s2) -valued M2( bool [:(Paths (s2,s2)),(Paths (s2,s2)):])
[:(Paths (s2,s2)),(Paths (s2,s2)):] is Relation-like set
bool [:(Paths (s2,s2)),(Paths (s2,s2)):] is set
g is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),g) is M2( bool (Loops [s1,s2]))
bool (Loops [s1,s2]) is set
(S,T,s1,s2,g) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,g)) is M2( bool (Loops s1))
bool (Loops s1) is set
(S,T,s1,s2,g) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,g)) is M2( bool (Loops s2))
bool (Loops s2) is set
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,g))),(Class ((EqRel (T,s2)),(S,T,s1,s2,g)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),lb) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,lb)) is M2( bool (Loops s1))
(S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,lb)) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lb))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lb)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
the carrier of (FundamentalGroup (T,s2)) is non empty set
the carrier of (FundamentalGroup (S,s1)) is non empty set
lab is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),lab) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,lab) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),(S,T,s1,s2,lab)) is M2( bool (Loops s1))
(S,T,s1,s2,lab) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),(S,T,s1,s2,lab)) is M2( bool (Loops s2))
<*(Class ((EqRel (S,s1)),(S,T,s1,s2,lab))),(Class ((EqRel (T,s2)),(S,T,s1,s2,lab)))*> is non empty Relation-like K32() -defined Function-like V32() V39(2) FinSequence-like FinSubsequence-like set
g + lb is Relation-like the carrier of K554() -defined the carrier of [:S,T:] -valued Function-like quasi_total Path of [s1,s2],[s1,s2]
Class ((EqRel ([:S,T:],[s1,s2])),(g + lb)) is M2( bool (Loops [s1,s2]))
(S,T,s1,s2,(g + lb)) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
(S,T,s1,s2,(g + lb)) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
B1 is M2( the carrier of (FundamentalGroup (T,s2)))
B2 is M2( the carrier of (FundamentalGroup (T,s2)))
B1 * B2 is M2( the carrier of (FundamentalGroup (T,s2)))
(S,T,s1,s2,g) + (S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of T -valued Function-like quasi_total Path of s2,s2
Class ((EqRel (T,s2)),((S,T,s1,s2,g) + (S,T,s1,s2,lb))) is M2( bool (Loops s2))
Class ((EqRel (T,s2)),(S,T,s1,s2,(g + lb))) is M2( bool (Loops s2))
A1 is M2( the carrier of (FundamentalGroup (S,s1)))
A2 is M2( the carrier of (FundamentalGroup (S,s1)))
A1 * A2 is M2( the carrier of (FundamentalGroup (S,s1)))
(S,T,s1,s2,g) + (S,T,s1,s2,lb) is Relation-like the carrier of K554() -defined the carrier of S -valued Function-like quasi_total Path of s1,s1
Class ((EqRel (S,s1)),((S,T,s1,s2,g) + (S,T,s1,s2,lb))) is M2( bool (Loops s1))
Class ((EqRel (S,s1)),(S,T,s1,s2,(g + lb))) is M2( bool (Loops s1))
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)
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
s2 is M2( the carrier of T)
[s1,s2] is V24() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like one-to-one quasi_total onto multiplicative M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is set
rng (S,T,s1,s2) is M2( bool the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>))
bool the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,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
[:S,T:] is non empty strict TopSpace-like TopStruct
s1 is M2( the carrier of S)
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
s2 is M2( the carrier of T)
[s1,s2] is V24() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
FundamentalGroup ([:S,T:],[s1,s2]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
(S,T,s1,s2) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) -valued Function-like one-to-one quasi_total onto multiplicative M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):])
the carrier of (FundamentalGroup ([:S,T:],[s1,s2])) is non empty set
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>) is non empty set
[: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,s2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,s2])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,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
[:S,T:] is non empty strict TopSpace-like TopStruct
s1 is M2( the carrier of S)
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup (S,s1)) is non empty set
s2 is M2( the carrier of S)
FundamentalGroup (S,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup (S,s2)) is non empty set
[: the carrier of (FundamentalGroup (S,s1)), the carrier of (FundamentalGroup (S,s2)):] is Relation-like set
bool [: the carrier of (FundamentalGroup (S,s1)), the carrier of (FundamentalGroup (S,s2)):] is set
t1 is M2( the carrier of T)
FundamentalGroup (T,t1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup (T,t1)) is non empty set
[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
FundamentalGroup ([:S,T:],[s1,t1]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup ([:S,T:],[s1,t1])) is non empty set
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>) is non empty set
(S,T,s1,t1) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,t1])) -defined the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>) -valued Function-like one-to-one quasi_total onto multiplicative M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>):])
[: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>):] is set
t2 is M2( the carrier of T)
FundamentalGroup (T,t2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (FundamentalGroup (T,t2)) is non empty set
[: the carrier of (FundamentalGroup (T,t1)), the carrier of (FundamentalGroup (T,t2)):] is Relation-like set
bool [: the carrier of (FundamentalGroup (T,t1)), the carrier of (FundamentalGroup (T,t2)):] is set
<*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*> 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 <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>) is non empty set
f is Relation-like the carrier of (FundamentalGroup (S,s1)) -defined the carrier of (FundamentalGroup (S,s2)) -valued Function-like quasi_total multiplicative M2( bool [: the carrier of (FundamentalGroup (S,s1)), the carrier of (FundamentalGroup (S,s2)):])
g is Relation-like the carrier of (FundamentalGroup (T,t1)) -defined the carrier of (FundamentalGroup (T,t2)) -valued Function-like quasi_total multiplicative M2( bool [: the carrier of (FundamentalGroup (T,t1)), the carrier of (FundamentalGroup (T,t2)):])
((FundamentalGroup (S,s1)),(FundamentalGroup (T,t1)),(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2)),f,g) is Relation-like the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>) -defined the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>) -valued Function-like quasi_total multiplicative M2( bool [: the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):])
[: the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):] is Relation-like set
bool [: the carrier of (product <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*>), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):] is set
((FundamentalGroup (S,s1)),(FundamentalGroup (T,t1)),(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2)),f,g) * (S,T,s1,t1) is Relation-like the carrier of (FundamentalGroup ([:S,T:],[s1,t1])) -defined the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>) -valued Function-like M2( bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):])
[: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):] is Relation-like set
bool [: the carrier of (FundamentalGroup ([:S,T:],[s1,t1])), the carrier of (product <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*>):] 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
s1 is M2( the carrier of S)
s2 is M2( the carrier of S)
FundamentalGroup (S,s2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
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
FundamentalGroup ([:S,T:],[s1,t1]) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
t2 is M2( the carrier of T)
FundamentalGroup (T,t2) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*> 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 <*(FundamentalGroup (S,s2)),(FundamentalGroup (T,t2))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (S,s1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
FundamentalGroup (T,t1) is non empty strict unital Group-like V96() V148() V149() V150() V151() V152() V153() multMagma
<*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*> 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 <*(FundamentalGroup (S,s1)),(FundamentalGroup (T,t1))*> is non empty strict unital Group-like V96() V138() V148() V149() V150() V151() V152() V153() multMagma