:: 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

dom c

(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