K92() is Element of bool K88()
K88() is set
bool K88() is non empty set
K47() is set
bool K47() is non empty set
bool K92() is non empty set
K235() is TopStruct
the carrier of K235() is set
K89() is set
K90() is set
K91() is set
[:K88(),K88():] is Relation-like set
bool [:K88(),K88():] is non empty set
K391() is non empty V104() L9()
the carrier of K391() is non empty set
<REAL,+> is non empty V104() V126() V127() V128() V130() left-invertible right-invertible V182() left-cancelable right-cancelable V185() L9()
K397() is non empty V104() V128() V130() left-cancelable right-cancelable V185() SubStr of <REAL,+>
<NAT,+> is non empty V104() V126() V128() V130() left-cancelable right-cancelable V185() uniquely-decomposable SubStr of K397()
<REAL,*> is non empty V104() V126() V128() V130() L9()
<NAT,*> is non empty V104() V126() V128() V130() uniquely-decomposable SubStr of <REAL,*>
{} is empty Relation-like non-empty empty-yielding set
the empty Relation-like non-empty empty-yielding set is empty Relation-like non-empty empty-yielding set
1 is non empty set
{{},1} is non empty 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
S is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima Scott non void TopRelStr
SCMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (S,T)
MonMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of S is non empty set
T |^ the carrier of S is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of (SCMaps (S,T)) is non empty set
bool the carrier of (SCMaps (S,T)) 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
Sm is Element of bool the carrier of (SCMaps (S,T))
"\/" (Sm,(SCMaps (S,T))) is Element of the carrier of (SCMaps (S,T))
the carrier of (MonMaps (S,T)) is non empty set
S is non empty RelStr
the carrier of S is non empty set
T is non empty reflexive 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
Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Element of the carrier of S
a is Element of the carrier of S
Sm . SC is Element of the carrier of T
Sm . a is Element of the carrier of T
dom Sm is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
T is non empty reflexive non void RelStr
the carrier of T is non empty set
S is non empty RelStr
Sm is Element of the carrier of T
S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
the carrier of S 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
the carrier of S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is Element of the carrier of S
f is Element of the carrier of S
(S --> Sm) . a is Element of the carrier of T
(S --> Sm) . f is Element of the carrier of T
( the carrier of S --> Sm) . a is Element of the carrier of T
( the carrier of S --> Sm) . f is Element of the carrier of T
S is non empty RelStr
T is non empty reflexive antisymmetric lower-bounded non void RelStr
MonMaps (S,T) is non empty strict reflexive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of S is non empty set
T |^ the carrier of S is non empty strict reflexive antisymmetric non void RelStr
Bottom (MonMaps (S,T)) is Element of the carrier of (MonMaps (S,T))
the carrier of (MonMaps (S,T)) is non empty set
Bottom T is Element of the carrier of T
the carrier of T is non empty set
S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( 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
the carrier of S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Element of the carrier of (MonMaps (S,T))
f is Element of the carrier of (MonMaps (S,T))
the carrier of (T |^ the carrier of S) is non empty set
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
g9 is Element of the carrier of S
a . g9 is Element of the carrier of T
b9 . g9 is Element of the carrier of T
( the carrier of S --> (Bottom T)) . g9 is Element of the carrier of T
g1 is Element of the carrier of (T |^ the carrier of S)
i is Element of the carrier of (T |^ the carrier of S)
"\/" ({},(MonMaps (S,T))) is Element of the carrier of (MonMaps (S,T))
S is non empty RelStr
T is non empty reflexive antisymmetric upper-bounded non void RelStr
MonMaps (S,T) is non empty strict reflexive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of S is non empty set
T |^ the carrier of S is non empty strict reflexive antisymmetric non void RelStr
Top (MonMaps (S,T)) is Element of the carrier of (MonMaps (S,T))
the carrier of (MonMaps (S,T)) is non empty set
Top T is Element of the carrier of T
the carrier of T is non empty set
S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( 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
the carrier of S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Element of the carrier of (MonMaps (S,T))
f is Element of the carrier of (MonMaps (S,T))
the carrier of (T |^ the carrier of S) is non empty set
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
g9 is Element of the carrier of S
b9 . g9 is Element of the carrier of T
a . g9 is Element of the carrier of T
( the carrier of S --> (Top T)) . g9 is Element of the carrier of T
i is Element of the carrier of (T |^ the carrier of S)
g1 is Element of the carrier of (T |^ the carrier of S)
"/\" ({},(MonMaps (S,T))) is Element of the carrier of (MonMaps (S,T))
F2() is non empty RelStr
the carrier of F2() is non empty set
F4() is Relation-like Function-like set
dom F4() is set
F1() is non empty RelStr
the carrier of F1() is non empty set
{ F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
F4() .: { F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ (F4() . F3(b1)) where b1 is Element of the carrier of F1() : P1[b1] } is set
T is set
Sm is set
F4() . Sm is set
SC is Element of the carrier of F1()
F3(SC) is Element of the carrier of F2()
T is set
Sm is Element of the carrier of F1()
F3(Sm) is Element of the carrier of F2()
F4() . F3(Sm) is set
F1() is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of F1() is non empty set
{ F2(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ F2(b1) where b1 is Element of the carrier of F1() : P2[b1] } is set
S is set
T is Element of the carrier of F1()
F2(T) is set
S is set
T is Element of the carrier of F1()
F2(T) is set
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete 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
Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
SC is Element of the carrier of S
Sm . SC is Element of the carrier of T
downarrow SC is non empty directed lower Element of bool the carrier of S
bool the carrier of S is non empty set
{SC} is non empty Element of bool the carrier of S
downarrow {SC} is non empty lower Element of bool the carrier of S
Sm .: (downarrow SC) is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((Sm .: (downarrow SC)),T) is Element of the carrier of T
a is Element of the carrier of T
dom Sm is non empty Element of bool the carrier of S
"\/" ((downarrow SC),S) is Element of the carrier of S
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete 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
Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
SC is Element of the carrier of S
Sm . SC is Element of the carrier of T
{ (Sm . b1) where b1 is Element of the carrier of S : b1 <= SC } is set
"\/" ( { (Sm . b1) where b1 is Element of the carrier of S : b1 <= SC } ,T) is Element of the carrier of T
{SC} is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
dom Sm is non empty Element of bool the carrier of S
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
Sm .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of bool the carrier of T
bool the carrier of T is non empty set
{ (Sm . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
a is Element of the carrier of S
f is Element of the carrier of S
{ H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
downarrow SC is non empty directed lower Element of bool the carrier of S
downarrow {SC} is non empty lower Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : b1 <= SC } is set
Sm .: (downarrow SC) is Element of bool the carrier of T
"\/" ((Sm .: (downarrow SC)),T) is Element of the carrier of T
"\/" ((downarrow SC),S) is Element of the carrier of S
Sm . ("\/" ((downarrow SC),S)) is Element of the carrier of T
S is RelStr
the carrier of S is set
T is non empty RelStr
T |^ the carrier of S is non empty strict RelStr
the carrier of (T |^ the carrier of S) is non empty set
bool the carrier of (T |^ the carrier of S) is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
Sm is Element of bool the carrier of (T |^ the carrier of S)
"\/" (Sm,(T |^ the carrier of S)) is Element of the carrier of (T |^ the carrier of S)
Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T
a is Relation-like Function-like set
dom a is set
rng a is set
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
curry SC is Relation-like Function-like set
a is Element of the carrier of S
(curry SC) . a is set
the carrier of T is non empty set
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
Funcs ( the carrier of T, the carrier of Sm) is non empty functional FUNCTION_DOMAIN of the carrier of T, the carrier of Sm
[: the carrier of S,(Funcs ( the carrier of T, the carrier of Sm)):] is non empty Relation-like set
bool [: the carrier of S,(Funcs ( the carrier of T, the carrier of Sm)):] is non empty set
S is non empty RelStr
the carrier of S is non empty set
T is non empty RelStr
the carrier of T is non empty set
Sm is non empty RelStr
[:T,Sm:] is non empty strict RelStr
the carrier of [:T,Sm:] is non empty set
[: the carrier of [:T,Sm:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:T,Sm:], the carrier of S:] is non empty set
the carrier of Sm is non empty set
SC is non empty Relation-like the carrier of [:T,Sm:] -defined the carrier of S -valued Function-like V14( the carrier of [:T,Sm:]) quasi_total Element of bool [: the carrier of [:T,Sm:], the carrier of S:]
a is Element of the carrier of T
(T,Sm,S,SC,a) is non empty Relation-like the carrier of Sm -defined the carrier of S -valued Function-like V14( the carrier of Sm) quasi_total Element of bool [: the carrier of Sm, the carrier of S:]
[: the carrier of Sm, the carrier of S:] is non empty Relation-like set
bool [: the carrier of Sm, the carrier of S:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
f is Element of the carrier of Sm
(T,Sm,S,SC,a) . f is Element of the carrier of S
SC . (a,f) is set
[a,f] is set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
SC . [a,f] is set
dom SC is non empty Element of bool the carrier of [:T,Sm:]
bool the carrier of [:T,Sm:] is non empty set
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
[a,f] is Element of the carrier of [:T,Sm:]
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
curry' SC is Relation-like Function-like set
a is Element of the carrier of T
(curry' SC) . a is set
the carrier of S is non empty set
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
Funcs ( the carrier of S, the carrier of Sm) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of Sm
[: the carrier of T,(Funcs ( the carrier of S, the carrier of Sm)):] is non empty Relation-like set
bool [: the carrier of T,(Funcs ( the carrier of S, the carrier of Sm)):] is non empty set
S is non empty RelStr
the carrier of S is non empty set
T is non empty RelStr
the carrier of T is non empty set
Sm is non empty RelStr
[:Sm,T:] is non empty strict RelStr
the carrier of [:Sm,T:] is non empty set
[: the carrier of [:Sm,T:], the carrier of S:] is non empty Relation-like set
bool [: the carrier of [:Sm,T:], the carrier of S:] is non empty set
the carrier of Sm is non empty set
SC is non empty Relation-like the carrier of [:Sm,T:] -defined the carrier of S -valued Function-like V14( the carrier of [:Sm,T:]) quasi_total Element of bool [: the carrier of [:Sm,T:], the carrier of S:]
a is Element of the carrier of T
(Sm,T,S,SC,a) is non empty Relation-like the carrier of Sm -defined the carrier of S -valued Function-like V14( the carrier of Sm) quasi_total Element of bool [: the carrier of Sm, the carrier of S:]
[: the carrier of Sm, the carrier of S:] is non empty Relation-like set
bool [: the carrier of Sm, the carrier of S:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . a is set
f is Element of the carrier of Sm
(Sm,T,S,SC,a) . f is Element of the carrier of S
SC . (f,a) is set
[f,a] is set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
SC . [f,a] is set
dom SC is non empty Element of bool the carrier of [:Sm,T:]
bool the carrier of [:Sm,T:] is non empty set
[: the carrier of Sm, the carrier of T:] is non empty Relation-like set
[f,a] is Element of the carrier of [:Sm,T:]
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
f is Element of the carrier of T
(S,T,Sm,SC,a) . f is Element of the carrier of Sm
(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . f is set
(S,T,Sm,SC,f) . a is Element of the carrier of Sm
SC . (a,f) is set
[a,f] is set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
SC . [a,f] is set
S is non empty RelStr
the carrier of S is non empty set
T is non empty reflexive 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
the Element of the carrier of T is Element of the carrier of T
S --> the Element of the carrier of T is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
the carrier of S --> the Element of the carrier of T is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
a is Element of the carrier of S
f is Element of the carrier of S
SC . a is set
SC . f is set
[a,f] is Element of the carrier of [:S,S:]
[:S,S:] is non empty strict RelStr
the carrier of [:S,S:] is non empty set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} 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
b9 is Element of the carrier of T
i is Element of the carrier of T
SC . a is Element of the carrier of T
SC . f is Element of the carrier of T
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
f is Element of the carrier of T
(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . f is set
i is Element of the carrier of T
(S,T,Sm,SC,i) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
(curry' SC) . i is set
b9 is Element of the carrier of S
(S,T,Sm,SC,b9) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
(curry SC) . b9 is set
L is Element of the carrier of S
(S,T,Sm,SC,i) . L is Element of the carrier of Sm
SC . (L,i) is set
[L,i] is set
{L,i} is non empty set
{L} is non empty set
{{L,i},{L}} is non empty set
SC . [L,i] is set
P is Element of the carrier of S
(S,T,Sm,SC,i) . P is Element of the carrier of Sm
SC . (P,i) is set
[P,i] is set
{P,i} is non empty set
{P} is non empty set
{{P,i},{P}} is non empty set
SC . [P,i] is set
[L,i] is Element of the carrier of [:S,T:]
[P,i] is Element of the carrier of [:S,T:]
L is Element of the carrier of T
(S,T,Sm,SC,b9) . L is Element of the carrier of Sm
SC . (b9,L) is set
[b9,L] is set
{b9,L} is non empty set
{b9} is non empty set
{{b9,L},{b9}} is non empty set
SC . [b9,L] is set
P is Element of the carrier of T
(S,T,Sm,SC,b9) . P is Element of the carrier of Sm
SC . (b9,P) is set
[b9,P] is set
{b9,P} is non empty set
{{b9,P},{b9}} is non empty set
SC . [b9,P] is set
[b9,L] is Element of the carrier of [:S,T:]
[b9,P] is Element of the carrier of [:S,T:]
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
f is Element of the carrier of T
(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . f is set
g9 is Element of the carrier of T
L is Element of the carrier of S
(S,T,Sm,SC,f) . L is Element of the carrier of Sm
SC . (L,f) is set
[L,f] is set
{L,f} is non empty set
{L} is non empty set
{{L,f},{L}} is non empty set
SC . [L,f] is set
P is Element of the carrier of S
(S,T,Sm,SC,f) . P is Element of the carrier of Sm
SC . (P,f) is set
[P,f] is set
{P,f} is non empty set
{P} is non empty set
{{P,f},{P}} is non empty set
SC . [P,f] is set
[L,g9] is Element of the carrier of [:S,T:]
{L,g9} is non empty set
{{L,g9},{L}} is non empty set
[P,g9] is Element of the carrier of [:S,T:]
{P,g9} is non empty set
{{P,g9},{P}} is non empty set
b9 is Element of the carrier of S
g9 is Element of the carrier of T
(S,T,Sm,SC,a) . g9 is Element of the carrier of Sm
SC . (a,g9) is set
[a,g9] is set
{a,g9} is non empty set
{a} is non empty set
{{a,g9},{a}} is non empty set
SC . [a,g9] is set
L is Element of the carrier of T
(S,T,Sm,SC,a) . L is Element of the carrier of Sm
SC . (a,L) is set
[a,L] is set
{a,L} is non empty set
{{a,L},{a}} is non empty set
SC . [a,L] is set
[b9,g9] is Element of the carrier of [:S,T:]
{b9,g9} is non empty set
{b9} is non empty set
{{b9,g9},{b9}} is non empty set
[b9,L] is Element of the carrier of [:S,T:]
{b9,L} is non empty set
{{b9,L},{b9}} is non empty set
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
the carrier of T is non empty set
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of T
(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
the carrier of S is non empty set
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . a is set
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total antitone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
the carrier of T is non empty set
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total antitone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of T
(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
the carrier of S is non empty set
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . a is set
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of [:S,T:]
f is Element of the carrier of [:S,T:]
a `1 is Element of the carrier of S
f `1 is Element of the carrier of S
a `2 is Element of the carrier of T
f `2 is Element of the carrier of T
SC . ((a `1),(f `2)) is set
[(a `1),(f `2)] is set
{(a `1),(f `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(f `2)},{(a `1)}} is non empty set
SC . [(a `1),(f `2)] is set
(S,T,Sm,SC,(a `1)) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . (a `1) is set
(S,T,Sm,SC,(a `1)) . (f `2) is Element of the carrier of Sm
SC . ((a `1),(a `2)) is set
[(a `1),(a `2)] is set
{(a `1),(a `2)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
SC . [(a `1),(a `2)] is set
(S,T,Sm,SC,(a `1)) . (a `2) is Element of the carrier of Sm
[(a `1),(a `2)] is Element of the carrier of [:S,T:]
SC . [(a `1),(a `2)] is Element of the carrier of Sm
[(a `1),(f `2)] is Element of the carrier of [:S,T:]
SC . [(a `1),(f `2)] is Element of the carrier of Sm
SC . ((f `1),(f `2)) is set
[(f `1),(f `2)] is set
{(f `1),(f `2)} is non empty set
{(f `1)} is non empty set
{{(f `1),(f `2)},{(f `1)}} is non empty set
SC . [(f `1),(f `2)] is set
(S,T,Sm,SC,(f `2)) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . (f `2) is set
(S,T,Sm,SC,(f `2)) . (f `1) is Element of the carrier of Sm
(S,T,Sm,SC,(f `2)) . (a `1) is Element of the carrier of Sm
[(f `1),(f `2)] is Element of the carrier of [:S,T:]
SC . [(f `1),(f `2)] is Element of the carrier of Sm
[: the carrier of S, the carrier of T:] is non empty Relation-like set
SC . f is Element of the carrier of Sm
SC . a is Element of the carrier of Sm
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of [:S,T:]
f is Element of the carrier of [:S,T:]
a `1 is Element of the carrier of S
f `1 is Element of the carrier of S
a `2 is Element of the carrier of T
f `2 is Element of the carrier of T
SC . ((a `1),(f `2)) is set
[(a `1),(f `2)] is set
{(a `1),(f `2)} is non empty set
{(a `1)} is non empty set
{{(a `1),(f `2)},{(a `1)}} is non empty set
SC . [(a `1),(f `2)] is set
(S,T,Sm,SC,(a `1)) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . (a `1) is set
(S,T,Sm,SC,(a `1)) . (f `2) is Element of the carrier of Sm
SC . ((a `1),(a `2)) is set
[(a `1),(a `2)] is set
{(a `1),(a `2)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
SC . [(a `1),(a `2)] is set
(S,T,Sm,SC,(a `1)) . (a `2) is Element of the carrier of Sm
[(a `1),(f `2)] is Element of the carrier of [:S,T:]
SC . [(a `1),(f `2)] is Element of the carrier of Sm
[(a `1),(a `2)] is Element of the carrier of [:S,T:]
SC . [(a `1),(a `2)] is Element of the carrier of Sm
SC . ((f `1),(f `2)) is set
[(f `1),(f `2)] is set
{(f `1),(f `2)} is non empty set
{(f `1)} is non empty set
{{(f `1),(f `2)},{(f `1)}} is non empty set
SC . [(f `1),(f `2)] is set
(S,T,Sm,SC,(f `2)) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . (f `2) is set
(S,T,Sm,SC,(f `2)) . (f `1) is Element of the carrier of Sm
(S,T,Sm,SC,(f `2)) . (a `1) is Element of the carrier of Sm
[(f `1),(f `2)] is Element of the carrier of [:S,T:]
SC . [(f `1),(f `2)] is Element of the carrier of Sm
[: the carrier of S, the carrier of T:] is non empty Relation-like set
SC . f is Element of the carrier of Sm
SC . a is Element of the carrier of Sm
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of T is non empty set
the carrier of S is non empty set
bool the carrier of S is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of T
(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . a is set
{a} is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
f is Element of bool the carrier of S
(S,T,Sm,SC,a) .: f is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
[:f,{a}:] is Relation-like Element of bool the carrier of [:S,T:]
bool the carrier of [:S,T:] is non empty set
SC .: [:f,{a}:] is Element of bool the carrier of Sm
b9 is set
dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of S
i is set
(S,T,Sm,SC,a) . i is set
[i,a] is set
{i,a} is non empty set
{i} is non empty set
{{i,a},{i}} is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
dom SC is non empty Element of bool the carrier of [:S,T:]
SC . (i,a) is set
SC . [i,a] is set
b9 is set
dom SC is non empty Element of bool the carrier of [:S,T:]
i is set
SC . i is set
g1 is set
g9 is set
[g1,g9] is set
{g1,g9} is non empty set
{g1} is non empty set
{{g1,g9},{g1}} is non empty set
SC . (g1,g9) is set
SC . [g1,g9] is set
dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of S
(S,T,Sm,SC,a) . g1 is set
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
bool the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
{a} is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
f is Element of bool the carrier of T
(S,T,Sm,SC,a) .: f is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
[:{a},f:] is Relation-like Element of bool the carrier of [:S,T:]
bool the carrier of [:S,T:] is non empty set
SC .: [:{a},f:] is Element of bool the carrier of Sm
b9 is set
dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of T
i is set
(S,T,Sm,SC,a) . i is set
[a,i] is set
{a,i} is non empty set
{a} is non empty set
{{a,i},{a}} is non empty set
[: the carrier of S, the carrier of T:] is non empty Relation-like set
dom SC is non empty Element of bool the carrier of [:S,T:]
SC . (a,i) is set
SC . [a,i] is set
b9 is set
dom SC is non empty Element of bool the carrier of [:S,T:]
i is set
SC . i is set
g1 is set
g9 is set
[g1,g9] is set
{g1,g9} is non empty set
{g1} is non empty set
{{g1,g9},{g1}} is non empty set
SC . (g1,g9) is set
SC . [g1,g9] is set
dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of T
(S,T,Sm,SC,a) . g9 is set
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . a is set
f is Element of the carrier of T
(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . f is set
bool the carrier of T is non empty set
bool the carrier of S is non empty set
{a} is non empty Element of bool the carrier of S
i is Element of bool the carrier of T
b9 is non empty directed Element of bool the carrier of S
"\/" (b9,S) is Element of the carrier of S
g1 is non empty directed Element of bool the carrier of T
[:b9,g1:] is non empty Relation-like directed Element of bool the carrier of [:S,T:]
bool the carrier of [:S,T:] is non empty set
(S,T,Sm,SC,a) .: i is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
SC .: [:b9,g1:] is Element of bool the carrier of Sm
"\/" (((S,T,Sm,SC,a) .: i),Sm) is Element of the carrier of Sm
"\/" (i,T) is Element of the carrier of T
(S,T,Sm,SC,a) . ("\/" (i,T)) is Element of the carrier of Sm
"\/" ((SC .: [:b9,g1:]),Sm) is Element of the carrier of Sm
"\/" ([:b9,g1:],[:S,T:]) is Element of the carrier of [:S,T:]
SC . ("\/" ([:b9,g1:],[:S,T:])) is Element of the carrier of Sm
"\/" (g1,T) is Element of the carrier of T
SC . (("\/" (b9,S)),("\/" (g1,T))) is set
[("\/" (b9,S)),("\/" (g1,T))] is set
{("\/" (b9,S)),("\/" (g1,T))} is non empty set
{("\/" (b9,S))} is non empty set
{{("\/" (b9,S)),("\/" (g1,T))},{("\/" (b9,S))}} is non empty set
SC . [("\/" (b9,S)),("\/" (g1,T))] is set
bool the carrier of S is non empty set
{f} is non empty Element of bool the carrier of T
i is Element of bool the carrier of S
b9 is non empty directed Element of bool the carrier of T
"\/" (b9,T) is Element of the carrier of T
g1 is non empty directed Element of bool the carrier of S
[:g1,b9:] is non empty Relation-like directed Element of bool the carrier of [:S,T:]
bool the carrier of [:S,T:] is non empty set
(S,T,Sm,SC,f) .: i is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
SC .: [:g1,b9:] is Element of bool the carrier of Sm
"\/" (((S,T,Sm,SC,f) .: i),Sm) is Element of the carrier of Sm
"\/" (i,S) is Element of the carrier of S
(S,T,Sm,SC,f) . ("\/" (i,S)) is Element of the carrier of Sm
"\/" ((SC .: [:g1,b9:]),Sm) is Element of the carrier of Sm
"\/" ([:g1,b9:],[:S,T:]) is Element of the carrier of [:S,T:]
SC . ("\/" ([:g1,b9:],[:S,T:])) is Element of the carrier of Sm
"\/" (g1,S) is Element of the carrier of S
SC . (("\/" (g1,S)),("\/" (b9,T))) is set
[("\/" (g1,S)),("\/" (b9,T))] is set
{("\/" (g1,S)),("\/" (b9,T))} is non empty set
{("\/" (g1,S))} is non empty set
{{("\/" (g1,S)),("\/" (b9,T))},{("\/" (g1,S))}} is non empty set
SC . [("\/" (g1,S)),("\/" (b9,T))] is set
S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
bool the carrier of [:S,T:] is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
a is Element of the carrier of S
f is Element of the carrier of T
[a,f] is Element of the carrier of [:S,T:]
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
SC . [a,f] is Element of the carrier of Sm
b9 is directed Element of bool the carrier of [:S,T:]
SC .: b9 is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
proj1 b9 is Element of bool the carrier of S
bool the carrier of S is non empty set
proj2 b9 is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((SC .: b9),Sm) is Element of the carrier of Sm
i is set
[i,f] is set
{i,f} is non empty set
{i} is non empty set
{{i,f},{i}} is non empty set
g9 is set
[a,g9] is set
{a,g9} is non empty set
{{a,g9},{a}} is non empty set
L is Element of the carrier of T
[a,L] is Element of the carrier of [:S,T:]
{a,L} is non empty set
{{a,L},{a}} is non empty set
g1 is Element of the carrier of S
[g1,f] is Element of the carrier of [:S,T:]
{g1,f} is non empty set
{g1} is non empty set
{{g1,f},{g1}} is non empty set
P is Element of the carrier of [:S,T:]
[a,L] "\/" [g1,f] is Element of the carrier of [:S,T:]
P "\/" P is Element of the carrier of [:S,T:]
a "\/" g1 is Element of the carrier of S
L "\/" f is Element of the carrier of T
[(a "\/" g1),(L "\/" f)] is Element of the carrier of [:S,T:]
{(a "\/" g1),(L "\/" f)} is non empty set
{(a "\/" g1)} is non empty set
{{(a "\/" g1),(L "\/" f)},{(a "\/" g1)}} is non empty set
SC . [(a "\/" g1),(L "\/" f)] is Element of the carrier of Sm
SC . P is Element of the carrier of Sm
dom SC is non empty Element of bool the carrier of [:S,T:]
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of [:S,T:] is non empty set
Sm is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of Sm is non empty set
[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of [:S,T:], the carrier of Sm:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]
bool the carrier of [:S,T:] is non empty set
a is Element of bool the carrier of [:S,T:]
b9 is Element of the carrier of S
(S,T,Sm,SC,b9) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . b9 is set
i is Element of the carrier of T
(S,T,Sm,SC,i) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . i is set
f is non empty directed Element of bool the carrier of [:S,T:]
proj1 f is Element of bool the carrier of S
bool the carrier of S is non empty set
proj2 f is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((proj2 f),T) is Element of the carrier of T
(S,T,Sm,SC,("\/" ((proj2 f),T))) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]
[: the carrier of S, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of S, the carrier of Sm:] is non empty set
curry' SC is Relation-like Function-like set
(curry' SC) . ("\/" ((proj2 f),T)) is set
(S,T,Sm,SC,("\/" ((proj2 f),T))) .: (proj1 f) is Element of bool the carrier of Sm
bool the carrier of Sm is non empty set
SC .: f is Element of bool the carrier of Sm
"\/" ((SC .: f),Sm) is Element of the carrier of Sm
"\/" (f,[:S,T:]) is Element of the carrier of [:S,T:]
SC . ("\/" (f,[:S,T:])) is Element of the carrier of Sm
b9 is Element of the carrier of Sm
dom (S,T,Sm,SC,("\/" ((proj2 f),T))) is non empty Element of bool the carrier of S
i is set
(S,T,Sm,SC,("\/" ((proj2 f),T))) . i is set
g1 is Element of the carrier of S
(S,T,Sm,SC,g1) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]
[: the carrier of T, the carrier of Sm:] is non empty Relation-like set
bool [: the carrier of T, the carrier of Sm:] is non empty set
curry SC is Relation-like Function-like set
(curry SC) . g1 is set
(S,T,Sm,SC,g1) .: (proj2 f) is Element of bool the carrier of Sm
g9 is Element of the carrier of Sm
dom (S,T,Sm,SC,g1) is non empty Element of bool the carrier of T
L is set
(S,T,Sm,SC,g1) . L is set
P is Element of the carrier of T
SC . (g1,P) is set
[g1,P] is set
{g1,P} is non empty set
{g1} is non empty set
{{g1,P},{g1}} is non empty set
SC . [g1,P] is set
(S,T,Sm,SC,g1) . ("\/" ((proj2 f),T)) is Element of the carrier of Sm
"\/" (((S,T,Sm,SC,g1) .: (proj2 f)),Sm) is Element of the carrier of Sm
"\/" ((proj1 f),S) is Element of the carrier of S
SC . (("\/" ((proj1 f),S)),("\/" ((proj2 f),T))) is set
[("\/" ((proj1 f),S)),("\/" ((proj2 f),T))] is set
{("\/" ((proj1 f),S)),("\/" ((proj2 f),T))} is non empty set
{("\/" ((proj1 f),S))} is non empty set
{{("\/" ((proj1 f),S)),("\/" ((proj2 f),T))},{("\/" ((proj1 f),S))}} is non empty set
SC . [("\/" ((proj1 f),S)),("\/" ((proj2 f),T))] is set
(S,T,Sm,SC,("\/" ((proj2 f),T))) . ("\/" ((proj1 f),S)) is Element of the carrier of Sm
"\/" (((S,T,Sm,SC,("\/" ((proj2 f),T))) .: (proj1 f)),Sm) is Element of the carrier of Sm
S is set
T is non empty RelStr
T |^ S is non empty strict RelStr
the carrier of (T |^ S) is non empty set
the carrier of T is non empty set
[:S, the carrier of T:] is Relation-like set
bool [:S, the carrier of T:] is non empty set
Sm is set
Funcs (S, the carrier of T) is non empty functional FUNCTION_DOMAIN of S, the carrier of T
SC is Relation-like Function-like set
dom SC is set
rng SC is set
S is TopStruct
the carrier of S is set
T is non empty TopRelStr
T |^ the carrier of S is non empty strict RelStr
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is Relation-like set
bool [: the carrier of S, the carrier of T:] is non empty set
the carrier of (T |^ the carrier of S) is non empty set
Sm is set
SC is set
bool the carrier of (T |^ the carrier of S) is non empty set
SC is Element of bool the carrier of (T |^ the carrier of S)
subrelstr SC is strict full SubRelStr of T |^ the carrier of S
a is strict full SubRelStr of T |^ the carrier of S
the carrier of a is set
f is set
b9 is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
i is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
b9 is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of 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
Sm is strict RelStr
the carrier of Sm is set
SC is strict RelStr
the carrier of SC is set
a is set
f is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is set
f is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopRelStr
(S,T) is strict RelStr
the carrier of S 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
the non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:] is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]
the carrier of (S,T) is set
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopRelStr
(S,T) is non empty strict RelStr
the carrier of (S,T) is non empty set
Sm is Element of the carrier of (S,T)
the carrier of S 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
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is non empty TopSpace-like reflexive non void TopRelStr
(S,T) is non empty constituted-Functions strict RelStr
the carrier of (S,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 is non empty set
[: 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
Sm is Relation-like Function-like Element of the carrier of (S,T)
SC is Relation-like Function-like Element of the carrier of (S,T)
T |^ the carrier of S is non empty strict reflexive non void RelStr
the carrier of (T |^ the carrier of S) 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
a is Element of the carrier of (T |^ the carrier of S)
f is Element of the carrier of (T |^ the carrier of S)
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
i is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
g1 is Element of the carrier of S
b9 . g1 is Element of the carrier of T
i . g1 is Element of the carrier of T
Sm . g1 is set
SC . g1 is set
[(Sm . g1),(SC . g1)] is set
{(Sm . g1),(SC . g1)} is non empty set
{(Sm . g1)} is non empty set
{{(Sm . g1),(SC . g1)},{(Sm . g1)}} is non empty set
g9 is Element of the carrier of T
L is Element of the carrier of T
g1 is set
g9 is Element of the carrier of S
b9 . g9 is Element of the carrier of T
i . g9 is Element of the carrier of T
L is Element of the carrier of T
P is Element of the carrier of T
b is Element of the carrier of T
b9 . g1 is set
i9 is Element of the carrier of T
i . g1 is set
[b,i9] is Element of the carrier of [:T,T:]
[:T,T:] is non empty strict reflexive non void RelStr
the carrier of [:T,T:] is non empty set
{b,i9} is non empty set
{b} is non empty set
{{b,i9},{b}} is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
T is non empty TopSpace-like reflexive non void TopRelStr
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
(S,T) is non empty constituted-Functions strict RelStr
the carrier of (S,T) is non empty set
Sm is set
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like reflexive non void TopRelStr
(S,T) is non empty constituted-Functions strict RelStr
the carrier of S is non empty set
T |^ the carrier of S is non empty strict reflexive non void RelStr
Sm is reflexive full SubRelStr of T |^ the carrier of S
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like transitive TopRelStr
(S,T) is non empty constituted-Functions strict RelStr
the carrier of S is non empty set
T |^ the carrier of S is non empty strict transitive RelStr
Sm is transitive full SubRelStr of T |^ the carrier of S
S is non empty TopSpace-like TopStruct
T is non empty TopSpace-like antisymmetric TopRelStr
(S,T) is non empty constituted-Functions strict RelStr
the carrier of S is non empty set
T |^ the carrier of S is non empty strict antisymmetric RelStr
Sm is antisymmetric full SubRelStr of T |^ the carrier of S
S is set
T is non empty RelStr
T |^ S is non empty strict RelStr
the carrier of (T |^ S) is non empty set
Sm is Element of the carrier of (T |^ S)
S is non empty 1-sorted
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete 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
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
{Sm,SC} is non empty Element of bool (bool [: the carrier of S, the carrier of T:])
bool (bool [: the carrier of S, the carrier of T:]) is non empty set
"\/" ({Sm,SC},(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
f is Element of the carrier of S
a . f is Element of the carrier of T
Sm . f is Element of the carrier of T
SC . f is Element of the carrier of T
{(Sm . f),(SC . f)} is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ({(Sm . f),(SC . f)},T) is Element of the carrier of T
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like V14( the carrier of S) quasi_total RelStr-yielding non-Empty reflexive-yielding 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
g1 is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty set
g9 is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty reflexive-yielding set
L is Element of the carrier of S
g9 . L is non empty reflexive non void RelStr
product g9 is non empty constituted-Functions strict reflexive non void RelStr
the carrier of (product g9) is non empty set
b9 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
i is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
bool the carrier of (product g9) is non empty set
L is Relation-like Function-like Element of the carrier of (product g9)
P is Relation-like Function-like Element of the carrier of (product g9)
{L,P} is non empty Element of bool the carrier of (product g9)
b is Element of bool the carrier of (product g9)
"\/" (b,(product g9)) is Relation-like Function-like Element of the carrier of (product g9)
("\/" (b,(product g9))) . f is Element of the carrier of (g9 . f)
g9 . f is non empty reflexive non void RelStr
the carrier of (g9 . f) is non empty set
pi ({Sm,SC},f) is set
"\/" ((pi ({Sm,SC},f)),(g9 . f)) is Element of the carrier of (g9 . f)
"\/" ((pi ({Sm,SC},f)),T) is Element of the carrier of T
S is non empty set
T is Relation-like S -defined Function-like V14(S) RelStr-yielding non-Empty reflexive-yielding set
product T is non empty constituted-Functions strict reflexive non void RelStr
the carrier of (product T) is non empty set
bool the carrier of (product T) is non empty set
SC is Element of bool the carrier of (product T)
"/\" (SC,(product T)) is Relation-like Function-like Element of the carrier of (product T)
a is Element of S
("/\" (SC,(product T))) . a is Element of the carrier of (T . a)
T . a is non empty reflexive non void RelStr
the carrier of (T . a) is non empty set
pi (SC,a) is Element of bool the carrier of (T . a)
bool the carrier of (T . a) is non empty set
"/\" ((pi (SC,a)),(T . a)) is Element of the carrier of (T . a)
Sm is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
f is Element of the carrier of (T . a)
b9 is Relation-like Function-like set
b9 . a is set
i is Relation-like Function-like Element of the carrier of (product T)
f is Element of the carrier of (T . a)
("/\" (SC,(product T))) +* (a,f) is Relation-like Function-like set
dom (("/\" (SC,(product T))) +* (a,f)) is set
dom ("/\" (SC,(product T))) is set
i is Element of S
(("/\" (SC,(product T))) +* (a,f)) . i is set
("/\" (SC,(product T))) . i is Element of the carrier of (T . i)
T . i is non empty reflexive non void RelStr
the carrier of (T . i) is non empty set
i is Relation-like Function-like Element of the carrier of (product T)
g1 is Relation-like Function-like Element of the carrier of (product T)
g1 . a is Element of the carrier of (T . a)
g9 is Element of S
i . g9 is Element of the carrier of (T . g9)
T . g9 is non empty reflexive non void RelStr
the carrier of (T . g9) is non empty set
("/\" (SC,(product T))) . g9 is Element of the carrier of (T . g9)
g1 . g9 is Element of the carrier of (T . g9)
i . a is Element of the carrier of (T . a)
S is non empty 1-sorted
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete 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
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
{Sm,SC} is non empty Element of bool (bool [: the carrier of S, the carrier of T:])
bool (bool [: the carrier of S, the carrier of T:]) is non empty set
"/\" ({Sm,SC},(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
f is Element of the carrier of S
a . f is Element of the carrier of T
Sm . f is Element of the carrier of T
SC . f is Element of the carrier of T
{(Sm . f),(SC . f)} is non empty Element of bool the carrier of T
bool the carrier of T is non empty set
"/\" ({(Sm . f),(SC . f)},T) is Element of the carrier of T
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like V14( the carrier of S) quasi_total RelStr-yielding non-Empty reflexive-yielding 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
g1 is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty set
g9 is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty reflexive-yielding set
L is Element of the carrier of S
g9 . L is non empty reflexive non void RelStr
product g9 is non empty constituted-Functions strict reflexive non void RelStr
the carrier of (product g9) is non empty set
b9 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
i is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
bool the carrier of (product g9) is non empty set
L is Relation-like Function-like Element of the carrier of (product g9)
P is Relation-like Function-like Element of the carrier of (product g9)
{L,P} is non empty Element of bool the carrier of (product g9)
b is Element of bool the carrier of (product g9)
"/\" (b,(product g9)) is Relation-like Function-like Element of the carrier of (product g9)
("/\" (b,(product g9))) . f is Element of the carrier of (g9 . f)
g9 . f is non empty reflexive non void RelStr
the carrier of (g9 . f) is non empty set
pi ({Sm,SC},f) is set
"/\" ((pi ({Sm,SC},f)),(g9 . f)) is Element of the carrier of (g9 . f)
"/\" ((pi ({Sm,SC},f)),T) is Element of the carrier of T
S is non empty RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of (T |^ the carrier of S) is non empty set
bool the carrier of (T |^ the carrier of S) is non empty set
Sm is non empty Element of bool the carrier of (T |^ the carrier of S)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
SC is Element of the carrier of S
("\/" (Sm,(T |^ the carrier of S))) . SC is set
{ (b1 . SC) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . SC) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
the carrier of T is non empty set
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like V14( the carrier of S) quasi_total RelStr-yielding non-Empty reflexive-yielding 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
a is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty set
f is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty reflexive-yielding set
product f is non empty constituted-Functions strict reflexive non void RelStr
the carrier of (product f) is non empty set
bool the carrier of (product f) is non empty set
b9 is Element of bool the carrier of (product f)
pi (b9,SC) is Element of bool the carrier of (f . SC)
f . SC is non empty reflexive non void RelStr
the carrier of (f . SC) is non empty set
bool the carrier of (f . SC) is non empty set
i is set
g1 is Relation-like Function-like set
g1 . SC is set
i is set
g1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
g1 . SC is set
i is Element of the carrier of S
f . i is non empty reflexive non void RelStr
"\/" ((pi (b9,SC)),(f . SC)) is Element of the carrier of (f . SC)
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (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 lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of (T |^ the carrier of S) is non empty set
Sm is non empty Element of bool the carrier of (S,T)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
SC is Element of the carrier of S
("\/" (Sm,(T |^ the carrier of S))) . SC is set
{ (b1 . SC) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . SC) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
the carrier of T is non empty set
the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like V14( the carrier of S) quasi_total RelStr-yielding non-Empty reflexive-yielding 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
a is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty set
f is Relation-like the carrier of S -defined Function-like V14( the carrier of S) RelStr-yielding non-Empty reflexive-yielding set
product f is non empty constituted-Functions strict reflexive non void RelStr
the carrier of (product f) is non empty set
bool the carrier of (product f) is non empty set
b9 is Element of bool the carrier of (product f)
pi (b9,SC) is Element of bool the carrier of (f . SC)
f . SC is non empty reflexive non void RelStr
the carrier of (f . SC) is non empty set
bool the carrier of (f . SC) is non empty set
i is set
g1 is Relation-like Function-like set
g1 . SC is set
i is set
g1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
g1 . SC is set
i is Element of the carrier of S
f . i is non empty reflexive non void RelStr
"\/" ((pi (b9,SC)),(f . SC)) is Element of the carrier of (f . SC)
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of (T |^ the carrier of S) is non empty set
bool the carrier of (T |^ the carrier of S) is non empty set
Sm is non empty Element of bool the carrier of (T |^ the carrier of S)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
SC is non empty Element of bool the carrier of S
("\/" (Sm,(T |^ the carrier of S))) .: SC is set
{ ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } is set
a is set
dom ("\/" (Sm,(T |^ the carrier of S))) is set
f is set
("\/" (Sm,(T |^ the carrier of S))) . f is set
b9 is Element of the carrier of S
{ (b1 . b9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . b9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
the carrier of T 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
dom ("\/" (Sm,(T |^ the carrier of S))) is set
a is set
f is Element of the carrier of S
{ (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
("\/" (Sm,(T |^ the carrier of S))) . f is set
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (S,T) is non empty set
the carrier of S is non empty set
bool the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of (T |^ the carrier of S) is non empty set
Sm is non empty Element of bool the carrier of (S,T)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
SC is non empty Element of bool the carrier of S
("\/" (Sm,(T |^ the carrier of S))) .: SC is set
{ ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } is set
a is set
dom ("\/" (Sm,(T |^ the carrier of S))) is set
f is set
("\/" (Sm,(T |^ the carrier of S))) . f is set
b9 is Element of the carrier of S
{ (b1 . b9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . b9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
the carrier of T 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
dom ("\/" (Sm,(T |^ the carrier of S))) is set
a is set
f is Element of the carrier of S
{ (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
("\/" (Sm,(T |^ the carrier of S))) . f is set
F1() is non empty TopRelStr
the carrier of F1() is non empty set
{ F2(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
Sm is set
SC is Element of the carrier of F1()
F3(SC) is set
F2(SC) is set
Sm is set
SC is Element of the carrier of F1()
F2(SC) is set
F3(SC) is set
F1() is non empty RelStr
the carrier of F1() is non empty set
{ F2(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
Sm is set
SC is Element of the carrier of F1()
F3(SC) is set
F2(SC) is set
Sm is set
SC is Element of the carrier of F1()
F2(SC) is set
F3(SC) is set
F2() is non empty TopRelStr
the carrier of F2() is non empty set
F4() is Relation-like Function-like set
dom F4() is set
F1() is non empty TopRelStr
the carrier of F1() is non empty set
{ F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
F4() .: { F3(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ (F4() . F3(b1)) where b1 is Element of the carrier of F1() : P1[b1] } is set
T is set
Sm is set
F4() . Sm is set
SC is Element of the carrier of F1()
F3(SC) is Element of the carrier of F2()
T is set
Sm is Element of the carrier of F1()
F3(Sm) is Element of the carrier of F2()
F4() . F3(Sm) is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : b1 in T } is set
Sm is set
Sm is set
SC is Element of the carrier of S
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (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 lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete 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
Sm is non empty Element of bool the carrier of (S,T)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
bool the carrier of (T |^ the carrier of S) is non empty set
SC is Element of bool the carrier of (T |^ the carrier of S)
"\/" (SC,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
f is Element of the carrier of S
{ (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in SC } is set
b9 is Element of the carrier of S
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a . b9 is Element of the carrier of T
g1 is Element of the carrier of T
g9 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
g9 . f is set
L is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
P is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
P . b9 is Element of the carrier of T
P . f is Element of the carrier of T
a . f is Element of the carrier of T
"\/" ( { (b1 . f) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in SC } ,T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (S,T) is non empty set
the carrier of S is non empty set
bool the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of (T |^ the carrier of S) is non empty set
Sm is non empty Element of bool the carrier of (S,T)
SC is non empty directed Element of bool the carrier of S
{ ("\/" ( { (b1 . b2) where b2 is Element of the carrier of S : b2 in SC } ,T)) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { ("\/" ( { (b1 . b2) where b2 is Element of the carrier of S : b2 in SC } ,T)) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
the carrier of T is non empty set
{ ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of 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
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
{ (a1 . b1) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { (a1 . b1) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
"\/" (SC,S) is Element of the carrier of S
P is Element of the carrier of T
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a .: SC is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((a .: SC),T) is Element of the carrier of T
b is Element of the carrier of T
i9 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
{ (i9 . b1) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { (i9 . b1) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
g1 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
g1 .: SC is Element of bool the carrier of T
a is Element of the carrier of T
dom g1 is non empty Element of bool the carrier of S
x is set
g1 . x is set
x9 is Element of the carrier of S
dom a is non empty Element of bool the carrier of S
a . x9 is Element of the carrier of T
g1 . x9 is Element of the carrier of T
dom g1 is non empty Element of bool the carrier of S
dom i9 is set
{ H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
i9 .: { H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
{ (i9 . H1(b1)) where b1 is Element of the carrier of S : S2[b1] } is set
i9 .: SC is set
"\/" ((i9 .: SC),T) is Element of the carrier of T
L is Element of the carrier of T
b is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
{ (b . b1) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { (b . b1) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
b . ("\/" (SC,S)) is set
i9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
dom i9 is non empty Element of bool the carrier of S
dom b is set
{ H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
b .: { H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
{ (b . H1(b1)) where b1 is Element of the carrier of S : S2[b1] } is set
i9 .: SC is Element of bool the carrier of T
"\/" ((i9 .: SC),T) is Element of the carrier of T
{ H2(b1) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : S1[b1] } is set
{ H3(b1) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : S1[b1] } is set
a . ("\/" (SC,S)) is Element of the carrier of T
b is Element of the carrier of T
i9 is Element of the carrier of S
{ (b1 . i9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { (b1 . i9) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
dom a is non empty Element of bool the carrier of S
a . i9 is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (S,T) is non empty set
the carrier of S is non empty set
bool the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
Sm is non empty Element of bool the carrier of (S,T)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
SC is non empty directed Element of bool the carrier of S
("\/" (Sm,(T |^ the carrier of S))) .: SC is set
"\/" ((("\/" (Sm,(T |^ the carrier of S))) .: SC),T) is Element of the carrier of T
the carrier of T is non empty set
"\/" (SC,S) is Element of the carrier of S
("\/" (Sm,(T |^ the carrier of S))) . ("\/" (SC,S)) is set
bool the carrier of (T |^ the carrier of S) 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
a is non empty Element of bool the carrier of (T |^ the carrier of S)
"\/" (a,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
{ ("\/" ( { (b1 . b2) where b2 is Element of the carrier of S : b2 in SC } ,T)) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } is set
"\/" ( { ("\/" ( { (b1 . b2) where b2 is Element of the carrier of S : b2 in SC } ,T)) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b1 in Sm } ,T) is Element of the carrier of T
{ ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { ("\/" ( { (b2 . b1) where b2 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : b2 in Sm } ,T)) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
{ (a1 . b1) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { (a1 . b1) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
g1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
{ (g1 . b1) where b1 is Element of the carrier of S : b1 in SC } is set
"\/" ( { (g1 . b1) where b1 is Element of the carrier of S : b1 in SC } ,T) is Element of the carrier of T
g1 . ("\/" (SC,S)) is set
g9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
dom g9 is non empty Element of bool the carrier of S
dom g1 is set
{ H3(b1) where b1 is Element of the carrier of S : S2[b1] } is set
g1 .: { H3(b1) where b1 is Element of the carrier of S : S2[b1] } is set
{ (g1 . H3(b1)) where b1 is Element of the carrier of S : S2[b1] } is set
g9 .: SC is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((g9 .: SC),T) is Element of the carrier of T
{ H1(b1) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : S1[b1] } is set
{ H2(b1) where b1 is Relation-like Function-like Element of the carrier of (T |^ the carrier of S) : S1[b1] } is set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
f . ("\/" (SC,S)) is Element of the carrier of T
f .: SC is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((f .: SC),T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of (S,T) is non empty set
bool the carrier of (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 lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
Sm is non empty Element of bool the carrier of (S,T)
"\/" (Sm,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) 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
bool the carrier of S is non empty set
SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is Element of bool the carrier of S
f is non empty directed Element of bool the carrier of S
SC .: f is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" ((SC .: f),T) is Element of the carrier of T
"\/" (f,S) is Element of the carrier of S
SC . ("\/" (f,S)) is Element of the carrier of T
S is non empty RelStr
the carrier of S is non empty set
T is non empty antisymmetric lower-bounded RelStr
T |^ the carrier of S is non empty constituted-Functions strict antisymmetric RelStr
Bottom (T |^ the carrier of S) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
Bottom T is Element of the carrier of T
the carrier of T is non empty set
S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( 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
the carrier of S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
f is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
i is Element of the carrier of S
a . i is Element of the carrier of T
b9 . i is Element of the carrier of T
( the carrier of S --> (Bottom T)) . i is Element of the carrier of T
"\/" ({},(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
S is non empty RelStr
the carrier of S is non empty set
T is non empty antisymmetric upper-bounded RelStr
T |^ the carrier of S is non empty constituted-Functions strict antisymmetric RelStr
Top (T |^ the carrier of S) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
Top T is Element of the carrier of T
the carrier of T is non empty set
S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( 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
the carrier of S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
f is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
i is Element of the carrier of S
b9 . i is Element of the carrier of T
a . i is Element of the carrier of T
( the carrier of S --> (Top T)) . i is Element of the carrier of T
"/\" ({},(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of T is non empty set
S is non empty reflexive non void RelStr
Sm is Element of the carrier of T
S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]
the carrier of S 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
the carrier of S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( 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
a is Element of bool the carrier of S
(S --> Sm) .: a is Element of bool the carrier of T
bool the carrier of T is non empty set
"\/" (((S --> Sm) .: a),T) is Element of the carrier of T
"\/" (a,S) is Element of the carrier of S
(S --> Sm) . ("\/" (a,S)) is Element of the carrier of T
{Sm} is non empty Element of bool the carrier of T
f is non empty directed Element of bool the carrier of S
the Element of f is Element of f
i is set
( the carrier of S --> Sm) . the Element of f is Element of the carrier of T
(S --> Sm) . the Element of f is Element of the carrier of T
dom (S --> Sm) is non empty Element of bool the carrier of S
rng (S --> Sm) is non empty Element of bool the carrier of T
"\/" ({Sm},T) is Element of the carrier of T
( the carrier of S --> Sm) . ("\/" (a,S)) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
SC is reflexive transitive antisymmetric full SubRelStr of T |^ the carrier of S
the carrier of SC is set
bool the carrier of SC is non empty set
a is Element of bool the carrier of SC
"\/" (a,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
"\/" (a,(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
the carrier of (T |^ the carrier of S) is non empty set
Bottom (T |^ the carrier of S) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)
Bottom T is Element of the carrier of T
the carrier of T is non empty set
S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving 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
the carrier of S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric non void RelStr
the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
Bottom (S,T) is Relation-like Function-like Element of the carrier of (S,T)
the carrier of (S,T) is non empty set
Bottom T is Element of the carrier of T
the carrier of T is non empty set
S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
the carrier of S 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
the carrier of S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Relation-like Function-like Element of the carrier of (S,T)
f is Relation-like Function-like Element of the carrier of (S,T)
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
i is Element of the carrier of S
SC . i is set
f . i is set
[(SC . i),(f . i)] is set
{(SC . i),(f . i)} is non empty set
{(SC . i)} is non empty set
{{(SC . i),(f . i)},{(SC . i)}} is non empty set
( the carrier of S --> (Bottom T)) . i is Element of the carrier of T
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a . i is Element of the carrier of T
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
b9 . i is Element of the carrier of T
"\/" ({},(S,T)) is Relation-like Function-like Element of the carrier of (S,T)
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
Top (S,T) is Relation-like Function-like Element of the carrier of (S,T)
the carrier of (S,T) is non empty set
Top T is Element of the carrier of T
the carrier of T is non empty set
S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous monotone directed-sups-preserving Element of bool [: the carrier of S, the carrier of T:]
the carrier of S 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
the carrier of S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
SC is Relation-like Function-like Element of the carrier of (S,T)
f is Relation-like Function-like Element of the carrier of (S,T)
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
i is Element of the carrier of S
f . i is set
SC . i is set
[(f . i),(SC . i)] is set
{(f . i),(SC . i)} is non empty set
{(f . i)} is non empty set
{{(f . i),(SC . i)},{(f . i)}} is non empty set
( the carrier of S --> (Top T)) . i is Element of the carrier of T
b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
b9 . i is Element of the carrier of T
a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a . i is Element of the carrier of T
"/\" ({},(S,T)) is Relation-like Function-like Element of the carrier of (S,T)
S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete Scott non void TopRelStr
SCMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (S,T)
MonMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of S is non empty set
T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
(S,T) is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr
SC is non empty reflexive transitive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of SC is non empty set
the carrier of (MonMaps (S,T)) is non empty set
Sm is non empty reflexive transitive antisymmetric full non void SubRelStr of T |^ the carrier of S
the carrier of Sm is non empty set
a is 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 -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]
a is 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