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