:: YELLOW14 semantic presentation

K126() is Element of K6(K122())
K122() is set
K6(K122()) is non empty set
K121() is set
K6(K121()) is non empty set
K6(K126()) is non empty set
K123() is set
K124() is set
K125() is set
K7(K122(),K122()) is Relation-like set
K6(K7(K122(),K122())) is non empty set
K439() is non empty V152() L13()
the carrier of K439() is non empty set
<REAL,+> is non empty V152() V174() V175() V176() V178() left-invertible right-invertible V230() left-cancelable right-cancelable V233() L13()
K445() is non empty V152() V176() V178() left-cancelable right-cancelable V233() SubStr of <REAL,+>
<NAT,+> is non empty V152() V174() V176() V178() left-cancelable right-cancelable V233() uniquely-decomposable SubStr of K445()
<REAL,*> is non empty V152() V174() V176() V178() L13()
<NAT,*> is non empty V152() V174() V176() V178() uniquely-decomposable SubStr of <REAL,*>
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() set
1 is non empty set
{{},1} is non empty finite set
K659() is set
{{}} is non empty functional finite V38() set
K410({{}}) is M23({{}})
K7(K410({{}}),{{}}) is Relation-like set
K6(K7(K410({{}}),{{}})) is non empty set
K41(K410({{}}),{{}}) is set
bool 1 is non empty Element of K6(K6(1))
K6(1) is non empty set
K6(K6(1)) is non empty set
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() Element of K126()
{0,1} is non empty finite set
I is set
K6(I) is non empty set
id I is Relation-like I -defined I -valued Function-like one-to-one V18(I) quasi_total Element of K6(K7(I,I))
K7(I,I) is Relation-like set
K6(K7(I,I)) is non empty set
T is Element of K6(I)
(id I) | T is Relation-like I -defined T -defined I -defined I -valued Function-like Element of K6(K7(I,I))
rng ((id I) | T) is Element of K6(I)
K7(T,I) is Relation-like set
K6(K7(T,I)) is non empty set
a is set
dom ((id I) | T) is Element of K6(I)
a is set
((id I) | T) . a is set
(id I) . a is set
a is set
((id I) | T) . a is set
(id I) . a is set
I is empty trivial finite {} -element 1-sorted
the carrier of I is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() set
T is 1-sorted
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is empty Relation-like non-empty empty-yielding the carrier of I -defined the carrier of T -valued Function-like one-to-one constant functional V18( the carrier of I) quasi_total Function-yielding V33() finite finite-yielding V38() Element of K6(K7( the carrier of I, the carrier of T))
rng p is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() with_non-empty_elements Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
[#] T is non proper Element of K6( the carrier of T)
I is 1-sorted
the carrier of I is set
T is empty trivial finite {} -element 1-sorted
the carrier of T is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is empty Relation-like non-empty empty-yielding the carrier of I -defined the carrier of T -valued Function-like one-to-one constant functional quasi_total Function-yielding V33() finite finite-yielding V38() Element of K6(K7( the carrier of I, the carrier of T))
dom p is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
[#] I is non proper Element of K6( the carrier of I)
I is non empty 1-sorted
the carrier of I is non empty set
T is 1-sorted
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
dom p is Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
[#] I is non empty non proper Element of K6( the carrier of I)
I is 1-sorted
the carrier of I is set
T is non empty 1-sorted
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
rng p is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
[#] T is non empty non proper Element of K6( the carrier of T)
I is non empty reflexive RelStr
the carrier of I is non empty set
T is non empty RelStr
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
K6( the carrier of I) is non empty set
a is non empty directed Element of K6( the carrier of I)
a is Element of K6( the carrier of I)
I is 1-sorted
1-sorted(# {{}} #) is strict 1-sorted
I is strict 1-sorted
the carrier of I is set
T is Element of the carrier of I
id {{}} is non empty Relation-like {{}} -defined {{}} -valued Function-like one-to-one V18({{}}) quasi_total Function-yielding V33() finite Element of K6(K7({{}},{{}}))
K7({{}},{{}}) is non empty Relation-like finite set
K6(K7({{}},{{}})) is non empty finite V38() set
RelStr(# {{}},(id {{}}) #) is non empty trivial finite 1 -element strict RelStr
I is non empty trivial finite 1 -element strict RelStr
the carrier of I is non empty trivial finite set
T is Element of the carrier of I
I is constituted-Functions 1-sorted
T is NetStr over I
p is set
the mapping of T is Relation-like the carrier of T -defined the carrier of I -valued Function-like quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is set
the carrier of I is set
K7( the carrier of T, the carrier of I) is Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
dom the mapping of T is set
the mapping of T . p is set
dom the mapping of T is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
rng the mapping of T is Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
I is constituted-Functions 1-sorted
the carrier of I is set
id the carrier of I is Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
K7( the carrier of I, the carrier of I) is Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
NetStr(# the carrier of I,(id the carrier of I),(id the carrier of I) #) is strict (I) NetStr over I
T is strict (I) NetStr over I
p is set
the mapping of T is Relation-like the carrier of T -defined the carrier of I -valued Function-like quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is set
K7( the carrier of T, the carrier of I) is Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
dom the mapping of T is set
the mapping of T . p is set
dom the mapping of T is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
I is non empty constituted-Functions 1-sorted
the carrier of I is non empty set
id the carrier of I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
K7( the carrier of I, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
NetStr(# the carrier of I,(id the carrier of I),(id the carrier of I) #) is non empty strict (I) NetStr over I
T is non empty strict (I) NetStr over I
p is set
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
dom the mapping of T is non empty set
the mapping of T . p is set
dom the mapping of T is non empty Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
I is constituted-Functions 1-sorted
T is (I) NetStr over I
the mapping of T is Relation-like the carrier of T -defined the carrier of I -valued Function-like quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is set
the carrier of I is set
K7( the carrier of T, the carrier of I) is Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
I is non empty constituted-Functions 1-sorted
the carrier of I is non empty set
the Relation-like Function-like Element of the carrier of I is Relation-like Function-like Element of the carrier of I
the non empty transitive directed (I) NetStr over I is non empty transitive directed (I) NetStr over I
ConstantNet ( the non empty transitive directed (I) NetStr over I, the Relation-like Function-like Element of the carrier of I) is non empty transitive strict directed constant (I) NetStr over I
I is non empty 1-sorted
the carrier of I is non empty set
T is non empty NetStr over I
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
rng the mapping of T is non empty Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
I is non empty 1-sorted
the carrier of I is non empty set
T is non empty NetStr over I
netmap (T,I) is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
rng (netmap (T,I)) is non empty Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
T is non empty RelStr
the carrier of T is non empty set
p is non empty RelStr
the carrier of p is non empty set
K7( the carrier of T, the carrier of p) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of p)) is non empty set
I is non empty RelStr
the carrier of I is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
a is non empty Relation-like the carrier of T -defined the carrier of p -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of p))
a is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a * a is non empty Relation-like the carrier of I -defined the carrier of p -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of p))
K7( the carrier of I, the carrier of p) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of p)) is non empty set
a * p is non empty Relation-like the carrier of I -defined the carrier of p -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of p))
i is Element of the carrier of I
(a * a) . i is Element of the carrier of p
(a * p) . i is Element of the carrier of p
a . i is Element of the carrier of T
a . (a . i) is Element of the carrier of p
p . i is Element of the carrier of T
a . (p . i) is Element of the carrier of p
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
T is non empty TopSpace-like TopRelStr
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
ContMaps (I,T) is non empty strict constituted-Functions RelStr
the carrier of (ContMaps (I,T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a is Relation-like Function-like Element of the carrier of (ContMaps (I,T))
p is Relation-like Function-like Element of the carrier of (ContMaps (I,T))
T |^ the carrier of I is non empty strict constituted-Functions RelStr
the carrier of (T |^ the carrier of I) is non empty set
i is Relation-like Function-like Element of the carrier of (T |^ the carrier of I)
i is Relation-like Function-like Element of the carrier of (T |^ the carrier of I)
I is non empty set
T is non empty RelStr
T |^ I is non empty strict constituted-Functions RelStr
the carrier of (T |^ I) is non empty set
p is Relation-like Function-like Element of the carrier of (T |^ I)
a is Element of I
p . a is set
the carrier of T is non empty set
I --> T is non empty Relation-like I -defined {T} -valued Function-like constant V18(I) quasi_total V320() V365() non-Empty Element of K6(K7(I,{T}))
{T} is non empty finite set
K7(I,{T}) is non empty Relation-like set
K6(K7(I,{T})) is non empty set
product (I --> T) is non empty strict RelStr
the carrier of (product (I --> T)) is non empty functional set
a is Relation-like Function-like Element of the carrier of (product (I --> T))
a . a is Element of the carrier of ((I --> T) . a)
(I --> T) . a is RelStr
the carrier of ((I --> T) . a) is set
I is RelStr
the carrier of I is set
T is RelStr
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
rng p is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
rng p is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
I is RelStr
the carrier of I is set
T is RelStr
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
I is non empty RelStr
the carrier of I is non empty set
T is non empty RelStr
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
p /" is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
p " is Relation-like Function-like set
rng p is non empty Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
a is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
I is non empty RelStr
T is non empty RelStr
the carrier of I is non empty set
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a is Element of the carrier of T
a is Element of the carrier of T
p /" is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
(p /") . a is Element of the carrier of I
(p /") . a is Element of the carrier of I
p is Element of the carrier of I
p . p is Element of the carrier of T
p " is Relation-like Function-like set
rng p is non empty Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
p . ((p /") . a) is Element of the carrier of T
p . ((p /") . a) is Element of the carrier of T
i is Element of the carrier of T
(p /") . i is Element of the carrier of I
i is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
p . ((p /") . i) is Element of the carrier of T
I is non empty RelStr
T is non empty RelStr
the carrier of I is non empty set
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a is Element of the carrier of T
a is Element of the carrier of T
p /" is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
(p /") . a is Element of the carrier of I
(p /") . a is Element of the carrier of I
p is Element of the carrier of I
p . p is Element of the carrier of T
p " is Relation-like Function-like set
rng p is non empty Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
p . ((p /") . a) is Element of the carrier of T
p . ((p /") . a) is Element of the carrier of T
i is Element of the carrier of T
(p /") . i is Element of the carrier of I
i is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
p . ((p /") . i) is Element of the carrier of T
I is RelStr
the carrier of I is set
the Element of the carrier of I is Element of the carrier of I
p is Element of the carrier of I
p is Element of the carrier of I
I is RelStr
I is RelStr
T is RelStr
the carrier of I is set
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
p is Element of the carrier of I
a is non empty RelStr
the carrier of a is non empty set
a is non empty RelStr
the carrier of a is non empty set
K7( the carrier of a, the carrier of a) is non empty Relation-like set
K6(K7( the carrier of a, the carrier of a)) is non empty set
i is non empty Relation-like the carrier of a -defined the carrier of a -valued Function-like V18( the carrier of a) quasi_total Element of K6(K7( the carrier of a, the carrier of a))
i is Element of the carrier of a
i . i is Element of the carrier of a
y is Element of the carrier of T
[#] I is non proper Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
i .: ([#] I) is Element of K6( the carrier of a)
K6( the carrier of a) is non empty set
rng i is non empty Element of K6( the carrier of a)
a is lower-bounded upper-bounded bounded RelStr
I is RelStr
T is RelStr
the carrier of I is set
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
p is Element of the carrier of I
a is non empty RelStr
the carrier of a is non empty set
a is non empty RelStr
the carrier of a is non empty set
K7( the carrier of a, the carrier of a) is non empty Relation-like set
K6(K7( the carrier of a, the carrier of a)) is non empty set
i is non empty Relation-like the carrier of a -defined the carrier of a -valued Function-like V18( the carrier of a) quasi_total Element of K6(K7( the carrier of a, the carrier of a))
i is Element of the carrier of a
i . i is Element of the carrier of a
y is Element of the carrier of T
[#] I is non proper Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
i .: ([#] I) is Element of K6( the carrier of a)
K6( the carrier of a) is non empty set
rng i is non empty Element of K6( the carrier of a)
a is lower-bounded upper-bounded bounded RelStr
I is non empty RelStr
the carrier of I is non empty set
K6( the carrier of I) is non empty set
T is non empty RelStr
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Element of K6( the carrier of I)
a is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a .: p is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
a " (a .: p) is Element of K6( the carrier of I)
rng a is non empty Element of K6( the carrier of T)
[#] T is non empty non proper lower upper Element of K6( the carrier of T)
a /" is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
a " is Relation-like Function-like set
a is Element of the carrier of I
a . a is Element of the carrier of T
dom a is non empty Element of K6( the carrier of I)
p is Element of the carrier of T
(a /") .: (a .: p) is Element of K6( the carrier of I)
(a /") . p is Element of the carrier of I
a . ((a /") . p) is Element of the carrier of T
p is Element of the carrier of T
(a /") . p is Element of the carrier of I
i is Element of the carrier of I
a . i is Element of the carrier of T
(a /") . (a . i) is Element of the carrier of I
I is non empty RelStr
the carrier of I is non empty set
K6( the carrier of I) is non empty set
T is non empty RelStr
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is Element of K6( the carrier of I)
a is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a .: p is Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
a " (a .: p) is Element of K6( the carrier of I)
rng a is non empty Element of K6( the carrier of T)
[#] T is non empty non proper lower upper Element of K6( the carrier of T)
a /" is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
a " is Relation-like Function-like set
a is Element of the carrier of I
a . a is Element of the carrier of T
dom a is non empty Element of K6( the carrier of I)
p is Element of the carrier of T
(a /") .: (a .: p) is Element of K6( the carrier of I)
(a /") . p is Element of the carrier of I
a . ((a /") . p) is Element of the carrier of T
p is Element of the carrier of T
(a /") . p is Element of the carrier of I
i is Element of the carrier of I
a . i is Element of the carrier of T
(a /") . (a . i) is Element of the carrier of I
I is TopStruct
T is TopStruct
the carrier of I is set
the carrier of T is set
K7( the carrier of I, the carrier of T) is Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
[#] I is non proper dense Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
[#] T is non proper dense Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
rng p is Element of K6( the carrier of T)
dom p is Element of K6( the carrier of I)
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
dom p is Element of K6( the carrier of I)
rng p is Element of K6( the carrier of T)
p is Relation-like the carrier of I -defined the carrier of T -valued Function-like quasi_total Element of K6(K7( the carrier of I, the carrier of T))
dom p is Element of K6( the carrier of I)
rng p is Element of K6( the carrier of T)
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6( the carrier of I) is non empty set
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of I, the topology of I #) is non empty set
K7( the carrier of I, the carrier of TopStruct(# the carrier of I, the topology of I #)) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of TopStruct(# the carrier of I, the topology of I #))) is non empty set
id I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total onto bijective continuous being_homeomorphism open Element of K6(K7( the carrier of I, the carrier of I))
K7( the carrier of I, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
id the carrier of I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
T is non empty Relation-like the carrier of I -defined the carrier of TopStruct(# the carrier of I, the topology of I #) -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of TopStruct(# the carrier of I, the topology of I #)))
dom T is non empty Element of K6( the carrier of I)
[#] I is non empty non proper open closed dense non boundary Element of K6( the carrier of I)
rng T is non empty Element of K6( the carrier of TopStruct(# the carrier of I, the topology of I #))
K6( the carrier of TopStruct(# the carrier of I, the topology of I #)) is non empty set
[#] TopStruct(# the carrier of I, the topology of I #) is non empty non proper open closed dense non boundary Element of K6( the carrier of TopStruct(# the carrier of I, the topology of I #))
T /" is non empty Relation-like the carrier of TopStruct(# the carrier of I, the topology of I #) -defined the carrier of I -valued Function-like V18( the carrier of TopStruct(# the carrier of I, the topology of I #)) quasi_total Element of K6(K7( the carrier of TopStruct(# the carrier of I, the topology of I #), the carrier of I))
K7( the carrier of TopStruct(# the carrier of I, the topology of I #), the carrier of I) is non empty Relation-like set
K6(K7( the carrier of TopStruct(# the carrier of I, the topology of I #), the carrier of I)) is non empty set
I is non empty reflexive Scott TopRelStr
the carrier of I is non empty set
K6( the carrier of I) is non empty set
T is Element of K6( the carrier of I)
T is Element of K6( the carrier of I)
I is TopStruct
the carrier of I is set
K6( the carrier of I) is non empty set
T is Element of the carrier of I
{T} is non empty finite set
a is Element of K6( the carrier of I)
Cl a is Element of K6( the carrier of I)
a is Element of K6( the carrier of I)
Cl a is Element of K6( the carrier of I)
I is TopStruct
the carrier of I is set
K6( the carrier of I) is non empty set
p is Element of the carrier of I
{p} is non empty finite set
T is Element of the carrier of I
a is Element of K6( the carrier of I)
Cl a is Element of K6( the carrier of I)
a is Element of K6( the carrier of I)
I is TopStruct
the carrier of I is set
K6( the carrier of I) is non empty set
T is Element of the carrier of I
{T} is non empty finite set
p is Element of the carrier of I
{p} is non empty finite set
a is Element of K6( the carrier of I)
a is Element of K6( the carrier of I)
Cl a is Element of K6( the carrier of I)
Cl a is Element of K6( the carrier of I)
p is set
i is Element of K6( the carrier of I)
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
K6( the carrier of I) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopSpace-like TopStruct
the topology of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
p is non empty irreducible Element of K6( the carrier of I)
a is Element of K6( the carrier of T)
a is Element of K6( the carrier of T)
p is Element of K6( the carrier of T)
K20(K6( the carrier of T),a,p) is Element of K6( the carrier of T)
a \/ p is Element of K6( the carrier of T)
i is Element of K6( the carrier of I)
i is Element of K6( the carrier of I)
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of I) is non empty set
K6( the carrier of T) is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopSpace-like TopStruct
the topology of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
p is Element of the carrier of I
a is Element of the carrier of T
a is Element of K6( the carrier of I)
p is Element of K6( the carrier of T)
{p} is non empty finite Element of K6( the carrier of I)
Cl {p} is non empty closed Element of K6( the carrier of I)
{a} is non empty finite Element of K6( the carrier of T)
Cl {a} is non empty closed Element of K6( the carrier of T)
I is TopStruct
the carrier of I is set
K6( the carrier of I) is non empty set
T is TopStruct
the carrier of T is set
K6( the carrier of T) is non empty set
the topology of I is Element of K6(K6( the carrier of I))
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is strict TopStruct
the topology of T is Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
p is Element of K6( the carrier of I)
a is Element of K6( the carrier of T)
a is Element of K6(K6( the carrier of T))
p is Element of K6(K6( the carrier of I))
i is Element of K6(K6( the carrier of I))
i is Element of K6(K6( the carrier of T))
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6( the carrier of I) is non empty set
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the topology of T is non empty Element of K6(K6( the carrier of T))
K6( the carrier of T) is non empty set
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
p is non empty irreducible Element of K6( the carrier of T)
a is non empty irreducible Element of K6( the carrier of I)
a is Element of the carrier of I
p is Element of the carrier of T
i is Element of the carrier of T
i is Element of the carrier of I
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6( the carrier of I) is non empty set
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the topology of T is non empty Element of K6(K6( the carrier of T))
K6( the carrier of T) is non empty set
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
p is Element of the carrier of T
a is Element of K6( the carrier of T)
a is Element of K6( the carrier of I)
p is Element of K6( the carrier of I)
Int p is open Element of K6( the carrier of I)
i is Element of K6( the carrier of T)
Int i is open Element of K6( the carrier of T)
I is TopStruct
the carrier of I is set
the topology of I is Element of K6(K6( the carrier of I))
K6( the carrier of I) is non empty set
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is strict TopStruct
T is TopStruct
the carrier of T is set
the topology of T is Element of K6(K6( the carrier of T))
K6( the carrier of T) is non empty set
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is strict TopStruct
p is Element of K6(K6( the carrier of T))
a is Element of K6(K6( the carrier of I))
a is Element of K6(K6( the carrier of I))
p is Element of K6(K6( the carrier of T))
I is non empty set
T is non empty TopSpace-like TopStruct
I --> T is non empty Relation-like I -defined {T} -valued Function-like constant V18(I) quasi_total V365() non-Empty TopStruct-yielding Element of K6(K7(I,{T}))
{T} is non empty finite set
K7(I,{T}) is non empty Relation-like set
K6(K7(I,{T})) is non empty set
product (I --> T) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product (I --> T)) is non empty set
p is Relation-like Function-like Element of the carrier of (product (I --> T))
a is Element of I
p . a is set
the carrier of T is non empty set
p . a is Element of the carrier of ((I --> T) . a)
(I --> T) . a is non empty TopStruct
the carrier of ((I --> T) . a) is non empty set
I is non empty set
T is Relation-like I -defined Function-like V18(I) V365() non-Empty TopStruct-yielding set
product T is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product T) is non empty set
p is Relation-like Function-like Element of the carrier of (product T)
a is Relation-like Function-like Element of the carrier of (product T)
{a} is non empty functional finite Element of K6( the carrier of (product T))
K6( the carrier of (product T)) is non empty set
Cl {a} is non empty closed Element of K6( the carrier of (product T))
Carrier T is Relation-like non-empty I -defined Function-like V18(I) set
product (Carrier T) is set
dom (Carrier T) is Element of K6(I)
K6(I) is non empty set
p is Relation-like Function-like set
dom p is set
a is Element of I
T . a is non empty TopStruct
the carrier of (T . a) is non empty set
K6( the carrier of (T . a)) is non empty set
p . a is Element of the carrier of (T . a)
a . a is Element of the carrier of (T . a)
{(a . a)} is non empty finite Element of K6( the carrier of (T . a))
i is Element of K6( the carrier of (T . a))
[#] (T . a) is non empty non proper dense Element of K6( the carrier of (T . a))
proj (T,a) is non empty Relation-like the carrier of (product T) -defined the carrier of (T . a) -valued Function-like V18( the carrier of (product T)) quasi_total Element of K6(K7( the carrier of (product T), the carrier of (T . a)))
K7( the carrier of (product T), the carrier of (T . a)) is non empty Relation-like set
K6(K7( the carrier of (product T), the carrier of (T . a))) is non empty set
i is Element of K6( the carrier of (T . a))
(proj (T,a)) " i is Element of K6( the carrier of (product T))
(Carrier T) +* (a,i) is Relation-like Function-like set
dom ((Carrier T) +* (a,i)) is set
y is set
p . y is set
((Carrier T) +* (a,i)) . y is set
(Carrier T) . y is set
(Carrier T) +* (a,i) is Relation-like Function-like set
product ((Carrier T) +* (a,i)) is set
product ((Carrier T) +* (a,i)) is set
y is Relation-like Function-like set
dom y is set
y . a is set
((Carrier T) +* (a,i)) . a is set
Cl {(a . a)} is Element of K6( the carrier of (T . a))
K6(K6( the carrier of (product T))) is non empty set
product_prebasis T is Element of K6(K6((product (Carrier T))))
K6((product (Carrier T))) is non empty set
K6(K6((product (Carrier T)))) is non empty set
a is open quasi_prebasis Element of K6(K6( the carrier of (product T)))
p is finite Element of K6(K6( the carrier of (product T)))
Intersect p is Element of K6( the carrier of (product T))
i is set
i is Relation-like Function-like set
dom i is set
m is TopStruct
the carrier of m is set
K6( the carrier of m) is non empty set
y is set
V is Element of K6( the carrier of m)
T . y is set
(Carrier T) +* (y,V) is Relation-like Function-like set
product ((Carrier T) +* (y,V)) is set
i is Element of I
T . i is non empty TopStruct
the carrier of (T . i) is non empty set
K6( the carrier of (T . i)) is non empty set
V is Element of K6( the carrier of (T . i))
(Carrier T) +* (i,V) is Relation-like Function-like set
dom ((Carrier T) +* (i,V)) is set
p . i is Element of the carrier of (T . i)
a . i is Element of the carrier of (T . i)
{(a . i)} is non empty finite Element of K6( the carrier of (T . i))
Cl {(a . i)} is Element of K6( the carrier of (T . i))
z is set
i . z is set
((Carrier T) +* (i,V)) . z is set
c₁₅ is Relation-like Function-like set
dom c₁₅ is set
(Carrier T) . z is set
I is non empty set
T is non empty TopSpace-like TopStruct
I --> T is non empty Relation-like I -defined {T} -valued Function-like constant V18(I) quasi_total V365() non-Empty TopStruct-yielding Element of K6(K7(I,{T}))
{T} is non empty finite set
K7(I,{T}) is non empty Relation-like set
K6(K7(I,{T})) is non empty set
product (I --> T) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product (I --> T)) is non empty set
the carrier of T is non empty set
p is Relation-like Function-like Element of the carrier of (product (I --> T))
a is Relation-like Function-like Element of the carrier of (product (I --> T))
{a} is non empty functional finite Element of K6( the carrier of (product (I --> T)))
K6( the carrier of (product (I --> T))) is non empty set
Cl {a} is non empty closed Element of K6( the carrier of (product (I --> T)))
a is Relation-like I -defined Function-like V18(I) V365() non-Empty TopStruct-yielding set
product a is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product a) is non empty set
i is Element of I
(I,T,p,i) is Element of the carrier of T
(I,T,a,i) is Element of the carrier of T
{(I,T,a,i)} is non empty finite Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
Cl {(I,T,a,i)} is non empty closed Element of K6( the carrier of T)
p is Relation-like Function-like Element of the carrier of (product a)
p . i is Element of the carrier of (a . i)
a . i is non empty TopStruct
the carrier of (a . i) is non empty set
i is Relation-like Function-like Element of the carrier of (product a)
i . i is Element of the carrier of (a . i)
{(i . i)} is non empty finite Element of K6( the carrier of (a . i))
K6( the carrier of (a . i)) is non empty set
Cl {(i . i)} is Element of K6( the carrier of (a . i))
p is Relation-like Function-like Element of the carrier of (product a)
i is Relation-like Function-like Element of the carrier of (product a)
i is Element of I
p . i is Element of the carrier of (a . i)
a . i is non empty TopStruct
the carrier of (a . i) is non empty set
i . i is Element of the carrier of (a . i)
{(i . i)} is non empty finite Element of K6( the carrier of (a . i))
K6( the carrier of (a . i)) is non empty set
Cl {(i . i)} is Element of K6( the carrier of (a . i))
(I,T,p,i) is Element of the carrier of T
(I,T,a,i) is Element of the carrier of T
{(I,T,a,i)} is non empty finite Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
Cl {(I,T,a,i)} is non empty closed Element of K6( the carrier of T)
I is non empty set
T is Element of I
p is Relation-like I -defined Function-like V18(I) V365() non-Empty TopStruct-yielding set
product p is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product p) is non empty set
p . T is non empty TopStruct
the carrier of (p . T) is non empty set
a is Relation-like Function-like Element of the carrier of (product p)
{a} is non empty functional finite Element of K6( the carrier of (product p))
K6( the carrier of (product p)) is non empty set
Cl {a} is non empty closed Element of K6( the carrier of (product p))
pi ((Cl {a}),T) is set
a . T is Element of the carrier of (p . T)
{(a . T)} is non empty finite Element of K6( the carrier of (p . T))
K6( the carrier of (p . T)) is non empty set
Cl {(a . T)} is Element of K6( the carrier of (p . T))
a is set
p is set
i is Relation-like Function-like set
i . T is set
i is set
p is Relation-like Function-like Element of the carrier of (product p)
T .--> i is Relation-like I -defined {T} -defined Function-like one-to-one finite set
{T} is non empty finite set
{T} --> i is non empty Relation-like {T} -defined {i} -valued Function-like constant V18({T}) quasi_total finite Element of K6(K7({T},{i}))
{i} is non empty finite set
K7({T},{i}) is non empty Relation-like finite set
K6(K7({T},{i})) is non empty finite V38() set
p +* (T .--> i) is Relation-like Function-like set
Carrier p is Relation-like non-empty I -defined Function-like V18(I) set
dom (Carrier p) is Element of K6(I)
K6(I) is non empty set
product (Carrier p) is set
dom p is set
dom (T .--> i) is finite Element of K6(I)
{T} is non empty finite Element of K6(I)
y is set
(p +* (T .--> i)) . y is set
(Carrier p) . y is set
p . y is set
m is 1-sorted
the carrier of m is set
p . y is set
dom (p +* (T .--> i)) is set
(dom p) \/ (dom (T .--> i)) is set
I \/ {T} is non empty set
y is Relation-like Function-like Element of the carrier of (product p)
m is Element of I
y . m is Element of the carrier of (p . m)
p . m is non empty TopStruct
the carrier of (p . m) is non empty set
a . m is Element of the carrier of (p . m)
{(a . m)} is non empty finite Element of K6( the carrier of (p . m))
K6( the carrier of (p . m)) is non empty set
Cl {(a . m)} is Element of K6( the carrier of (p . m))
p . m is Element of the carrier of (p . m)
(p +* (T .--> i)) . T is set
I is non empty set
T is Element of I
p is non empty TopSpace-like TopStruct
I --> p is non empty Relation-like I -defined {p} -valued Function-like constant V18(I) quasi_total V365() non-Empty TopStruct-yielding Element of K6(K7(I,{p}))
{p} is non empty finite set
K7(I,{p}) is non empty Relation-like set
K6(K7(I,{p})) is non empty set
product (I --> p) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product (I --> p)) is non empty set
the carrier of p is non empty set
a is Relation-like Function-like Element of the carrier of (product (I --> p))
{a} is non empty functional finite Element of K6( the carrier of (product (I --> p)))
K6( the carrier of (product (I --> p))) is non empty set
Cl {a} is non empty closed Element of K6( the carrier of (product (I --> p)))
pi ((Cl {a}),T) is set
(I,p,a,T) is Element of the carrier of p
{(I,p,a,T)} is non empty finite Element of K6( the carrier of p)
K6( the carrier of p) is non empty set
Cl {(I,p,a,T)} is non empty closed Element of K6( the carrier of p)
(I --> p) . T is non empty TopStruct
I is non empty TopStruct
the carrier of I is non empty set
T is non empty TopStruct
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
id I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total onto bijective continuous being_homeomorphism open Element of K6(K7( the carrier of I, the carrier of I))
K7( the carrier of I, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
id the carrier of I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
the topology of I is Element of K6(K6( the carrier of I))
K6( the carrier of I) is non empty set
K6(K6( the carrier of I)) is non empty set
TopStruct(# the carrier of I, the topology of I #) is non empty strict TopStruct
the topology of T is Element of K6(K6( the carrier of T))
K6( the carrier of T) is non empty set
K6(K6( the carrier of T)) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopStruct
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
a is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
dom p is non empty Element of K6( the carrier of I)
[#] T is non empty non proper dense Element of K6( the carrier of T)
[#] I is non empty non proper dense Element of K6( the carrier of I)
a is set
p is Element of K6( the carrier of I)
a " p is Element of K6( the carrier of T)
a is set
p is Element of K6( the carrier of T)
p " p is Element of K6( the carrier of I)
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K7( the carrier of I, the carrier of T) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of T)) is non empty set
p is non empty Relation-like the carrier of I -defined the carrier of T -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of T))
Image p is non empty TopSpace-like SubSpace of T
corestr p is non empty Relation-like the carrier of I -defined the carrier of (Image p) -valued Function-like V18( the carrier of I) quasi_total onto Element of K6(K7( the carrier of I, the carrier of (Image p)))
the carrier of (Image p) is non empty set
K7( the carrier of I, the carrier of (Image p)) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of (Image p))) is non empty set
I is non empty TopSpace-like TopStruct
T is non empty TopSpace-like SubSpace of I
incl T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is non empty set
the carrier of I is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
I is non empty TopSpace-like TopStruct
the carrier of I is non empty set
K7( the carrier of I, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
T is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
T * T is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
Image T is non empty TopSpace-like SubSpace of I
the carrier of (Image T) is non empty set
incl (Image T) is non empty Relation-like the carrier of (Image T) -defined the carrier of I -valued Function-like V18( the carrier of (Image T)) quasi_total continuous Element of K6(K7( the carrier of (Image T), the carrier of I))
K7( the carrier of (Image T), the carrier of I) is non empty Relation-like set
K6(K7( the carrier of (Image T), the carrier of I)) is non empty set
corestr T is non empty Relation-like the carrier of I -defined the carrier of (Image T) -valued Function-like V18( the carrier of I) quasi_total onto Element of K6(K7( the carrier of I, the carrier of (Image T)))
K7( the carrier of I, the carrier of (Image T)) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of (Image T))) is non empty set
(corestr T) * (incl (Image T)) is non empty Relation-like the carrier of (Image T) -defined the carrier of (Image T) -valued Function-like V18( the carrier of (Image T)) quasi_total Element of K6(K7( the carrier of (Image T), the carrier of (Image T)))
K7( the carrier of (Image T), the carrier of (Image T)) is non empty Relation-like set
K6(K7( the carrier of (Image T), the carrier of (Image T))) is non empty set
id (Image T) is non empty Relation-like the carrier of (Image T) -defined the carrier of (Image T) -valued Function-like one-to-one V18( the carrier of (Image T)) quasi_total onto bijective continuous being_homeomorphism open Element of K6(K7( the carrier of (Image T), the carrier of (Image T)))
id the carrier of (Image T) is non empty Relation-like the carrier of (Image T) -defined the carrier of (Image T) -valued Function-like one-to-one V18( the carrier of (Image T)) quasi_total Element of K6(K7( the carrier of (Image T), the carrier of (Image T)))
a is set
((corestr T) * (incl (Image T))) . a is set
(id (Image T)) . a is set
rng T is non empty Element of K6( the carrier of I)
K6( the carrier of I) is non empty set
dom T is non empty Element of K6( the carrier of I)
(incl (Image T)) . a is set
(corestr T) . ((incl (Image T)) . a) is set
(corestr T) . a is set
T . a is set
p is set
T . p is set
I is non empty TopSpace-like TopStruct
T is non empty TopSpace-like SubSpace of I
incl T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total continuous Element of K6(K7( the carrier of T, the carrier of I))
the carrier of T is non empty set
the carrier of I is non empty set
K7( the carrier of T, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of I)) is non empty set
Image (incl T) is non empty TopSpace-like SubSpace of I
corestr (incl T) is non empty Relation-like the carrier of T -defined the carrier of (Image (incl T)) -valued Function-like V18( the carrier of T) quasi_total onto Element of K6(K7( the carrier of T, the carrier of (Image (incl T))))
the carrier of (Image (incl T)) is non empty set
K7( the carrier of T, the carrier of (Image (incl T))) is non empty Relation-like set
K6(K7( the carrier of T, the carrier of (Image (incl T)))) is non empty set
dom (corestr (incl T)) is non empty Element of K6( the carrier of T)
K6( the carrier of T) is non empty set
[#] T is non empty non proper open closed dense non boundary Element of K6( the carrier of T)
rng (corestr (incl T)) is non empty Element of K6( the carrier of (Image (incl T)))
K6( the carrier of (Image (incl T))) is non empty set
[#] (Image (incl T)) is non empty non proper open closed dense non boundary Element of K6( the carrier of (Image (incl T)))
(corestr (incl T)) /" is non empty Relation-like the carrier of (Image (incl T)) -defined the carrier of T -valued Function-like V18( the carrier of (Image (incl T))) quasi_total Element of K6(K7( the carrier of (Image (incl T)), the carrier of T))
K7( the carrier of (Image (incl T)), the carrier of T) is non empty Relation-like set
K6(K7( the carrier of (Image (incl T)), the carrier of T)) is non empty set
id I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total onto bijective continuous being_homeomorphism open Element of K6(K7( the carrier of I, the carrier of I))
K7( the carrier of I, the carrier of I) is non empty Relation-like set
K6(K7( the carrier of I, the carrier of I)) is non empty set
id the carrier of I is non empty Relation-like the carrier of I -defined the carrier of I -valued Function-like one-to-one V18( the carrier of I) quasi_total Element of K6(K7( the carrier of I, the carrier of I))
(id I) | T is non empty Relation-like the carrier of T -defined the carrier of I -valued Function-like V18( the carrier of T) quasi_total Element of K6(K7( the carrier of T, the carrier of I))
(id the carrier of I) | the carrier of T is Relation-like the carrier of T -defined the carrier of I -defined the carrier of I -valued Function-like Element of K6(K7( the carrier of I, the carrier of I))
a is Element of K6( the carrier of T)
((corestr (incl T)) /") " a is Element of K6( the carrier of (Image (incl T)))
the topology of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
K6( the carrier of I) is non empty set
the topology of I is non empty Element of K6(K6( the carrier of I))
K6(K6( the carrier of I)) is non empty set
rng ((id the carrier of I) | the carrier of T) is Element of K6( the carrier of I)
rng ((id I) | T) is non empty Element of K6( the carrier of I)
rng (incl T) is non empty Element of K6( the carrier of I)
((id the carrier of I) | the carrier of T) .: a is Element of K6( the carrier of I)
(id the carrier of I) .: a is Element of K6( the carrier of I)
the topology of (Image (incl T)) is non empty Element of K6(K6( the carrier of (Image (incl T))))
K6(K6( the carrier of (Image (incl T)))) is non empty set
a is Element of K6( the carrier of I)
a /\ ([#] T) is Element of K6( the carrier of T)
I is non empty set
T is Relation-like I -defined Function-like V18(I) V365() non-Empty TopStruct-yielding set
product T is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product T) is non empty set
p is Relation-like Function-like Element of the carrier of (product T)
a is Relation-like Function-like Element of the carrier of (product T)
{p} is non empty functional finite Element of K6( the carrier of (product T))
K6( the carrier of (product T)) is non empty set
Cl {p} is non empty closed Element of K6( the carrier of (product T))
{a} is non empty functional finite Element of K6( the carrier of (product T))
Cl {a} is non empty closed Element of K6( the carrier of (product T))
Carrier T is Relation-like non-empty I -defined Function-like V18(I) set
product (Carrier T) is set
dom a is set
dom (Carrier T) is Element of K6(I)
K6(I) is non empty set
dom p is set
a is set
p . a is set
a . a is set
p is Element of I
pi ((Cl {a}),p) is set
T . p is non empty TopStruct
the carrier of (T . p) is non empty set
a . p is Element of the carrier of (T . p)
{(a . p)} is non empty finite Element of K6( the carrier of (T . p))
K6( the carrier of (T . p)) is non empty set
Cl {(a . p)} is Element of K6( the carrier of (T . p))
pi ((Cl {p}),p) is set
p . p is Element of the carrier of (T . p)
{(p . p)} is non empty finite Element of K6( the carrier of (T . p))
Cl {(p . p)} is Element of K6( the carrier of (T . p))
I is non empty set
T is non empty TopSpace-like T_0 TopStruct
I --> T is non empty Relation-like I -defined {T} -valued Function-like constant V18(I) quasi_total V365() non-Empty TopStruct-yielding Element of K6(K7(I,{T}))
{T} is non empty finite set
K7(I,{T}) is non empty Relation-like set
K6(K7(I,{T})) is non empty set
product (I --> T) is non empty strict TopSpace-like constituted-Functions TopStruct
p is Element of I
(I --> T) . p is non empty TopStruct
I is non empty set
T is Relation-like I -defined Function-like V18(I) V365() non-Empty TopStruct-yielding set
product T is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (product T) is non empty set
p is Relation-like Function-like Element of the carrier of (product T)
{p} is non empty functional finite Element of K6( the carrier of (product T))
K6( the carrier of (product T)) is non empty set
Cl {p} is non empty closed Element of K6( the carrier of (product T))
a is set
a is Relation-like Function-like Element of the carrier of (product T)
p is Relation-like Function-like Element of the carrier of (product T)
i is set
a . i is set
p . i is set
i is Element of I
T . i is non empty TopStruct
the carrier of (T . i) is non empty set
p . i is Element of the carrier of (T . i)
{(p . i)} is non empty finite Element of K6( the carrier of (T . i))
K6( the carrier of (T . i)) is non empty set
a . i is Element of the carrier of (T . i)
Cl {(p . i)} is Element of K6( the carrier of (T . i))
Carrier T is Relation-like non-empty I -defined Function-like V18(I) set
product (Carrier T) is set
dom p is set
dom (Carrier T) is Element of K6(I)
K6(I) is non empty set
dom a is set
I is non empty set
T is non empty TopSpace-like T_0 T_1 TopStruct
I --> T is non empty Relation-like I -defined {T} -valued Function-like constant V18(I) quasi_total V365() non-Empty TopStruct-yielding Element of K6(K7(I,{T}))
{T} is non empty finite set
K7(I,{T}) is non empty Relation-like set
K6(K7(I,{T})) is non empty set
product (I --> T) is non empty strict TopSpace-like T_0 constituted-Functions TopStruct
p is Element of I
(I --> T) . p is non empty TopStruct
a is Element of I
(I --> T) . a is non empty TopStruct