:: TOPALG_3 semantic presentation

K28() is V192() V193() V194() V198() set
K32() is V192() V193() V194() V195() V196() V197() V198() Element of bool K28()
bool K28() is non empty set
K527() is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected SubSpace of K525()
K525() is non empty strict TopSpace-like V255() TopStruct
the carrier of K527() is non empty V192() V193() V194() set
[:K527(),K527():] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:K527(),K527():] is non empty set
K27() is V192() V193() V194() V195() V196() V197() V198() set
bool K27() is non empty set
bool K32() is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set
1 is non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() Element of K32()
{{},1} is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],K28():] is Relation-like set
bool [:[:1,1:],K28():] is non empty set
[:K28(),K28():] is Relation-like set
[:[:K28(),K28():],K28():] is Relation-like set
bool [:[:K28(),K28():],K28():] is non empty set
2 is non empty V10() V11() V12() ext-real V168() V169() V192() V193() V194() V195() V196() V197() Element of K32()
[:2,2:] is non empty Relation-like set
[:[:2,2:],K28():] is Relation-like set
bool [:[:2,2:],K28():] is non empty set
K29() is V192() V198() set
K30() is V192() V193() V194() V195() V198() set
K31() is V192() V193() V194() V195() V196() V198() set
bool [:K28(),K28():] is non empty set
TOP-REAL 2 is non empty TopSpace-like V89() V117() V118() V119() V120() V121() V122() V123() V207() L18()
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is non empty set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V255() pathwise_connected TopStruct
the carrier of I[01] is non empty V192() V193() V194() set
K333() is V170() V255() L17()
[: the carrier of K527(), the carrier of K527():] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of K527():] is non empty set
bool the carrier of [:K527(),K527():] is non empty set
[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of [:I[01],I[01]:] is non empty set
0[01] is V11() V12() ext-real Element of the carrier of I[01]
0 is empty V10() V11() V12() Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V168() V169() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of K32()
1[01] is V11() V12() ext-real Element of the carrier of I[01]
K52(1,2) is V11() V12() ext-real Element of K28()
[: the carrier of I[01], the carrier of I[01]:] is non empty Relation-like set
S is set
T is set
[:S,T:] is Relation-like set
bool [:S,T:] is non empty set
s is set
t is set
s .--> t is Relation-like {s} -defined Function-like one-to-one set
{s} is non empty set
{s} --> t is non empty Relation-like {s} -defined {t} -valued Function-like constant V26({s}) quasi_total Element of bool [:{s},{t}:]
{t} is non empty set
[:{s},{t}:] is non empty Relation-like set
bool [:{s},{t}:] is non empty set
f is Relation-like S -defined T -valued Function-like quasi_total Element of bool [:S,T:]
f +* (s .--> t) is Relation-like Function-like set
rng (s .--> t) is set
rng (f +* (s .--> t)) is set
rng f is Element of bool T
bool T is non empty set
(rng f) \/ (rng (s .--> t)) is set
T \/ T is set
dom (f +* (s .--> t)) is set
dom f is Element of bool S
bool S is non empty set
dom (s .--> t) is Element of bool {s}
bool {s} is non empty set
(dom f) \/ (dom (s .--> t)) is set
S \/ (dom (s .--> t)) is set
S \/ {s} is non empty set
S is Relation-like Function-like set
T is set
S | T is Relation-like Function-like set
s is set
rng (S | T) is set
(S | T) " is Relation-like Function-like set
((S | T) ") * S is Relation-like Function-like set
(((S | T) ") * S) . s is set
dom (S | T) is set
f is set
(S | T) . f is set
dom S is set
(dom S) /\ T is set
dom ((S | T) ") is set
((S | T) ") . s is set
S . (((S | T) ") . s) is set
S . f is set
S is set
T is set
s is set
{T,s} is non empty set
[:S,{T,s}:] is Relation-like set
bool [:S,{T,s}:] is non empty set
{T} is non empty set
{s} is non empty set
t is Relation-like S -defined {T,s} -valued Function-like V26(S) quasi_total Element of bool [:S,{T,s}:]
t " {T} is Element of bool S
bool S is non empty set
t " {s} is Element of bool S
(t " {T}) \/ (t " {s}) is Element of bool S
t " {T,s} is Element of bool S
{T} \/ {s} is non empty set
t " ({T} \/ {s}) is Element of bool S
S is non empty 1-sorted
the carrier of S is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
t is Element of the carrier of T
S --> t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
the carrier of S --> t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like constant V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
{t} is non empty set
[: the carrier of S,{t}:] is non empty Relation-like set
s is Element of the carrier of S
(S --> t) . s is Element of the carrier of T
S is non empty TopStruct
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of the carrier of S
{T} is non empty set
Sspace T is non empty strict SubSpace of S
s is Element of bool the carrier of S
S | s is strict SubSpace of S
the carrier of (Sspace T) is non empty set
[#] (S | s) is non proper Element of bool the carrier of (S | s)
the carrier of (S | s) is set
bool the carrier of (S | s) is non empty set
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
the topology of S is non empty open Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set
T is Element of bool the carrier of S
s is Element of bool the carrier of S
t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
Cl T is closed Element of bool the carrier of S
Cl t is closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
Cl s is closed Element of bool the carrier of S
Cl f is closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
{0,1} is non empty V192() V193() V194() V195() V196() V197() set
1TopSp {0,1} is non empty strict TopSpace-like V156() TopStruct
the carrier of (1TopSp {0,1}) is non empty set
{0} is non empty functional V192() V193() V194() V195() V196() V197() set
{1} is non empty V192() V193() V194() V195() V196() V197() set
t is non empty TopSpace-like TopStruct
the carrier of t is non empty set
[: the carrier of t, the carrier of (1TopSp {0,1}):] is non empty Relation-like set
bool [: the carrier of t, the carrier of (1TopSp {0,1}):] is non empty set
bool the carrier of (1TopSp {0,1}) is non empty set
[#] t is non empty non proper open closed Element of bool the carrier of t
bool the carrier of t is non empty set
P is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]
f is non empty open Element of bool the carrier of (1TopSp {0,1})
P " f is Element of bool the carrier of t
f is non empty open Element of bool the carrier of (1TopSp {0,1})
P " f is Element of bool the carrier of t
rng P is non empty Element of bool the carrier of (1TopSp {0,1})
{} t is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t
(P " f) \/ (P " f) is Element of bool the carrier of t
[#] (1TopSp {0,1}) is non empty non proper open closed Element of bool the carrier of (1TopSp {0,1})
c₁₁ is Element of the carrier of (1TopSp {0,1})
P is Element of the carrier of (1TopSp {0,1})
{} t is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t
x2 is Element of bool the carrier of t
ls1 is Element of bool the carrier of t
x2 \/ ls1 is Element of bool the carrier of t
ls2 is set
ls2 is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]
a1 is non empty Relation-like the carrier of t -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of t) quasi_total Element of bool [: the carrier of t, the carrier of (1TopSp {0,1}):]
dom a1 is non empty Element of bool the carrier of t
f is non empty open Element of bool the carrier of (1TopSp {0,1})
a1 " f is Element of bool the carrier of t
a2 is set
a1 . a2 is set
a2 is set
a1 . a2 is set
f is non empty open Element of bool the carrier of (1TopSp {0,1})
a1 " f is Element of bool the carrier of t
a2 is set
a1 . a2 is set
a2 is set
a1 . a2 is set
rng a1 is non empty Element of bool the carrier of (1TopSp {0,1})
a2 is set
P2 is set
a1 . P2 is set
P2 is set
a1 . P2 is set
{} (1TopSp {0,1}) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of (1TopSp {0,1})
a1 " ({} (1TopSp {0,1})) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of t
[#] (1TopSp {0,1}) is non empty non proper open closed Element of bool the carrier of (1TopSp {0,1})
a1 " ([#] (1TopSp {0,1})) is Element of bool the carrier of t
a2 is Element of bool the carrier of (1TopSp {0,1})
a1 " a2 is Element of bool the carrier of t
S is TopStruct
the carrier of S is set
bool the carrier of S is non empty set
[#] S is non proper Element of bool the carrier of S
T is Element of bool the carrier of S
{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S
s is empty trivial V45() {} -element T_0 T_1 T_2 TopStruct
the carrier of s is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V30() V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() set
t is Element of bool the carrier of S
T \/ t is Element of bool the carrier of S
S is TopSpace-like TopStruct
the carrier of S is set
the topology of S is non empty open Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
[#] S is non proper open closed Element of bool the carrier of S
s is Element of bool the carrier of S
t is Element of bool the carrier of S
s \/ t is Element of bool the carrier of S
{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set
[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
f \/ f is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
{} TopStruct(# the carrier of S, the topology of S #) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
S is TopSpace-like connected TopStruct
the carrier of S is set
the topology of S is non empty open Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set
[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
s is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
s \/ t is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
{} TopStruct(# the carrier of S, the topology of S #) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
[#] S is non proper open closed Element of bool the carrier of S
f is Element of bool the carrier of S
f is Element of bool the carrier of S
f \/ f is Element of bool the carrier of S
{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of T
f is Element of the carrier of T
s " is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is non empty Relation-like set
bool [: the carrier of T, the carrier of S:] is non empty set
(s ") . t is Element of the carrier of S
(s ") . f is Element of the carrier of S
[: the carrier of I[01], the carrier of S:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of S:] is non empty set
f is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total Element of 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 non empty Relation-like set
bool [: the carrier of I[01], the carrier of T:] is non empty set
s * f is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
P . 0 is set
P . 1 is set
rng s is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
[#] T is non empty non proper open closed Element of bool the carrier of T
s . ((s ") . t) is Element of the carrier of T
s * (s ") is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
(s * (s ")) . t is Element of the carrier of T
id T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total continuous V247(T,T) Element of bool [: the carrier of T, the carrier of T:]
id the carrier of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
(id T) . t is Element of the carrier of T
s . ((s ") . f) is Element of the carrier of T
(s * (s ")) . f is Element of the carrier of T
(id T) . f is Element of the carrier of T
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is Element of the carrier of S
s is Element of the carrier of S
[: the carrier of I[01], the carrier of S:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of S:] is non empty set
I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of S:]
the carrier of I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like constant V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of S:]
{T} is non empty set
[: the carrier of I[01],{T}:] is non empty Relation-like set
t is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of S:]
t . 0 is set
t . 1 is set
S is TopSpace-like SubSpace of TOP-REAL 2
the carrier of S is set
s is Element of the carrier of S
t is Element of the carrier of S
T is non empty compact being_simple_closed_curve Element of bool the carrier of (TOP-REAL 2)
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
{f,f} is non empty set
P is non empty Element of bool the carrier of (TOP-REAL 2)
c₁₁ is non empty Element of bool the carrier of (TOP-REAL 2)
P \/ c₁₁ is non empty Element of bool the carrier of (TOP-REAL 2)
P /\ c₁₁ is Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
[: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):] is non empty set
x2 is non empty Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of ((TOP-REAL 2) | P):]
x2 . 0 is set
x2 . 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 non empty set
ls1 is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of S:]
ls1 . 0 is set
ls1 . 1 is set
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
P is non empty TopSpace-like SubSpace of TOP-REAL 2
the carrier of P is non empty 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 non empty set
c₁₁ is Element of the carrier of P
I[01] --> c₁₁ is non empty Relation-like the carrier of I[01] -defined the carrier of P -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of P:]
[: the carrier of I[01], the carrier of P:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of P:] is non empty set
the carrier of I[01] --> c₁₁ is non empty Relation-like the carrier of I[01] -defined the carrier of P -valued Function-like constant V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of P:]
{c₁₁} is non empty set
[: the carrier of I[01],{c₁₁}:] is non empty Relation-like set
x2 is Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of I[01], the carrier of S:]
x2 . 0 is set
x2 . 1 is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
x2 . j0 is Element of the carrier of S
j1 is V11() V12() ext-real Element of the carrier of I[01]
x2 . j1 is Element of the carrier of S
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
f is V37(2) V113() V184() Element of the carrier of (TOP-REAL 2)
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
{ the carrier of S} is non empty set
bool the carrier of S is non empty Element of bool (bool the carrier of S)
s is set
s is Element of bool (bool the carrier of S)
union s is Element of bool the carrier of S
t is Element of bool the carrier of S
[#] S is non proper open closed Element of bool the carrier of S
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
{} S is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of S
{({} S)} is non empty functional set
bool the carrier of S is non empty Element of bool (bool the carrier of S)
s is set
s is Element of bool (bool the carrier of S)
t is Element of bool the carrier of S
t is Element of bool the carrier of S
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
T is open mutually-disjoint Element of bool (bool the carrier of S)
s is Element of bool the carrier of S
t is set
S | s is strict TopSpace-like SubSpace of S
f is set
union T is Element of bool the carrier of S
f is set
P is set
{ (b₁ /\ s) where b₁ is Element of bool the carrier of S : ( b₁ in T & not f in b₁ ) } is set
bool s is non empty Element of bool (bool s)
bool s is non empty set
bool (bool s) is non empty set
x2 is set
ls1 is Element of bool the carrier of S
ls1 /\ s is Element of bool the carrier of S
the carrier of (S | s) is set
bool the carrier of (S | s) is non empty set
bool (bool the carrier of (S | s)) is non empty set
t /\ s is Element of bool the carrier of S
x2 is Element of bool (bool the carrier of (S | s))
union x2 is Element of bool the carrier of (S | s)
{ (b₁ /\ s) where b₁ is Element of bool the carrier of S : ( b₁ in T & f in b₁ ) } is set
ls2 is set
a1 is Element of bool the carrier of S
a1 /\ s is Element of bool the carrier of S
ls2 is Element of bool (bool the carrier of (S | s))
union ls2 is Element of bool the carrier of (S | s)
(union ls2) \/ (union x2) is Element of bool the carrier of (S | s)
a1 is set
a2 is set
P2 is Element of bool the carrier of S
P2 /\ s is Element of bool the carrier of S
P /\ s is Element of bool the carrier of S
[#] (S | s) is non proper open closed Element of bool the carrier of (S | s)
a1 is Element of bool the carrier of (S | s)
a2 is Element of bool the carrier of S
a2 /\ s is Element of bool the carrier of S
a1 is Element of bool the carrier of (S | s)
a2 is Element of bool the carrier of S
a2 /\ s is Element of bool the carrier of S
{} (S | s) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional open closed compact V192() V193() V194() V195() V196() V197() V198() Function-yielding V258() Element of bool the carrier of (S | s)
a1 is set
a2 is set
P2 is Element of bool the carrier of S
P2 /\ s is Element of bool the carrier of S
P1 is set
M is Element of bool the carrier of S
M /\ s is Element of bool the carrier of S
S is TopSpace-like TopStruct
T is TopSpace-like TopStruct
[:S,T:] is strict TopSpace-like TopStruct
the carrier of [:S,T:] is set
the topology of [:S,T:] is non empty open Element of bool (bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
bool (bool the carrier of [:S,T:]) is non empty set
TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct
the carrier of S is set
the topology of S is non empty open Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
the carrier of T is set
the topology of T is non empty open Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
[: the carrier of S, the carrier of T:] is Relation-like set
the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is set
bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is non empty set
s is Element of bool the carrier of [:S,T:]
t is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
f is Element of bool (bool the carrier of [:S,T:])
union f is Element of bool the carrier of [:S,T:]
bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]) is non empty set
f is Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):])
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set
the carrier of TopStruct(# the carrier of T, the topology of T #) is set
bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
P is set
c₁₁ is Element of bool the carrier of S
x2 is Element of bool the carrier of T
[:c₁₁,x2:] is Relation-like Element of bool the carrier of [:S,T:]
ls2 is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
ls1 is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)
[:ls2,ls1:] is Relation-like Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
f is Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):])
union f is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
f is Element of bool (bool the carrier of [:S,T:])
P is set
c₁₁ is Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
x2 is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)
[:c₁₁,x2:] is Relation-like Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
ls2 is Element of bool the carrier of S
ls1 is Element of bool the carrier of T
[:ls2,ls1:] is Relation-like Element of bool the carrier of [:S,T:]
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
[:S,T:] is strict TopSpace-like TopStruct
s is Element of bool the carrier of S
Cl s is closed Element of bool the carrier of S
t is Element of bool the carrier of T
[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
Cl [:s,t:] is closed Element of bool the carrier of [:S,T:]
Cl t is closed Element of bool the carrier of T
[:(Cl s),(Cl t):] is Relation-like Element of bool the carrier of [:S,T:]
f is set
f is non empty TopSpace-like TopStruct
P is non empty TopSpace-like TopStruct
[:f,P:] is non empty strict TopSpace-like TopStruct
the carrier of [:f,P:] is non empty set
c₁₁ is Element of the carrier of [:f,P:]
bool the carrier of [:f,P:] is non empty set
bool (bool the carrier of [:f,P:]) is non empty set
x2 is open V218([:f,P:],c₁₁) Element of bool (bool the carrier of [:f,P:])
the carrier of f is non empty set
the carrier of P is non empty set
ls1 is Element of the carrier of f
ls2 is Element of the carrier of P
[ls1,ls2] is Element of the carrier of [:f,P:]
{ls1,ls2} is non empty set
{ls1} is non empty set
{{ls1,ls2},{ls1}} is non empty set
bool the carrier of P is non empty set
a1 is Element of bool the carrier of P
[#] f is non empty non proper open closed Element of bool the carrier of f
bool the carrier of f is non empty set
[:([#] f),a1:] is Relation-like Element of bool the carrier of [:f,P:]
a2 is Element of bool the carrier of [:f,P:]
P2 is set
[:s,t:] /\ [:([#] f),a1:] is Relation-like Element of bool the carrier of [:f,P:]
s /\ ([#] f) is Element of bool the carrier of f
t /\ a1 is Element of bool the carrier of P
[:(s /\ ([#] f)),(t /\ a1):] is Relation-like Element of bool the carrier of [:f,P:]
P1 is set
M is set
[P1,M] is set
{P1,M} is non empty set
{P1} is non empty set
{{P1,M},{P1}} is non empty set
bool the carrier of f is non empty set
a1 is Element of bool the carrier of f
[#] P is non empty non proper open closed Element of bool the carrier of P
[:a1,([#] P):] is Relation-like Element of bool the carrier of [:f,P:]
a2 is Element of bool the carrier of [:f,P:]
P2 is set
[:s,t:] /\ [:a1,([#] P):] is Relation-like Element of bool the carrier of [:f,P:]
s /\ a1 is Element of bool the carrier of f
t /\ ([#] P) is Element of bool the carrier of P
[:(s /\ a1),(t /\ ([#] P)):] is Relation-like Element of bool the carrier of [:f,P:]
P1 is set
M is set
[P1,M] is set
{P1,M} is non empty set
{P1} is non empty set
{{P1,M},{P1}} is non empty set
f is set
f is set
P is set
[f,P] is set
{f,P} is non empty set
{f} is non empty set
{{f,P},{f}} is non empty set
c₁₁ is non empty TopSpace-like TopStruct
the carrier of c₁₁ is non empty set
ls1 is Element of the carrier of c₁₁
bool the carrier of c₁₁ is non empty set
bool (bool the carrier of c₁₁) is non empty set
ls2 is open V218(c₁₁,ls1) Element of bool (bool the carrier of c₁₁)
x2 is non empty TopSpace-like TopStruct
the carrier of x2 is non empty set
a1 is Element of the carrier of x2
bool the carrier of x2 is non empty set
bool (bool the carrier of x2) is non empty set
a2 is open V218(x2,a1) Element of bool (bool the carrier of x2)
[:c₁₁,x2:] is non empty strict TopSpace-like TopStruct
the carrier of [:c₁₁,x2:] is non empty set
bool the carrier of [:c₁₁,x2:] is non empty set
[ls1,a1] is Element of the carrier of [:c₁₁,x2:]
{ls1,a1} is non empty set
{ls1} is non empty set
{{ls1,a1},{ls1}} is non empty set
P2 is Element of bool the carrier of [:c₁₁,x2:]
bool (bool the carrier of [:c₁₁,x2:]) is non empty set
P1 is Element of bool (bool the carrier of [:c₁₁,x2:])
union P1 is Element of bool the carrier of [:c₁₁,x2:]
M is set
x0 is Element of bool the carrier of c₁₁
x1 is Element of bool the carrier of x2
[:x0,x1:] is Relation-like Element of bool the carrier of [:c₁₁,x2:]
S is Element of bool the carrier of x2
T is set
Y1 is Element of bool the carrier of c₁₁
h is set
[h,T] is set
{h,T} is non empty set
{h} is non empty set
{{h,T},{h}} is non empty set
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
[:S,T:] is strict TopSpace-like TopStruct
s is closed Element of bool the carrier of S
t is closed Element of bool the carrier of T
[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
Cl s is closed Element of bool the carrier of S
Cl [:s,t:] is closed Element of bool the carrier of [:S,T:]
Cl t is closed Element of bool the carrier of T
[:(Cl s),(Cl t):] is Relation-like Element of bool the carrier of [:S,T:]
S is TopSpace-like connected TopStruct
T is TopSpace-like connected TopStruct
[:S,T:] is strict TopSpace-like TopStruct
the carrier of S is set
the topology of S is non empty open Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like connected TopStruct
the carrier of T is set
the topology of T is non empty open Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like connected TopStruct
the carrier of [:S,T:] is set
the topology of [:S,T:] is non empty open Element of bool (bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
bool (bool the carrier of [:S,T:]) is non empty set
TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is set
[: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):] is Relation-like set
bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):] is non empty set
f is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]) quasi_total Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]
rng f is Element of bool the carrier of (1TopSp {0,1})
bool the carrier of (1TopSp {0,1}) is non empty set
dom f is Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is non empty set
P is Element of the carrier of (1TopSp {0,1})
x2 is set
f . x2 is set
c₁₁ is Element of the carrier of (1TopSp {0,1})
ls1 is set
f . ls1 is set
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
the carrier of TopStruct(# the carrier of T, the topology of T #) is set
[: the carrier of TopStruct(# the carrier of S, the topology of S #), the carrier of TopStruct(# the carrier of T, the topology of T #):] is Relation-like set
ls2 is set
a1 is set
[ls2,a1] is set
{ls2,a1} is non empty set
{ls2} is non empty set
{{ls2,a1},{ls2}} is non empty set
a2 is set
P2 is set
[a2,P2] is set
{a2,P2} is non empty set
{a2} is non empty set
{{a2,P2},{a2}} is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
M is Element of the carrier of TopStruct(# the carrier of T, the topology of T #)
{M} is non empty set
S is non empty TopSpace-like TopStruct
[#] S is non empty non proper open closed Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is non empty set
Y1 is non empty Element of bool the carrier of T
[:([#] S),Y1:] is non empty Relation-like Element of bool the carrier of [:S,T:]
[:S,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
f | [:([#] S),Y1:] is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined [:([#] S),Y1:] -defined the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]
dom (f | [:([#] S),Y1:]) is Relation-like [#] S -defined Y1 -valued Element of bool [:([#] S),Y1:]
bool [:([#] S),Y1:] is non empty set
T | Y1 is non empty strict TopSpace-like SubSpace of T
[:S,(T | Y1):] is non empty strict TopSpace-like TopStruct
the carrier of [:S,(T | Y1):] is non empty set
the carrier of (T | Y1) is non empty set
[: the carrier of S, the carrier of (T | Y1):] is non empty Relation-like set
rng (f | [:([#] S),Y1:]) is Element of bool the carrier of (1TopSp {0,1})
[: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):] is non empty Relation-like set
bool [: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):] is non empty set
[:(T | Y1),S:] is non empty strict TopSpace-like TopStruct
S | ([#] S) is non empty strict TopSpace-like SubSpace of S
[:(S | ([#] S)),(T | Y1):] is non empty strict TopSpace-like TopStruct
[:S,T:] | [:([#] S),Y1:] is non empty strict TopSpace-like SubSpace of [:S,T:]
h is non empty Relation-like the carrier of [:S,(T | Y1):] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:S,(T | Y1):]) quasi_total Element of bool [: the carrier of [:S,(T | Y1):], the carrier of (1TopSp {0,1}):]
x0 is Element of the carrier of TopStruct(# the carrier of S, the topology of S #)
[x0,M] is set
{x0,M} is non empty set
{x0} is non empty set
{{x0,M},{x0}} is non empty set
f . [x0,M] is set
rng h is non empty Element of bool the carrier of (1TopSp {0,1})
X0 is set
x1 is Element of the carrier of TopStruct(# the carrier of S, the topology of S #)
[x1,M] is set
{x1,M} is non empty set
{x1} is non empty set
{{x1,M},{x1}} is non empty set
dom h is non empty Element of bool the carrier of [:S,(T | Y1):]
bool the carrier of [:S,(T | Y1):] is non empty set
h . [x1,M] is set
dom h is non empty Element of bool the carrier of [:S,(T | Y1):]
bool the carrier of [:S,(T | Y1):] is non empty set
h . [x0,M] is set
X0 is non empty Element of bool the carrier of S
[#] T is non empty non proper open closed Element of bool the carrier of T
[:X0,([#] T):] is non empty Relation-like Element of bool the carrier of [:S,T:]
f | [:X0,([#] T):] is Relation-like the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined [:X0,([#] T):] -defined the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] -defined the carrier of (1TopSp {0,1}) -valued Function-like Element of bool [: the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):], the carrier of (1TopSp {0,1}):]
dom (f | [:X0,([#] T):]) is Relation-like X0 -defined [#] T -valued Element of bool [:X0,([#] T):]
bool [:X0,([#] T):] is non empty set
S | X0 is non empty strict TopSpace-like SubSpace of S
[:(S | X0),T:] is non empty strict TopSpace-like TopStruct
the carrier of [:(S | X0),T:] is non empty set
the carrier of (S | X0) is non empty set
[: the carrier of (S | X0), the carrier of T:] is non empty Relation-like set
rng (f | [:X0,([#] T):]) is Element of bool the carrier of (1TopSp {0,1})
[: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):] is non empty Relation-like set
bool [: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):] is non empty set
T | ([#] T) is non empty strict TopSpace-like SubSpace of T
[:(S | X0),(T | ([#] T)):] is non empty strict TopSpace-like TopStruct
[:S,T:] | [:X0,([#] T):] is non empty strict TopSpace-like SubSpace of [:S,T:]
g is non empty Relation-like the carrier of [:(S | X0),T:] -defined the carrier of (1TopSp {0,1}) -valued Function-like V26( the carrier of [:(S | X0),T:]) quasi_total Element of bool [: the carrier of [:(S | X0),T:], the carrier of (1TopSp {0,1}):]
rng g is non empty Element of bool the carrier of (1TopSp {0,1})
y is set
P1 is Element of the carrier of TopStruct(# the carrier of T, the topology of T #)
[x0,P1] is set
{x0,P1} is non empty set
{{x0,P1},{x0}} is non empty set
dom g is non empty Element of bool the carrier of [:(S | X0),T:]
bool the carrier of [:(S | X0),T:] is non empty set
g . [x0,P1] is set
dom g is non empty Element of bool the carrier of [:(S | X0),T:]
bool the carrier of [:(S | X0),T:] is non empty set
g . [x0,M] is set
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
[:S,T:] is strict TopSpace-like TopStruct
s is Element of bool the carrier of S
t is Element of bool the carrier of T
[:s,t:] is Relation-like Element of bool the carrier of [:S,T:]
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
S | s is strict TopSpace-like SubSpace of S
T | t is strict TopSpace-like SubSpace of T
f is TopSpace-like connected TopStruct
f is TopSpace-like connected TopStruct
[:f,f:] is strict TopSpace-like connected TopStruct
[:S,T:] | [:s,t:] is strict TopSpace-like SubSpace of [:S,T:]
S is TopSpace-like TopStruct
the carrier of S is set
bool the carrier of S is non empty set
T is TopSpace-like TopStruct
[:S,T:] is strict TopSpace-like TopStruct
the carrier of [:S,T:] is set
the carrier of T is set
s is non empty TopSpace-like TopStruct
the carrier of s is non empty set
[: the carrier of [:S,T:], the carrier of s:] is Relation-like set
bool [: the carrier of [:S,T:], the carrier of s:] is non empty set
t is Element of bool the carrier of S
S | t is strict TopSpace-like SubSpace of S
[:(S | t),T:] is strict TopSpace-like TopStruct
the carrier of [:(S | t),T:] is set
[: the carrier of [:(S | t),T:], the carrier of s:] is Relation-like set
bool [: the carrier of [:(S | t),T:], the carrier of s:] is non empty set
[:t, the carrier of T:] is Relation-like set
f is Relation-like the carrier of [:S,T:] -defined the carrier of s -valued Function-like V26( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of s:]
f | [:t, the carrier of T:] is Relation-like the carrier of [:S,T:] -defined [:t, the carrier of T:] -defined the carrier of [:S,T:] -defined the carrier of s -valued Function-like Element of bool [: the carrier of [:S,T:], the carrier of s:]
f is Relation-like the carrier of [:(S | t),T:] -defined the carrier of s -valued Function-like V26( the carrier of [:(S | t),T:]) quasi_total Element of bool [: the carrier of [:(S | t),T:], the carrier of s:]
the topology of T is non empty open Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct
[:(S | t),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
[#] TopStruct(# the carrier of T, the topology of T #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)
the carrier of TopStruct(# the carrier of T, the topology of T #) is set
bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
TopStruct(# the carrier of T, the topology of T #) | ([#] TopStruct(# the carrier of T, the topology of T #)) is strict TopSpace-like SubSpace of TopStruct(# the carrier of T, the topology of T #)
[:(S | t),(TopStruct(# the carrier of T, the topology of T #) | ([#] TopStruct(# the carrier of T, the topology of T #))):] is strict TopSpace-like TopStruct
[:S,TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
[:t,([#] TopStruct(# the carrier of T, the topology of T #)):] is Relation-like Element of bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):]
the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):] is set
bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):] is non empty set
[:S,TopStruct(# the carrier of T, the topology of T #):] | [:t,([#] TopStruct(# the carrier of T, the topology of T #)):] is strict TopSpace-like SubSpace of [:S,TopStruct(# the carrier of T, the topology of T #):]
the topology of [:S,T:] is non empty open Element of bool (bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
bool (bool the carrier of [:S,T:]) is non empty set
TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct
the topology of S is non empty open Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
the topology of [:S,TopStruct(# the carrier of T, the topology of T #):] is non empty open Element of bool (bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):])
bool (bool the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):]) is non empty set
TopStruct(# the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):], the topology of [:S,TopStruct(# the carrier of T, the topology of T #):] #) is strict TopSpace-like TopStruct
the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is set
the topology of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is non empty open Element of bool (bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):])
bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] is non empty set
bool (bool the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):]) is non empty set
TopStruct(# the carrier of [:(S | t),TopStruct(# the carrier of T, the topology of T #):], the topology of [:(S | t),TopStruct(# the carrier of T, the topology of T #):] #) is strict TopSpace-like TopStruct
the topology of [:(S | t),T:] is non empty open Element of bool (bool the carrier of [:(S | t),T:])
bool the carrier of [:(S | t),T:] is non empty set
bool (bool the carrier of [:(S | t),T:]) is non empty set
TopStruct(# the carrier of [:(S | t),T:], the topology of [:(S | t),T:] #) is strict TopSpace-like TopStruct
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
S is TopSpace-like TopStruct
[:S,T:] is strict TopSpace-like TopStruct
the carrier of [:S,T:] is set
the carrier of S is set
s is non empty TopSpace-like TopStruct
the carrier of s is non empty set
[: the carrier of [:S,T:], the carrier of s:] is Relation-like set
bool [: the carrier of [:S,T:], the carrier of s:] is non empty set
t is Element of bool the carrier of T
T | t is strict TopSpace-like SubSpace of T
[:S,(T | t):] is strict TopSpace-like TopStruct
the carrier of [:S,(T | t):] is set
[: the carrier of [:S,(T | t):], the carrier of s:] is Relation-like set
bool [: the carrier of [:S,(T | t):], the carrier of s:] is non empty set
[: the carrier of S,t:] is Relation-like set
f is Relation-like the carrier of [:S,T:] -defined the carrier of s -valued Function-like V26( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of s:]
f | [: the carrier of S,t:] is Relation-like the carrier of [:S,T:] -defined [: the carrier of S,t:] -defined the carrier of [:S,T:] -defined the carrier of s -valued Function-like Element of bool [: the carrier of [:S,T:], the carrier of s:]
f is Relation-like the carrier of [:S,(T | t):] -defined the carrier of s -valued Function-like V26( the carrier of [:S,(T | t):]) quasi_total Element of bool [: the carrier of [:S,(T | t):], the carrier of s:]
the topology of S is non empty open Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),(T | t):] is strict TopSpace-like TopStruct
[#] TopStruct(# the carrier of S, the topology of S #) is non proper open closed Element of bool the carrier of TopStruct(# the carrier of S, the topology of S #)
the carrier of TopStruct(# the carrier of S, the topology of S #) is set
bool the carrier of TopStruct(# the carrier of S, the topology of S #) is non empty set
TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #)) is strict TopSpace-like SubSpace of TopStruct(# the carrier of S, the topology of S #)
[:(TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #))),(T | t):] is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),T:] is strict TopSpace-like TopStruct
[:([#] TopStruct(# the carrier of S, the topology of S #)),t:] is Relation-like Element of bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:]
the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:] is set
bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:] is non empty set
[:TopStruct(# the carrier of S, the topology of S #),T:] | [:([#] TopStruct(# the carrier of S, the topology of S #)),t:] is strict TopSpace-like SubSpace of [:TopStruct(# the carrier of S, the topology of S #),T:]
the topology of [:S,T:] is non empty open Element of bool (bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
bool (bool the carrier of [:S,T:]) is non empty set
TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) is strict TopSpace-like TopStruct
the topology of T is non empty open Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopSpace-like TopStruct
[:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] is strict TopSpace-like TopStruct
the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] is non empty open Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:])
bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:]) is non empty set
TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:], the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] #) is strict TopSpace-like TopStruct
the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is set
the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is non empty open Element of bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):])
bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] is non empty set
bool (bool the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):]) is non empty set
TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | t):], the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | t):] #) is strict TopSpace-like TopStruct
the topology of [:S,(T | t):] is non empty open Element of bool (bool the carrier of [:S,(T | t):])
bool the carrier of [:S,(T | t):] is non empty set
bool (bool the carrier of [:S,(T | t):]) is non empty set
TopStruct(# the carrier of [:S,(T | t):], the topology of [:S,(T | t):] #) is strict TopSpace-like TopStruct
f is non empty TopSpace-like TopStruct
s is non empty TopSpace-like TopStruct
[:f,s:] is non empty strict TopSpace-like TopStruct
the carrier of [:f,s:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:f,s:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:f,s:], the carrier of S:] is non empty set
t is non empty TopSpace-like TopStruct
[:f,t:] is non empty strict TopSpace-like TopStruct
the carrier of [:f,t:] is non empty set
[: the carrier of [:f,t:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:f,t:], the carrier of S:] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[#] s is non empty non proper open closed Element of bool the carrier of s
the carrier of s is non empty set
bool the carrier of s is non empty set
[#] t is non empty non proper open closed Element of bool the carrier of t
the carrier of t is non empty set
bool the carrier of t is non empty set
([#] s) \/ ([#] t) is non empty set
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] [:f,s:] is non empty non proper open closed Element of bool the carrier of [:f,s:]
bool the carrier of [:f,s:] is non empty set
[#] [:f,t:] is non empty non proper open closed Element of bool the carrier of [:f,t:]
bool the carrier of [:f,t:] is non empty set
([#] [:f,s:]) /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]
[:f,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:f,T:] is non empty set
[: the carrier of [:f,T:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:f,T:], the carrier of S:] is non empty set
f is non empty Relation-like the carrier of [:f,s:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,s:]) quasi_total Element of bool [: the carrier of [:f,s:], the carrier of S:]
P is non empty Relation-like the carrier of [:f,t:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,t:]) quasi_total Element of bool [: the carrier of [:f,t:], the carrier of S:]
f +* P is Relation-like Function-like set
c₁₁ is closed Element of bool the carrier of T
x2 is closed Element of bool the carrier of T
dom f is non empty Element of bool the carrier of [:f,s:]
the carrier of f is non empty set
[: the carrier of f, the carrier of t:] is non empty Relation-like set
rng (f +* P) is set
rng f is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
rng P is non empty Element of bool the carrier of S
(rng f) \/ (rng P) is non empty Element of bool the carrier of S
dom P is non empty Element of bool the carrier of [:f,t:]
dom (f +* P) is set
(dom f) \/ (dom P) is non empty set
[: the carrier of f, the carrier of s:] is non empty Relation-like set
[: the carrier of f, the carrier of T:] is non empty Relation-like set
ls2 is non empty Relation-like the carrier of [:f,T:] -defined the carrier of S -valued Function-like V26( the carrier of [:f,T:]) quasi_total Element of bool [: the carrier of [:f,T:], the carrier of S:]
bool the carrier of [:f,T:] is non empty set
[#] f is non empty non proper open closed Element of bool the carrier of f
bool the carrier of f is non empty set
[:([#] f),c₁₁:] is Relation-like Element of bool the carrier of [:f,T:]
a2 is Element of bool the carrier of S
ls2 " a2 is Element of bool the carrier of [:f,T:]
P2 is set
(ls2 " a2) /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]
P " a2 is Element of bool the carrier of [:f,t:]
ls2 . P2 is set
P . P2 is set
P . P2 is set
ls2 . P2 is set
dom ls2 is non empty Element of bool the carrier of [:f,T:]
P2 is set
ls2 . P2 is set
f . P2 is set
P . P2 is set
P2 is set
(ls2 " a2) /\ ([#] [:f,s:]) is Element of bool the carrier of [:f,s:]
f " a2 is Element of bool the carrier of [:f,s:]
ls2 . P2 is set
f . P2 is set
f . P2 is set
ls2 . P2 is set
[#] [:f,T:] is non empty non proper open closed Element of bool the carrier of [:f,T:]
([#] [:f,s:]) \/ ([#] [:f,t:]) is non empty set
(ls2 " a2) /\ (([#] [:f,s:]) \/ ([#] [:f,t:])) is Element of bool the carrier of [:f,T:]
((ls2 " a2) /\ ([#] [:f,s:])) \/ ((ls2 " a2) /\ ([#] [:f,t:])) is set
(f " a2) \/ (P " a2) is set
a1 is Element of bool the carrier of [:f,T:]
P1 is Element of bool the carrier of [:f,T:]
M is Element of bool the carrier of [:f,T:]
M /\ ([#] [:f,s:]) is Element of bool the carrier of [:f,s:]
[:([#] f),x2:] is Relation-like Element of bool the carrier of [:f,T:]
M is Element of bool the carrier of [:f,T:]
P2 is Element of bool the carrier of [:f,T:]
x0 is Element of bool the carrier of [:f,T:]
x0 /\ ([#] [:f,t:]) is Element of bool the carrier of [:f,t:]
s is non empty TopSpace-like TopStruct
f is non empty TopSpace-like TopStruct
[:s,f:] is non empty strict TopSpace-like TopStruct
the carrier of [:s,f:] is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of [:s,f:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:s,f:], the carrier of S:] is non empty set
t is non empty TopSpace-like TopStruct
[:t,f:] is non empty strict TopSpace-like TopStruct
the carrier of [:t,f:] is non empty set
[: the carrier of [:t,f:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:t,f:], the carrier of S:] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[#] s is non empty non proper open closed Element of bool the carrier of s
the carrier of s is non empty set
bool the carrier of s is non empty set
[#] t is non empty non proper open closed Element of bool the carrier of t
the carrier of t is non empty set
bool the carrier of t is non empty set
([#] s) \/ ([#] t) is non empty set
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] [:s,f:] is non empty non proper open closed Element of bool the carrier of [:s,f:]
bool the carrier of [:s,f:] is non empty set
[#] [:t,f:] is non empty non proper open closed Element of bool the carrier of [:t,f:]
bool the carrier of [:t,f:] is non empty set
([#] [:s,f:]) /\ ([#] [:t,f:]) is Element of bool the carrier of [:t,f:]
[:T,f:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,f:] is non empty set
[: the carrier of [:T,f:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:T,f:], the carrier of S:] is non empty set
f is non empty Relation-like the carrier of [:s,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:s,f:]) quasi_total Element of bool [: the carrier of [:s,f:], the carrier of S:]
P is non empty Relation-like the carrier of [:t,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:t,f:]) quasi_total Element of bool [: the carrier of [:t,f:], the carrier of S:]
f +* P is Relation-like Function-like set
c₁₁ is closed Element of bool the carrier of T
x2 is closed Element of bool the carrier of T
dom f is non empty Element of bool the carrier of [:s,f:]
the carrier of f is non empty set
[: the carrier of t, the carrier of f:] is non empty Relation-like set
dom (f +* P) is set
dom P is non empty Element of bool the carrier of [:t,f:]
(dom f) \/ (dom P) is non empty set
rng (f +* P) is set
rng f is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
rng P is non empty Element of bool the carrier of S
(rng f) \/ (rng P) is non empty Element of bool the carrier of S
[: the carrier of s, the carrier of f:] is non empty Relation-like set
[: the carrier of T, the carrier of f:] is non empty Relation-like set
ls2 is non empty Relation-like the carrier of [:T,f:] -defined the carrier of S -valued Function-like V26( the carrier of [:T,f:]) quasi_total Element of bool [: the carrier of [:T,f:], the carrier of S:]
bool the carrier of [:T,f:] is non empty set
[#] f is non empty non proper open closed Element of bool the carrier of f
bool the carrier of f is non empty set
[:c₁₁,([#] f):] is Relation-like Element of bool the carrier of [:T,f:]
a2 is Element of bool the carrier of S
ls2 " a2 is Element of bool the carrier of [:T,f:]
P2 is set
(ls2 " a2) /\ ([#] [:t,f:]) is Element of bool the carrier of [:t,f:]
P " a2 is Element of bool the carrier of [:t,f:]
ls2 . P2 is set
P . P2 is set
P . P2 is set
ls2 . P2 is set
dom ls2 is non empty Element of bool the carrier of [:T,f:]
P2 is set
ls2 . P2 is set
f . P2 is set
P . P2 is set
P2 is set
(ls2 " a2) /\ ([#] [:s,f:]) is Element of bool the carrier of [:s,f:]
f " a2 is Element of bool the carrier of [:s,f:]
ls2 . P2 is set
f . P2 is set
f . P2 is set
ls2 . P2 is set
[#] [:T,f:] is non empty non proper open closed Element of bool the carrier of [:T,f:]
([#] [:s,f:]) \/ ([#] [:t,f:]) is non empty set
(ls2 " a2) /\ (([#] [:s,f:]) \/ ([#] [:t,f:])) is Element of bool the carrier of [:T,f:]
((ls2 " a2) /\ ([#] [:s,f:])) \/ ((ls2 " a2) /\ ([#] [:t,f:])) is set
(f " a2) \/ (P " a2) is set
a1 is Element of bool the carrier of [:T,f:]
P1 is Element of bool the carrier of [:T,f:]
M is Element of bool the carrier of [:T,f:]
M /\ ([#] [:s,f:]) is Element of bool the carrier of [:s,f:]
[:x2,([#] f):] is Relation-like Element of bool the carrier of [:T,f:]
M is Element of bool the carrier of [:T,f:]
P2 is Element of bool the carrier of [:T,f:]
x0 is Element of bool the carrier of [:T,f:]
x0 /\ ([#] [:t,f:]) is Element of bool the carrier of [:t,f:]
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is Element of the carrier of S
s is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of T,T
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is Element of the carrier of S
s is V11() V12() ext-real Element of the carrier of I[01]
t is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like constant V26( the carrier of K527()) quasi_total continuous Path of T,T
t . s is Element of the carrier of S
I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total continuous Element of bool [: the carrier of I[01], the carrier of S:]
[: the carrier of I[01], the carrier of S:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of S:] is non empty set
the carrier of I[01] --> T is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like constant V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of S:]
{T} is non empty set
[: the carrier of I[01],{T}:] is non empty Relation-like set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is Element of the carrier of S
s is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of T,T
s . 0 is set
s . 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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
[: the carrier of I[01], the carrier of S:] is non empty Relation-like set
bool [: the carrier of I[01], the carrier of S:] is non empty set
f is non empty Relation-like the carrier of I[01] -defined the carrier of S -valued Function-like V26( the carrier of I[01]) quasi_total Element of 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 non empty Relation-like set
bool [: the carrier of I[01], the carrier of T:] is non empty set
s * f is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
P is non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V26( the carrier of I[01]) quasi_total Element of bool [: the carrier of I[01], the carrier of T:]
P . 0 is set
P . 1 is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
f . j0 is Element of the carrier of S
s . (f . j0) is Element of the carrier of T
j1 is V11() V12() ext-real Element of the carrier of I[01]
f . j1 is Element of the carrier of S
s . (f . j1) is Element of the carrier of T
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
s * f is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
(s * f) . 1 is set
j1 is V11() V12() ext-real Element of the carrier of I[01]
f . j1 is Element of the carrier of S
s . (f . j1) is Element of the carrier of T
(s * f) . 0 is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
f . j0 is Element of the carrier of S
s . (f . j0) is Element of the carrier of T
S is non empty TopSpace-like connected pathwise_connected TopStruct
the carrier of S is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,f
s * f is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total continuous Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
(s * f) . 1 is set
j1 is V11() V12() ext-real Element of the carrier of I[01]
f . j1 is Element of the carrier of S
s . (f . j1) is Element of the carrier of T
(s * f) . 0 is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
f . j0 is Element of the carrier of S
s . (f . j0) is Element of the carrier of T
S is non empty TopSpace-like connected pathwise_connected TopStruct
the carrier of S is non empty set
s is Element of the carrier of S
t is Element of the carrier of S
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,t
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
f * f is Relation-like the carrier of K527() -defined the carrier of T -valued Function-like set
f . s is Element of the carrier of T
f . t is Element of the carrier of T
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
s . t is Element of the carrier of T
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,t
s * f is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total continuous Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
(s * f) . 1 is set
j1 is V11() V12() ext-real Element of the carrier of I[01]
f . j1 is Element of the carrier of S
s . (f . j1) is Element of the carrier of T
(s * f) . 0 is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
f . j0 is Element of the carrier of S
s . (f . j0) is Element of the carrier of T
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
s is Element of the carrier of S
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
t is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t * f is Relation-like the carrier of K527() -defined the carrier of T -valued Function-like set
f . s is Element of the carrier of T
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
P is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
s * f is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
s * P is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P is non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P
[: the carrier of [:K527(),K527():], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:K527(),K527():], the carrier of T:] is non empty set
s * the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P is non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of T -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Element of bool [: the carrier of [:K527(),K527():], the carrier of T:]
ls2 is non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of T -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Element of bool [: the carrier of [:K527(),K527():], the carrier of T:]
a1 is V11() V12() ext-real Element of the carrier of I[01]
ls2 . (a1,0) is set
c₁₁ . a1 is Element of the carrier of T
ls2 . (a1,1) is set
x2 . a1 is Element of the carrier of T
ls2 . (0,a1) is set
ls2 . (1,a1) is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (a1,j0) is set
s . ( the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (a1,j0)) is set
f . a1 is Element of the carrier of S
s . (f . a1) is Element of the carrier of T
c₁₁ . a1 is Element of the carrier of T
j1 is V11() V12() ext-real Element of the carrier of I[01]
the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (a1,j1) is set
s . ( the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (a1,j1)) is set
P . a1 is Element of the carrier of S
s . (P . a1) is Element of the carrier of T
x2 . a1 is Element of the carrier of T
the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (j0,a1) is set
s . ( the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (j0,a1)) is set
the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (j1,a1) is set
s . ( the non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P . (j1,a1)) 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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
P is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
s * f is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
s * P is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
ls1 is non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of S -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Homotopy of f,P
s * ls1 is non empty Relation-like the carrier of [:K527(),K527():] -defined the carrier of T -valued Function-like V26( the carrier of [:K527(),K527():]) quasi_total Element of bool [: the carrier of [:K527(),K527():], the carrier of T:]
[: the carrier of [:K527(),K527():], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:K527(),K527():], the carrier of T:] is non empty set
a1 is V11() V12() ext-real Element of the carrier of I[01]
(s * ls1) . (a1,0) is set
c₁₁ . a1 is Element of the carrier of T
(s * ls1) . (a1,1) is set
x2 . a1 is Element of the carrier of T
(s * ls1) . (0,a1) is set
(s * ls1) . (1,a1) is set
j0 is V11() V12() ext-real Element of the carrier of I[01]
ls1 . (a1,j0) is set
s . (ls1 . (a1,j0)) is set
f . a1 is Element of the carrier of S
s . (f . a1) is Element of the carrier of T
c₁₁ . a1 is Element of the carrier of T
j1 is V11() V12() ext-real Element of the carrier of I[01]
ls1 . (a1,j1) is set
s . (ls1 . (a1,j1)) is set
P . a1 is Element of the carrier of S
s . (P . a1) is Element of the carrier of T
x2 . a1 is Element of the carrier of T
ls1 . (j0,a1) is set
s . (ls1 . (j0,a1)) is set
ls1 . (j1,a1) is set
s . (ls1 . (j1,a1)) 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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t is Element of the carrier of S
f is Element of the carrier of S
f is Element of the carrier of S
s . t is Element of the carrier of T
s . f is Element of the carrier of T
s . f is Element of the carrier of T
P is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
s * P is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of f,f
s * c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
P + c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f
s * (P + c₁₁) is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
ls1 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . f,s . f
x2 + ls1 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of s . t,s . f
ls2 is V11() V12() ext-real Element of the carrier of I[01]
(x2 + ls1) . ls2 is Element of the carrier of T
(s * (P + c₁₁)) . ls2 is Element of the carrier of T
1 / 2 is V11() V12() ext-real set
2 * ls2 is V11() V12() ext-real set
x2 . (2 * ls2) is set
P . (2 * ls2) is set
s . (P . (2 * ls2)) is set
(P + c₁₁) . ls2 is Element of the carrier of S
s . ((P + c₁₁) . ls2) is Element of the carrier of T
1 / 2 is V11() V12() ext-real set
2 * ls2 is V11() V12() ext-real set
(2 * ls2) - 1 is V11() V12() ext-real set
ls1 . ((2 * ls2) - 1) is set
c₁₁ . ((2 * ls2) - 1) is set
s . (c₁₁ . ((2 * ls2) - 1)) is set
(P + c₁₁) . ls2 is Element of the carrier of S
s . ((P + c₁₁) . ls2) is Element of the carrier of T
1 / 2 is V11() V12() ext-real 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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
s is Element of the carrier of S
t . s is Element of the carrier of T
FundamentalGroup (T,(t . s)) is non empty strict V260() V261() L9()
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (S,s)) is non empty set
the carrier of (FundamentalGroup (T,(t . s))) is non empty set
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty set
Loops s is non empty set
Paths (s,s) is non empty set
EqRel (S,s) is non empty Relation-like Loops s -defined Loops s -valued V26( Loops s) quasi_total V240() V245() Element of bool [:(Loops s),(Loops s):]
[:(Loops s),(Loops s):] is non empty Relation-like set
bool [:(Loops s),(Loops s):] is non empty set
EqRel (S,s,s) is Relation-like Paths (s,s) -defined Paths (s,s) -valued Element of bool [:(Paths (s,s)),(Paths (s,s)):]
[:(Paths (s,s)),(Paths (s,s)):] is non empty Relation-like set
bool [:(Paths (s,s)),(Paths (s,s)):] is non empty set
Loops (t . s) is non empty set
Paths ((t . s),(t . s)) is non empty set
EqRel (T,(t . s)) is non empty Relation-like Loops (t . s) -defined Loops (t . s) -valued V26( Loops (t . s)) quasi_total V240() V245() Element of bool [:(Loops (t . s)),(Loops (t . s)):]
[:(Loops (t . s)),(Loops (t . s)):] is non empty Relation-like set
bool [:(Loops (t . s)),(Loops (t . s)):] is non empty set
EqRel (T,(t . s),(t . s)) is Relation-like Paths ((t . s),(t . s)) -defined Paths ((t . s),(t . s)) -valued Element of bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):]
[:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty Relation-like set
bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty set
P is Element of the carrier of (FundamentalGroup (S,s))
c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),c₁₁) is Element of bool (Loops s)
bool (Loops s) is non empty set
t * c₁₁ is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),x2) is Element of bool (Loops (t . s))
bool (Loops (t . s)) is non empty set
ls1 is Element of the carrier of (FundamentalGroup (T,(t . s)))
Class ((EqRel (T,(t . s))),(t * c₁₁)) is Element of bool (Loops (t . s))
P is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(t . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):]
P is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(t . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):]
c₁₁ is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(t . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):]
x2 is Element of the carrier of (FundamentalGroup (S,s))
P . x2 is Element of the carrier of (FundamentalGroup (T,(t . s)))
ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls1) is Element of bool (Loops s)
bool (Loops s) is non empty set
t * ls1 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
Class ((EqRel (T,(t . s))),(t * ls1)) is Element of bool (Loops (t . s))
bool (Loops (t . s)) is non empty set
c₁₁ . x2 is Element of the carrier of (FundamentalGroup (T,(t . s)))
ls2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls2) is Element of bool (Loops s)
t * ls2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
Class ((EqRel (T,(t . s))),(t * ls2)) is Element of bool (Loops (t . s))
a1 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t . s,t . s
a2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t . s,t . s
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is Element of the carrier of S
Loops s is non empty set
Paths (s,s) is non empty set
EqRel (S,s) is non empty Relation-like Loops s -defined Loops s -valued V26( Loops s) quasi_total V240() V245() Element of bool [:(Loops s),(Loops s):]
[:(Loops s),(Loops s):] is non empty Relation-like set
bool [:(Loops s),(Loops s):] is non empty set
EqRel (S,s,s) is Relation-like Paths (s,s) -defined Paths (s,s) -valued Element of bool [:(Paths (s,s)),(Paths (s,s)):]
[:(Paths (s,s)),(Paths (s,s)):] is non empty Relation-like set
bool [:(Paths (s,s)),(Paths (s,s)):] is non empty set
t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
(S,T,s,t) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(t . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):]
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (S,s)) is non empty set
t . s is Element of the carrier of T
FundamentalGroup (T,(t . s)) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (T,(t . s))) is non empty set
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty set
Loops (t . s) is non empty set
Paths ((t . s),(t . s)) is non empty set
EqRel (T,(t . s)) is non empty Relation-like Loops (t . s) -defined Loops (t . s) -valued V26( Loops (t . s)) quasi_total V240() V245() Element of bool [:(Loops (t . s)),(Loops (t . s)):]
[:(Loops (t . s)),(Loops (t . s)):] is non empty Relation-like set
bool [:(Loops (t . s)),(Loops (t . s)):] is non empty set
EqRel (T,(t . s),(t . s)) is Relation-like Paths ((t . s),(t . s)) -defined Paths ((t . s),(t . s)) -valued Element of bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):]
[:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty Relation-like set
bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty set
f is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),f) is Element of bool (Loops s)
bool (Loops s) is non empty set
(S,T,s,t) . (Class ((EqRel (S,s)),f)) is set
(S,T,s,f,t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),(S,T,s,f,t)) is Element of bool (Loops (t . s))
bool (Loops (t . s)) is non empty set
f is Element of the carrier of (FundamentalGroup (S,s))
(S,T,s,t) . f is Element of the carrier of (FundamentalGroup (T,(t . s)))
P is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),P) is Element of bool (Loops s)
(S,T,s,P,t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),(S,T,s,P,t)) is Element of bool (Loops (t . s))
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is Element of the carrier of S
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
t is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
t . s is Element of the carrier of T
FundamentalGroup (T,(t . s)) is non empty strict V260() V261() L9()
(S,T,s,t) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(t . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):]
the carrier of (FundamentalGroup (S,s)) is non empty set
the carrier of (FundamentalGroup (T,(t . s))) is non empty set
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(t . s))):] is non empty set
P is Element of the carrier of (FundamentalGroup (S,s))
c₁₁ is Element of the carrier of (FundamentalGroup (S,s))
P * c₁₁ is Element of the carrier of (FundamentalGroup (S,s))
(S,T,s,t) . (P * c₁₁) is Element of the carrier of (FundamentalGroup (T,(t . s)))
(S,T,s,t) . P is Element of the carrier of (FundamentalGroup (T,(t . s)))
(S,T,s,t) . c₁₁ is Element of the carrier of (FundamentalGroup (T,(t . s)))
((S,T,s,t) . P) * ((S,T,s,t) . c₁₁) is Element of the carrier of (FundamentalGroup (T,(t . s)))
Loops s is non empty set
Paths (s,s) is non empty set
EqRel (S,s) is non empty Relation-like Loops s -defined Loops s -valued V26( Loops s) quasi_total V240() V245() Element of bool [:(Loops s),(Loops s):]
[:(Loops s),(Loops s):] is non empty Relation-like set
bool [:(Loops s),(Loops s):] is non empty set
EqRel (S,s,s) is Relation-like Paths (s,s) -defined Paths (s,s) -valued Element of bool [:(Paths (s,s)),(Paths (s,s)):]
[:(Paths (s,s)),(Paths (s,s)):] is non empty Relation-like set
bool [:(Paths (s,s)),(Paths (s,s)):] is non empty set
Loops (t . s) is non empty set
Paths ((t . s),(t . s)) is non empty set
EqRel (T,(t . s)) is non empty Relation-like Loops (t . s) -defined Loops (t . s) -valued V26( Loops (t . s)) quasi_total V240() V245() Element of bool [:(Loops (t . s)),(Loops (t . s)):]
[:(Loops (t . s)),(Loops (t . s)):] is non empty Relation-like set
bool [:(Loops (t . s)),(Loops (t . s)):] is non empty set
EqRel (T,(t . s),(t . s)) is Relation-like Paths ((t . s),(t . s)) -defined Paths ((t . s),(t . s)) -valued Element of bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):]
[:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty Relation-like set
bool [:(Paths ((t . s),(t . s))),(Paths ((t . s),(t . s))):] is non empty set
x2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),x2) is Element of bool (Loops s)
bool (Loops s) is non empty set
(S,T,s,x2,t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),(S,T,s,x2,t)) is Element of bool (Loops (t . s))
bool (Loops (t . s)) is non empty set
ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls1) is Element of bool (Loops s)
(S,T,s,ls1,t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),(S,T,s,ls1,t)) is Element of bool (Loops (t . s))
(S,T,s,x2,t) + (S,T,s,ls1,t) is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t . s,t . s
x2 + ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
(S,T,s,(x2 + ls1),t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
ls2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls2) is Element of bool (Loops s)
(S,T,s,ls2,t) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of t . s,t . s
Class ((EqRel (T,(t . s))),(S,T,s,ls2,t)) is Element of bool (Loops (t . s))
Class ((EqRel (S,s)),(x2 + ls1)) is Element of bool (Loops s)
Class ((EqRel (T,(t . s))),((S,T,s,x2,t) + (S,T,s,ls1,t))) is Element of bool (Loops (t . s))
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is Element of the carrier of S
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (S,s)) is non empty set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
f . s is Element of the carrier of T
FundamentalGroup (T,(f . s)) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (T,(f . s))) is non empty set
(S,T,s,f) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(f . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total V264( FundamentalGroup (S,s), FundamentalGroup (T,(f . s))) multiplicative Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):]
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty set
f " is Relation-like Function-like set
(f ") . (f . s) is set
f " is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]
[: the carrier of T, the carrier of S:] is non empty Relation-like set
bool [: the carrier of T, the carrier of S:] is non empty set
rng f is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
[#] T is non empty non proper open closed Element of bool the carrier of T
dom (S,T,s,f) is non empty Element of bool the carrier of (FundamentalGroup (S,s))
bool the carrier of (FundamentalGroup (S,s)) is non empty set
rng (S,T,s,f) is non empty Element of bool the carrier of (FundamentalGroup (T,(f . s)))
bool the carrier of (FundamentalGroup (T,(f . s))) is non empty set
c₁₁ is set
Loops (f . s) is non empty set
Paths ((f . s),(f . s)) is non empty set
EqRel (T,(f . s)) is non empty Relation-like Loops (f . s) -defined Loops (f . s) -valued V26( Loops (f . s)) quasi_total V240() V245() Element of bool [:(Loops (f . s)),(Loops (f . s)):]
[:(Loops (f . s)),(Loops (f . s)):] is non empty Relation-like set
bool [:(Loops (f . s)),(Loops (f . s)):] is non empty set
EqRel (T,(f . s),(f . s)) is Relation-like Paths ((f . s),(f . s)) -defined Paths ((f . s),(f . s)) -valued Element of bool [:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):]
[:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):] is non empty Relation-like set
bool [:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):] is non empty set
x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of f . s,f . s
Class ((EqRel (T,(f . s))),x2) is Element of bool (Loops (f . s))
bool (Loops (f . s)) is non empty set
(f ") * x2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of S:]
[: the carrier of K527(), the carrier of S:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of S:] is non empty set
Loops s is non empty set
Paths (s,s) is non empty set
EqRel (S,s) is non empty Relation-like Loops s -defined Loops s -valued V26( Loops s) quasi_total V240() V245() Element of bool [:(Loops s),(Loops s):]
[:(Loops s),(Loops s):] is non empty Relation-like set
bool [:(Loops s),(Loops s):] is non empty set
EqRel (S,s,s) is Relation-like Paths (s,s) -defined Paths (s,s) -valued Element of bool [:(Paths (s,s)),(Paths (s,s)):]
[:(Paths (s,s)),(Paths (s,s)):] is non empty Relation-like set
bool [:(Paths (s,s)),(Paths (s,s)):] is non empty set
ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls1) is Element of bool (Loops s)
bool (Loops s) is non empty set
(S,T,s,f) . (Class ((EqRel (S,s)),ls1)) is set
a1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),a1) is Element of bool (Loops s)
(S,T,s,a1,f) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of f . s,f . s
Class ((EqRel (T,(f . s))),(S,T,s,a1,f)) is Element of bool (Loops (f . s))
(S,T,s,ls1,f) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of f . s,f . s
f * (f ") is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] is non empty Relation-like set
bool [: the carrier of T, the carrier of T:] is non empty set
(f * (f ")) * x2 is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of T:]
[: the carrier of K527(), the carrier of T:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of T:] is non empty set
id (rng f) is non empty Relation-like rng f -defined rng f -valued Function-like one-to-one V26( rng f) quasi_total Element of bool [:(rng f),(rng f):]
[:(rng f),(rng f):] is non empty Relation-like set
bool [:(rng f),(rng f):] is non empty set
(id (rng f)) * x2 is Relation-like the carrier of K527() -defined rng f -valued Function-like Element of bool [: the carrier of K527(),(rng f):]
[: the carrier of K527(),(rng f):] is non empty Relation-like set
bool [: the carrier of K527(),(rng f):] is non empty set
dom f is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
[#] S is non empty non proper open closed Element of bool the carrier of S
c₁₁ is set
dom (S,T,s,f) is non empty set
x2 is set
(S,T,s,f) . c₁₁ is set
(S,T,s,f) . x2 is set
Loops s is non empty set
Paths (s,s) is non empty set
EqRel (S,s) is non empty Relation-like Loops s -defined Loops s -valued V26( Loops s) quasi_total V240() V245() Element of bool [:(Loops s),(Loops s):]
[:(Loops s),(Loops s):] is non empty Relation-like set
bool [:(Loops s),(Loops s):] is non empty set
EqRel (S,s,s) is Relation-like Paths (s,s) -defined Paths (s,s) -valued Element of bool [:(Paths (s,s)),(Paths (s,s)):]
[:(Paths (s,s)),(Paths (s,s)):] is non empty Relation-like set
bool [:(Paths (s,s)),(Paths (s,s)):] is non empty set
Loops (f . s) is non empty set
Paths ((f . s),(f . s)) is non empty set
EqRel (T,(f . s)) is non empty Relation-like Loops (f . s) -defined Loops (f . s) -valued V26( Loops (f . s)) quasi_total V240() V245() Element of bool [:(Loops (f . s)),(Loops (f . s)):]
[:(Loops (f . s)),(Loops (f . s)):] is non empty Relation-like set
bool [:(Loops (f . s)),(Loops (f . s)):] is non empty set
EqRel (T,(f . s),(f . s)) is Relation-like Paths ((f . s),(f . s)) -defined Paths ((f . s),(f . s)) -valued Element of bool [:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):]
[:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):] is non empty Relation-like set
bool [:(Paths ((f . s),(f . s))),(Paths ((f . s),(f . s))):] is non empty set
ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls1) is Element of bool (Loops s)
bool (Loops s) is non empty set
(S,T,s,ls1,f) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of f . s,f . s
Class ((EqRel (T,(f . s))),(S,T,s,ls1,f)) is Element of bool (Loops (f . s))
bool (Loops (f . s)) is non empty set
ls2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
Class ((EqRel (S,s)),ls2) is Element of bool (Loops s)
(S,T,s,ls2,f) is non empty Relation-like the carrier of K527() -defined the carrier of K527() -defined the carrier of T -valued the carrier of T -valued Function-like V26( the carrier of K527()) V26( the carrier of K527()) quasi_total quasi_total quasi_total continuous Path of f . s,f . s
Class ((EqRel (T,(f . s))),(S,T,s,ls2,f)) is Element of bool (Loops (f . s))
(f ") * (S,T,s,ls1,f) is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of S:]
[: the carrier of K527(), the carrier of S:] is non empty Relation-like set
bool [: the carrier of K527(), the carrier of S:] is non empty set
(f ") * (S,T,s,ls2,f) is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of S:]
a1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
a2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of s,s
(f ") * f is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
id (dom f) is non empty Relation-like dom f -defined dom f -valued Function-like one-to-one V26( dom f) quasi_total Element of bool [:(dom f),(dom f):]
[:(dom f),(dom f):] is non empty Relation-like set
bool [:(dom f),(dom f):] is non empty set
((f ") * f) * ls1 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of S:]
((f ") * f) * ls2 is non empty Relation-like the carrier of K527() -defined the carrier of S -valued Function-like V26( the carrier of K527()) quasi_total Element of bool [: the carrier of K527(), the carrier of S:]
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
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
s is Element of the carrier of S
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (S,s)) is non empty set
t is Element of the carrier of T
FundamentalGroup (T,t) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (T,t)) is non empty set
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):] is non empty set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
f . s is Element of the carrier of T
FundamentalGroup (T,(f . s)) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (T,(f . s))) is non empty set
(S,T,s,f) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(f . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total V264( FundamentalGroup (S,s), FundamentalGroup (T,(f . s))) multiplicative Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):]
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty set
f is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total Path of t,f . s
pi_1-iso f is non empty Relation-like the carrier of (FundamentalGroup (T,(f . s))) -defined the carrier of (FundamentalGroup (T,t)) -valued Function-like V26( the carrier of (FundamentalGroup (T,(f . s)))) quasi_total Element of bool [: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):]
[: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):] is non empty set
(pi_1-iso f) * (S,T,s,f) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,t)) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):]
P is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,t)) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total V264( FundamentalGroup (S,s), FundamentalGroup (T,t)) multiplicative Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):]
c₁₁ is non empty Relation-like the carrier of (FundamentalGroup (T,(f . s))) -defined the carrier of (FundamentalGroup (T,t)) -valued Function-like V26( the carrier of (FundamentalGroup (T,(f . s)))) quasi_total V264( FundamentalGroup (T,(f . s)), FundamentalGroup (T,t)) multiplicative Element of bool [: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):]
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is non empty TopSpace-like connected pathwise_connected TopStruct
the carrier of T is non empty set
s is Element of the carrier of S
FundamentalGroup (S,s) is non empty strict V260() V261() L9()
t is Element of the carrier of T
FundamentalGroup (T,t) is non empty strict V260() V261() L9()
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V26( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
f . s is Element of the carrier of T
the non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,f . s is non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,f . s
the carrier of (FundamentalGroup (S,s)) is non empty set
FundamentalGroup (T,(f . s)) is non empty strict V260() V261() L9()
the carrier of (FundamentalGroup (T,(f . s))) is non empty set
the carrier of (FundamentalGroup (T,t)) is non empty set
(S,T,s,f) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,(f . s))) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) quasi_total V264( FundamentalGroup (S,s), FundamentalGroup (T,(f . s))) multiplicative Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):]
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,(f . s))):] is non empty set
pi_1-iso the non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,f . s is non empty Relation-like the carrier of (FundamentalGroup (T,(f . s))) -defined the carrier of (FundamentalGroup (T,t)) -valued Function-like one-to-one V26( the carrier of (FundamentalGroup (T,(f . s)))) quasi_total onto bijective V264( FundamentalGroup (T,(f . s)), FundamentalGroup (T,t)) multiplicative Element of bool [: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):]
[: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (T,(f . s))), the carrier of (FundamentalGroup (T,t)):] is non empty set
(pi_1-iso the non empty Relation-like the carrier of K527() -defined the carrier of T -valued Function-like V26( the carrier of K527()) quasi_total continuous Path of t,f . s) * (S,T,s,f) is non empty Relation-like the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (S,s)) -defined the carrier of (FundamentalGroup (T,t)) -valued the carrier of (FundamentalGroup (T,t)) -valued Function-like V26( the carrier of (FundamentalGroup (S,s))) V26( the carrier of (FundamentalGroup (S,s))) quasi_total quasi_total V264( FundamentalGroup (S,s), FundamentalGroup (T,t)) multiplicative Element of bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):]
[: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):] is non empty Relation-like set
bool [: the carrier of (FundamentalGroup (S,s)), the carrier of (FundamentalGroup (T,t)):] is non empty set