K99() is Element of bool K95()
K95() is set
bool K95() is non empty set
K54() is set
bool K54() is non empty set
bool K99() is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
K96() is set
K97() is set
K98() is set
[:K95(),K95():] is set
bool [:K95(),K95():] is non empty set
K407() is non empty V113() L9()
the carrier of K407() is non empty set
<REAL,+> is non empty V113() V135() V136() associative commutative left-invertible right-invertible V191() left-cancelable right-cancelable V194() L9()
K413() is non empty V113() associative commutative left-cancelable right-cancelable V194() SubStr of <REAL,+>
<NAT,+> is non empty V113() V135() associative commutative left-cancelable right-cancelable V194() uniquely-decomposable SubStr of K413()
<REAL,*> is non empty V113() V135() associative commutative L9()
<NAT,*> is non empty V113() V135() associative commutative uniquely-decomposable SubStr of <REAL,*>
{} is Function-like functional empty finite V45() set
the Function-like functional empty finite V45() set is Function-like functional empty finite V45() set
1 is non empty set
{{},1} is non empty finite set
K722() is set
{{}} is non empty finite V45() set
K378({{}}) is M19({{}})
[:K378({{}}),{{}}:] is set
bool [:K378({{}}),{{}}:] is non empty set
K39(K378({{}}),{{}}) is set
union {} is finite set
Sierpinski_Space is non empty strict TopSpace-like T_0 non T_1 injective monotone-convergence TopStruct
0 is Function-like functional empty finite V45() Element of K99()
{0,1} is non empty finite set
{1} is non empty finite set
{{},{1},{0,1}} is non empty finite set
BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() directed up-complete /\-complete V354() V361() V362() V363() RelStr
the topology of Sierpinski_Space is non empty Element of bool (bool the carrier of Sierpinski_Space)
the carrier of Sierpinski_Space is non empty set
bool the carrier of Sierpinski_Space is non empty set
bool (bool the carrier of Sierpinski_Space) is non empty set
bool 1 is non empty Element of bool (bool 1)
bool 1 is non empty set
bool (bool 1) is non empty set
id Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
[: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:] is non empty set
id the carrier of Sierpinski_Space is Relation-like the carrier of Sierpinski_Space -defined the carrier of Sierpinski_Space -valued Function-like one-to-one non empty V24( the carrier of Sierpinski_Space) quasi_total Element of bool [: the carrier of Sierpinski_Space, the carrier of Sierpinski_Space:]
X is set
X is set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty strict RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
S is set
F is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
S is set
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
the carrier of X is non empty set
the carrier of (Omega Y) is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
S is Relation-like Function-like Element of the carrier of (X,Y)
F is Relation-like Function-like Element of the carrier of (X,Y)
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
F is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
W is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
y is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
W1 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega Y):]
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
S is Element of the carrier of X
F is Element of bool the carrier of (X,Y)
pi (F,S) is set
the carrier of (Omega Y) is non empty set
bool the carrier of (Omega Y) is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
W is Element of bool the carrier of ((Omega Y) |^ the carrier of X)
pi (W,S) is Element of bool the carrier of (Omega Y)
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
S is set
F is non empty Element of bool the carrier of (X,Y)
pi (F,S) is set
the carrier of X is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
W is non empty Element of bool the carrier of ((Omega Y) |^ the carrier of X)
pi (W,S) is non empty set
Omega Sierpinski_Space is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict satisfying_axiom_of_approximation continuous TopRelStr
the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:] is non empty set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1:] is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 #) is strict RelStr
InclPoset (bool 1) is non empty strict reflexive transitive antisymmetric RelStr
the carrier of (BoolePoset 1) is non empty set
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1)
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1) is non empty set
Omega the non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict Scott monotone-convergence TopAugmentation of BoolePoset 1 is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete strict TopRelStr
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
the carrier of (InclPoset the topology of X) is non empty non trivial set
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (X,Sierpinski_Space) is non empty set
[: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
[: the carrier of X,{{},1}:] is non empty set
bool [: the carrier of X,{{},1}:] is non empty set
Y is Relation-like Function-like set
proj1 Y is set
proj2 Y is set
S is set
F is set
Y . F is set
F is Element of bool the carrier of X
chi (F, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
[: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
F is Element of the carrier of (InclPoset the topology of X)
W is Element of the carrier of (InclPoset the topology of X)
y is open Element of bool the carrier of X
chi (y, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W1 is open Element of bool the carrier of X
chi (W1, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
F is Relation-like the carrier of (InclPoset the topology of X) -defined the carrier of (X,Sierpinski_Space) -valued Function-like non empty V24( the carrier of (InclPoset the topology of X)) quasi_total Element of bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):]
F . F is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
F . W is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
[: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
bool [: the carrier of X, the carrier of Sierpinski_Space:] is non empty set
the carrier of (Omega Sierpinski_Space) is non empty set
[: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):] is non empty set
x is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
g1x is Relation-like the carrier of X -defined the carrier of (Omega Sierpinski_Space) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Sierpinski_Space):]
rng F is Element of bool the carrier of (X,Sierpinski_Space)
bool the carrier of (X,Sierpinski_Space) is non empty set
y is set
[#] Sierpinski_Space is non empty non proper closed Element of bool the carrier of Sierpinski_Space
W1 is Relation-like the carrier of X -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Sierpinski_Space:]
W is open Element of bool the carrier of Sierpinski_Space
W1 " W is Element of bool the carrier of X
chi ((W1 " W), the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
j is Element of the carrier of X
W1 . j is Element of the carrier of Sierpinski_Space
W2 is Relation-like the carrier of X -defined the carrier of Sierpinski_Space -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Sierpinski_Space:]
W2 . j is Element of the carrier of Sierpinski_Space
F . (W1 " W) is set
W is Element of the carrier of (InclPoset the topology of X)
F . W is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
y is Element of the carrier of (InclPoset the topology of X)
F . y is Relation-like Function-like Element of the carrier of (X,Sierpinski_Space)
W1 is Element of bool the carrier of X
chi (W1, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W2 is Element of bool the carrier of X
chi (W2, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
W is open Element of bool the carrier of X
F . W is set
chi (W, the carrier of X) is Relation-like the carrier of X -defined {{},1} -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X,{{},1}:]
X is non empty TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
the carrier of X is non empty set
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
InclPoset the topology of X is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete V319() V320() V321() up-complete /\-complete RelStr
(X,Sierpinski_Space) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (InclPoset the topology of X) is non empty non trivial set
the carrier of (X,Sierpinski_Space) is non empty set
[: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):] is non empty set
Y is Relation-like the carrier of (InclPoset the topology of X) -defined the carrier of (X,Sierpinski_Space) -valued Function-like non empty V24( the carrier of (InclPoset the topology of X)) quasi_total Element of bool [: the carrier of (InclPoset the topology of X), the carrier of (X,Sierpinski_Space):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
F is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
W is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
y is Relation-like Function-like Element of the carrier of (X,Y)
F . y is Relation-like Function-like Element of the carrier of (X,S)
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
W . y is Relation-like Function-like Element of the carrier of (X,S)
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
W is set
y is set
F . y is set
W1 is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W1 (#) F is Relation-like Function-like set
F * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
W is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
y is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
W . y is set
F * y is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
y (#) F is Relation-like Function-like set
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (S,X) is non empty set
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
F is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
W is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
y is Relation-like Function-like Element of the carrier of (S,X)
F . y is Relation-like Function-like Element of the carrier of (Y,X)
W1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
W . y is Relation-like Function-like Element of the carrier of (Y,X)
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
W is set
y is set
F . y is set
W1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
F (#) W1 is Relation-like Function-like set
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
W is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
y is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
W . y is set
y * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
F (#) y is Relation-like Function-like set
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of X is non empty set
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
F is Relation-like Function-like Element of the carrier of (X,Y)
W is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,S,F) . F is Relation-like Function-like Element of the carrier of (X,S)
(X,Y,S,F) . W is Relation-like Function-like Element of the carrier of (X,S)
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega S) is non empty set
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of (Omega Y):] is non empty set
bool [: the carrier of X, the carrier of (Omega Y):] is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
W1 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
y is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
y * W1 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of (Omega S) -valued the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 is Relation-like the carrier of X -defined the carrier of (Omega Y) -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega Y):]
y * W2 is Relation-like the carrier of X -defined the carrier of X -defined the carrier of (Omega S) -valued the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of (Omega S):]
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
g2x is set
a is Element of the carrier of X
(y * W2) . a is Element of the carrier of (Omega S)
W2 . a is Element of the carrier of (Omega Y)
y . (W2 . a) is Element of the carrier of (Omega S)
W1 . a is Element of the carrier of (Omega Y)
(y * W1) . a is Element of the carrier of (Omega S)
y . (W1 . a) is Element of the carrier of (Omega S)
b is Element of the carrier of (Omega Y)
A is Element of the carrier of (Omega Y)
(y * W1) . g2x is set
(y * W2) . g2x is set
x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
g1x is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
X is non empty TopSpace-like TopStruct
S is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(X,Y,Y,S) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,Y):] is non empty set
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) * (X,Y,Y,S) is Relation-like the carrier of (X,Y) -defined the carrier of (X,Y) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,Y):]
((X,Y,Y,S) * (X,Y,Y,S)) . F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) . F is Relation-like Function-like Element of the carrier of (X,Y)
(X,Y,Y,S) . ((X,Y,Y,S) . F) is Relation-like Function-like Element of the carrier of (X,Y)
W is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
S * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
(X,Y,Y,S) . (S * W) is set
S * (S * W) is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
S * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(S * S) * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
the carrier of (S,X) is non empty set
the carrier of (Y,X) is non empty set
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
F is Relation-like Function-like Element of the carrier of (S,X)
W is Relation-like Function-like Element of the carrier of (S,X)
(X,Y,S,F) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,S,F) . W is Relation-like Function-like Element of the carrier of (Y,X)
the carrier of (Omega X) is non empty set
[: the carrier of S, the carrier of (Omega X):] is non empty set
bool [: the carrier of S, the carrier of (Omega X):] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
the carrier of (Omega S) is non empty set
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
W1 is Relation-like the carrier of S -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of (Omega X):]
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
j is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
j (#) W1 is Relation-like Function-like set
y is Relation-like the carrier of S -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of (Omega X):]
j (#) y is Relation-like Function-like set
[: the carrier of Y, the carrier of (Omega X):] is non empty set
bool [: the carrier of Y, the carrier of (Omega X):] is non empty set
g2x is set
y * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of (Omega X) -valued the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of (Omega X):]
a is Element of the carrier of Y
(y * F) . a is Element of the carrier of (Omega X)
F . a is Element of the carrier of S
y . (F . a) is Element of the carrier of (Omega X)
W1 * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of (Omega X) -valued the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of (Omega X):]
(W1 * F) . a is Element of the carrier of (Omega X)
W1 . (F . a) is Element of the carrier of (Omega X)
(y * F) . g2x is set
(W1 * F) . g2x is set
x is Relation-like the carrier of Y -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of (Omega X):]
g1x is Relation-like the carrier of Y -defined the carrier of (Omega X) -valued Function-like non empty V24( the carrier of Y) quasi_total Element of bool [: the carrier of Y, the carrier of (Omega X):]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of Y, the carrier of Y:] is non empty set
bool [: the carrier of Y, the carrier of Y:] is non empty set
X is non empty TopSpace-like TopStruct
S is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
(X,Y,Y,S) is Relation-like the carrier of (Y,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (Y,X)) quasi_total Element of bool [: the carrier of (Y,X), the carrier of (Y,X):]
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
[: the carrier of (Y,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (Y,X), the carrier of (Y,X):] is non empty set
the carrier of X is non empty set
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) * (X,Y,Y,S) is Relation-like the carrier of (Y,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (Y,X)) quasi_total Element of bool [: the carrier of (Y,X), the carrier of (Y,X):]
((X,Y,Y,S) * (X,Y,Y,S)) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) . F is Relation-like Function-like Element of the carrier of (Y,X)
(X,Y,Y,S) . ((X,Y,Y,S) . F) is Relation-like Function-like Element of the carrier of (Y,X)
W is Relation-like the carrier of Y -defined the carrier of X -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
W * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
(X,Y,Y,S) . (W * S) is set
(W * S) * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
S * S is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of Y -valued the carrier of Y -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of Y:]
W * (S * S) is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,Y) is non empty set
bool the carrier of (X,Y) is non empty set
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (X,S) is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
W is Element of the carrier of X
y is Element of bool the carrier of (X,Y)
(X,Y,S,F) .: y is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
(X,S,W,((X,Y,S,F) .: y)) is Element of bool the carrier of (Omega S)
the carrier of (Omega S) is non empty set
bool the carrier of (Omega S) is non empty set
(X,Y,W,y) is Element of bool the carrier of (Omega Y)
the carrier of (Omega Y) is non empty set
bool the carrier of (Omega Y) is non empty set
F .: (X,Y,W,y) is Element of bool the carrier of S
bool the carrier of S is non empty set
W1 is set
W2 is Relation-like Function-like set
W2 . W is set
j is set
(X,Y,S,F) . j is set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
x . W is Element of the carrier of Y
F . (x . W) is Element of the carrier of S
W1 is set
W2 is set
F . W2 is set
j is Relation-like Function-like set
j . W is set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
x is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * x is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(X,Y,S,F) . x is set
(F * x) . W is Element of the carrier of S
X is non empty TopSpace-like TopStruct
Y is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
(X,Y) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega Y is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (X,Y) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (X,Y)) quasi_total Element of bool [: the carrier of (X,Y), the carrier of (X,S):]
the carrier of (X,Y) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool [: the carrier of (X,Y), the carrier of (X,S):] is non empty set
bool the carrier of (X,Y) is non empty set
F is Element of bool the carrier of (X,Y)
the carrier of X is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
"\/" (F,(X,Y)) is Relation-like Function-like Element of the carrier of (X,Y)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
(X,Y,S,F) .: F is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
"\/" (((X,Y,S,F) .: F),(X,S)) is Relation-like Function-like Element of the carrier of (X,S)
(X,Y,S,F) . ("\/" (F,(X,Y))) is Relation-like Function-like Element of the carrier of (X,S)
(Omega S) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
x is non empty directed Element of bool the carrier of (X,Y)
(X,Y,S,F) .: x is non empty Element of bool the carrier of (X,S)
(Omega Y) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of ((Omega Y) |^ the carrier of X) is non empty set
bool the carrier of ((Omega Y) |^ the carrier of X) is non empty set
a is non empty directed Element of bool the carrier of g2x
j is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of X
the carrier of j is non empty set
bool the carrier of j is non empty set
g1x is non empty directed Element of bool the carrier of (X,S)
the carrier of ((Omega S) |^ the carrier of X) is non empty set
bool the carrier of ((Omega S) |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of X --> (Omega Y) is Relation-like the carrier of X -defined {(Omega Y)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega Y)}:]
{(Omega Y)} is non empty finite set
[: the carrier of X,{(Omega Y)}:] is non empty set
bool [: the carrier of X,{(Omega Y)}:] is non empty set
the carrier of X --> (Omega S) is Relation-like the carrier of X -defined {(Omega S)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega S)}:]
{(Omega S)} is non empty finite set
[: the carrier of X,{(Omega S)}:] is non empty set
bool [: the carrier of X,{(Omega S)}:] is non empty set
the topology of Y is non empty Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty set
bool (bool the carrier of Y) is non empty set
TopStruct(# the carrier of Y, the topology of Y #) is non empty strict TopSpace-like TopStruct
the carrier of (Omega Y) is non empty set
the topology of (Omega Y) is non empty Element of bool (bool the carrier of (Omega Y))
bool the carrier of (Omega Y) is non empty set
bool (bool the carrier of (Omega Y)) is non empty set
TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) is non empty strict TopSpace-like TopStruct
the topology of S is non empty Element of bool (bool the carrier of S)
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set
TopStruct(# the carrier of S, the topology of S #) is non empty strict TopSpace-like TopStruct
the topology of (Omega S) is non empty Element of bool (bool the carrier of (Omega S))
bool the carrier of (Omega S) is non empty set
bool (bool the carrier of (Omega S)) is non empty set
TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) is non empty strict TopSpace-like TopStruct
[: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
bool [: the carrier of (Omega Y), the carrier of (Omega S):] is non empty set
hh is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of X)
"\/" (hh,((Omega S) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of X)
product ( the carrier of X --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega S))) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> (Omega S)) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega S)))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c1)
the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
product ( the carrier of X --> (Omega Y)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega Y))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega Y))) is non empty set
b is non empty directed Element of bool the carrier of ((Omega Y) |^ the carrier of X)
"\/" (b,((Omega Y) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega Y) |^ the carrier of X)
c is Element of the carrier of X
( the carrier of X --> (Omega Y)) . c is non empty reflexive transitive antisymmetric RelStr
c1 is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega Y)))
pi (c1,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega Y)) . c)
( the carrier of X --> (Omega Y)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega Y)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega Y)) . c) is non empty set
( the carrier of X --> (Omega S)) . c is non empty reflexive transitive antisymmetric RelStr
b is non empty directed Element of bool the carrier of (Omega Y)
"\/" (c1,(product ( the carrier of X --> (Omega Y)))) is Relation-like Function-like Element of the carrier of (product ( the carrier of X --> (Omega Y)))
("\/" (c1,(product ( the carrier of X --> (Omega Y))))) . c is Element of the carrier of (( the carrier of X --> (Omega Y)) . c)
"\/" ((pi (c1,c)),(( the carrier of X --> (Omega Y)) . c)) is Element of the carrier of (( the carrier of X --> (Omega Y)) . c)
Q is Relation-like the carrier of (Omega Y) -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of (Omega Y)) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of (Omega Y), the carrier of (Omega S):]
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c)
( the carrier of X --> (Omega S)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
Q .: b is non empty Element of bool the carrier of (Omega S)
W1 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W1 . c is Element of the carrier of (Omega S)
"\/" ((pi (Q,c)),(( the carrier of X --> (Omega S)) . c)) is Element of the carrier of (( the carrier of X --> (Omega S)) . c)
"\/" (b,(Omega Y)) is Element of the carrier of (Omega Y)
F . ("\/" (b,(Omega Y))) is set
W is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
F * W is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(F * W) . c is Element of the carrier of S
W2 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 . c is Element of the carrier of (Omega S)
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
X is non empty TopSpace-like TopStruct
(S,X) is non empty constituted-Functions strict reflexive transitive RelStr
Omega X is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (S,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (S,X) is non empty set
bool the carrier of (S,X) is non empty set
(Y,X) is non empty constituted-Functions strict reflexive transitive RelStr
ContMaps (Y,(Omega X)) is non empty constituted-Functions strict reflexive transitive RelStr
the carrier of (Y,X) is non empty set
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
(X,Y,S,F) is Relation-like the carrier of (S,X) -defined the carrier of (Y,X) -valued Function-like non empty V24( the carrier of (S,X)) quasi_total Element of bool [: the carrier of (S,X), the carrier of (Y,X):]
[: the carrier of (S,X), the carrier of (Y,X):] is non empty set
bool [: the carrier of (S,X), the carrier of (Y,X):] is non empty set
W is Element of the carrier of Y
F . W is Element of the carrier of S
y is Element of bool the carrier of (S,X)
(X,Y,S,F) .: y is Element of bool the carrier of (Y,X)
bool the carrier of (Y,X) is non empty set
(Y,X,W,((X,Y,S,F) .: y)) is Element of bool the carrier of (Omega X)
the carrier of (Omega X) is non empty set
bool the carrier of (Omega X) is non empty set
(S,X,(F . W),y) is Element of bool the carrier of (Omega X)
W1 is set
W2 is Relation-like Function-like set
W2 . W is set
j is set
(X,Y,S,F) . j is set
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
x is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
x * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
x . (F . W) is Element of the carrier of X
W1 is set
W2 is Relation-like Function-like set
W2 . (F . W) is set
the carrier of X is non empty set
[: the carrier of S, the carrier of X:] is non empty set
bool [: the carrier of S, the carrier of X:] is non empty set
j is Relation-like the carrier of S -defined the carrier of X -valued Function-like non empty V24( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of X:]
j * F is Relation-like the carrier of Y -defined the carrier of Y -defined the carrier of X -valued the carrier of X -valued Function-like non empty V24( the carrier of Y) V24( the carrier of Y) quasi_total quasi_total continuous Element of bool [: the carrier of Y, the carrier of X:]
[: the carrier of Y, the carrier of X:] is non empty set
bool [: the carrier of Y, the carrier of X:] is non empty set
(X,Y,S,F) . j is set
(j * F) . W is Element of the carrier of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
Y is non empty TopSpace-like TopStruct
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
S is non empty TopSpace-like T_0 monotone-convergence TopStruct
(Y,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
Omega S is non empty TopSpace-like reflexive transitive antisymmetric up-complete strict TopRelStr
ContMaps (Y,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
(X,S) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
F is Relation-like the carrier of X -defined the carrier of Y -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of Y:]
(S,X,Y,F) is Relation-like the carrier of (Y,S) -defined the carrier of (X,S) -valued Function-like non empty V24( the carrier of (Y,S)) quasi_total Element of bool [: the carrier of (Y,S), the carrier of (X,S):]
the carrier of (Y,S) is non empty set
the carrier of (X,S) is non empty set
[: the carrier of (Y,S), the carrier of (X,S):] is non empty set
bool [: the carrier of (Y,S), the carrier of (X,S):] is non empty set
bool the carrier of (Y,S) is non empty set
F is Element of bool the carrier of (Y,S)
the carrier of S is non empty set
[: the carrier of Y, the carrier of S:] is non empty set
bool [: the carrier of Y, the carrier of S:] is non empty set
"\/" (F,(Y,S)) is Relation-like Function-like Element of the carrier of (Y,S)
the carrier of (Omega S) is non empty set
[: the carrier of X, the carrier of (Omega S):] is non empty set
bool [: the carrier of X, the carrier of (Omega S):] is non empty set
(S,X,Y,F) .: F is Element of bool the carrier of (X,S)
bool the carrier of (X,S) is non empty set
"\/" (((S,X,Y,F) .: F),(X,S)) is Relation-like Function-like Element of the carrier of (X,S)
(S,X,Y,F) . ("\/" (F,(Y,S))) is Relation-like Function-like Element of the carrier of (X,S)
(Omega S) |^ the carrier of X is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
x is non empty directed Element of bool the carrier of (Y,S)
(S,X,Y,F) .: x is non empty Element of bool the carrier of (X,S)
(Omega S) |^ the carrier of Y is non empty constituted-Functions strict reflexive transitive antisymmetric up-complete RelStr
g2x is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of Y
the carrier of g2x is non empty set
bool the carrier of g2x is non empty set
the carrier of ((Omega S) |^ the carrier of Y) is non empty set
bool the carrier of ((Omega S) |^ the carrier of Y) is non empty set
a is non empty directed Element of bool the carrier of g2x
j is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of (Omega S) |^ the carrier of X
the carrier of j is non empty set
bool the carrier of j is non empty set
g1x is non empty directed Element of bool the carrier of (X,S)
the carrier of ((Omega S) |^ the carrier of X) is non empty set
bool the carrier of ((Omega S) |^ the carrier of X) is non empty set
A is non empty directed Element of bool the carrier of j
the carrier of Y --> (Omega S) is Relation-like the carrier of Y -defined {(Omega S)} -valued Function-like non empty V24( the carrier of Y) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of Y,{(Omega S)}:]
{(Omega S)} is non empty finite set
[: the carrier of Y,{(Omega S)}:] is non empty set
bool [: the carrier of Y,{(Omega S)}:] is non empty set
the carrier of X --> (Omega S) is Relation-like the carrier of X -defined {(Omega S)} -valued Function-like non empty V24( the carrier of X) quasi_total RelStr-yielding V384() non-Empty reflexive-yielding TopStruct-yielding Poset-yielding Element of bool [: the carrier of X,{(Omega S)}:]
[: the carrier of X,{(Omega S)}:] is non empty set
bool [: the carrier of X,{(Omega S)}:] is non empty set
hh is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of X)
"\/" (hh,((Omega S) |^ the carrier of X)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of X)
product ( the carrier of X --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of X --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of X --> (Omega S))) is non empty set
c1 is Element of the carrier of X
( the carrier of X --> (Omega S)) . c1 is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c1 is non empty reflexive RelStr
Q is functional non empty directed Element of bool the carrier of (product ( the carrier of X --> (Omega S)))
pi (Q,c1) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c1)
the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c1) is non empty set
product ( the carrier of Y --> (Omega S)) is non empty constituted-Functions strict reflexive transitive antisymmetric RelStr
the carrier of (product ( the carrier of Y --> (Omega S))) is functional non empty set
bool the carrier of (product ( the carrier of Y --> (Omega S))) is non empty set
b is non empty directed Element of bool the carrier of ((Omega S) |^ the carrier of Y)
"\/" (b,((Omega S) |^ the carrier of Y)) is Relation-like Function-like Element of the carrier of ((Omega S) |^ the carrier of Y)
c is Element of the carrier of X
F . c is Element of the carrier of Y
( the carrier of Y --> (Omega S)) . (F . c) is non empty reflexive transitive antisymmetric RelStr
( the carrier of X --> (Omega S)) . c is non empty reflexive transitive antisymmetric RelStr
pi (Q,c) is non empty Element of bool the carrier of (( the carrier of X --> (Omega S)) . c)
( the carrier of X --> (Omega S)) . c is non empty reflexive RelStr
the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
bool the carrier of (( the carrier of X --> (Omega S)) . c) is non empty set
c1 is functional non empty directed Element of bool the carrier of (product ( the carrier of Y --> (Omega S)))
pi (c1,(F . c)) is non empty Element of bool the carrier of (( the carrier of Y --> (Omega S)) . (F . c))
( the carrier of Y --> (Omega S)) . (F . c) is non empty reflexive RelStr
the carrier of (( the carrier of Y --> (Omega S)) . (F . c)) is non empty set
bool the carrier of (( the carrier of Y --> (Omega S)) . (F . c)) is non empty set
W1 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W1 . c is Element of the carrier of (Omega S)
"\/" ((pi (Q,c)),(( the carrier of X --> (Omega S)) . c)) is Element of the carrier of (( the carrier of X --> (Omega S)) . c)
"\/" (c1,(product ( the carrier of Y --> (Omega S)))) is Relation-like Function-like Element of the carrier of (product ( the carrier of Y --> (Omega S)))
("\/" (c1,(product ( the carrier of Y --> (Omega S))))) . (F . c) is Element of the carrier of (( the carrier of Y --> (Omega S)) . (F . c))
W is Relation-like the carrier of Y -defined the carrier of S -valued Function-like non empty V24( the carrier of Y) quasi_total continuous Element of bool [: the carrier of Y, the carrier of S:]
W * F is Relation-like the carrier of X -defined the carrier of X -defined the carrier of S -valued the carrier of S -valued Function-like non empty V24( the carrier of X) V24( the carrier of X) quasi_total quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
(W * F) . c is Element of the carrier of S
W2 is Relation-like the carrier of X -defined the carrier of (Omega S) -valued Function-like non empty V24( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of (Omega S):]
W2 . c is Element of the carrier of (Omega S)
Y is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
(X,Y) is non empty constituted-Functions strict reflexive transitive RelStr
Omega Y is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega Y)) is non empty constituted-Functions strict reflexive transitive RelStr
S is non empty TopSpace-like SubSpace of Y
(X,S) is non empty constituted-Functions strict reflexive transitive RelStr
Omega S is non empty TopSpace-like reflexive transitive strict TopRelStr
ContMaps (X,(Omega S)) is non empty constituted-Functions strict reflexive transitive RelStr
[#] S is non empty non proper closed Element of bool the carrier of S
the carrier of S is non empty set
bool the carrier of S is non empty set
[#] Y is non empty non proper closed Element of bool the carrier of Y
the carrier of Y is non empty set
bool the carrier of Y is non empty set
the carrier of (X,S) is non empty set
the carrier of (X,Y) is non empty set
W is set
the carrier of X is non empty set
[: the carrier of X, the carrier of S:] is non empty set
bool [: the carrier of X, the carrier of S:] is non empty set
y is Relation-like the carrier of X -defined the carrier of S -valued Function-like non empty V24( the carrier of X) quasi_total continuous Element of bool [: the carrier of X, the carrier of S:]
dom y is Element of bool the carrier of X
bool the carrier of X is non empty set
rng y is Element of bool the carrier of S
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty