:: 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 V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott non void monotone-convergence TopAugmentation of S -valued Element of bool [: 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, 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:]
[: 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, 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 Relation-like set
bool [: 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, 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
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, 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 strict reflexive transitive antisymmetric V219() V220() upper-bounded up-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 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 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
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 R 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 R 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 R -defined 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 R -valued Element of bool [: 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 R, 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 R:]
[: 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 R, 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 R:] is non empty Relation-like set
bool [: 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 R, 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 R:] is non empty set
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 R, 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 R #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-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, 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 constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
SCMaps ( 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, 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 constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps ( 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, 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)
MonMaps ( 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, 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 constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr 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 |^ 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 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 |^ 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 R is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
ContMaps ( 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, 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 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,S) is non empty functional set
bool the carrier of (R,S) is non empty set
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
T is functional Element of bool the carrier of (R,S)
"\/" (T,(R,S)) is Relation-like Function-like Element of the carrier of (R,S)
"\/" (T,(S |^ the carrier of R)) is Relation-like Function-like Element of the carrier of (S |^ the carrier of R)
the carrier of (S |^ the carrier of R) is non empty functional set
R is non empty reflexive antisymmetric non void RelStr
the carrier of R is non empty set
S is non empty 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
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:]
T is non empty reflexive antisymmetric non void RelStr
the carrier of T is non empty set
F is non empty reflexive antisymmetric non void RelStr
the carrier of F is non empty set
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] is non empty set
G is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of F:]
(S,T) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr
the carrier of (S,T) is non empty functional set
(R,F) is non empty constituted-Functions strict reflexive antisymmetric non void RelStr
the carrier of (R,F) is non empty functional set
[: the carrier of (S,T), the carrier of (R,F):] is non empty Relation-like set
bool [: the carrier of (S,T), the carrier of (R,F):] is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
G is Relation-like Function-like Element of the carrier of (S,T)
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
x * 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:]
[: 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 * (x * F) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
G * x 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:]
[: 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 * x) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
f is Relation-like Function-like Element of the carrier of (R,F)
x is Relation-like Function-like set
x * G is Relation-like the carrier of F -valued Function-like set
F * (x * G) is Relation-like the carrier of R -defined the carrier of F -valued Function-like set
G is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
x is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
x . f is Relation-like Function-like set
G * f 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:]
[: 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 * f) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
G is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
x is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
f is set
G . f is Relation-like Function-like set
x . f is Relation-like Function-like set
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
G * x 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:]
[: 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 * x) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric non void RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
R is non empty reflexive transitive antisymmetric non void RelStr
the carrier of R 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 reflexive transitive antisymmetric non void RelStr
the carrier of F is non empty set
F is non empty reflexive transitive antisymmetric non void RelStr
the carrier of F is non empty 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 reflexive transitive antisymmetric non void RelStr
the carrier of G is non empty set
[: the carrier of F, the carrier of G:] is non empty Relation-like set
bool [: the carrier of F, the carrier of G:] is non empty set
(T,F) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (T,F) is non empty functional set
(R,G) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (R,G) is non empty functional set
(S,F) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,F) is non empty functional set
G is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
x is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]
G * x 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:]
[: 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 F -defined the carrier of F -valued Function-like V27( the carrier of F) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of F, the carrier of F:]
(S,T,F,F,G,f) is non empty Relation-like the carrier of (T,F) -defined the carrier of (S,F) -valued Function-like V27( the carrier of (T,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (T,F), the carrier of (S,F):]
[: the carrier of (T,F), the carrier of (S,F):] is non empty Relation-like set
bool [: the carrier of (T,F), the carrier of (S,F):] is non empty set
x is non empty Relation-like the carrier of F -defined the carrier of G -valued Function-like V27( the carrier of F) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of F, the carrier of G:]
(R,S,F,G,x,x) is non empty Relation-like the carrier of (S,F) -defined the carrier of (R,G) -valued Function-like V27( the carrier of (S,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,F), the carrier of (R,G):]
[: the carrier of (S,F), the carrier of (R,G):] is non empty Relation-like set
bool [: the carrier of (S,F), the carrier of (R,G):] is non empty set
(R,S,F,G,x,x) * (S,T,F,F,G,f) is non empty Relation-like the carrier of (T,F) -defined the carrier of (R,G) -valued Function-like V27( the carrier of (T,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (T,F), the carrier of (R,G):]
[: the carrier of (T,F), the carrier of (R,G):] is non empty Relation-like set
bool [: the carrier of (T,F), the carrier of (R,G):] is non empty set
x * f is non empty Relation-like the carrier of F -defined the carrier of G -valued Function-like V27( the carrier of F) quasi_total Element of bool [: the carrier of F, the carrier of G:]
[: the carrier of F, the carrier of G:] is non empty Relation-like set
bool [: the carrier of F, the carrier of G:] is non empty set
(R,T,F,G,(G * x),(x * f)) is non empty Relation-like the carrier of (T,F) -defined the carrier of (R,G) -valued Function-like V27( the carrier of (T,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (T,F), the carrier of (R,G):]
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] is non empty set
s is non empty Relation-like the carrier of R -defined the carrier of T -valued Function-like V27( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of T:]
s1 is non empty Relation-like the carrier of F -defined the carrier of G -valued Function-like V27( the carrier of F) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of F, the carrier of G:]
As is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of T, the carrier of F:]
((R,S,F,G,x,x) * (S,T,F,F,G,f)) . As is Relation-like Function-like set
s1 * As is non empty Relation-like the carrier of T -defined the carrier of G -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of G:]
[: the carrier of T, the carrier of G:] is non empty Relation-like set
bool [: the carrier of T, the carrier of G:] is non empty set
(s1 * As) * s is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
[: the carrier of R, the carrier of G:] is non empty Relation-like set
bool [: the carrier of R, the carrier of G:] is non empty set
f * As is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of F:]
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] 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
(f * As) * 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:]
dom (S,T,F,F,G,f) is non empty functional Element of bool the carrier of (T,F)
bool the carrier of (T,F) is non empty set
(S,T,F,F,G,f) . As is Relation-like Function-like set
(R,S,F,G,x,x) . ((S,T,F,F,G,f) . As) is Relation-like Function-like set
(R,S,F,G,x,x) . ((f * As) * G) is Relation-like Function-like set
gX is non empty Relation-like the carrier of S -defined the carrier of F -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of F:]
x * gX is non empty Relation-like the carrier of S -defined the carrier of G -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of G:]
[: the carrier of S, the carrier of G:] is non empty Relation-like set
bool [: the carrier of S, the carrier of G:] is non empty set
(x * gX) * x is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
((f * As) * G) * x is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
x * (((f * As) * G) * x) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
As * 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:]
[: 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
f * (As * 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:]
(f * (As * G)) * x is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
x * ((f * (As * G)) * x) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
(As * G) * x is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
f * ((As * G) * x) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
x * (f * ((As * G) * x)) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
As * (G * x) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
f * (As * (G * x)) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
x * (f * (As * (G * x))) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
(f * As) * (G * x) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
x * ((f * As) * (G * x)) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
x * (f * As) is non empty Relation-like the carrier of T -defined the carrier of G -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of G:]
(x * (f * As)) * (G * x) is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of G:]
R is non empty reflexive antisymmetric non void 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
id R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is non empty set
[: 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
id the carrier of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of R) quasi_total onto bijective Element of bool [: the carrier of R, the carrier of R:]
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V27( the carrier of S) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of S, the carrier of S:]
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
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of S) quasi_total onto bijective Element of bool [: the carrier of S, the carrier of S:]
(R,R,S,S,(id R),(id S)) is non empty Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Function-like V27( the carrier of (R,S)) quasi_total Function-yielding V33() 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
id (R,S) is non empty Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Function-like one-to-one V27( the carrier of (R,S)) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (R,S), the carrier of (R,S):]
id the carrier of (R,S) is non empty Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (R,S)) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (R,S), the carrier of (R,S):]
T is set
(R,R,S,S,(id R),(id S)) . T is Relation-like Function-like 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 monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]
(R,R,S,S,(id R),(id S)) . F is Relation-like Function-like set
(id S) * 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:]
((id S) * F) * (id R) 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 * (id R) 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:]
dom (R,R,S,S,(id R),(id S)) is non empty functional Element of bool the carrier of (R,S)
bool the carrier of (R,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
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 R, the carrier of S:] is non empty Relation-like set
bool [: the carrier of R, the carrier of S:] is non empty set
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
the carrier of T is non empty set
F is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
the carrier of F is non empty set
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] is non empty set
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,F) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
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 monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]
G is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of T, the carrier of F:]
(R,S,T,F,F,G) is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
the carrier of (S,T) is non empty functional set
the carrier of (R,F) is non empty functional set
[: the carrier of (S,T), the carrier of (R,F):] is non empty Relation-like set
bool [: the carrier of (S,T), the carrier of (R,F):] is non empty set
bool the carrier of (S,T) is non empty set
G is functional Element of bool the carrier of (S,T)
(R,S,T,F,F,G) .: G is functional Element of bool the carrier of (R,F)
bool the carrier of (R,F) is non empty set
"\/" (((R,S,T,F,F,G) .: G),(R,F)) is Relation-like Function-like Element of the carrier of (R,F)
"\/" (G,(S,T)) is Relation-like Function-like Element of the carrier of (S,T)
(R,S,T,F,F,G) . ("\/" (G,(S,T))) is Relation-like Function-like Element of the carrier of (R,F)
T |^ the carrier of 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 (T |^ the carrier of S) is non empty functional set
bool the carrier of (T |^ the carrier of S) is non empty set
x is non empty functional directed Element of bool the carrier of (S,T)
F |^ 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 (F |^ the carrier of R) is non empty functional set
"\/" (x,(S,T)) is Relation-like Function-like Element of the carrier of (S,T)
(R,S,T,F,F,G) . ("\/" (x,(S,T))) is Relation-like Function-like Element of the carrier of (R,F)
bool the carrier of (F |^ the carrier of R) is non empty set
(R,S,T,F,F,G) .: x is non empty functional Element of bool the carrier of (R,F)
the carrier of R --> F is non empty Relation-like the carrier of R -defined {F} -valued Function-like constant V27( the carrier of R) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [: the carrier of R,{F}:]
{F} is non empty set
[: the carrier of R,{F}:] is non empty Relation-like set
bool [: the carrier of R,{F}:] is non empty set
product ( the carrier of R --> F) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
s is non empty functional Element of bool the carrier of (F |^ the carrier of R)
"\/" (s,(F |^ the carrier of R)) is Relation-like Function-like Element of the carrier of (F |^ the carrier of R)
proj1 ("\/" (s,(F |^ the carrier of R))) is set
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like constant V27( the carrier of S) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [: the carrier of S,{T}:]
{T} is non empty set
[: the carrier of S,{T}:] is non empty Relation-like set
bool [: the carrier of S,{T}:] is non empty set
product ( the carrier of S --> T) 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 (product ( the carrier of S --> T)) is non empty functional set
bool the carrier of (product ( the carrier of S --> T)) is non empty set
f is non empty functional directed Element of bool the carrier of (T |^ the carrier of S)
dom F is non empty Element of bool the carrier of R
bool the carrier of R is non empty set
As is set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
gX is Element of the carrier of R
F . gX is Element of the carrier of S
( the carrier of S --> T) . (F . gX) is non empty reflexive transitive antisymmetric non void RelStr
sH is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
dom sH is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
sH * 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:]
[: 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
dom (sH * F) is non empty Element of bool the carrier of R
pi (s,gX) is non empty Element of bool the carrier of F
bool the carrier of F is non empty set
pi (G,(F . gX)) is set
G .: (pi (G,(F . gX))) is Element of bool the carrier of F
a is set
dom G is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
F is Relation-like Function-like set
F . gX is set
dom (R,S,T,F,F,G) is non empty functional Element of bool the carrier of (S,T)
G is set
(R,S,T,F,F,G) . G is Relation-like Function-like set
G is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
G . (F . gX) is Element of the carrier of T
dom G is non empty Element of bool the carrier of S
G * 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:]
dom (G * F) is non empty Element of bool the carrier of R
G * 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:]
[: 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 * G) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
((G * G) * F) . gX is Element of the carrier of F
G * (G * F) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
(G * (G * F)) . gX is Element of the carrier of F
(G * F) . gX is Element of the carrier of T
G . ((G * F) . gX) is Element of the carrier of F
G . (G . (F . gX)) is Element of the carrier of F
a is set
dom (R,S,T,F,F,G) is non empty functional Element of bool the carrier of (S,T)
dom G is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
F is set
G . F is set
G is Relation-like Function-like set
G . (F . gX) is set
G is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
G * 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:]
[: 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 * G) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
(R,S,T,F,F,G) . G is Relation-like Function-like set
dom G is non empty Element of bool the carrier of S
G * 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:]
dom (G * F) is non empty Element of bool the carrier of R
(G * F) . gX is Element of the carrier of T
G . ((G * F) . gX) is Element of the carrier of F
G * (G * F) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
(G * (G * F)) . gX is Element of the carrier of F
((G * G) * F) . gX is Element of the carrier of F
pi (f,(F . gX)) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
( the carrier of S --> T) . (F . gX) is non empty reflexive non void RelStr
s1 is functional directed Element of bool the carrier of (product ( the carrier of S --> T))
pi (s1,(F . gX)) is Element of bool the carrier of (( the carrier of S --> T) . (F . gX))
the carrier of (( the carrier of S --> T) . (F . gX)) is non empty set
bool the carrier of (( the carrier of S --> T) . (F . gX)) is non empty set
( the carrier of R --> F) . gX is non empty reflexive transitive antisymmetric non void RelStr
("\/" (s,(F |^ the carrier of R))) . As is set
"\/" ((pi (s,gX)),F) is Element of the carrier of F
"\/" ((pi (f,(F . gX))),T) is Element of the carrier of T
G . ("\/" ((pi (f,(F . gX))),T)) is Element of the carrier of F
"\/" (f,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
( the carrier of S,T,("\/" (f,(T |^ the carrier of S))),(F . gX)) is Element of the carrier of T
G . ( the carrier of S,T,("\/" (f,(T |^ the carrier of S))),(F . gX)) is Element of the carrier of F
sH . (F . gX) is Element of the carrier of T
G . (sH . (F . gX)) is Element of the carrier of F
(sH * F) . gX is Element of the carrier of T
G . ((sH * F) . gX) is Element of the carrier of F
G * (sH * F) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
(G * (sH * F)) . gX is Element of the carrier of F
G * sH 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:]
[: 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 * sH) * F is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
((G * sH) * F) . As is set
x is Relation-like Function-like Element of the carrier of (F |^ the carrier of R)
x . As is set
proj1 x is set
InclPoset (bool 1) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (BoolePoset 1) is non empty set
the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1)
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 is non empty set
bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1) 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 strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 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 strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1:]
[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1:] is non empty Relation-like set
bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1:] is non empty set
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 strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr
Omega the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1 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
R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
T 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
oContMaps (T,Sierpinski_Space) is non empty strict RelStr
(T,(BoolePoset 1)) 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 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 transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr
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 R
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 monotone-convergence TopStruct
TopStruct(# the carrier of Sierpinski_Space, the topology of Sierpinski_Space #) is strict V381() TopStruct
Omega S is non empty TopSpace-like reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete strict non void TopRelStr
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 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
ContMaps (T,(Omega Sierpinski_Space)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
SCMaps (T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (T,S)
MonMaps (T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of S |^ the carrier of T
S |^ the carrier of T is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(T,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 (BoolePoset 1) is non empty set
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(T,(BoolePoset 1)) 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 (T,(BoolePoset 1)) is non empty functional set
sigma T is non empty Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
InclPoset (sigma T) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (InclPoset (sigma T)) is non empty set
[: the carrier of (T,(BoolePoset 1)), the carrier of (InclPoset (sigma T)):] is non empty Relation-like set
bool [: the carrier of (T,(BoolePoset 1)), the carrier of (InclPoset (sigma T)):] is non empty set
[: the carrier of T, the carrier of (BoolePoset 1):] is non empty Relation-like set
bool [: the carrier of T, the carrier of (BoolePoset 1):] is non empty set
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 T 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 T
S is non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of BoolePoset 1
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 topology 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 T is Element of bool (bool 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 T)
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 T is non empty set
bool 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 T is non empty set
bool (bool 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 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 transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr
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 T 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 T -defined 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 T -valued Element of bool [: 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 T, 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 T:]
[: 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 T, 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 T:] is non empty Relation-like set
bool [: 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 T, 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 T:] is non empty set
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 T, 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 T #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-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 T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
SCMaps ( 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 T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps ( 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 T,S)
MonMaps ( 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 T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of S |^ 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 T
S |^ 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 T is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
ContMaps ( 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 T,S) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
oContMaps ( 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 T,Sierpinski_Space) is non empty strict RelStr
[: the carrier of (InclPoset (sigma T)), the carrier of (T,(BoolePoset 1)):] is non empty Relation-like set
bool [: the carrier of (InclPoset (sigma T)), the carrier of (T,(BoolePoset 1)):] is non empty set
F is non empty Relation-like the carrier of (InclPoset (sigma T)) -defined the carrier of (T,(BoolePoset 1)) -valued Function-like V27( the carrier of (InclPoset (sigma T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (InclPoset (sigma T)), the carrier of (T,(BoolePoset 1)):]
F " is non empty Relation-like the carrier of (T,(BoolePoset 1)) -defined the carrier of (InclPoset (sigma T)) -valued Function-like V27( the carrier of (T,(BoolePoset 1))) quasi_total Element of bool [: the carrier of (T,(BoolePoset 1)), the carrier of (InclPoset (sigma T)):]
G is non empty Relation-like the carrier of (T,(BoolePoset 1)) -defined the carrier of (InclPoset (sigma T)) -valued Function-like V27( the carrier of (T,(BoolePoset 1))) quasi_total Element of bool [: the carrier of (T,(BoolePoset 1)), the carrier of (InclPoset (sigma T)):]
rng F is non empty functional Element of bool the carrier of (T,(BoolePoset 1))
bool the carrier of (T,(BoolePoset 1)) is non empty set
[#] (T,(BoolePoset 1)) is non empty non proper functional directed filtered lower upper Element of bool the carrier of (T,(BoolePoset 1))
F " is Relation-like Function-like set
G is non empty Relation-like the carrier of T -defined the carrier of (BoolePoset 1) -valued Function-like V27( the carrier of T) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of T, the carrier of (BoolePoset 1):]
G . G is set
G " {1} is Element of bool the carrier of T
dom F is non empty Element of bool the carrier of (InclPoset (sigma T))
bool the carrier of (InclPoset (sigma T)) is non empty set
x is set
F . x is Relation-like Function-like set
f is open Element of bool 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 T
chi (f, 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 T) 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 T -defined {{},1} -valued Function-like V27( 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 T) quasi_total Element of bool [: 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 T,{{},1}:]
[: 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 T,{{},1}:] is non empty Relation-like set
bool [: 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 T,{{},1}:] is non empty set
(chi (f, 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 T)) " {1} is Element of bool 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 T
R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,(BoolePoset 1)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
sigma R is non empty Element of bool (bool the carrier of R)
the carrier of R is non empty set
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
InclPoset (sigma R) is non empty strict reflexive transitive antisymmetric non void RelStr
the carrier of (R,(BoolePoset 1)) is non empty functional set
the carrier of (InclPoset (sigma R)) is non empty set
[: the carrier of (R,(BoolePoset 1)), the carrier of (InclPoset (sigma R)):] is non empty Relation-like set
bool [: the carrier of (R,(BoolePoset 1)), the carrier of (InclPoset (sigma R)):] is non empty set
[: the carrier of R, the carrier of (BoolePoset 1):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (BoolePoset 1):] is non empty set
S is non empty Relation-like the carrier of (R,(BoolePoset 1)) -defined the carrier of (InclPoset (sigma R)) -valued Function-like V27( the carrier of (R,(BoolePoset 1))) quasi_total Element of bool [: the carrier of (R,(BoolePoset 1)), the carrier of (InclPoset (sigma R)):]
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
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 R, the carrier of S:] is non empty Relation-like set
bool [: the carrier of R, the carrier of S:] is non empty set
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
the carrier of T is non empty set
F is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
the carrier of F is non empty set
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] is non empty set
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,F) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
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:]
G is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of F:]
(R,S,T,F,F,G) is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
the carrier of (S,T) is non empty functional set
the carrier of (R,F) is non empty functional set
[: the carrier of (S,T), the carrier of (R,F):] is non empty Relation-like set
bool [: the carrier of (S,T), the carrier of (R,F):] is non empty set
[: the carrier of F, the carrier of T:] is non empty Relation-like set
bool [: the carrier of F, the carrier of T:] is non empty set
id F is non empty Relation-like the carrier of F -defined the carrier of F -valued Function-like one-to-one V27( the carrier of F) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of F is non empty Relation-like the carrier of F -defined the carrier of F -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of F) quasi_total onto bijective Element of bool [: the carrier of F, the carrier of F:]
id T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V27( the carrier of T) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of T) quasi_total onto bijective Element of bool [: the carrier of T, the carrier of T:]
G is non empty Relation-like the carrier of F -defined the carrier of T -valued Function-like V27( the carrier of F) quasi_total monotone Element of bool [: the carrier of F, the carrier of T:]
G * 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 Element of bool [: the carrier of F, the carrier of F:]
G * G is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of S, the carrier of R:] is non empty Relation-like set
bool [: the carrier of S, the carrier of R:] is non empty set
id S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V27( the carrier of S) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of S) quasi_total onto bijective Element of bool [: the carrier of S, the carrier of S:]
id R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of R) quasi_total onto bijective Element of bool [: the carrier of R, the carrier of R:]
x is non empty Relation-like the carrier of S -defined the carrier of R -valued Function-like V27( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of R:]
F * x 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:]
x * F is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
(S,R,F,T,x,G) is non empty Relation-like the carrier of (R,F) -defined the carrier of (S,T) -valued Function-like V27( the carrier of (R,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,F), the carrier of (S,T):]
[: the carrier of (R,F), the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of (R,F), the carrier of (S,T):] is non empty set
(S,R,F,T,x,G) * (R,S,T,F,F,G) is non empty Relation-like the carrier of (S,T) -defined the carrier of (S,T) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (S,T):]
[: the carrier of (S,T), the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of (S,T), the carrier of (S,T):] is non empty set
(S,S,T,T,(id S),(id T)) is non empty Relation-like the carrier of (S,T) -defined the carrier of (S,T) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (S,T):]
id (S,T) is non empty Relation-like the carrier of (S,T) -defined the carrier of (S,T) -valued Function-like one-to-one V27( the carrier of (S,T)) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (S,T), the carrier of (S,T):]
id the carrier of (S,T) is non empty Relation-like the carrier of (S,T) -defined the carrier of (S,T) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (S,T)) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (S,T):]
(R,S,T,F,F,G) * (S,R,F,T,x,G) is non empty Relation-like the carrier of (R,F) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (R,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,F), the carrier of (R,F):]
[: the carrier of (R,F), the carrier of (R,F):] is non empty Relation-like set
bool [: the carrier of (R,F), the carrier of (R,F):] is non empty set
(R,R,F,F,(id R),(id F)) is non empty Relation-like the carrier of (R,F) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (R,F)) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,F), the carrier of (R,F):]
id (R,F) is non empty Relation-like the carrier of (R,F) -defined the carrier of (R,F) -valued Function-like one-to-one V27( the carrier of (R,F)) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (R,F), the carrier of (R,F):]
id the carrier of (R,F) is non empty Relation-like the carrier of (R,F) -defined the carrier of (R,F) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (R,F)) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (R,F), the carrier of (R,F):]
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
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
F is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,F) 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
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 T is non empty set
the carrier of F is non empty set
[: the carrier of T, the carrier of F:] is non empty Relation-like set
bool [: the carrier of T, the carrier of F:] is non empty set
G is non empty Relation-like the carrier of T -defined the carrier of F -valued Function-like V27( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of F:]
(R,S,T,F,F,G) is non empty Relation-like the carrier of (S,T) -defined the carrier of (R,F) -valued Function-like V27( the carrier of (S,T)) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,T), the carrier of (R,F):]
the carrier of (S,T) is non empty functional set
the carrier of (R,F) is non empty functional set
[: the carrier of (S,T), the carrier of (R,F):] is non empty Relation-like set
bool [: the carrier of (S,T), the carrier of (R,F):] is non empty 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
(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
id R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is non empty set
[: 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
id the carrier of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of R) quasi_total onto bijective Element of bool [: the carrier of R, the carrier of R:]
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 monotone directed-sups-preserving projection Element of bool [: the carrier of S, the carrier of S:]
(R,R,S,S,(id R),T) is non empty Relation-like the carrier of (R,S) -defined the carrier of (R,S) -valued Function-like V27( the carrier of (R,S)) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,S), the carrier of (R,S):]
the carrier of (R,S) is non empty functional set
[: 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
Image (R,R,S,S,(id R),T) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of (R,S)
rng (R,R,S,S,(id R),T) is non empty functional Element of bool the carrier of (R,S)
bool the carrier of (R,S) is non empty set
subrelstr (rng (R,R,S,S,(id R),T)) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of (R,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
(R,(Image T)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
F is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
F |^ 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
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
(R,F) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(Image T) |^ the carrier of R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
F is reflexive transitive antisymmetric full SubRelStr of S |^ the carrier of R
the carrier of F is set
G is reflexive transitive antisymmetric full SubRelStr of S |^ the carrier of R
the carrier of G is set
G is set
dom (R,R,S,S,(id R),T) is non empty functional Element of bool the carrier of (R,S)
the carrier of F is non empty set
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
x is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of F:]
rng x is non empty Element of bool the carrier of F
bool the carrier of F is non empty set
dom x is non empty Element of bool the carrier of R
bool the carrier of R 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:]
x is Element of bool the carrier of R
x .: x is Element of bool the carrier of F
f .: x is Element of bool the carrier of S
"\/" ((f .: x),S) is Element of the carrier of S
"\/" (x,R) is Element of the carrier of R
f . ("\/" (x,R)) is Element of the carrier of S
s is non empty directed Element of bool the carrier of F
"\/" (s,F) is Element of the carrier of F
x . ("\/" (x,R)) is Element of the carrier of F
(R,R,S,S,(id R),T) . f is Relation-like Function-like set
T * 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:]
(T * f) * (id R) 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:]
x * (id R) is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
G is set
the carrier of (subrelstr (rng T)) is non empty set
dom (R,R,S,S,(id R),T) is non empty functional Element of bool the carrier of (R,S)
x is set
(R,R,S,S,(id R),T) . x is Relation-like Function-like 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 monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]
T * 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:]
(T * f) * (id R) 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:]
x is non empty Relation-like the carrier of R -defined the carrier of S -valued Function-like V27( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of S:]
rng x is non empty Element of bool the carrier of S
dom x is non empty Element of bool the carrier of R
bool the carrier of R is non empty set
the carrier of F is non empty set
[: the carrier of R, the carrier of F:] is non empty Relation-like set
bool [: the carrier of R, the carrier of F:] is non empty set
s is non empty Relation-like the carrier of R -defined the carrier of F -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of F:]
s1 is Element of bool the carrier of R
x .: s1 is Element of bool the carrier of S
bool the carrier of F is non empty set
s .: s1 is Element of bool the carrier of F
"\/" ((s .: s1),F) is Element of the carrier of F
"\/" (s1,R) is Element of the carrier of R
s . ("\/" (s1,R)) is Element of the carrier of F
gX is non empty directed Element of bool the carrier of F
"\/" (gX,F) is Element of the carrier of F
As is non empty directed Element of bool the carrier of S
"\/" (As,S) is Element of the carrier of S
S is non empty reflexive transitive antisymmetric non void RelStr
the carrier of 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
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
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
F is non empty Relation-like the carrier of S -defined the carrier of (T |^ R) -valued Function-like V27( the carrier of S) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of (T |^ R):]
rng F is non empty functional Element of bool the carrier of (T |^ R)
bool the carrier of (T |^ R) is non empty set
dom F is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
Funcs ( the carrier of S,(Funcs (R, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of S, Funcs (R, the carrier of T)
commute F is Relation-like Function-like Function-yielding V33() set
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs (R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of R, Funcs ( the carrier of S, the carrier of T)
proj2 (commute F) is set
proj1 (commute F) is set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
R is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
the carrier of S 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
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
F is non empty Relation-like the carrier of S -defined the carrier of (T |^ R) -valued Function-like V27( the carrier of S) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of (T |^ R):]
commute F is Relation-like Function-like Function-yielding V33() set
F is Element of R
(commute F) . F is Relation-like Function-like set
R --> T is non empty Relation-like R -defined {T} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [:R,{T}:]
{T} is non empty set
[:R,{T}:] is non empty Relation-like set
bool [:R,{T}:] is non empty set
(R --> T) . F is non empty reflexive transitive antisymmetric non void RelStr
proj1 (commute F) is set
proj2 (commute F) is set
Funcs (R, the carrier of T) is non empty functional FUNCTION_DOMAIN of R, the carrier of T
Funcs ( the carrier of S,(Funcs (R, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of S, Funcs (R, the carrier of T)
[: the carrier of S,(Funcs (R, the carrier of T)):] is non empty Relation-like set
bool [: the carrier of S,(Funcs (R, the carrier of T)):] is non empty set
rng F is non empty functional Element of bool the carrier of (T |^ R)
bool the carrier of (T |^ R) is non empty set
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
G is Relation-like Function-like set
proj1 G is set
proj2 G is set
product (R --> T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
G is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
bool the carrier of S is non empty set
x is Element of bool the carrier of S
G .: x is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((G .: x),T) is Element of the carrier of T
"\/" (x,S) is Element of the carrier of S
G . ("\/" (x,S)) is Element of the carrier of T
f is non empty directed Element of bool the carrier of S
F .: f is non empty functional Element of bool the carrier of (T |^ R)
F .: x is functional Element of bool the carrier of (T |^ R)
pi ((F .: x),F) is Element of bool the carrier of T
"\/" ((F .: f),(T |^ R)) is Relation-like Function-like Element of the carrier of (T |^ R)
"\/" (f,S) is Element of the carrier of S
F . ("\/" (f,S)) is Relation-like Function-like Element of the carrier of (T |^ R)
"\/" ((pi ((F .: x),F)),T) is Element of the carrier of T
F . ("\/" (x,S)) is Relation-like Function-like Element of the carrier of (T |^ R)
(R,T,(F . ("\/" (x,S))),F) is Element of the carrier of T
R is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
the carrier of S 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
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty functional set
[:R, the carrier of (S,T):] is non empty Relation-like set
bool [:R, the carrier of (S,T):] is non empty set
F is non empty Relation-like the carrier of S -defined the carrier of (T |^ R) -valued Function-like V27( the carrier of S) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of (T |^ R):]
commute F is Relation-like Function-like Function-yielding V33() set
proj2 (commute F) is set
F is set
proj1 (commute F) is set
G is set
(commute F) . G is Relation-like Function-like set
G is Element of R
(commute F) . G is Relation-like Function-like set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
proj1 (commute F) is set
R is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
T is non empty reflexive transitive antisymmetric non void RelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty functional set
[:R, the carrier of (S,T):] is non empty Relation-like set
bool [:R, the carrier of (S,T):] is non empty set
the carrier of S is non empty set
T |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
F is non empty Relation-like R -defined the carrier of (S,T) -valued Function-like V27(R) quasi_total Function-yielding V33() Element of bool [:R, the carrier of (S,T):]
commute F is Relation-like Function-like Function-yielding V33() set
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 (R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of R, the carrier of (S,T)
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs (R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of R, Funcs ( the carrier of S, the carrier of T)
Funcs ( the carrier of S,(Funcs (R, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of S, Funcs (R, the carrier of T)
F is non empty Relation-like the carrier of S -defined the carrier of (T |^ R) -valued Function-like V27( the carrier of S) quasi_total Function-yielding V33() Element of bool [: the carrier of S, the carrier of (T |^ R):]
rng F is non empty functional Element of bool the carrier of (T |^ R)
bool the carrier of (T |^ R) is non empty set
bool the carrier of S is non empty set
G is Element of bool the carrier of S
R --> T is non empty Relation-like R -defined {T} -valued Function-like constant V27(R) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [:R,{T}:]
{T} is non empty set
[:R,{T}:] is non empty Relation-like set
bool [:R,{T}:] is non empty set
product (R --> T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
"\/" (G,S) is Element of the carrier of S
F . ("\/" (G,S)) is Relation-like Function-like Element of the carrier of (T |^ R)
proj1 (F . ("\/" (G,S))) is set
F .: G is functional Element of bool the carrier of (T |^ R)
"\/" ((F .: G),(T |^ R)) is Relation-like Function-like Element of the carrier of (T |^ R)
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
x is Element of R
F . x is Relation-like Function-like Element of the carrier of (S,T)
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
G is non empty directed Element of bool the carrier of S
commute F is Relation-like Function-like Function-yielding V33() set
f .: G is Element of bool the carrier of T
bool the carrier of T is non empty set
pi ((F .: G),x) is Element of bool the carrier of T
(R --> T) . x is non empty reflexive transitive antisymmetric non void RelStr
x is set
f is Element of R
F . f is Relation-like Function-like Element of the carrier of (S,T)
(R --> T) . f is non empty reflexive transitive antisymmetric non void RelStr
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
x .: G is Element of bool the carrier of T
pi ((F .: G),f) is Element of bool the carrier of T
F .: G is non empty functional Element of bool the carrier of (T |^ R)
pi ((F .: G),f) is non empty Element of bool the carrier of T
"\/" ((pi ((F .: G),f)),T) is Element of the carrier of T
x . ("\/" (G,S)) is Element of the carrier of T
"\/" ((F .: G),(T |^ R)) is Relation-like Function-like Element of the carrier of (T |^ R)
(R,T,("\/" ((F .: G),(T |^ R))),f) is Element of the carrier of T
("\/" ((F .: G),(T |^ R))) . x is set
(F . ("\/" (G,S))) . x is set
proj1 ("\/" ((F .: G),(T |^ R))) is set
R is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
T is non empty reflexive transitive antisymmetric non void RelStr
T |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(S,(T |^ R)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,(T |^ R)) is non empty functional set
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(S,T) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of ((S,T) |^ R) is non empty functional set
[: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):] is non empty Relation-like set
bool [: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):] is non empty set
F is Relation-like the carrier of (S,(T |^ R)) -defined Function-like V27( the carrier of (S,(T |^ R))) set
dom F is functional Element of bool the carrier of (S,(T |^ R))
bool the carrier of (S,(T |^ R)) is non empty set
proj2 F is set
F is set
G is set
F . G is set
the carrier of S is non empty set
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
G is non empty Relation-like the carrier of S -defined the carrier of (T |^ R) -valued Function-like V27( the carrier of S) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of (T |^ R):]
commute G is Relation-like Function-like Function-yielding V33() set
the carrier of (S,T) is non empty functional set
[:R, the carrier of (S,T):] is non empty Relation-like set
bool [:R, the carrier of (S,T):] is non empty set
x is non empty Relation-like R -defined the carrier of (S,T) -valued Function-like V27(R) quasi_total Function-yielding V33() Element of bool [:R, the carrier of (S,T):]
rng x is non empty functional Element of bool the carrier of (S,T)
bool the carrier of (S,T) is non empty set
dom x is non empty Element of bool R
bool R is non empty set
Funcs (R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of R, the carrier of (S,T)
F is non empty Relation-like the carrier of (S,(T |^ R)) -defined the carrier of ((S,T) |^ R) -valued Function-like V27( the carrier of (S,(T |^ R))) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):]
G is Relation-like the carrier of ((S,T) |^ R) -defined Function-like V27( the carrier of ((S,T) |^ R)) set
dom G is functional Element of bool the carrier of ((S,T) |^ R)
bool the carrier of ((S,T) |^ R) is non empty set
proj2 G is set
G is set
x is set
G . x is set
the carrier of (S,T) is non empty functional set
Funcs (R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of R, the carrier of (S,T)
[:R, the carrier of (S,T):] is non empty Relation-like set
bool [:R, the carrier of (S,T):] is non empty set
f is non empty Relation-like R -defined the carrier of (S,T) -valued Function-like V27(R) quasi_total Function-yielding V33() Element of bool [:R, the carrier of (S,T):]
commute f is Relation-like Function-like Function-yielding V33() set
the carrier of S is non empty set
the carrier of (T |^ R) is non empty functional set
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
[: the carrier of ((S,T) |^ R), the carrier of (S,(T |^ R)):] is non empty Relation-like set
bool [: the carrier of ((S,T) |^ R), the carrier of (S,(T |^ R)):] is non empty set
G is non empty Relation-like the carrier of ((S,T) |^ R) -defined the carrier of (S,(T |^ R)) -valued Function-like V27( the carrier of ((S,T) |^ R)) quasi_total Function-yielding V33() Element of bool [: the carrier of ((S,T) |^ R), the carrier of (S,(T |^ R)):]
x is set
dom G is non empty functional Element of bool the carrier of ((S,T) |^ R)
the carrier of (S,T) is non empty functional set
Funcs (R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of R, the carrier of (S,T)
[:R, the carrier of (S,T):] is non empty Relation-like set
bool [:R, the carrier of (S,T):] is non empty set
proj1 G is non empty set
x is Relation-like Function-like set
G . x is Relation-like Function-like set
commute x is Relation-like Function-like Function-yielding V33() set
the carrier of (T |^ R) is non empty functional set
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
the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(T |^ the carrier of S) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(T |^ R) |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
x is set
dom F is non empty functional Element of bool the carrier of (S,(T |^ R))
[: the carrier of S, the carrier of (T |^ R):] is non empty Relation-like set
bool [: the carrier of S, the carrier of (T |^ R):] is non empty set
proj1 F is non empty set
x is Relation-like Function-like set
F . x is Relation-like Function-like set
commute x is Relation-like Function-like Function-yielding V33() set
the carrier of (S,T) is non empty functional set
Funcs (R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of R, the carrier of (S,T)
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs (R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of R, Funcs ( the carrier of S, the carrier of T)
F * G is non empty Relation-like the carrier of ((S,T) |^ R) -defined the carrier of ((S,T) |^ R) -valued Function-like V27( the carrier of ((S,T) |^ R)) quasi_total Function-yielding V33() Element of bool [: the carrier of ((S,T) |^ R), the carrier of ((S,T) |^ R):]
[: the carrier of ((S,T) |^ R), the carrier of ((S,T) |^ R):] is non empty Relation-like set
bool [: the carrier of ((S,T) |^ R), the carrier of ((S,T) |^ R):] is non empty set
id ((S,T) |^ R) is non empty Relation-like the carrier of ((S,T) |^ R) -defined the carrier of ((S,T) |^ R) -valued Function-like one-to-one V27( the carrier of ((S,T) |^ R)) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of ((S,T) |^ R), the carrier of ((S,T) |^ R):]
id the carrier of ((S,T) |^ R) is non empty Relation-like the carrier of ((S,T) |^ R) -defined the carrier of ((S,T) |^ R) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of ((S,T) |^ R)) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of ((S,T) |^ R), the carrier of ((S,T) |^ R):]
Funcs ( the carrier of S, the carrier of (T |^ R)) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of (T |^ R)
G * F is non empty Relation-like the carrier of (S,(T |^ R)) -defined the carrier of (S,(T |^ R)) -valued Function-like V27( the carrier of (S,(T |^ R))) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,(T |^ R)), the carrier of (S,(T |^ R)):]
[: the carrier of (S,(T |^ R)), the carrier of (S,(T |^ R)):] is non empty Relation-like set
bool [: the carrier of (S,(T |^ R)), the carrier of (S,(T |^ R)):] is non empty set
id (S,(T |^ R)) is non empty Relation-like the carrier of (S,(T |^ R)) -defined the carrier of (S,(T |^ R)) -valued Function-like one-to-one V27( the carrier of (S,(T |^ R))) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (S,(T |^ R)), the carrier of (S,(T |^ R)):]
id the carrier of (S,(T |^ R)) is non empty Relation-like the carrier of (S,(T |^ R)) -defined the carrier of (S,(T |^ R)) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (S,(T |^ R))) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (S,(T |^ R)), the carrier of (S,(T |^ R)):]
R is non empty set
S is non empty reflexive transitive antisymmetric non void RelStr
T is non empty reflexive transitive antisymmetric non void RelStr
T |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(S,(T |^ R)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(S,T) |^ R is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,(T |^ R)) is non empty functional set
the carrier of ((S,T) |^ R) is non empty functional set
[: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):] is non empty Relation-like set
bool [: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):] is non empty set
F is non empty Relation-like the carrier of (S,(T |^ R)) -defined the carrier of ((S,T) |^ R) -valued Function-like V27( the carrier of (S,(T |^ R))) quasi_total Function-yielding V33() Element of bool [: the carrier of (S,(T |^ R)), the carrier of ((S,T) |^ R):]
R is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete V375() continuous non void RelStr
S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete V375() continuous 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
T is non empty set
BoolePoset T 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 T) is non empty set
[: the carrier of (BoolePoset T), the carrier of (BoolePoset T):] is non empty Relation-like set
bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):] is non empty set
F is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of (BoolePoset T)) quasi_total idempotent monotone projection Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
Image F is non empty strict reflexive transitive antisymmetric full non void SubRelStr of BoolePoset T
rng F is non empty Element of bool the carrier of (BoolePoset T)
bool the carrier of (BoolePoset T) is non empty set
subrelstr (rng F) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of BoolePoset T
the carrier of R is non empty set
id R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of R) quasi_total onto bijective Element of bool [: the carrier of R, the carrier of R:]
(id R) * (id R) is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
(R,(Image F)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
(R,(BoolePoset T)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
the carrier of (R,(BoolePoset T)) is non empty functional set
[: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):] is non empty Relation-like set
bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):] is non empty set
Image (R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of (R,(BoolePoset T))
rng (R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty functional Element of bool the carrier of (R,(BoolePoset T))
bool the carrier of (R,(BoolePoset T)) is non empty set
subrelstr (rng (R,R,(BoolePoset T),(BoolePoset T),(id R),F)) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of (R,(BoolePoset T))
the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R
sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty Element of bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R)
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty set
bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty set
bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R) is non empty set
InclPoset (sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R) is non empty strict reflexive transitive antisymmetric non void RelStr
(R,(BoolePoset 1)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
sigma R is non empty 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
InclPoset (sigma R) is non empty strict reflexive transitive antisymmetric non void RelStr
F * F is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of (BoolePoset T)) quasi_total Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) * (R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
(BoolePoset 1) |^ T is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,((BoolePoset 1) |^ T)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R -defined 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R -valued Element of bool [: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:]
[: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:] is non empty Relation-like set
bool [: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:] is non empty set
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr
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:]
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
T --> (R,(BoolePoset 1)) is non empty Relation-like T -defined {(R,(BoolePoset 1))} -valued Function-like constant V27(T) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [:T,{(R,(BoolePoset 1))}:]
{(R,(BoolePoset 1))} is non empty set
[:T,{(R,(BoolePoset 1))}:] is non empty Relation-like set
bool [:T,{(R,(BoolePoset 1))}:] is non empty set
G is Element of T
(T --> (R,(BoolePoset 1))) . G is non empty reflexive transitive antisymmetric non void RelStr
product (T --> (R,(BoolePoset 1))) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,(BoolePoset 1)) |^ T 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() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous non void RelStr
S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() satisfying_axiom_K algebraic up-complete /\-complete V375() continuous 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
T is non empty set
BoolePoset T 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 T) is non empty set
[: the carrier of (BoolePoset T), the carrier of (BoolePoset T):] is non empty Relation-like set
bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):] is non empty set
F is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of (BoolePoset T)) quasi_total idempotent monotone projection closure Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
Image F is non empty strict reflexive transitive antisymmetric V220() full meet-inheriting infs-inheriting filtered-infs-inheriting non void SubRelStr of BoolePoset T
rng F is non empty Element of bool the carrier of (BoolePoset T)
bool the carrier of (BoolePoset T) is non empty set
subrelstr (rng F) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of BoolePoset T
(R,(BoolePoset T)) 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,(BoolePoset T)) is non empty functional set
the carrier of R is non empty set
[: the carrier of R, the carrier of (BoolePoset T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (BoolePoset T):] is non empty set
F is Relation-like Function-like Element of the carrier of (R,(BoolePoset T))
id R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel 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
id the carrier of R is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of R) quasi_total onto bijective Element of bool [: the carrier of R, the carrier of R:]
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
[: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):] is non empty Relation-like set
bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):] is non empty set
G is non empty Relation-like the carrier of R -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of R) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of (BoolePoset T):]
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) . G is Relation-like Function-like set
F * G is non empty Relation-like the carrier of R -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of (BoolePoset T):]
(F * G) * (id the carrier of R) is non empty Relation-like the carrier of R -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of (BoolePoset T):]
id (BoolePoset T) is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like one-to-one V27( the carrier of (BoolePoset T)) quasi_total idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
id the carrier of (BoolePoset T) is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (BoolePoset T)) quasi_total onto bijective Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
G is Element of the carrier of R
(R,(BoolePoset T),F,G) is Element of the carrier of (BoolePoset T)
(id (BoolePoset T)) . (R,(BoolePoset T),F,G) is Element of the carrier of (BoolePoset T)
(F * G) . G is Element of the carrier of (BoolePoset T)
G . G is Element of the carrier of (BoolePoset T)
F . (G . G) is Element of the carrier of (BoolePoset T)
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) . F is Relation-like Function-like Element of the carrier of (R,(BoolePoset T))
(R,(BoolePoset T),((R,R,(BoolePoset T),(BoolePoset T),(id R),F) . F),G) is Element of the carrier of (BoolePoset T)
id (R,(BoolePoset T)) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like one-to-one V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
id the carrier of (R,(BoolePoset T)) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (R,(BoolePoset T))) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
(id (R,(BoolePoset T))) . F is Relation-like Function-like Element of the carrier of (R,(BoolePoset T))
(id R) * (id R) is non empty Relation-like the carrier of R -defined the carrier of R -valued Function-like one-to-one V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of R:]
F * F is non empty Relation-like the carrier of (BoolePoset T) -defined the carrier of (BoolePoset T) -valued Function-like V27( the carrier of (BoolePoset T)) quasi_total Element of bool [: the carrier of (BoolePoset T), the carrier of (BoolePoset T):]
(R,R,(BoolePoset T),(BoolePoset T),(id R),F) * (R,R,(BoolePoset T),(BoolePoset T),(id R),F) is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
(R,(Image F)) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
F is non empty Relation-like the carrier of (R,(BoolePoset T)) -defined the carrier of (R,(BoolePoset T)) -valued Function-like V27( the carrier of (R,(BoolePoset T))) quasi_total Function-yielding V33() idempotent monotone directed-sups-preserving projection closure Element of bool [: the carrier of (R,(BoolePoset T)), the carrier of (R,(BoolePoset T)):]
Image F is non empty constituted-Functions strict reflexive transitive antisymmetric V220() full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting non void SubRelStr of (R,(BoolePoset T))
rng F is non empty functional Element of bool the carrier of (R,(BoolePoset T))
bool the carrier of (R,(BoolePoset T)) is non empty set
subrelstr (rng F) is non empty constituted-Functions strict reflexive transitive antisymmetric full non void SubRelStr of (R,(BoolePoset T))
(BoolePoset 1) |^ T is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,((BoolePoset 1) |^ T)) 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 V375() continuous V381() 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R
sigma R is non empty 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
InclPoset (sigma R) is non empty strict reflexive transitive antisymmetric non void RelStr
the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R is Element of bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R)
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty set
bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty set
bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R) is non empty set
InclPoset the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty non trivial strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void distributive RelStr
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R -defined 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R -valued Element of bool [: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:]
[: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:] is non empty Relation-like set
bool [: 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R:] is non empty set
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 V375() continuous V381() non void monotone-convergence TopAugmentation of R, 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded up-complete non void RelStr
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:]
RelStr(# the carrier of R, the InternalRel of R #) is non empty strict reflexive transitive antisymmetric V219() V220() upper-bounded satisfying_axiom_K algebraic up-complete V375() continuous non void RelStr
CompactSublatt the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty strict reflexive transitive antisymmetric V219() full join-inheriting non void SubRelStr of the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R
the carrier of (CompactSublatt the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R) is non empty set
{ (uparrow b₁) where b₁ is Element of 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R : b₁ in the carrier of (CompactSublatt the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R) } is set
sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R is non empty Element of bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R)
InclPoset (sigma the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R) is non empty strict reflexive transitive antisymmetric non void RelStr
G is open V79( the non empty TopSpace-like T_0 reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete Scott V375() continuous V381() non void monotone-convergence TopAugmentation of R) Element of bool (bool 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 V375() continuous V381() non void monotone-convergence TopAugmentation of R)
(R,(BoolePoset 1)) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
T --> (R,(BoolePoset 1)) is non empty Relation-like T -defined {(R,(BoolePoset 1))} -valued Function-like constant V27(T) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [:T,{(R,(BoolePoset 1))}:]
{(R,(BoolePoset 1))} is non empty set
[:T,{(R,(BoolePoset 1))}:] is non empty Relation-like set
bool [:T,{(R,(BoolePoset 1))}:] is non empty set
product (T --> (R,(BoolePoset 1))) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,(BoolePoset 1)) |^ T 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
the carrier of R is non empty set
S is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(S,T) 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 (S,T) is non empty functional set
[: the carrier of R, the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (S,T):] is non empty set
[:R,S:] is non empty 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 set
the carrier of T is non empty set
[: the carrier of [:R,S:], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:R,S:], the carrier of T:] is non empty set
F is non empty Relation-like the carrier of R -defined the carrier of (S,T) -valued Function-like V27( the carrier of R) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of (S,T):]
uncurry F is Relation-like Function-like set
Funcs ( the carrier of R, the carrier of (S,T)) is non empty functional FUNCTION_DOMAIN of the carrier of R, the carrier of (S,T)
the carrier of S is non empty set
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of R, Funcs ( the carrier of S, the carrier of T)
[: the carrier of R, the carrier of S:] is non empty Relation-like set
Funcs ([: the carrier of R, the carrier of S:], the carrier of T) is non empty functional FUNCTION_DOMAIN of [: the carrier of R, the carrier of S:], the carrier of T
Funcs ( the carrier of [:R,S:], the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of [:R,S:], the carrier of T
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
G is non empty constituted-Functions reflexive transitive antisymmetric V219() full join-inheriting sups-inheriting directed-sups-inheriting non void SubRelStr of T |^ the carrier of S
the carrier of G is non empty functional set
[: the carrier of R, the carrier of G:] is non empty Relation-like set
bool [: the carrier of R, the carrier of G:] is non empty set
incl (G,(T |^ the carrier of S)) is non empty Relation-like the carrier of G -defined the carrier of (T |^ the carrier of S) -valued Function-like V27( the carrier of G) quasi_total Function-yielding V33() monotone Element of bool [: the carrier of G, the carrier of (T |^ the carrier of S):]
the carrier of (T |^ the carrier of S) is non empty functional set
[: the carrier of G, the carrier of (T |^ the carrier of S):] is non empty Relation-like set
bool [: the carrier of G, the carrier of (T |^ the carrier of S):] is non empty set
f is non empty Relation-like the carrier of R -defined the carrier of G -valued Function-like V27( the carrier of R) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of G:]
(incl (G,(T |^ the carrier of S))) * f is non empty Relation-like the carrier of R -defined the carrier of (T |^ the carrier of S) -valued Function-like V27( the carrier of R) quasi_total Function-yielding V33() Element of bool [: the carrier of R, the carrier of (T |^ the carrier of S):]
[: the carrier of R, the carrier of (T |^ the carrier of S):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (T |^ the carrier of S):] is non empty set
id the carrier of G is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of G) quasi_total onto bijective Function-yielding V33() 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
commute F is Relation-like Function-like Function-yielding V33() set
x is Element of the carrier of S
(commute F) . x is Relation-like Function-like 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
rng F is non empty functional Element of bool the carrier of (S,T)
bool the carrier of (S,T) is non empty set
F is non empty Relation-like the carrier of [:R,S:] -defined the carrier of T -valued Function-like V27( the carrier of [:R,S:]) quasi_total Element of bool [: the carrier of [:R,S:], the carrier of T:]
curry F is Relation-like Function-like set
G is Element of the carrier of R
Proj (F,G) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
F . G is Relation-like Function-like Element of the carrier of (S,T)
Proj (F,x) 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:]
curry' F is Relation-like Function-like set
(curry' F) . x is set
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 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 set
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
the carrier of T is non empty set
[: the carrier of [:R,S:], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:R,S:], the carrier of T:] is non empty set
the carrier of R is non empty set
(S,T) 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 (S,T) is non empty functional set
[: the carrier of R, the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (S,T):] 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
F is non empty Relation-like the carrier of [:R,S:] -defined the carrier of T -valued Function-like V27( the carrier of [:R,S:]) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of [:R,S:], the carrier of T:]
curry F is Relation-like Function-like set
([:R,S:],T) 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:],T) is non empty functional set
Funcs ( the carrier of [:R,S:], the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of [:R,S:], the carrier of T
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of R, Funcs ( the carrier of S, the carrier of T)
[: the carrier of R,(Funcs ( the carrier of S, the carrier of T)):] is non empty Relation-like set
bool [: the carrier of R,(Funcs ( the carrier of S, the carrier of T)):] is non empty set
proj1 (curry F) is set
proj2 (curry F) is set
F is set
G is set
(curry F) . G is set
G is Element of the carrier of R
Proj (F,G) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
[: the carrier of S, the carrier of T:] is non empty Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
dom F is non empty Element of bool the carrier of [:R,S:]
bool the carrier of [:R,S:] is non empty set
F is non empty Relation-like the carrier of R -defined the carrier of (S,T) -valued Function-like V27( the carrier of R) quasi_total Function-yielding V33() Element of bool [: the carrier of R, the carrier of (S,T):]
bool the carrier of R is non empty set
G is Element of bool the carrier of R
the carrier of (T |^ the carrier of S) is non empty functional set
"\/" (G,R) is Element of the carrier of R
F . ("\/" (G,R)) is Relation-like Function-like Element of the carrier of (S,T)
F .: G is functional Element of bool the carrier of (S,T)
bool the carrier of (S,T) is non empty set
"\/" ((F .: G),(S,T)) is Relation-like Function-like Element of the carrier of (S,T)
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like constant V27( the carrier of S) quasi_total RelStr-yielding V371() V377() V378() V383() Element of bool [: the carrier of S,{T}:]
{T} is non empty set
[: the carrier of S,{T}:] is non empty Relation-like set
bool [: the carrier of S,{T}:] is non empty set
f is Element of the carrier of S
( the carrier of S --> T) . f is non empty reflexive transitive antisymmetric non void RelStr
G is non empty directed Element of bool the carrier of R
F .: G is non empty functional Element of bool the carrier of (S,T)
bool the carrier of (T |^ the carrier of S) is non empty set
product ( the carrier of S --> T) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
x is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
proj1 x is set
x is set
bool the carrier of S is non empty set
s is Element of the carrier of S
{s} is non empty Element of bool the carrier of S
s1 is non empty directed Element of bool the carrier of S
[:G,s1:] is non empty Relation-like directed Element of bool the carrier of [:R,S:]
As is non empty directed Element of bool the carrier of [:R,S:]
( the carrier of S --> T) . s is non empty reflexive transitive antisymmetric non void RelStr
f is non empty functional Element of bool the carrier of (T |^ the carrier of S)
"\/" (f,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
("\/" (f,(T |^ the carrier of S))) . x is set
pi (f,s) is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((pi (f,s)),T) is Element of the carrier of T
F .: As is non empty Element of bool the carrier of T
"\/" ((F .: As),T) is Element of the carrier of T
"\/" (As,[:R,S:]) is Element of the carrier of [:R,S:]
F . ("\/" (As,[:R,S:])) is Element of the carrier of T
proj1 As is Element of bool the carrier of R
"\/" ((proj1 As),R) is Element of the carrier of R
proj2 As is Element of bool the carrier of S
"\/" ((proj2 As),S) is Element of the carrier of S
[("\/" ((proj1 As),R)),("\/" ((proj2 As),S))] is V1() Element of the carrier of [:R,S:]
{("\/" ((proj1 As),R)),("\/" ((proj2 As),S))} is non empty set
{("\/" ((proj1 As),R))} is non empty set
{{("\/" ((proj1 As),R)),("\/" ((proj2 As),S))},{("\/" ((proj1 As),R))}} is non empty set
F . [("\/" ((proj1 As),R)),("\/" ((proj2 As),S))] is Element of the carrier of T
[("\/" (G,R)),("\/" ((proj2 As),S))] is V1() Element of the carrier of [:R,S:]
{("\/" (G,R)),("\/" ((proj2 As),S))} is non empty set
{("\/" (G,R))} is non empty set
{{("\/" (G,R)),("\/" ((proj2 As),S))},{("\/" (G,R))}} is non empty set
F . [("\/" (G,R)),("\/" ((proj2 As),S))] is Element of the carrier of T
"\/" ({s},S) is Element of the carrier of S
[("\/" (G,R)),("\/" ({s},S))] is V1() Element of the carrier of [:R,S:]
{("\/" (G,R)),("\/" ({s},S))} is non empty set
{{("\/" (G,R)),("\/" ({s},S))},{("\/" (G,R))}} is non empty set
F . [("\/" (G,R)),("\/" ({s},S))] is Element of the carrier of T
F . (("\/" (G,R)),s) is set
[("\/" (G,R)),s] is V1() set
{("\/" (G,R)),s} is non empty set
{{("\/" (G,R)),s},{("\/" (G,R))}} is non empty set
F . [("\/" (G,R)),s] is set
x . x is set
proj1 ("\/" (f,(T |^ the carrier of S))) is set
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
T is non empty reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
(R,(S,T)) 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,T)) is non empty functional set
[:R,S:] is non empty strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
([:R,S:],T) 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:],T) is non empty functional set
[: the carrier of (R,(S,T)), the carrier of ([:R,S:],T):] is non empty Relation-like set
bool [: the carrier of (R,(S,T)), the carrier of ([:R,S:],T):] is non empty set
F is Relation-like the carrier of (R,(S,T)) -defined Function-like V27( the carrier of (R,(S,T))) set
dom F is functional Element of bool the carrier of (R,(S,T))
bool the carrier of (R,(S,T)) is non empty set
proj2 F is set
F is set
G is set
F . G is set
the carrier of R is non empty set
the carrier of (S,T) is non empty functional set
[: the carrier of R, the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (S,T):] is non empty set
G is non empty Relation-like the carrier of R -defined the carrier of (S,T) -valued Function-like V27( the carrier of R) quasi_total Function-yielding V33() monotone directed-sups-preserving Element of bool [: the carrier of R, the carrier of (S,T):]
uncurry G is Relation-like Function-like set
the carrier of [:R,S:] is non empty set
the carrier of T is non empty set
[: the carrier of [:R,S:], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:R,S:], the carrier of T:] is non empty set
F is non empty Relation-like the carrier of (R,(S,T)) -defined the carrier of ([:R,S:],T) -valued Function-like V27( the carrier of (R,(S,T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(S,T)), the carrier of ([:R,S:],T):]
G is set
dom F is non empty functional Element of bool the carrier of (R,(S,T))
the carrier of R is non empty set
the carrier of (S,T) is non empty functional set
[: the carrier of R, the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (S,T):] is non empty set
proj1 F is non empty set
G is Relation-like Function-like set
F . G is Relation-like Function-like set
uncurry G is Relation-like Function-like set
G is Relation-like the carrier of ([:R,S:],T) -defined Function-like V27( the carrier of ([:R,S:],T)) set
dom G is functional Element of bool the carrier of ([:R,S:],T)
bool the carrier of ([:R,S:],T) is non empty set
proj2 G is set
G is set
x is set
G . x is set
the carrier of [:R,S:] is non empty set
the carrier of T is non empty set
[: the carrier of [:R,S:], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:R,S:], the carrier of T:] is non empty set
f is non empty Relation-like the carrier of [:R,S:] -defined the carrier of T -valued Function-like V27( the carrier of [:R,S:]) quasi_total monotone directed-sups-preserving Element of bool [: the carrier of [:R,S:], the carrier of T:]
curry f is Relation-like Function-like set
the carrier of R is non empty set
the carrier of (S,T) is non empty functional set
[: the carrier of R, the carrier of (S,T):] is non empty Relation-like set
bool [: the carrier of R, the carrier of (S,T):] is non empty set
[: the carrier of ([:R,S:],T), the carrier of (R,(S,T)):] is non empty Relation-like set
bool [: the carrier of ([:R,S:],T), the carrier of (R,(S,T)):] is non empty set
the carrier of S is non empty set
T |^ the carrier of 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,T) |^ 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
(T |^ the carrier of 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 set
[: the carrier of R, the carrier of S:] is non empty Relation-like set
T |^ [: the carrier of R, the carrier of S:] is non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete lower-bounded upper-bounded V307() up-complete /\-complete non void RelStr
G is non empty Relation-like the carrier of ([:R,S:],T) -defined the carrier of (R,(S,T)) -valued Function-like V27( the carrier of ([:R,S:],T)) quasi_total Function-yielding V33() Element of bool [: the carrier of ([:R,S:],T), the carrier of (R,(S,T)):]
x is set
dom G is non empty functional Element of bool the carrier of ([:R,S:],T)
the carrier of T is non empty set
[: the carrier of [:R,S:], the carrier of T:] is non empty Relation-like set
bool [: the carrier of [:R,S:], the carrier of T:] is non empty set
f is non empty Relation-like the carrier of [:R,S:] -defined the carrier of T -valued Function-like V27( the carrier of [:R,S:]) quasi_total Element of bool [: the carrier of [:R,S:], the carrier of T:]
proj1 f is non empty set
proj1 x is set
proj1 G is non empty set
x is Relation-like Function-like set
G . x is Relation-like Function-like set
curry x is Relation-like Function-like set
the carrier of ((T |^ the carrier of S) |^ the carrier of R) is non empty functional set
the carrier of (T |^ the carrier of S) is non empty functional set
Funcs ( the carrier of R, the carrier of (T |^ the carrier of S)) is non empty functional FUNCTION_DOMAIN of the carrier of R, the carrier of (T |^ the carrier of S)
the carrier of T is non empty set
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) is non empty functional FUNCTION_DOMAIN of the carrier of R, Funcs ( the carrier of S, the carrier of T)
G * F is non empty Relation-like the carrier of (R,(S,T)) -defined the carrier of (R,(S,T)) -valued Function-like V27( the carrier of (R,(S,T))) quasi_total Function-yielding V33() Element of bool [: the carrier of (R,(S,T)), the carrier of (R,(S,T)):]
[: the carrier of (R,(S,T)), the carrier of (R,(S,T)):] is non empty Relation-like set
bool [: the carrier of (R,(S,T)), the carrier of (R,(S,T)):] is non empty set
id (R,(S,T)) is non empty Relation-like the carrier of (R,(S,T)) -defined the carrier of (R,(S,T)) -valued Function-like one-to-one V27( the carrier of (R,(S,T))) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of (R,(S,T)), the carrier of (R,(S,T)):]
id the carrier of (R,(S,T)) is non empty Relation-like the carrier of (R,(S,T)) -defined the carrier of (R,(S,T)) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of (R,(S,T))) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of (R,(S,T)), the carrier of (R,(S,T)):]
the carrier of (T |^ [: the carrier of R, the carrier of S:]) is non empty functional set
Funcs ([: the carrier of R, the carrier of S:], the carrier of T) is non empty functional FUNCTION_DOMAIN of [: the carrier of R, the carrier of S:], the carrier of T
F * G is non empty Relation-like the carrier of ([:R,S:],T) -defined the carrier of ([:R,S:],T) -valued Function-like V27( the carrier of ([:R,S:],T)) quasi_total Function-yielding V33() Element of bool [: the carrier of ([:R,S:],T), the carrier of ([:R,S:],T):]
[: the carrier of ([:R,S:],T), the carrier of ([:R,S:],T):] is non empty Relation-like set
bool [: the carrier of ([:R,S:],T), the carrier of ([:R,S:],T):] is non empty set
id ([:R,S:],T) is non empty Relation-like the carrier of ([:R,S:],T) -defined the carrier of ([:R,S:],T) -valued Function-like one-to-one V27( the carrier of ([:R,S:],T)) quasi_total Function-yielding V33() idempotent monotone infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving isomorphic projection closure kernel Element of bool [: the carrier of ([:R,S:],T), the carrier of ([:R,S:],T):]
id the carrier of ([:R,S:],T) is non empty Relation-like the carrier of ([:R,S:],T) -defined the carrier of ([:R,S:],T) -valued Function-like one-to-one V19() V21() V22() V26() V27( the carrier of ([:R,S:],T)) quasi_total onto bijective Function-yielding V33() Element of bool [: the carrier of ([:R,S:],T), the carrier of ([:R,S:],T):]