:: WAYBEL26 semantic presentation

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