:: 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() associative commutative L9()

1 is non empty set
{{},1} is non empty set
K658() is set
is non empty functional set
K319() is M12()

bool 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

is non empty Relation-like set
bool is non empty set
RelStr(# ,() #) is non empty trivial V56() 1 -element strict RelStr

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

{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 ()
the carrier of Sierpinski_Space is non empty set
bool the carrier of Sierpinski_Space is non empty set
bool () is non empty set
bool {} is non empty set

proj1 R is set
S is set

R . S is set

S is set
proj1 S is set

R . S is set

S is set

R . S is set

S is set

proj1 (R | S) is set

(R | S) . T is set

proj1 R is set
R . T is set
T is set
proj1 R is set

S is set

proj1 (R | S) is set

(R | S) . T is 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

proj2 F is set
F is non empty functional set

proj2 G is set
x is set
dom G is Element of bool F
bool F is non empty set

proj1 f is set
proj2 f is set
x is set
f . x is set
proj1 G is set

G . x is set

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

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

proj2 F is set
F is non empty functional 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

proj1 f is set
proj2 f is set
proj1 G is set

G . x is set

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

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

proj1 F is set
proj2 F is set

proj1 F is set

[:(),():] is Relation-like set
bool [:(),():] is non empty set
G is set
F . G is set
(F * F) . G is set
F . (F . G) is 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

proj1 F is set
proj2 F is set

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

proj1 F is set

G is set

F . G is set
(F * F) . G is set
F . (F . G) is 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

proj1 F is set
proj2 F is set

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

proj1 F is set

G is set

F . G is set
(F * F) . G is set
F . (F . G) is set

proj1 f is set
proj2 f is set
proj1 (F * F) is set

proj1 () is set
S is set

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

F is set
proj1 (() . S) is set
F is set
(() . 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 (~ ()) 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 () 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

proj1 G is set

[F,S] `2 is set
[F,S] `1 is set
(~ ()) . (S,F) is set
(~ ()) . [S,F] is set
() . (F,S) is set
() . [F,S] is set
(R . F) . S is set

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

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

F . S is set
proj1 R is set
G is 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

proj1 () 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

proj1 (~ ()) is set
proj1 (proj1 (~ ())) is set

proj1 (curry (~ ())) is set
proj2 (proj1 (~ ())) is set
[:{S},(proj2 (proj1 (~ ()))):] is Relation-like set
(proj1 (~ ())) /\ [:{S},(proj2 (proj1 (~ ()))):] is Relation-like set
proj2 ((proj1 (~ ())) /\ [:{S},(proj2 (proj1 (~ ()))):]) is set
[G,S] `2 is set
[G,S] `1 is set

(curry (~ ())) . S is set
proj1 (() . S) is set

proj1 G is set
(() . S) . G is set
(~ ()) . (S,G) is set
(~ ()) . [S,G] is set
() . (G,S) is set
() . [G,S] is set

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

proj2 T is set

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

F is set
(() . F) .: F is set
T .: F is set
pi ((T .: F),F) is set
Funcs ((),S) is functional set
Funcs (R,(Funcs ((),S))) is functional set

proj1 G is set
proj2 G is set

proj1 G is set

proj1 G is set
proj2 G is set

proj1 R is set

T is set
S is set
{S} is non empty set

() .: T is set
pi ((() .: T),S) is set
R .: [:T,{S}:] is set
F is set

F . S is set
proj1 () is set
G is set
() . 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
() . G is set
proj1 () is set

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

the carrier of R is set
S is set

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

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

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:]

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 () is non empty set
[: the carrier of R, the carrier of ():] is non empty Relation-like set
bool [: the carrier of R, the carrier of ():] is non empty set
F is non empty Relation-like the carrier of R -defined the carrier of () -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of ():]
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 ()
bool the carrier of () 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
is non empty functional set
R is set
bool R is non empty set
S is Element of bool R

[: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)) " 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

{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)

{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

{S} is non empty set

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

{T} is non empty set

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

dom () is Element of bool R
bool R is non empty set

G is set
() . G is set
() . 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 () is Element of bool R
the carrier of (T |^ R) is non empty functional set

the carrier of () is set
product () is set
product () is set

the carrier of () 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

product () 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)

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)

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 () is 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

product () 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)

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)

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 () is 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

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

() |^ the carrier of R is non empty constituted-Functions strict reflexive transitive non void RelStr
ContMaps (R,()) is non empty constituted-Functions strict reflexive transitive non void RelStr
G is reflexive transitive full SubRelStr of () |^ the carrier of R
the carrier of G is set
F is reflexive transitive full SubRelStr of () |^ the carrier of R
the carrier of F is set
G is set
the carrier of () is non empty set
the topology of () is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct
the carrier of (ContMaps (R,())) is non empty functional set
the carrier of () is non empty set
[: the carrier of R, the carrier of ():] is non empty Relation-like set
bool [: the carrier of R, the carrier of ():] is non empty set
x is non empty Relation-like the carrier of R -defined the carrier of () -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of ():]
the topology of () is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct
[: the carrier of S, the carrier of ():] is non empty Relation-like set
bool [: the carrier of S, the carrier of ():] is non empty set
f is non empty Relation-like the carrier of S -defined the carrier of () -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of ():]
x is Element of bool the carrier of ()
f " x is Element of bool the carrier of S
s is Element of bool the carrier of ()
x " s is Element of bool the carrier of R
the carrier of (ContMaps (S,())) is non empty functional set
G is set
the carrier of () is non empty set
the topology of () is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct
the carrier of (ContMaps (S,())) is non empty functional set
the carrier of () is non empty set
[: the carrier of S, the carrier of ():] is non empty Relation-like set
bool [: the carrier of S, the carrier of ():] is non empty set
x is non empty Relation-like the carrier of S -defined the carrier of () -valued Function-like V27( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of ():]
the topology of () is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct
[: the carrier of R, the carrier of ():] is non empty Relation-like set
bool [: the carrier of R, the carrier of ():] is non empty set
f is non empty Relation-like the carrier of R -defined the carrier of () -valued Function-like V27( the carrier of R) quasi_total Element of bool [: the carrier of R, the carrier of ():]
x is Element of bool the carrier of ()
f " x is Element of bool the carrier of R
s is Element of bool the carrier of ()
x " s is Element of bool the carrier of S
the carrier of (ContMaps (R,())) is non empty functional set
R is set

the carrier of () is non empty set

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

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
RelStr(# (),() #) is strict RelStr
S is non empty Relation-like the carrier of () -defined the carrier of (() |^ R) -valued Function-like V27( the carrier of ()) quasi_total Function-yielding V33() Element of bool [: the carrier of (), the carrier of (() |^ R):]
rng () is non empty functional Element of bool
bool is non empty set
T is Element of the carrier of ()
F is Element of the carrier of ()
S . 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)
F is Element of the carrier of ()
S . F is Relation-like Function-like Element of the carrier of (() |^ R)
G is Element of the carrier of ()
S . G is Relation-like Function-like Element of the carrier of (() |^ R)
T is Element of bool R

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

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

R is set

the carrier of () is non empty set
the carrier of (() |^ R) is non empty functional set
[: the carrier of (), the carrier of (() |^ R):] is non empty Relation-like set
bool [: the carrier of (), the carrier of (() |^ R):] is non empty set
bool R is non empty set
S is non empty Relation-like the carrier of () -defined the carrier of (() |^ R) -valued Function-like V27( the carrier of ()) quasi_total Function-yielding V33() Element of bool [: the carrier of (), the carrier of (() |^ R):]
S is non empty set
R is non empty set
T is non empty 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

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)

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

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 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)

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)

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

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 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:])

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)

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

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)

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

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

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

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

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)

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

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

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

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

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 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

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

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

the carrier of R is non empty set

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