:: WAYBEL27 semantic presentation

K181() is Element of bool K177()

K177() is set

bool K177() is non empty set

K147() is set

bool K147() is non empty set

bool K181() is non empty set

K178() is set

K179() is set

K180() is set

[:K177(),K177():] is Relation-like set

bool [:K177(),K177():] is non empty set

K348() is non empty V102() L9()

the carrier of K348() is non empty set

<REAL,+> is non empty V102() V124() V125() associative commutative left-invertible right-invertible V180() left-cancelable right-cancelable V183() L9()

K354() is non empty V102() associative commutative left-cancelable right-cancelable V183() SubStr of <REAL,+>

<NAT,+> is non empty V102() V124() associative commutative left-cancelable right-cancelable V183() uniquely-decomposable SubStr of K354()

<REAL,*> is non empty V102() V124() associative commutative L9()

<NAT,*> is non empty V102() V124() associative commutative uniquely-decomposable SubStr of <REAL,*>

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() set

1 is non empty set

{{},1} is non empty set

K658() is set

{{}} is non empty functional set

K319({{}}) is M12({{}})

[:K319({{}}),{{}}:] is Relation-like set

bool [:K319({{}}),{{}}:] is non empty set

K98(K319({{}}),{{}}) is non empty functional set

[:1,1:] is non empty Relation-like set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty Relation-like set

bool [:[:1,1:],1:] is non empty set

id {{}} is non empty Relation-like {{}} -defined {{}} -valued Function-like one-to-one V19() V21() V22() V26() V27({{}}) quasi_total onto bijective Function-yielding V33() Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is non empty Relation-like set

bool [:{{}},{{}}:] is non empty set

RelStr(# {{}},(id {{}}) #) is non empty trivial V56() 1 -element strict RelStr

Sierpinski_Space is non empty strict TopSpace-like T_0 non T_1 V381() monotone-convergence TopStruct

Omega Sierpinski_Space is non empty TopSpace-like reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict V375() continuous non void TopRelStr

BoolePoset 1 is non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean RelStr

proj1 {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() set

proj2 {} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() V185() set

commute {} is Relation-like Function-like Function-yielding V33() set

K377(1) is non empty Element of bool (bool 1)

bool 1 is non empty set

bool (bool 1) is non empty set

0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() Element of K181()

{0,1} is non empty set

{1} is non empty set

K5({},{1},{0,1}) is non empty set

the topology of Sierpinski_Space is 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 {} is non empty set

curry {} is Relation-like Function-like set

curry' {} is Relation-like Function-like set

R is Relation-like Function-like set

proj1 R is set

S is set

S is Relation-like Function-like set

R . S is set

uncurry S is Relation-like Function-like set

S is set

proj1 S is set

S is Relation-like Function-like set

R . S is set

curry S is Relation-like Function-like set

S is set

S is Relation-like Function-like set

R . S is set

commute S is Relation-like Function-like Function-yielding V33() set

R is Relation-like Function-like set

R is Relation-like Function-like () set

S is set

R | S is Relation-like Function-like set

proj1 (R | S) is set

T is Relation-like Function-like set

(R | S) . T is set

uncurry T is Relation-like Function-like set

proj1 R is set

R . T is set

T is set

proj1 R is set

R is Relation-like Function-like () set

S is set

R | S is Relation-like Function-like set

proj1 (R | S) is set

T is Relation-like Function-like set

(R | S) . T is set

curry T is Relation-like Function-like set

proj1 R is set

R . T is set

T is set

proj1 T is set

proj1 R is set

F is set

R is set

S is set

T is set

Funcs (S,T) is functional set

Funcs (R,(Funcs (S,T))) is functional set

[:R,S:] is Relation-like set

Funcs ([:R,S:],T) is functional set

F is Relation-like F -defined Function-like V27(F) set

proj2 F is set

F is non empty functional set

G is Relation-like F -defined Function-like V27(F) set

G is Relation-like F -defined Function-like V27(F) set

proj2 G is set

x is set

dom G is Element of bool F

bool F is non empty set

f is Relation-like Function-like set

proj1 f is set

proj2 f is set

x is set

f . x is set

proj1 G is set

x is Relation-like Function-like set

G . x is set

uncurry x is Relation-like Function-like set

f is Relation-like Function-like Element of F

G . f is set

x is set

dom G is Element of bool F

bool F is non empty set

f is set

G . f is set

x is Relation-like Function-like Element of F

uncurry x is Relation-like Function-like set

F is set

R is set

S is set

[:R,S:] is Relation-like set

T is set

Funcs ([:R,S:],T) is functional set

Funcs (S,T) is functional set

Funcs (R,(Funcs (S,T))) is functional set

F is Relation-like F -defined Function-like V27(F) set

proj2 F is set

F is non empty functional set

G is Relation-like F -defined Function-like V27(F) set

G is Relation-like F -defined Function-like V27(F) set

proj2 G is set

x is set

dom G is Element of bool F

bool F is non empty set

proj1 x is set

f is Relation-like Function-like set

proj1 f is set

proj2 f is set

proj1 G is set

x is Relation-like Function-like set

G . x is set

curry x is Relation-like Function-like set

f is Relation-like Function-like Element of F

G . f is set

x is set

dom G is Element of bool F

bool F is non empty set

f is set

G . f is set

x is Relation-like Function-like Element of F

curry x is Relation-like Function-like set

[:{},T:] is Relation-like set

bool [:{},T:] is non empty set

[:R,(Funcs (S,T)):] is Relation-like set

bool [:R,(Funcs (S,T)):] is non empty set

R is set

S is set

T is set

Funcs (S,T) is functional set

Funcs (R,(Funcs (S,T))) is functional set

[:R,S:] is Relation-like set

Funcs ([:R,S:],T) is functional set

F is Relation-like Funcs (R,(Funcs (S,T))) -defined Function-like V27( Funcs (R,(Funcs (S,T)))) set

proj2 F is set

[:R,S:] is Relation-like set

Funcs ([:R,S:],T) is functional set

F is Relation-like Funcs ([:R,S:],T) -defined Function-like V27( Funcs ([:R,S:],T)) set

proj2 F is set

R is non empty set

S is non empty set

T is set

Funcs (S,T) is functional set

Funcs (R,(Funcs (S,T))) is functional set

F is Relation-like Function-like () set

proj1 F is set

proj2 F is set

F is Relation-like Function-like () set

proj1 F is set

F * F is Relation-like Function-like set

id (proj1 F) is Relation-like proj1 F -defined proj1 F -valued Function-like one-to-one V19() V21() V22() V26() V27( proj1 F) quasi_total onto bijective Element of bool [:(proj1 F),(proj1 F):]

[:(proj1 F),(proj1 F):] is Relation-like set

bool [:(proj1 F),(proj1 F):] is non empty set

G is set

F . G is set

(F * F) . G is set

F . (F . G) is set

x is Relation-like Function-like set

commute x is Relation-like Function-like Function-yielding V33() set

G is Relation-like Function-like set

commute G is Relation-like Function-like Function-yielding V33() set

commute (commute G) is Relation-like Function-like Function-yielding V33() set

proj1 (F * F) is set

R is non empty set

S is set

T is set

Funcs (R,T) is functional set

Funcs (S,(Funcs (R,T))) is functional set

F is Relation-like Function-like () set

proj1 F is set

proj2 F is set

id (proj1 F) is Relation-like proj1 F -defined proj1 F -valued Function-like one-to-one V19() V21() V22() V26() V27( proj1 F) quasi_total onto bijective Element of bool [:(proj1 F),(proj1 F):]

[:(proj1 F),(proj1 F):] is Relation-like set

bool [:(proj1 F),(proj1 F):] is non empty set

F is Relation-like Function-like () set

proj1 F is set

F * F is Relation-like Function-like set

G is set

G is Relation-like Function-like set

F . G is set

(F * F) . G is set

F . (F . G) is set

x is Relation-like Function-like set

curry x is Relation-like Function-like set

uncurry G is Relation-like Function-like set

curry (uncurry G) is Relation-like Function-like set

f is Relation-like Function-like set

proj1 f is set

proj2 f is set

proj1 (F * F) is set

R is set

S is set

[:R,S:] is Relation-like set

T is set

Funcs ([:R,S:],T) is functional set

F is Relation-like Function-like () set

proj1 F is set

proj2 F is set

id (proj1 F) is Relation-like proj1 F -defined proj1 F -valued Function-like one-to-one V19() V21() V22() V26() V27( proj1 F) quasi_total onto bijective Element of bool [:(proj1 F),(proj1 F):]

[:(proj1 F),(proj1 F):] is Relation-like set

bool [:(proj1 F),(proj1 F):] is non empty set

F is Relation-like Function-like () set

proj1 F is set

F * F is Relation-like Function-like set

G is set

G is Relation-like Function-like set

F . G is set

(F * F) . G is set

F . (F . G) is set

x is Relation-like Function-like set

uncurry x is Relation-like Function-like set

curry G is Relation-like Function-like set

uncurry (curry G) is Relation-like Function-like set

f is Relation-like Function-like set

proj1 f is set

proj2 f is set

proj1 (F * F) is set

R is Relation-like Function-like Function-yielding V33() set

commute R is Relation-like Function-like Function-yielding V33() set

proj1 (commute R) is set

S is set

(commute R) . S is Relation-like Function-like set

T is set

((commute R) . S) .: T is set

R .: T is set

pi ((R .: T),S) is set

uncurry R is Relation-like Function-like set

curry' (uncurry R) is Relation-like Function-like set

~ (uncurry R) is Relation-like Function-like set

curry (~ (uncurry R)) is Relation-like Function-like set

F is set

proj1 ((commute R) . S) is set

F is set

((commute R) . S) . F is set

[S,F] is V1() set

{S,F} is non empty set

{S} is non empty set

{{S,F},{S}} is non empty set

proj1 (~ (uncurry R)) is set

[F,S] is V1() set

{F,S} is non empty set

{F} is non empty set

{{F,S},{F}} is non empty set

proj1 (uncurry R) is set

proj1 R is set

G is set

x is set

[G,x] is V1() set

{G,x} is non empty set

{G} is non empty set

{{G,x},{G}} is non empty set

G is Relation-like Function-like set

R . G is Relation-like Function-like set

proj1 G is set

R . F is Relation-like Function-like set

[F,S] `2 is set

[F,S] `1 is set

(~ (uncurry R)) . (S,F) is set

(~ (uncurry R)) . [S,F] is set

(uncurry R) . (F,S) is set

(uncurry R) . [F,S] is set

(R . F) . S is set

R is Relation-like Function-like Function-yielding V33() set

commute R is Relation-like Function-like Function-yielding V33() set

T is set

R .: T is set

S is set

pi ((R .: T),S) is set

(commute R) . S is Relation-like Function-like set

((commute R) . S) .: T is set

F is set

F is Relation-like Function-like set

F . S is set

proj1 R is set

G is set

R . G is Relation-like Function-like set

proj1 F is set

[G,S] is V1() set

{G,S} is non empty set

{G} is non empty set

{{G,S},{G}} is non empty set

uncurry R is Relation-like Function-like set

proj1 (uncurry R) is set

[S,G] is V1() set

{S,G} is non empty set

{S} is non empty set

{{S,G},{S}} is non empty set

~ (uncurry R) is Relation-like Function-like set

proj1 (~ (uncurry R)) is set

proj1 (proj1 (~ (uncurry R))) is set

curry (~ (uncurry R)) is Relation-like Function-like set

proj1 (curry (~ (uncurry R))) is set

proj2 (proj1 (~ (uncurry R))) is set

[:{S},(proj2 (proj1 (~ (uncurry R)))):] is Relation-like set

(proj1 (~ (uncurry R))) /\ [:{S},(proj2 (proj1 (~ (uncurry R)))):] is Relation-like set

proj2 ((proj1 (~ (uncurry R))) /\ [:{S},(proj2 (proj1 (~ (uncurry R)))):]) is set

[G,S] `2 is set

[G,S] `1 is set

curry' (uncurry R) is Relation-like Function-like set

(curry (~ (uncurry R))) . S is set

proj1 ((commute R) . S) is set

G is Relation-like Function-like set

proj1 G is set

((commute R) . S) . G is set

(~ (uncurry R)) . (S,G) is set

(~ (uncurry R)) . [S,G] is set

(uncurry R) . (G,S) is set

(uncurry R) . [G,S] is set

G is Relation-like Function-like set

proj1 G is set

R is set

S is set

Funcs (R,S) is functional set

T is Relation-like Function-like set

proj2 T is set

commute T is Relation-like Function-like Function-yielding V33() set

proj1 T is set

Funcs ((proj1 T),(Funcs (R,S))) is functional set

F is set

T . F is set

F is set

(commute T) . F is Relation-like Function-like set

F is set

((commute T) . F) .: F is set

T .: F is set

pi ((T .: F),F) is set

Funcs ((proj1 T),S) is functional set

Funcs (R,(Funcs ((proj1 T),S))) is functional set

G is Relation-like Function-like set

proj1 G is set

proj2 G is set

G is Relation-like Function-like set

proj1 G is set

G is Relation-like Function-like set

proj1 G is set

proj2 G is set

R is Relation-like Function-like set

proj1 R is set

curry R is Relation-like Function-like set

T is set

S is set

{S} is non empty set

[:T,{S}:] is Relation-like set

(curry R) .: T is set

pi (((curry R) .: T),S) is set

R .: [:T,{S}:] is set

F is set

F is Relation-like Function-like set

F . S is set

proj1 (curry R) is set

G is set

(curry R) . G is set

[G,S] is V1() set

{G,S} is non empty set

{G} is non empty set

{{G,S},{G}} is non empty set

R . (G,S) is set

R . [G,S] is set

F is set

F is set

R . F is set

G is set

G is set

[G,G] is V1() set

{G,G} is non empty set

{G} is non empty set

{{G,G},{G}} is non empty set

(curry R) . G is set

proj1 (curry R) is set

x is Relation-like Function-like set

R . (G,G) is set

R . [G,G] is set

x . S is set

R is constituted-Functions 1-sorted

the carrier of R is set

S is set

the non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr |^ {} is non empty trivial V56() 1 -element constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic arithmetic connected up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean RelStr

the non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr |^ {} is non empty trivial V56() 1 -element constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic arithmetic connected up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean RelStr

R is non empty constituted-Functions RelStr

S is non empty SubRelStr of R

the carrier of S is non empty set

T is Element of the carrier of S

the carrier of R is non empty functional set

S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the carrier of S is non empty set

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the carrier of R is non empty set

T is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V27( the carrier of S) quasi_total idempotent Element of bool [: the carrier of S, the carrier of S:]

Image T is non empty strict reflexive transitive antisymmetric full non void SubRelStr of S

rng T is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

subrelstr (rng T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of S

the carrier of (Image T) is non empty set

[: the carrier of R, the carrier of (Image T):] is non empty Relation-like set

bool [: the carrier of R, the carrier of (Image T):] is non empty set

F is non empty Relation-like the carrier of R -defined the carrier of (Image T) -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of (Image T):]

T * F is Relation-like the carrier of R -defined the carrier of S -valued Function-like Element of bool [: the carrier of R, the carrier of S:]

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

rng F is non empty Element of bool the carrier of (Image T)

bool the carrier of (Image T) is non empty set

T * T is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of S:]

dom T is non empty Element of bool the carrier of S

R is non empty RelStr

the carrier of R is non empty set

S is non empty RelStr

T is non empty RelStr

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

the carrier of T is non empty set

[: the carrier of R, the carrier of T:] is non empty Relation-like set

bool [: the carrier of R, the carrier of T:] is non empty set

F is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]

F is non empty Relation-like the carrier of R -defined the carrier of T -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]

G is Element of the carrier of R

G is Element of the carrier of R

F . G is Element of the carrier of T

F . G is Element of the carrier of T

F . G is Element of the carrier of S

F . G is Element of the carrier of S

R is non empty RelStr

the carrier of R is non empty set

S is non empty RelStr

T is non empty RelStr

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

the carrier of T is non empty set

[: the carrier of R, the carrier of T:] is non empty Relation-like set

bool [: the carrier of R, the carrier of T:] is non empty set

F is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]

F is non empty Relation-like the carrier of R -defined the carrier of T -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]

G is Element of the carrier of R

G is Element of the carrier of R

F . G is Element of the carrier of S

F . G is Element of the carrier of S

F . G is Element of the carrier of T

F . G is Element of the carrier of T

{0} is non empty functional set

R is set

bool R is non empty set

S is Element of bool R

chi (S,R) is Relation-like R -defined {{},1} -valued Function-like V27(R) quasi_total Element of bool [:R,{{},1}:]

[:R,{{},1}:] is Relation-like set

bool [:R,{{},1}:] is non empty set

(chi (S,R)) " {1} is Element of bool R

(chi (S,R)) " {0} is Element of bool R

R \ S is Element of bool R

T is set

(chi (S,R)) . T is set

T is set

(chi (S,R)) . T is set

dom (chi (S,R)) is Element of bool R

T is set

(chi (S,R)) . T is set

T is set

(chi (S,R)) . T is set

dom (chi (S,R)) is Element of bool R

R is non empty set

S is non empty RelStr

S |^ R is non empty constituted-Functions strict RelStr

the carrier of (S |^ R) is non empty functional set

T is Relation-like Function-like Element of the carrier of (S |^ R)

F is Element of R

T . F is set

the carrier of S is non empty set

R --> S is non empty Relation-like R -defined {S} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() Element of bool [:R,{S}:]

{S} is non empty set

[:R,{S}:] is non empty Relation-like set

bool [:R,{S}:] is non empty set

product (R --> S) is non empty constituted-Functions strict RelStr

the carrier of (product (R --> S)) is non empty functional set

F is Relation-like Function-like Element of the carrier of (product (R --> S))

F . F is Element of the carrier of ((R --> S) . F)

(R --> S) . F is non empty RelStr

the carrier of ((R --> S) . F) is non empty set

R is non empty set

S is non empty RelStr

S |^ R is non empty constituted-Functions strict RelStr

the carrier of (S |^ R) is non empty functional set

T is Relation-like Function-like Element of the carrier of (S |^ R)

F is Relation-like Function-like Element of the carrier of (S |^ R)

R --> S is non empty Relation-like R -defined {S} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() Element of bool [:R,{S}:]

{S} is non empty set

[:R,{S}:] is non empty Relation-like set

bool [:R,{S}:] is non empty set

product (R --> S) is non empty constituted-Functions strict RelStr

the carrier of (product (R --> S)) is non empty functional set

G is Element of R

(R --> S) . G is non empty RelStr

(R,S,T,G) is Element of the carrier of S

the carrier of S is non empty set

(R,S,F,G) is Element of the carrier of S

G is Element of R

(R --> S) . G is non empty RelStr

F is Relation-like Function-like Element of the carrier of (product (R --> S))

F . G is Element of the carrier of ((R --> S) . G)

the carrier of ((R --> S) . G) is non empty set

G is Relation-like Function-like Element of the carrier of (product (R --> S))

G . G is Element of the carrier of ((R --> S) . G)

R is set

S is non empty RelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict RelStr

T is non empty RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is non empty strict RelStr

S |^ R is non empty constituted-Functions strict RelStr

T |^ R is non empty constituted-Functions strict RelStr

R --> S is Relation-like R -defined {S} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() Element of bool [:R,{S}:]

{S} is non empty set

[:R,{S}:] is Relation-like set

bool [:R,{S}:] is non empty set

R --> T is Relation-like R -defined {T} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() Element of bool [:R,{T}:]

{T} is non empty set

[:R,{T}:] is Relation-like set

bool [:R,{T}:] is non empty set

F is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

Carrier F is Relation-like R -defined Function-like V27(R) set

dom (Carrier F) is Element of bool R

bool R is non empty set

F is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

Carrier F is Relation-like R -defined Function-like V27(R) set

G is set

(Carrier F) . G is set

(Carrier F) . G is set

F . G is set

F . G is set

G is 1-sorted

the carrier of G is set

G is 1-sorted

the carrier of G is set

dom (Carrier F) is Element of bool R

the carrier of (T |^ R) is non empty functional set

product F is strict RelStr

the carrier of (product F) is set

product (Carrier F) is set

product (Carrier F) is set

product F is strict RelStr

the carrier of (product F) is set

the carrier of (S |^ R) is non empty functional set

the InternalRel of (S |^ R) is Relation-like the carrier of (S |^ R) -defined the carrier of (S |^ R) -valued Element of bool [: the carrier of (S |^ R), the carrier of (S |^ R):]

[: the carrier of (S |^ R), the carrier of (S |^ R):] is non empty Relation-like set

bool [: the carrier of (S |^ R), the carrier of (S |^ R):] is non empty set

the InternalRel of (T |^ R) is Relation-like the carrier of (T |^ R) -defined the carrier of (T |^ R) -valued Element of bool [: the carrier of (T |^ R), the carrier of (T |^ R):]

[: the carrier of (T |^ R), the carrier of (T |^ R):] is non empty Relation-like set

bool [: the carrier of (T |^ R), the carrier of (T |^ R):] is non empty set

x is set

f is set

x is set

[f,x] is V1() set

{f,x} is non empty set

{f} is non empty set

{{f,x},{f}} is non empty set

G is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

product G is strict RelStr

Carrier G is Relation-like R -defined Function-like V27(R) set

product (Carrier G) is set

s is Relation-like Function-like Element of the carrier of (S |^ R)

s1 is Relation-like Function-like Element of the carrier of (S |^ R)

As is Relation-like Function-like set

gX is Relation-like Function-like set

sH is Relation-like Function-like Element of the carrier of (T |^ R)

a is Relation-like Function-like Element of the carrier of (T |^ R)

G is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

F is set

G . F is set

As . F is set

gX . F is set

G . F is set

G is RelStr

the carrier of G is set

G is Element of the carrier of G

yi is Element of the carrier of G

R1 is non empty RelStr

the carrier of R1 is non empty set

xi1 is Element of the carrier of R1

yi1 is Element of the carrier of R1

the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like set

bool [: the carrier of G, the carrier of G:] is non empty set

[xi1,yi1] is V1() Element of the carrier of [:R1,R1:]

[:R1,R1:] is non empty strict RelStr

the carrier of [:R1,R1:] is non empty set

{xi1,yi1} is non empty set

{xi1} is non empty set

{{xi1,yi1},{xi1}} is non empty set

the InternalRel of R1 is Relation-like the carrier of R1 -defined the carrier of R1 -valued Element of bool [: the carrier of R1, the carrier of R1:]

[: the carrier of R1, the carrier of R1:] is non empty Relation-like set

bool [: the carrier of R1, the carrier of R1:] is non empty set

product G is strict RelStr

Carrier G is Relation-like R -defined Function-like V27(R) set

product (Carrier G) is set

F is Relation-like Function-like set

G is Relation-like Function-like set

x is set

f is set

x is set

[f,x] is V1() set

{f,x} is non empty set

{f} is non empty set

{{f,x},{f}} is non empty set

G is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

product G is strict RelStr

Carrier G is Relation-like R -defined Function-like V27(R) set

product (Carrier G) is set

s is Relation-like Function-like Element of the carrier of (T |^ R)

s1 is Relation-like Function-like Element of the carrier of (T |^ R)

As is Relation-like Function-like set

gX is Relation-like Function-like set

sH is Relation-like Function-like Element of the carrier of (S |^ R)

a is Relation-like Function-like Element of the carrier of (S |^ R)

G is Relation-like R -defined Function-like V27(R) RelStr-yielding V371() set

F is set

G . F is set

As . F is set

gX . F is set

G . F is set

G is RelStr

the carrier of G is set

G is Element of the carrier of G

yi is Element of the carrier of G

R1 is non empty RelStr

the carrier of R1 is non empty set

xi1 is Element of the carrier of R1

yi1 is Element of the carrier of R1

the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like set

bool [: the carrier of G, the carrier of G:] is non empty set

[xi1,yi1] is V1() Element of the carrier of [:R1,R1:]

[:R1,R1:] is non empty strict RelStr

the carrier of [:R1,R1:] is non empty set

{xi1,yi1} is non empty set

{xi1} is non empty set

{{xi1,yi1},{xi1}} is non empty set

the InternalRel of R1 is Relation-like the carrier of R1 -defined the carrier of R1 -valued Element of bool [: the carrier of R1, the carrier of R1:]

[: the carrier of R1, the carrier of R1:] is non empty Relation-like set

bool [: the carrier of R1, the carrier of R1:] is non empty set

product G is strict RelStr

Carrier G is Relation-like R -defined Function-like V27(R) set

product (Carrier G) is set

F is Relation-like Function-like set

G is Relation-like Function-like set

R is non empty TopSpace-like TopStruct

the carrier of R is non empty set

the topology of R is Element of bool (bool the carrier of R)

bool the carrier of R is non empty set

bool (bool the carrier of R) is non empty set

TopStruct(# the carrier of R, the topology of R #) is strict TopStruct

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

the topology of S is Element of bool (bool the carrier of S)

bool the carrier of S is non empty set

bool (bool the carrier of S) is non empty set

TopStruct(# the carrier of S, the topology of S #) is strict TopStruct

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

the topology of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

TopStruct(# the carrier of T, the topology of T #) is strict TopStruct

F is non empty TopSpace-like TopStruct

the carrier of F is non empty set

the topology of F is Element of bool (bool the carrier of F)

bool the carrier of F is non empty set

bool (bool the carrier of F) is non empty set

TopStruct(# the carrier of F, the topology of F #) is strict TopStruct

oContMaps (R,T) is non empty strict RelStr

oContMaps (S,F) is non empty strict RelStr

Omega F is non empty TopSpace-like reflexive transitive strict non void TopRelStr

ContMaps (S,(Omega F)) is non empty constituted-Functions strict reflexive transitive non void RelStr

Omega T is non empty TopSpace-like reflexive transitive strict non void TopRelStr

(Omega T) |^ the carrier of R is non empty constituted-Functions strict reflexive transitive non void RelStr

ContMaps (R,(Omega T)) is non empty constituted-Functions strict reflexive transitive non void RelStr

G is reflexive transitive full SubRelStr of (Omega T) |^ the carrier of R

the carrier of G is set

F is reflexive transitive full SubRelStr of (Omega T) |^ the carrier of R

the carrier of F is set

G is set

the carrier of (Omega F) is non empty set

the topology of (Omega F) is Element of bool (bool the carrier of (Omega F))

bool the carrier of (Omega F) is non empty set

bool (bool the carrier of (Omega F)) is non empty set

TopStruct(# the carrier of (Omega F), the topology of (Omega F) #) is strict TopStruct

the carrier of (ContMaps (R,(Omega T))) is non empty functional set

the carrier of (Omega T) is non empty set

[: the carrier of R, the carrier of (Omega T):] is non empty Relation-like set

bool [: the carrier of R, the carrier of (Omega T):] is non empty set

x is non empty Relation-like the carrier of R -defined the carrier of (Omega T) -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of (Omega T):]

the topology of (Omega T) is Element of bool (bool the carrier of (Omega T))

bool the carrier of (Omega T) is non empty set

bool (bool the carrier of (Omega T)) is non empty set

TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) is strict TopStruct

[: the carrier of S, the carrier of (Omega F):] is non empty Relation-like set

bool [: the carrier of S, the carrier of (Omega F):] is non empty set

f is non empty Relation-like the carrier of S -defined the carrier of (Omega F) -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of (Omega F):]

x is Element of bool the carrier of (Omega F)

f " x is Element of bool the carrier of S

s is Element of bool the carrier of (Omega T)

x " s is Element of bool the carrier of R

the carrier of (ContMaps (S,(Omega F))) is non empty functional set

G is set

the carrier of (Omega T) is non empty set

the topology of (Omega T) is Element of bool (bool the carrier of (Omega T))

bool the carrier of (Omega T) is non empty set

bool (bool the carrier of (Omega T)) is non empty set

TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) is strict TopStruct

the carrier of (ContMaps (S,(Omega F))) is non empty functional set

the carrier of (Omega F) is non empty set

[: the carrier of S, the carrier of (Omega F):] is non empty Relation-like set

bool [: the carrier of S, the carrier of (Omega F):] is non empty set

x is non empty Relation-like the carrier of S -defined the carrier of (Omega F) -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of (Omega F):]

the topology of (Omega F) is Element of bool (bool the carrier of (Omega F))

bool the carrier of (Omega F) is non empty set

bool (bool the carrier of (Omega F)) is non empty set

TopStruct(# the carrier of (Omega F), the topology of (Omega F) #) is strict TopStruct

[: the carrier of R, the carrier of (Omega T):] is non empty Relation-like set

bool [: the carrier of R, the carrier of (Omega T):] is non empty set

f is non empty Relation-like the carrier of R -defined the carrier of (Omega T) -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of (Omega T):]

x is Element of bool the carrier of (Omega T)

f " x is Element of bool the carrier of R

s is Element of bool the carrier of (Omega F)

x " s is Element of bool the carrier of S

the carrier of (ContMaps (R,(Omega T))) is non empty functional set

R is set

BoolePoset R is non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean RelStr

the carrier of (BoolePoset R) is non empty set

(BoolePoset 1) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

the carrier of ((BoolePoset 1) |^ R) is non empty functional set

[: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):] is non empty Relation-like set

bool [: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):] is non empty set

bool R is non empty set

InclPoset (bool {}) is non empty strict reflexive transitive antisymmetric non void RelStr

RelIncl (bool {}) is Relation-like bool {} -defined bool {} -valued V19() V22() V26() V27( bool {}) quasi_total Element of bool [:(bool {}),(bool {}):]

[:(bool {}),(bool {}):] is non empty Relation-like set

bool [:(bool {}),(bool {}):] is non empty set

RelStr(# (bool {}),(RelIncl (bool {})) #) is strict RelStr

S is non empty Relation-like the carrier of (BoolePoset R) -defined the carrier of ((BoolePoset 1) |^ R) -valued Function-like V27( the carrier of (BoolePoset R)) quasi_total Function-yielding V33() Element of bool [: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):]

rng (id {{}}) is non empty functional Element of bool {{}}

bool {{}} is non empty set

T is Element of the carrier of (BoolePoset R)

F is Element of the carrier of (BoolePoset R)

S . T is Relation-like Function-like Element of the carrier of ((BoolePoset 1) |^ R)

S . F is Relation-like Function-like Element of the carrier of ((BoolePoset 1) |^ R)

F is Element of the carrier of (BoolePoset R)

S . F is Relation-like Function-like Element of the carrier of ((BoolePoset 1) |^ R)

G is Element of the carrier of (BoolePoset R)

S . G is Relation-like Function-like Element of the carrier of ((BoolePoset 1) |^ R)

T is Element of bool R

S . T is Relation-like Function-like set

chi (T,R) is Relation-like R -defined {{},1} -valued Function-like V27(R) quasi_total Element of bool [:R,{{},1}:]

[:R,{{},1}:] is Relation-like set

bool [:R,{{},1}:] is non empty set

S is non empty set

S --> (BoolePoset 1) is non empty Relation-like S -defined {(BoolePoset 1)} -valued Function-like constant V27(S) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [:S,{(BoolePoset 1)}:]

{(BoolePoset 1)} is non empty set

[:S,{(BoolePoset 1)}:] is non empty Relation-like set

bool [:S,{(BoolePoset 1)}:] is non empty set

product (S --> (BoolePoset 1)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void RelStr

R is set

BoolePoset R is non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void distributive V393() complemented Boolean RelStr

(BoolePoset 1) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

the carrier of (BoolePoset R) is non empty set

the carrier of ((BoolePoset 1) |^ R) is non empty functional set

[: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):] is non empty Relation-like set

bool [: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):] is non empty set

bool R is non empty set

S is non empty Relation-like the carrier of (BoolePoset R) -defined the carrier of ((BoolePoset 1) |^ R) -valued Function-like V27( the carrier of (BoolePoset R)) quasi_total Function-yielding V33() Element of bool [: the carrier of (BoolePoset R), the carrier of ((BoolePoset 1) |^ R):]

S is non empty set

R is non empty set

T is non empty reflexive transitive antisymmetric non void RelStr

T |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

(T |^ R) |^ S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

T |^ S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

(T |^ S) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of (T |^ R) |^ S

the carrier of F is non empty functional set

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of (T |^ S) |^ R

the carrier of F is non empty functional set

[: the carrier of F, the carrier of F:] is non empty Relation-like set

bool [: the carrier of F, the carrier of F:] is non empty set

G is non empty Relation-like the carrier of F -defined the carrier of F -valued Function-like V27( the carrier of F) quasi_total Function-yielding V33() Element of bool [: the carrier of F, the carrier of F:]

dom G is non empty functional Element of bool the carrier of F

bool the carrier of F is non empty set

G is Relation-like Function-like Element of the carrier of F

x is Relation-like Function-like Element of the carrier of F

G . G is Relation-like Function-like Element of the carrier of F

G . x is Relation-like Function-like Element of the carrier of F

commute x is Relation-like Function-like Function-yielding V33() set

the carrier of ((T |^ S) |^ R) is non empty functional set

the carrier of ((T |^ R) |^ S) is non empty functional set

the carrier of (T |^ R) is non empty functional set

Funcs (S, the carrier of (T |^ R)) is non empty functional FUNCTION_DOMAIN of S, the carrier of (T |^ R)

the carrier of T is non empty set

Funcs (R, the carrier of T) is non empty functional FUNCTION_DOMAIN of R, the carrier of T

Funcs (S,(Funcs (R, the carrier of T))) is non empty functional FUNCTION_DOMAIN of S, Funcs (R, the carrier of T)

s is Relation-like Function-like Element of the carrier of ((T |^ R) |^ S)

s1 is Relation-like Function-like Element of the carrier of ((T |^ R) |^ S)

commute s is Relation-like Function-like Function-yielding V33() set

f is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

As is Element of R

(R,(T |^ S),f,As) is Relation-like Function-like Element of the carrier of (T |^ S)

the carrier of (T |^ S) is non empty functional set

gX is Element of S

(S,T,(R,(T |^ S),f,As),gX) is Element of the carrier of T

(S,(T |^ R),s,gX) is Relation-like Function-like Element of the carrier of (T |^ R)

(R,T,(S,(T |^ R),s,gX),As) is Element of the carrier of T

x is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

(R,(T |^ S),x,As) is Relation-like Function-like Element of the carrier of (T |^ S)

(S,T,(R,(T |^ S),x,As),gX) is Element of the carrier of T

(S,(T |^ R),s1,gX) is Relation-like Function-like Element of the carrier of (T |^ R)

(R,T,(S,(T |^ R),s1,gX),As) is Element of the carrier of T

R is non empty set

S is non empty set

[:R,S:] is non empty Relation-like set

T is non empty reflexive transitive antisymmetric non void RelStr

T |^ S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

(T |^ S) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

T |^ [:R,S:] is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of (T |^ S) |^ R

the carrier of F is non empty functional set

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of T |^ [:R,S:]

the carrier of F is non empty functional set

[: the carrier of F, the carrier of F:] is non empty Relation-like set

bool [: the carrier of F, the carrier of F:] is non empty set

G is non empty Relation-like the carrier of F -defined the carrier of F -valued Function-like V27( the carrier of F) quasi_total Function-yielding V33() Element of bool [: the carrier of F, the carrier of F:]

dom G is non empty functional Element of bool the carrier of F

bool the carrier of F is non empty set

G is Relation-like Function-like Element of the carrier of F

x is Relation-like Function-like Element of the carrier of F

G . G is Relation-like Function-like Element of the carrier of F

G . x is Relation-like Function-like Element of the carrier of F

the carrier of ((T |^ S) |^ R) is non empty functional set

x is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

uncurry x is Relation-like Function-like set

the carrier of (T |^ [:R,S:]) is non empty functional set

f is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

the carrier of (T |^ S) is non empty functional set

the carrier of T is non empty set

Funcs (S, the carrier of T) is non empty functional FUNCTION_DOMAIN of S, the carrier of T

Funcs (R,(Funcs (S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of R, Funcs (S, the carrier of T)

uncurry f is Relation-like Function-like set

As is Element of [:R,S:]

gX is set

sH is set

[gX,sH] is V1() set

{gX,sH} is non empty set

{gX} is non empty set

{{gX,sH},{gX}} is non empty set

F is Element of R

(R,(T |^ S),f,F) is Relation-like Function-like Element of the carrier of (T |^ S)

(R,(T |^ S),x,F) is Relation-like Function-like Element of the carrier of (T |^ S)

[:R,(Funcs (S, the carrier of T)):] is non empty Relation-like set

bool [:R,(Funcs (S, the carrier of T)):] is non empty set

proj1 x is set

proj1 f is set

[:S, the carrier of T:] is non empty Relation-like set

bool [:S, the carrier of T:] is non empty set

proj1 (R,(T |^ S),x,F) is set

s1 is Relation-like Function-like Element of the carrier of (T |^ [:R,S:])

a is Element of S

s1 . (F,a) is set

[F,a] is V1() set

{F,a} is non empty set

{F} is non empty set

{{F,a},{F}} is non empty set

s1 . [F,a] is set

(S,T,(R,(T |^ S),x,F),a) is Element of the carrier of T

proj1 (R,(T |^ S),f,F) is set

s is Relation-like Function-like Element of the carrier of (T |^ [:R,S:])

s . (F,a) is set

s . [F,a] is set

(S,T,(R,(T |^ S),f,F),a) is Element of the carrier of T

([:R,S:],T,s,As) is Element of the carrier of T

([:R,S:],T,s1,As) is Element of the carrier of T

R is non empty set

S is non empty set

[:R,S:] is non empty Relation-like set

T is non empty reflexive transitive antisymmetric non void RelStr

T |^ S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

(T |^ S) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

T |^ [:R,S:] is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of (T |^ S) |^ R

the carrier of F is non empty functional set

F is non empty constituted-Functions reflexive transitive antisymmetric full non void SubRelStr of T |^ [:R,S:]

the carrier of F is non empty functional set

[: the carrier of F, the carrier of F:] is non empty Relation-like set

bool [: the carrier of F, the carrier of F:] is non empty set

G is non empty Relation-like the carrier of F -defined the carrier of F -valued Function-like V27( the carrier of F) quasi_total Function-yielding V33() Element of bool [: the carrier of F, the carrier of F:]

dom G is non empty functional Element of bool the carrier of F

bool the carrier of F is non empty set

G is Relation-like Function-like Element of the carrier of F

x is Relation-like Function-like Element of the carrier of F

G . G is Relation-like Function-like Element of the carrier of F

G . x is Relation-like Function-like Element of the carrier of F

the carrier of (T |^ [:R,S:]) is non empty functional set

x is Relation-like Function-like Element of the carrier of (T |^ [:R,S:])

curry x is Relation-like Function-like set

the carrier of ((T |^ S) |^ R) is non empty functional set

f is Relation-like Function-like Element of the carrier of (T |^ [:R,S:])

the carrier of (T |^ S) is non empty functional set

the carrier of T is non empty set

Funcs (S, the carrier of T) is non empty functional FUNCTION_DOMAIN of S, the carrier of T

Funcs (R,(Funcs (S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of R, Funcs (S, the carrier of T)

curry f is Relation-like Function-like set

As is Element of R

gX is Element of S

[As,gX] is V1() Element of [:R,S:]

{As,gX} is non empty set

{As} is non empty set

{{As,gX},{As}} is non empty set

s is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

(R,(T |^ S),s,As) is Relation-like Function-like Element of the carrier of (T |^ S)

[:S, the carrier of T:] is non empty Relation-like set

bool [:S, the carrier of T:] is non empty set

proj1 (R,(T |^ S),s,As) is set

[:R,(Funcs (S, the carrier of T)):] is non empty Relation-like set

bool [:R,(Funcs (S, the carrier of T)):] is non empty set

proj1 s is set

(S,T,(R,(T |^ S),s,As),gX) is Element of the carrier of T

f . (As,gX) is set

[As,gX] is V1() set

f . [As,gX] is set

sH is Element of [:R,S:]

([:R,S:],T,f,sH) is Element of the carrier of T

s1 is Relation-like Function-like Element of the carrier of ((T |^ S) |^ R)

(R,(T |^ S),s1,As) is Relation-like Function-like Element of the carrier of (T |^ S)

proj1 (R,(T |^ S),s1,As) is set

proj1 s1 is set

(S,T,(R,(T |^ S),s1,As),gX) is Element of the carrier of T

x . (As,gX) is set

x . [As,gX] is set

R is non empty RelStr

the carrier of R is non empty set

S is non empty reflexive antisymmetric non void RelStr

S |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

the carrier of (S |^ the carrier of R) is non empty functional set

T is set

F is set

bool the carrier of (S |^ the carrier of R) is non empty set

F is functional Element of bool the carrier of (S |^ the carrier of R)

subrelstr F is strict reflexive antisymmetric full SubRelStr of S |^ the carrier of R

F is strict reflexive antisymmetric full SubRelStr of S |^ the carrier of R

the carrier of F is set

G is set

T is strict RelStr

the carrier of T is set

F is strict RelStr

the carrier of F is set

F is set

F is set

R is non empty RelStr

S is non empty reflexive antisymmetric non void RelStr

(R,S) is strict RelStr

the carrier of R is non empty set

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

the non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:] is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]

the carrier of (R,S) is set

S |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

R is non empty RelStr

S is non empty reflexive transitive antisymmetric non void RelStr

(R,S) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of R is non empty set

S |^ the carrier of R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

R is non empty RelStr

the carrier of R is non empty set

S is non empty reflexive antisymmetric non void RelStr

(R,S) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (R,S) is non empty functional set

the carrier of S is non empty set

Funcs ( the carrier of R, the carrier of S) is non empty functional FUNCTION_DOMAIN of the carrier of R, the carrier of S

S |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (S |^ the carrier of R) is non empty functional set

R is non empty RelStr

S is non empty reflexive antisymmetric non void RelStr

(R,S) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (R,S) is non empty functional set

the carrier of R is non empty set

T is Relation-like Function-like Element of the carrier of (R,S)

F is Element of the carrier of R

T . F is set

the carrier of S is non empty set

S |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (S |^ the carrier of R) is non empty functional set

F is Relation-like Function-like Element of the carrier of (S |^ the carrier of R)

( the carrier of R,S,F,F) is Element of the carrier of S

R is non empty RelStr

the carrier of R is non empty set

S is non empty reflexive antisymmetric non void RelStr

(R,S) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (R,S) is non empty functional set

T is Relation-like Function-like Element of the carrier of (R,S)

F is Relation-like Function-like Element of the carrier of (R,S)

S |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (S |^ the carrier of R) is non empty functional set

F is Relation-like Function-like Element of the carrier of (S |^ the carrier of R)

G is Relation-like Function-like Element of the carrier of (S |^ the carrier of R)

G is Element of the carrier of R

(R,S,T,G) is Element of the carrier of S

the carrier of S is non empty set

(R,S,F,G) is Element of the carrier of S

R is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void TopRelStr

S is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void TopRelStr

(R,S) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

SCMaps (R,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (R,S)

MonMaps (R,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of S |^ the carrier of R

the carrier of R is non empty set

S |^ the carrier of R is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the carrier of (R,S) is non empty functional set

the carrier of (SCMaps (R,S)) is non empty functional set

T is set

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

F is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]

T is set

the carrier of (MonMaps (R,S)) is non empty functional set

the carrier of S is non empty set

[: the carrier of R, the carrier of S:] is non empty Relation-like set

bool [: the carrier of R, the carrier of S:] is non empty set

F is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of S:]

the carrier of (MonMaps (R,S)) is non empty functional set

the InternalRel of (R,S) is non empty Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Element of bool [: the carrier of (R,S), the carrier of (R,S):]

[: the carrier of (R,S), the carrier of (R,S):] is non empty Relation-like set

bool [: the carrier of (R,S), the carrier of (R,S):] is non empty set

the InternalRel of (S |^ the carrier of R) is non empty Relation-like the carrier of (S |^ the carrier of R) -defined the carrier of (S |^ the carrier of R) -valued Element of bool [: the carrier of (S |^ the carrier of R), the carrier of (S |^ the carrier of R):]

the carrier of (S |^ the carrier of R) is non empty functional set

[: the carrier of (S |^ the carrier of R), the carrier of (S |^ the carrier of R):] is non empty Relation-like set

bool [: the carrier of (S |^ the carrier of R), the carrier of (S |^ the carrier of R):] is non empty set

the InternalRel of (S |^ the carrier of R) |_2 the carrier of (R,S) is Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Element of bool [: the carrier of (R,S), the carrier of (R,S):]

the InternalRel of (S |^ the carrier of R) |_2 the carrier of (MonMaps (R,S)) is Relation-like the carrier of (MonMaps (R,S)) -defined the carrier of (MonMaps (R,S)) -valued Element of bool [: the carrier of (MonMaps (R,S)), the carrier of (MonMaps (R,S)):]

[: the carrier of (MonMaps (R,S)), the carrier of (MonMaps (R,S)):] is non empty Relation-like set

bool [: the carrier of (MonMaps (R,S)), the carrier of (MonMaps (R,S)):] is non empty set

( the InternalRel of (S |^ the carrier of R) |_2 the carrier of (MonMaps (R,S))) |_2 the carrier of (R,S) is Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Element of bool [: the carrier of (R,S), the carrier of (R,S):]

the InternalRel of (MonMaps (R,S)) is non empty Relation-like the carrier of (MonMaps (R,S)) -defined the carrier of (MonMaps (R,S)) -valued Element of bool [: the carrier of (MonMaps (R,S)), the carrier of (MonMaps (R,S)):]

the InternalRel of (MonMaps (R,S)) |_2 the carrier of (SCMaps (R,S)) is Relation-like the carrier of (SCMaps (R,S)) -defined the carrier of (SCMaps (R,S)) -valued Element of bool [: the carrier of (SCMaps (R,S)), the carrier of (SCMaps (R,S)):]

[: the carrier of (SCMaps (R,S)), the carrier of (SCMaps (R,S)):] is non empty Relation-like set

bool [: the carrier of (SCMaps (R,S)), the carrier of (SCMaps (R,S)):] is non empty set

the InternalRel of (SCMaps (R,S)) is non empty Relation-like the carrier of (SCMaps (R,S)) -defined the carrier of (SCMaps (R,S)) -valued Element of bool [: the carrier of (SCMaps (R,S)), the carrier of (SCMaps (R,S)):]

R is non empty RelStr

the carrier of R is non empty set

the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

bool [: the carrier of R, the carrier of R:] is non empty set

RelStr(# the carrier of R, the InternalRel of R #) is non empty strict RelStr

S is non empty RelStr

the carrier of S is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict RelStr

T is non empty reflexive antisymmetric non void RelStr

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive antisymmetric non void RelStr

F is non empty reflexive antisymmetric non void RelStr

the carrier of F is non empty set

the InternalRel of F is non empty Relation-like the carrier of F -defined the carrier of F -valued Element of bool [: the carrier of F, the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty Relation-like set

bool [: the carrier of F, the carrier of F:] is non empty set

RelStr(# the carrier of F, the InternalRel of F #) is non empty strict reflexive antisymmetric non void RelStr

(R,T) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

(S,F) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

T |^ the carrier of R is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

F |^ the carrier of S is non empty constituted-Functions strict reflexive antisymmetric non void RelStr

the carrier of (R,T) is non empty functional set

the carrier of (S,F) is non empty functional set

F is set

[: the carrier of R, the carrier of T:] is non empty Relation-like set

bool [: the carrier of R, the carrier of T:] is non empty set

[: the carrier of S, the carrier of F:] is non empty Relation-like set

bool [: the carrier of S, the carrier of F:] is non empty set

G is non empty Relation-like the carrier of R -defined the carrier of T -valued Function-like V27( the carrier of R) quasi_total directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]

G is non empty Relation-like the carrier of S -defined the carrier of F -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of F:]

bool the carrier of S is non empty set

x is Element of bool the carrier of S

bool the carrier of R is non empty set

f is Element of bool the carrier of R

F is set

[: the carrier of S, the carrier of F:] is non empty Relation-like set

bool [: the carrier of S, the carrier of F:] is non empty set

[: the carrier of R, the carrier of T:] is non empty Relation-like set

bool [: the carrier of R, the carrier of T:] is non empty set

G is non empty Relation-like the carrier of S -defined the carrier of F -valued Function-like V27( the carrier of S) quasi_total directed-sups-preserving Element of bool [: the carrier of S, the carrier of F:]

G is non empty Relation-like the carrier of R -defined the carrier of T -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of T:]

bool the carrier of R is non empty set

x is Element of bool the carrier of R

bool the carrier of S is non empty set

f is Element of bool the carrier of S

R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

(R,S) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S

the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of R is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of R

the carrier of S is non empty set

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr

G is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void TopRelStr

the carrier of G is non empty set

the InternalRel of G is non empty Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty Relation-like set

bool [: the carrier of G, the carrier of G:] is non empty set

RelStr(# the carrier of G, the InternalRel of G #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr

the carrier of R is non empty set

the InternalRel of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]

[: the carrier of R, the carrier of R:] is non empty Relation-like set

bool [: the carrier of R, the carrier of R:] is non empty set

RelStr(# the carrier of R, the InternalRel of R #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr

F is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void TopRelStr

the carrier of F is non empty set

the InternalRel of F is non empty Relation-like the carrier of F -defined the carrier of F -valued Element of bool [: the carrier of F, the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty Relation-like set

bool [: the carrier of F, the carrier of F:] is non empty set

RelStr(# the carrier of F, the InternalRel of F #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr

(F,G) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr

SCMaps (F,G) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (F,G)

MonMaps (F,G) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of G |^ the carrier of F

G |^ the carrier of F is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

ContMaps (F,G) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

(R,S) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the carrier of R is non empty set

S |^ the carrier of R is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr

the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of R is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of R

the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S

the carrier of S is non empty set

the InternalRel of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr

the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S is non empty set

the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric