REAL is V267() V268() V269() V273() set
NAT is non empty V17() V18() V19() V267() V268() V269() V270() V271() V272() V273() Element of K32(REAL)
K32(REAL) is non empty set
NAT is non empty V17() V18() V19() V267() V268() V269() V270() V271() V272() V273() set
K32(NAT) is non empty non empty-membered set
K32(NAT) is non empty non empty-membered set
{} is empty Function-like functional V17() V18() V19() V21() V22() V23() V267() V268() V269() V270() V271() V272() V273() set
the empty Function-like functional V17() V18() V19() V21() V22() V23() V267() V268() V269() V270() V271() V272() V273() set is empty Function-like functional V17() V18() V19() V21() V22() V23() V267() V268() V269() V270() V271() V272() V273() set
1 is non empty V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
{{},1} is non empty V267() V268() V269() V270() V271() V272() set
2 is non empty V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
S is non empty set
K33(NAT,S) is non empty set
K32(K33(NAT,S)) is non empty non empty-membered set
T is Element of S
f is Element of S
x is Relation-like Function-like set
dom x is set
rng x is set
{T,f} is non empty Element of K32(S)
K32(S) is non empty non empty-membered set
FW is set
FX is set
x . FX is set
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * fx is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * fx is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
FW is set
x . 2 is set
2 * 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * FX is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
x . 1 is set
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * FX is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
FW is non empty Relation-like NAT -defined S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT,S))
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
FW . FX is Element of S
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * fx is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
x is non empty Relation-like NAT -defined S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT,S))
FW is non empty Relation-like NAT -defined S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT,S))
dom x is V267() V268() V269() V270() V271() V272() Element of K32(NAT)
dom FW is V267() V268() V269() V270() V271() V272() Element of K32(NAT)
FX is set
x . FX is set
FW . FX is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
x . fx is Element of S
FW . fx is Element of S
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
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
f is set
F4() . f is set
x is Element of the carrier of F1()
F3(x) is Element of the carrier of F2()
T is set
f is Element of the carrier of F1()
F3(f) is Element of the carrier of F2()
F4() . F3(f) is set
F2() is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of F2() is non empty set
F4() is Relation-like Function-like set
dom F4() is set
F1() is non empty reflexive transitive antisymmetric with_suprema with_infima 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
f is set
F4() . f is set
x is Element of the carrier of F1()
F3(x) is Element of the carrier of F2()
T is set
f is Element of the carrier of F1()
F3(f) is Element of the carrier of F2()
F4() . F3(f) is set
S is non empty reflexive RelStr
the carrier of S is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
K32( the carrier of T) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is lower Element of K32( the carrier of T)
f " x is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
FW is Element of the carrier of S
FX is Element of the carrier of S
f . FX is Element of the carrier of T
f . FW is Element of the carrier of T
b is Element of the carrier of T
fx is Element of the carrier of T
S is non empty reflexive RelStr
the carrier of S is non empty set
T is non empty reflexive RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
K32( the carrier of T) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is upper Element of K32( the carrier of T)
f " x is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
FW is Element of the carrier of S
FX is Element of the carrier of S
f . FW is Element of the carrier of T
f . FX is Element of the carrier of T
b is Element of the carrier of T
fx is Element of the carrier of T
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of S is non empty set
T is Element of the carrier of S
downarrow T is non empty directed lower Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{T} is non empty Element of K32( the carrier of S)
downarrow {T} is non empty lower Element of K32( the carrier of S)
f is non empty directed Element of K32( the carrier of S)
"\/" (f,S) is Element of the carrier of S
x is Element of the carrier of S
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of S is non empty set
T is Element of the carrier of S
{T} is non empty Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
Cl {T} is closed Element of K32( the carrier of S)
downarrow T is non empty directed lower Element of K32( the carrier of S)
downarrow {T} is non empty lower Element of K32( the carrier of S)
f is Element of K32( the carrier of S)
x is Element of K32( the carrier of S)
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of S is non empty set
T is Element of the carrier of S
downarrow T is non empty directed lower Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{T} is non empty Element of K32( the carrier of S)
downarrow {T} is non empty lower Element of K32( the carrier of S)
Cl {T} is closed Element of K32( the carrier of S)
S is non empty reflexive antisymmetric RelStr
the carrier of S is non empty set
T is non empty reflexive antisymmetric RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
FW is Element of the carrier of S
f . x is Element of the carrier of T
f . FW is Element of the carrier of T
{x,FW} is non empty Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
FX is Element of the carrier of S
"\/" ({x,FW},S) is Element of the carrier of S
FX is Element of the carrier of S
fx is Element of the carrier of S
f .: {x,FW} is non empty Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"\/" ((f .: {x,FW}),T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
{(f . x),(f . FW)} is non empty Element of K32( the carrier of T)
"\/" ({(f . x),(f . FW)},T) is Element of the carrier of T
S is non empty reflexive antisymmetric RelStr
the carrier of S is non empty set
T is non empty reflexive antisymmetric RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
FW is Element of the carrier of S
f . x is Element of the carrier of T
f . FW is Element of the carrier of T
dom f is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
[#] T is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
downarrow (f . FW) is non empty directed lower Element of K32( the carrier of T)
{(f . FW)} is non empty Element of K32( the carrier of T)
downarrow {(f . FW)} is non empty lower Element of K32( the carrier of T)
(downarrow (f . FW)) ` is Element of K32( the carrier of T)
the carrier of T \ (downarrow (f . FW)) is set
f " ((downarrow (f . FW)) `) is Element of K32( the carrier of S)
b is upper Element of K32( the carrier of S)
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
K32( the carrier of T) is non empty non empty-membered set
x is Element of K32( the carrier of T)
f " x is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
FW is Element of K32( the carrier of T)
FX is non empty directed Element of K32( the carrier of S)
f .: FX is non empty Element of K32( the carrier of T)
"\/" ((f .: FX),T) is Element of the carrier of T
"\/" (FX,S) is Element of the carrier of S
f . ("\/" (FX,S)) is Element of the carrier of T
fx is directed Element of K32( the carrier of T)
"\/" (fx,T) is Element of the carrier of T
S is set
T is reflexive RelStr
S --> T is Relation-like S -defined {T} -valued Function-like constant V28(S) quasi_total RelStr-yielding Element of K32(K33(S,{T}))
{T} is non empty set
K33(S,{T}) is set
K32(K33(S,{T})) is non empty set
x is RelStr
rng (S --> T) is trivial set
rng (S --> T) is trivial Element of K32({T})
K32({T}) is non empty non empty-membered set
S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
T |^ S is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
S --> T is non empty Relation-like S -defined {T} -valued Function-like constant V28(S) quasi_total RelStr-yielding non-Empty reflexive-yielding Element of K32(K33(S,{T}))
{T} is non empty set
K33(S,{T}) is non empty set
K32(K33(S,{T})) is non empty non empty-membered set
product (S --> T) is non empty strict reflexive RelStr
f is Element of S
(S --> T) . f is non empty reflexive RelStr
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
MonMaps (S,T) is non empty strict full 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 RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
the carrier of (MonMaps (S,T)) is non empty set
f is set
x is set
K32( the carrier of (MonMaps (S,T))) is non empty non empty-membered set
x is Element of K32( the carrier of (MonMaps (S,T)))
subrelstr x is strict full SubRelStr of MonMaps (S,T)
FW is strict full SubRelStr of MonMaps (S,T)
the carrier of FW is set
FX is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
fx is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( 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
f is strict full SubRelStr of MonMaps (S,T)
the carrier of f is set
x is strict full SubRelStr of MonMaps (S,T)
the carrier of x is set
the carrier of (MonMaps (S,T)) is non empty set
FW is set
FX is Element of the carrier of f
fx is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
FW is set
FX is Element of the carrier of x
fx is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete Scott TopRelStr
(S,T) is strict full SubRelStr of MonMaps (S,T)
MonMaps (S,T) is non empty strict full 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 RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
the non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total continuous monotone Element of K32(K33( 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 V28( the carrier of S) quasi_total continuous monotone Element of K32(K33( the carrier of S, the carrier of T))
the carrier of (S,T) is set
S is non empty RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
K33(NAT,NAT) is non empty set
K32(K33(NAT,NAT)) is non empty non empty-membered set
x is Relation-like NAT -defined NAT -valued Element of K32(K33(NAT,NAT))
FW is Relation-like NAT -defined NAT -valued Element of K32(K33(NAT,NAT))
NetStr(# NAT,FW,( the carrier of S,T,f) #) is non empty strict NetStr over S
FX is non empty strict NetStr over S
the carrier of FX is non empty set
the mapping of FX is non empty Relation-like the carrier of FX -defined the carrier of S -valued Function-like V28( the carrier of FX) quasi_total Element of K32(K33( the carrier of FX, the carrier of S))
K33( the carrier of FX, the carrier of S) is non empty set
K32(K33( the carrier of FX, the carrier of S)) is non empty non empty-membered set
fx is Element of the carrier of FX
b is Element of the carrier of FX
ww is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
u is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
h is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
[w,h] is Element of K33(NAT,NAT)
{w,h} is non empty V267() V268() V269() V270() V271() V272() set
{w} is non empty V267() V268() V269() V270() V271() V272() set
{{w,h},{w}} is non empty set
the InternalRel of FX is Relation-like the carrier of FX -defined the carrier of FX -valued Element of K32(K33( the carrier of FX, the carrier of FX))
K33( the carrier of FX, the carrier of FX) is non empty set
K32(K33( the carrier of FX, the carrier of FX)) is non empty non empty-membered set
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
x is non empty strict NetStr over S
the carrier of x is non empty set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of S))
K33( the carrier of x, the carrier of S) is non empty set
K32(K33( the carrier of x, the carrier of S)) is non empty non empty-membered set
FW is non empty strict NetStr over S
the carrier of FW is non empty set
the mapping of FW is non empty Relation-like the carrier of FW -defined the carrier of S -valued Function-like V28( the carrier of FW) quasi_total Element of K32(K33( the carrier of FW, the carrier of S))
K33( the carrier of FW, the carrier of S) is non empty set
K32(K33( the carrier of FW, the carrier of S)) is non empty non empty-membered set
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K32(K33( the carrier of x, the carrier of x))
K33( the carrier of x, the carrier of x) is non empty set
K32(K33( the carrier of x, the carrier of x)) is non empty non empty-membered set
the InternalRel of FW is Relation-like the carrier of FW -defined the carrier of FW -valued Element of K32(K33( the carrier of FW, the carrier of FW))
K33( the carrier of FW, the carrier of FW) is non empty set
K32(K33( the carrier of FW, the carrier of FW)) is non empty non empty-membered set
FX is set
fx is set
[FX,fx] is set
{FX,fx} is non empty set
{FX} is non empty set
{{FX,fx},{FX}} is non empty set
b is Element of the carrier of x
ww is Element of the carrier of x
u is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
h is Element of the carrier of FW
z is Element of the carrier of FW
b is Element of the carrier of FW
ww is Element of the carrier of FW
h is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
u is Element of the carrier of x
w is Element of the carrier of x
S is non empty RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
(S,T,f) is non empty strict NetStr over S
the carrier of (S,T,f) is non empty set
FW is Element of the carrier of (S,T,f)
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
the carrier of (S,T,f) is non empty set
FW is Element of the carrier of (S,T,f)
FX is Element of the carrier of (S,T,f)
fx is Element of the carrier of (S,T,f)
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
ww is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
u is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
[#] (S,T,f) is non empty non proper lower upper Element of K32( the carrier of (S,T,f))
the carrier of (S,T,f) is non empty set
K32( the carrier of (S,T,f)) is non empty non empty-membered set
FW is Element of the carrier of (S,T,f)
FX is Element of the carrier of (S,T,f)
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
fx + b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
u is Element of the carrier of (S,T,f)
w is Element of the carrier of (S,T,f)
FW is Element of the carrier of (S,T,f)
FX is Element of the carrier of (S,T,f)
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
S is non empty RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
(S,T,f) is non empty reflexive transitive antisymmetric strict directed NetStr over S
the carrier of (S,T,f) is non empty set
x is Element of the carrier of (S,T,f)
(S,T,f) . x is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . x is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . x is set
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * fx is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * fx is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
S is non empty RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
(S,T,f) is non empty reflexive transitive antisymmetric strict directed NetStr over S
the carrier of (S,T,f) is non empty set
x is Element of the carrier of (S,T,f)
FW is Element of the carrier of (S,T,f)
(S,T,f) . x is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . x is Element of the carrier of S
(S,T,f) . FW is Element of the carrier of S
the mapping of (S,T,f) . FW is Element of the carrier of S
FX is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
FX + 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . x is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
ww is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * ww is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . x is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
(2 * b) + 1 is non empty V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
(S,T,f) is non empty reflexive transitive antisymmetric strict directed NetStr over S
lim_inf (S,T,f) is Element of the carrier of S
the carrier of (S,T,f) is non empty set
{ ("/\" ( { ((S,T,f) . b2) where b2 is Element of the carrier of (S,T,f) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T,f) : verum } is set
"\/" ( { ("/\" ( { ((S,T,f) . b2) where b2 is Element of the carrier of (S,T,f) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T,f) : verum } ,S) is Element of the carrier of S
T "/\" f is Element of the carrier of S
{T,f} is non empty Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
FW is Element of the carrier of (S,T,f)
{ ((S,T,f) . b1) where b1 is Element of the carrier of (S,T,f) : FW <= b1 } is set
FX is set
fx is Element of the carrier of (S,T,f)
(S,T,f) . fx is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . fx is Element of the carrier of S
FX is set
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(S,T,f) . FW is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . FW is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(S,T,f) . FW is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . FW is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
fx + 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is Element of the carrier of (S,T,f)
(S,T,f) . b is Element of the carrier of S
the mapping of (S,T,f) . b is Element of the carrier of S
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(S,T,f) . FW is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . FW is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(S,T,f) . FW is Element of the carrier of S
the mapping of (S,T,f) is non empty Relation-like the carrier of (S,T,f) -defined the carrier of S -valued Function-like V28( the carrier of (S,T,f)) quasi_total Element of K32(K33( the carrier of (S,T,f), the carrier of S))
K33( the carrier of (S,T,f), the carrier of S) is non empty set
K32(K33( the carrier of (S,T,f), the carrier of S)) is non empty non empty-membered set
the mapping of (S,T,f) . FW is Element of the carrier of S
( the carrier of S,T,f) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,T,f) . FW is set
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
fx + 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is Element of the carrier of (S,T,f)
(S,T,f) . b is Element of the carrier of S
the mapping of (S,T,f) . b is Element of the carrier of S
fx is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
b is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * b is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
{ ((S,T,f) . b1) where b1 is Element of the carrier of (S,T,f) : S1[b1,a1] } is set
FW is Element of the carrier of (S,T,f)
{ ((S,T,f) . b1) where b1 is Element of the carrier of (S,T,f) : S1[b1,FW] } is set
"/\" (H1(FW),S) is Element of the carrier of S
"/\" (H2(FW),S) is Element of the carrier of S
{ H3(b1) where b1 is Element of the carrier of (S,T,f) : S2[b1] } is set
{ H5(b1) where b1 is Element of the carrier of (S,T,f) : S2[b1] } is set
{ (T "/\" f) where b1 is Element of the carrier of (S,T,f) : S2[b1] } is set
{(T "/\" f)} is non empty Element of K32( the carrier of S)
FW is set
FW is set
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
T is Element of the carrier of S
f is Element of the carrier of S
(S,T,f) is non empty reflexive transitive antisymmetric strict directed NetStr over S
lim_inf (S,T,f) is Element of the carrier of S
the carrier of (S,T,f) is non empty set
{ ("/\" ( { ((S,T,f) . b2) where b2 is Element of the carrier of (S,T,f) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T,f) : verum } is set
"\/" ( { ("/\" ( { ((S,T,f) . b2) where b2 is Element of the carrier of (S,T,f) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T,f) : verum } ,S) is Element of the carrier of S
x is Element of the carrier of S
FW is Element of the carrier of S
x "/\" FW is Element of the carrier of S
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is Element of the carrier of S
x is Element of the carrier of S
(S,f,x) is non empty reflexive transitive antisymmetric strict directed NetStr over S
FW is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
FW * (S,f,x) is non empty reflexive transitive antisymmetric strict directed NetStr over T
lim_inf (FW * (S,f,x)) is Element of the carrier of T
the carrier of (FW * (S,f,x)) is non empty set
{ ("/\" ( { ((FW * (S,f,x)) . b2) where b2 is Element of the carrier of (FW * (S,f,x)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (FW * (S,f,x)) : verum } is set
"\/" ( { ("/\" ( { ((FW * (S,f,x)) . b2) where b2 is Element of the carrier of (FW * (S,f,x)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (FW * (S,f,x)) : verum } ,T) is Element of the carrier of T
FW . f is Element of the carrier of T
FW . x is Element of the carrier of T
(FW . f) "/\" (FW . x) is Element of the carrier of T
the InternalRel of (FW * (S,f,x)) is Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of (FW * (S,f,x)) -valued Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of (FW * (S,f,x))))
K33( the carrier of (FW * (S,f,x)), the carrier of (FW * (S,f,x))) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of (FW * (S,f,x)))) is non empty non empty-membered set
RelStr(# the carrier of (FW * (S,f,x)), the InternalRel of (FW * (S,f,x)) #) is strict RelStr
the carrier of (S,f,x) is non empty set
the InternalRel of (S,f,x) is Relation-like the carrier of (S,f,x) -defined the carrier of (S,f,x) -valued Element of K32(K33( the carrier of (S,f,x), the carrier of (S,f,x)))
K33( the carrier of (S,f,x), the carrier of (S,f,x)) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of (S,f,x))) is non empty non empty-membered set
RelStr(# the carrier of (S,f,x), the InternalRel of (S,f,x) #) is strict RelStr
{(FW . f),(FW . x)} is non empty Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
b is Element of the carrier of (FW * (S,f,x))
{ ((FW * (S,f,x)) . b1) where b1 is Element of the carrier of (FW * (S,f,x)) : b <= b1 } is set
u is set
w is Element of the carrier of (FW * (S,f,x))
(FW * (S,f,x)) . w is Element of the carrier of T
the mapping of (FW * (S,f,x)) is non empty Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of T -valued Function-like V28( the carrier of (FW * (S,f,x))) quasi_total Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of T))
K33( the carrier of (FW * (S,f,x)), the carrier of T) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of T)) is non empty non empty-membered set
the mapping of (FW * (S,f,x)) . w is Element of the carrier of T
the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of S -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of S))
K33( the carrier of (S,f,x), the carrier of S) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of S)) is non empty non empty-membered set
dom the mapping of (S,f,x) is Element of K32( the carrier of (S,f,x))
K32( the carrier of (S,f,x)) is non empty non empty-membered set
FW * the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of T -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of T))
K33( the carrier of (S,f,x), the carrier of T) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of T)) is non empty non empty-membered set
(FW * the mapping of (S,f,x)) . w is set
h is Element of the carrier of (S,f,x)
(S,f,x) . h is Element of the carrier of S
the mapping of (S,f,x) . h is Element of the carrier of S
FW . ((S,f,x) . h) is Element of the carrier of T
u is set
the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of S -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of S))
K33( the carrier of (S,f,x), the carrier of S) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of S)) is non empty non empty-membered set
dom the mapping of (S,f,x) is Element of K32( the carrier of (S,f,x))
K32( the carrier of (S,f,x)) is non empty non empty-membered set
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(FW * (S,f,x)) . b is Element of the carrier of T
the mapping of (FW * (S,f,x)) is non empty Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of T -valued Function-like V28( the carrier of (FW * (S,f,x))) quasi_total Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of T))
K33( the carrier of (FW * (S,f,x)), the carrier of T) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of T)) is non empty non empty-membered set
the mapping of (FW * (S,f,x)) . b is Element of the carrier of T
FW * the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of T -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of T))
K33( the carrier of (S,f,x), the carrier of T) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of T)) is non empty non empty-membered set
(FW * the mapping of (S,f,x)) . b is set
the mapping of (S,f,x) . b is set
FW . ( the mapping of (S,f,x) . b) is set
( the carrier of S,f,x) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,f,x) . b is set
FW . (( the carrier of S,f,x) . b) is set
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * z is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
h is Element of the carrier of (S,f,x)
(S,f,x) . h is Element of the carrier of S
the mapping of (S,f,x) . h is Element of the carrier of S
( the carrier of S,f,x) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,f,x) . h is set
w + 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is Element of the carrier of (FW * (S,f,x))
z is Element of the carrier of (S,f,x)
(FW * (S,f,x)) . z is Element of the carrier of T
the mapping of (FW * (S,f,x)) is non empty Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of T -valued Function-like V28( the carrier of (FW * (S,f,x))) quasi_total Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of T))
K33( the carrier of (FW * (S,f,x)), the carrier of T) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of T)) is non empty non empty-membered set
the mapping of (FW * (S,f,x)) . z is Element of the carrier of T
FW * the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of T -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of T))
K33( the carrier of (S,f,x), the carrier of T) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of T)) is non empty non empty-membered set
(FW * the mapping of (S,f,x)) . z is set
(S,f,x) . z is Element of the carrier of S
the mapping of (S,f,x) . z is Element of the carrier of S
FW . ((S,f,x) . z) is Element of the carrier of T
[h,z] is Element of K33( the carrier of (S,f,x), the carrier of (S,f,x))
{h,z} is non empty set
{h} is non empty set
{{h,z},{h}} is non empty set
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
z is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * z is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
(FW * (S,f,x)) . b is Element of the carrier of T
the mapping of (FW * (S,f,x)) is non empty Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of T -valued Function-like V28( the carrier of (FW * (S,f,x))) quasi_total Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of T))
K33( the carrier of (FW * (S,f,x)), the carrier of T) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of T)) is non empty non empty-membered set
the mapping of (FW * (S,f,x)) . b is Element of the carrier of T
FW * the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of T -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of T))
K33( the carrier of (S,f,x), the carrier of T) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of T)) is non empty non empty-membered set
(FW * the mapping of (S,f,x)) . b is set
the mapping of (S,f,x) . b is set
FW . ( the mapping of (S,f,x) . b) is set
( the carrier of S,f,x) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,f,x) . b is set
FW . (( the carrier of S,f,x) . b) is set
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
ww is Element of the carrier of (S,f,x)
(S,f,x) . ww is Element of the carrier of S
the mapping of (S,f,x) . ww is Element of the carrier of S
( the carrier of S,f,x) is non empty Relation-like NAT -defined the carrier of S -valued Function-like V28( NAT ) quasi_total Element of K32(K33(NAT, the carrier of S))
K33(NAT, the carrier of S) is non empty set
K32(K33(NAT, the carrier of S)) is non empty non empty-membered set
( the carrier of S,f,x) . b is set
h is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * h is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
w + 1 is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
h is Element of the carrier of (FW * (S,f,x))
z is Element of the carrier of (S,f,x)
(FW * (S,f,x)) . h is Element of the carrier of T
the mapping of (FW * (S,f,x)) is non empty Relation-like the carrier of (FW * (S,f,x)) -defined the carrier of T -valued Function-like V28( the carrier of (FW * (S,f,x))) quasi_total Element of K32(K33( the carrier of (FW * (S,f,x)), the carrier of T))
K33( the carrier of (FW * (S,f,x)), the carrier of T) is non empty set
K32(K33( the carrier of (FW * (S,f,x)), the carrier of T)) is non empty non empty-membered set
the mapping of (FW * (S,f,x)) . h is Element of the carrier of T
FW * the mapping of (S,f,x) is non empty Relation-like the carrier of (S,f,x) -defined the carrier of T -valued Function-like V28( the carrier of (S,f,x)) quasi_total Element of K32(K33( the carrier of (S,f,x), the carrier of T))
K33( the carrier of (S,f,x), the carrier of T) is non empty set
K32(K33( the carrier of (S,f,x), the carrier of T)) is non empty non empty-membered set
(FW * the mapping of (S,f,x)) . h is set
(S,f,x) . z is Element of the carrier of S
the mapping of (S,f,x) . z is Element of the carrier of S
FW . ((S,f,x) . z) is Element of the carrier of T
[ww,z] is Element of K33( the carrier of (S,f,x), the carrier of (S,f,x))
{ww,z} is non empty set
{ww} is non empty set
{{ww,z},{ww}} is non empty set
w is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
h is V17() V18() V19() V23() V24() ext-real V43() V44() V267() V268() V269() V270() V271() V272() Element of NAT
2 * h is V17() V18() V19() V23() V24() ext-real V43() V44() V59() V267() V268() V269() V270() V271() V272() Element of NAT
{ ((FW * (S,f,x)) . b1) where b1 is Element of the carrier of (FW * (S,f,x)) : S1[b1,a1] } is set
b is Element of the carrier of (FW * (S,f,x))
{ ((FW * (S,f,x)) . b1) where b1 is Element of the carrier of (FW * (S,f,x)) : S1[b1,b] } is set
"/\" (H1(b),T) is Element of the carrier of T
"/\" (H2(b),T) is Element of the carrier of T
{ H3(b1) where b1 is Element of the carrier of (FW * (S,f,x)) : S2[b1] } is set
{ H5(b1) where b1 is Element of the carrier of (FW * (S,f,x)) : S2[b1] } is set
{ ((FW . f) "/\" (FW . x)) where b1 is Element of the carrier of (FW * (S,f,x)) : S2[b1] } is set
{((FW . f) "/\" (FW . x))} is non empty Element of K32( the carrier of T)
b is set
b is set
S is non empty RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty Element of K32( the carrier of S)
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty strict NetStr over S
S is non empty reflexive RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
T is non empty Element of K32( the carrier of S)
(S,T) is strict NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty strict NetStr over S
Net-Str (T,((id the carrier of S) | T)) is non empty reflexive strict monotone NetStr over S
the carrier of (Net-Str (T,((id the carrier of S) | T))) is non empty set
the mapping of (Net-Str (T,((id the carrier of S) | T))) is non empty Relation-like the carrier of (Net-Str (T,((id the carrier of S) | T))) -defined the carrier of S -valued Function-like V28( the carrier of (Net-Str (T,((id the carrier of S) | T)))) quasi_total Element of K32(K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of S))
K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of S) is non empty set
K32(K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of S)) is non empty non empty-membered set
id T is non empty Relation-like T -defined T -valued Function-like one-to-one V28(T) quasi_total Element of K32(K33(T,T))
x is set
FW is set
[x,FW] is set
{x,FW} is non empty set
{x} is non empty set
{{x,FW},{x}} is non empty set
FX is Element of the carrier of (Net-Str (T,((id the carrier of S) | T)))
((id the carrier of S) | T) . FX is set
fx is Element of the carrier of (Net-Str (T,((id the carrier of S) | T)))
((id the carrier of S) | T) . fx is set
(Net-Str (T,((id the carrier of S) | T))) . FX is Element of the carrier of S
the mapping of (Net-Str (T,((id the carrier of S) | T))) . FX is Element of the carrier of S
(Net-Str (T,((id the carrier of S) | T))) . fx is Element of the carrier of S
the mapping of (Net-Str (T,((id the carrier of S) | T))) . fx is Element of the carrier of S
the InternalRel of (Net-Str (T,((id the carrier of S) | T))) is Relation-like the carrier of (Net-Str (T,((id the carrier of S) | T))) -defined the carrier of (Net-Str (T,((id the carrier of S) | T))) -valued Element of K32(K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of (Net-Str (T,((id the carrier of S) | T)))))
K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of (Net-Str (T,((id the carrier of S) | T)))) is non empty set
K32(K33( the carrier of (Net-Str (T,((id the carrier of S) | T))), the carrier of (Net-Str (T,((id the carrier of S) | T))))) is non empty non empty-membered set
FX is Element of the carrier of (Net-Str (T,((id the carrier of S) | T)))
fx is Element of the carrier of (Net-Str (T,((id the carrier of S) | T)))
(Net-Str (T,((id the carrier of S) | T))) . FX is Element of the carrier of S
the mapping of (Net-Str (T,((id the carrier of S) | T))) . FX is Element of the carrier of S
(Net-Str (T,((id the carrier of S) | T))) . fx is Element of the carrier of S
the mapping of (Net-Str (T,((id the carrier of S) | T))) . fx is Element of the carrier of S
[((Net-Str (T,((id the carrier of S) | T))) . FX),((Net-Str (T,((id the carrier of S) | T))) . fx)] is Element of K33( the carrier of S, the carrier of S)
{((Net-Str (T,((id the carrier of S) | T))) . FX),((Net-Str (T,((id the carrier of S) | T))) . fx)} is non empty set
{((Net-Str (T,((id the carrier of S) | T))) . FX)} is non empty set
{{((Net-Str (T,((id the carrier of S) | T))) . FX),((Net-Str (T,((id the carrier of S) | T))) . fx)},{((Net-Str (T,((id the carrier of S) | T))) . FX)}} is non empty set
((id the carrier of S) | T) . FX is set
((id the carrier of S) | T) . fx is set
S is non empty reflexive RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty directed Element of K32( the carrier of S)
(S,T) is strict NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty strict directed NetStr over S
Net-Str (T,((id the carrier of S) | T)) is non empty reflexive strict monotone NetStr over S
S is non empty reflexive transitive RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty directed Element of K32( the carrier of S)
(S,T) is non empty reflexive strict directed NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty transitive strict directed NetStr over S
S is non empty reflexive RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty directed Element of K32( the carrier of S)
(S,T) is non empty reflexive strict directed NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty strict directed NetStr over S
Net-Str (T,((id the carrier of S) | T)) is non empty reflexive strict monotone NetStr over S
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
T is non empty reflexive transitive directed monotone eventually-directed NetStr over S
lim_inf T is Element of the carrier of S
the carrier of S is non empty set
the carrier of T is non empty set
{ ("/\" ( { (T . b2) where b2 is Element of the carrier of T : b1 <= b2 } ,S)) where b1 is Element of the carrier of T : verum } is set
"\/" ( { ("/\" ( { (T . b2) where b2 is Element of the carrier of T : b1 <= b2 } ,S)) where b1 is Element of the carrier of T : verum } ,S) is Element of the carrier of S
sup T is Element of the carrier of S
{ (T . b1) where b1 is Element of the carrier of T : a1 <= b1 } is set
"/\" ( { (T . b1) where b1 is Element of the carrier of T : a1 <= b1 } ,S) is Element of the carrier of S
f is Element of the carrier of T
T . f is Element of the carrier of S
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V28( the carrier of T) quasi_total Element of K32(K33( the carrier of T, the carrier of S))
K33( the carrier of T, the carrier of S) is non empty set
K32(K33( the carrier of T, the carrier of S)) is non empty non empty-membered set
the mapping of T . f is Element of the carrier of S
{ (T . b1) where b1 is Element of the carrier of T : f <= b1 } is set
"/\" ( { (T . b1) where b1 is Element of the carrier of T : f <= b1 } ,S) is Element of the carrier of S
FW is Element of the carrier of S
FX is Element of the carrier of T
T . FX is Element of the carrier of S
the mapping of T . FX is Element of the carrier of S
FW is Element of the carrier of S
FX is Element of the carrier of T
T . FX is Element of the carrier of S
the mapping of T . FX is Element of the carrier of S
the mapping of T is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V28( the carrier of T) quasi_total Element of K32(K33( the carrier of T, the carrier of S))
K33( the carrier of T, the carrier of S) is non empty set
K32(K33( the carrier of T, the carrier of S)) is non empty non empty-membered set
rng the mapping of T is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ H1(b1) where b1 is Element of the carrier of T : S1[b1] } is set
{ H2(b1) where b1 is Element of the carrier of T : S1[b1] } is set
\\/ ( the mapping of T,S) is Element of the carrier of S
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty directed Element of K32( the carrier of S)
(S,T) is non empty reflexive transitive strict directed monotone eventually-directed NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 T is Relation-like T -defined T -valued Element of K32(K33(T,T))
K33(T,T) is non empty set
K32(K33(T,T)) is non empty non empty-membered set
the InternalRel of S /\ K33(T,T) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | T is non empty Relation-like T -defined the carrier of S -valued Function-like V28(T) quasi_total Element of K32(K33(T, the carrier of S))
K33(T, the carrier of S) is non empty set
K32(K33(T, the carrier of S)) is non empty non empty-membered set
NetStr(# T,( the InternalRel of S |_2 T),((id the carrier of S) | T) #) is non empty transitive strict directed NetStr over S
lim_inf (S,T) is Element of the carrier of S
the carrier of (S,T) is non empty set
{ ("/\" ( { ((S,T) . b2) where b2 is Element of the carrier of (S,T) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T) : verum } is set
"\/" ( { ("/\" ( { ((S,T) . b2) where b2 is Element of the carrier of (S,T) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,T) : verum } ,S) is Element of the carrier of S
"\/" (T,S) is Element of the carrier of S
id T is non empty Relation-like T -defined T -valued Function-like one-to-one V28(T) quasi_total Element of K32(K33(T,T))
sup (S,T) is Element of the carrier of S
\\/ (((id the carrier of S) | T),S) is Element of the carrier of S
rng ((id the carrier of S) | T) is Element of K32( the carrier of S)
"\/" ((rng ((id the carrier of S) | T)),S) is Element of the carrier of S
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
FW is Element of the carrier of S
(S,x,FW) is non empty reflexive transitive antisymmetric strict directed NetStr over S
lim_inf (S,x,FW) is Element of the carrier of S
the carrier of (S,x,FW) is non empty set
{ ("/\" ( { ((S,x,FW) . b2) where b2 is Element of the carrier of (S,x,FW) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,x,FW) : verum } is set
"\/" ( { ("/\" ( { ((S,x,FW) . b2) where b2 is Element of the carrier of (S,x,FW) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,x,FW) : verum } ,S) is Element of the carrier of S
f . (lim_inf (S,x,FW)) is Element of the carrier of T
f . x is Element of the carrier of T
f * (S,x,FW) is non empty reflexive transitive antisymmetric strict directed NetStr over T
lim_inf (f * (S,x,FW)) is Element of the carrier of T
the carrier of (f * (S,x,FW)) is non empty set
{ ("/\" ( { ((f * (S,x,FW)) . b2) where b2 is Element of the carrier of (f * (S,x,FW)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,x,FW)) : verum } is set
"\/" ( { ("/\" ( { ((f * (S,x,FW)) . b2) where b2 is Element of the carrier of (f * (S,x,FW)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,x,FW)) : verum } ,T) is Element of the carrier of T
f . FW is Element of the carrier of T
(f . x) "/\" (f . FW) is Element of the carrier of T
F3() is non empty TopRelStr
the carrier of F3() is non empty set
F5() is Relation-like Function-like set
dom F5() is set
F1() is non empty TopRelStr
the carrier of F1() is non empty set
F2() is non empty TopRelStr
the carrier of F2() is non empty set
{ F4(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
F5() .: { F4(b1) where b1 is Element of the carrier of F1() : P1[b1] } is set
{ (F5() . F4(b1)) where b1 is Element of the carrier of F2() : P1[b1] } is set
T is set
f is set
F5() . f is set
x is Element of the carrier of F1()
F4(x) is Element of the carrier of F3()
FW is Element of the carrier of F2()
F4(FW) is Element of the carrier of F3()
F5() . F4(FW) is set
T is set
f is Element of the carrier of F2()
F4(f) is Element of the carrier of F3()
F5() . F4(f) is set
x is Element of the carrier of F1()
F4(x) is Element of the carrier of F3()
S is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
waybelow x is non empty directed lower Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ b1 where b1 is Element of the carrier of S : b1 is_way_below x } is set
dom f is Element of K32( the carrier of S)
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
{ (f . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
"\/" ((waybelow x),S) is Element of the carrier of S
f . ("\/" ((waybelow x),S)) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
FW is Element of the carrier of S
f . x is Element of the carrier of T
f . FW is Element of the carrier of T
waybelow x is directed lower Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ b1 where b1 is Element of the carrier of S : b1 is_way_below x } is set
waybelow FW is directed lower Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : b1 is_way_below FW } is set
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
{ (f . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
{ H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S2[b1] } is Element of K32( the carrier of T)
{ (f . H1(b1)) where b1 is Element of the carrier of S : S2[b1] } is set
f .: (waybelow FW) is Element of K32( the carrier of T)
"\/" ((f .: (waybelow FW)),T) is Element of the carrier of T
f .: (waybelow x) is Element of K32( the carrier of T)
S is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
FW is Element of the carrier of T
K32( the carrier of T) is non empty non empty-membered set
waybelow x is non empty directed lower Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ b1 where b1 is Element of the carrier of S : b1 is_way_below x } is set
f .: (waybelow x) is non empty Element of K32( the carrier of T)
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of K32( the carrier of T)
{ (f . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
FX is non empty directed Element of K32( the carrier of T)
fx is Element of the carrier of T
b is set
f . b is set
ww is Element of the carrier of S
u is Element of the carrier of S
f . u is Element of the carrier of T
FX is Element of the carrier of S
f . FX is Element of the carrier of T
S is non empty RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is Element of K32( the carrier of S)
"\/" (f,S) is Element of the carrier of S
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x .: f is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"\/" ((x .: f),T) is Element of the carrier of T
x . ("\/" (f,S)) is Element of the carrier of T
S is non empty reflexive antisymmetric RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty reflexive antisymmetric RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty directed Element of K32( the carrier of S)
"\/" (f,S) is Element of the carrier of S
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x .: f is non empty Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"\/" ((x .: f),T) is Element of the carrier of T
x . ("\/" (f,S)) is Element of the carrier of T
FW is non empty directed Element of K32( the carrier of T)
S is non empty RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is Element of K32( the carrier of S)
"/\" (f,S) is Element of the carrier of S
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x .: f is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
x . ("/\" (f,S)) is Element of the carrier of T
"/\" ((x .: f),T) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is Element of K32( the carrier of S)
"/\" (f,S) is Element of the carrier of S
x is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x . ("/\" (f,S)) is Element of the carrier of T
x .: f is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"/\" ((x .: f),T) is Element of the carrier of T
FW is Element of K32( the carrier of S)
x .: FW is Element of K32( the carrier of T)
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is non empty monotone NetStr over S
f * x is non empty strict NetStr over T
netmap (x,S) is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of S))
the carrier of x is non empty set
K33( the carrier of x, the carrier of S) is non empty set
K32(K33( the carrier of x, the carrier of S)) is non empty non empty-membered set
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of S))
the carrier of (f * x) is non empty set
netmap ((f * x),T) is non empty Relation-like the carrier of (f * x) -defined the carrier of T -valued Function-like V28( the carrier of (f * x)) quasi_total Element of K32(K33( the carrier of (f * x), the carrier of T))
K33( the carrier of (f * x), the carrier of T) is non empty set
K32(K33( the carrier of (f * x), the carrier of T)) is non empty non empty-membered set
the mapping of (f * x) is non empty Relation-like the carrier of (f * x) -defined the carrier of T -valued Function-like V28( the carrier of (f * x)) quasi_total Element of K32(K33( the carrier of (f * x), the carrier of T))
f * (netmap (x,S)) is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of T))
K33( the carrier of x, the carrier of T) is non empty set
K32(K33( the carrier of x, the carrier of T)) is non empty non empty-membered set
FX is Element of the carrier of (f * x)
fx is Element of the carrier of (f * x)
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K32(K33( the carrier of x, the carrier of x))
K33( the carrier of x, the carrier of x) is non empty set
K32(K33( the carrier of x, the carrier of x)) is non empty non empty-membered set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the InternalRel of (f * x) is Relation-like the carrier of (f * x) -defined the carrier of (f * x) -valued Element of K32(K33( the carrier of (f * x), the carrier of (f * x)))
K33( the carrier of (f * x), the carrier of (f * x)) is non empty set
K32(K33( the carrier of (f * x), the carrier of (f * x))) is non empty non empty-membered set
RelStr(# the carrier of (f * x), the InternalRel of (f * x) #) is strict RelStr
dom (netmap (x,S)) is Element of K32( the carrier of x)
K32( the carrier of x) is non empty non empty-membered set
(netmap ((f * x),T)) . FX is Element of the carrier of T
(netmap (x,S)) . FX is set
f . ((netmap (x,S)) . FX) is set
(netmap ((f * x),T)) . fx is Element of the carrier of T
(netmap (x,S)) . fx is set
f . ((netmap (x,S)) . fx) is set
[FX,fx] is Element of K33( the carrier of (f * x), the carrier of (f * x))
{FX,fx} is non empty set
{FX} is non empty set
{{FX,fx},{FX}} is non empty set
b is Element of the carrier of x
ww is Element of the carrier of x
(netmap (x,S)) . b is Element of the carrier of S
(netmap (x,S)) . ww is Element of the carrier of S
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total monotone Element of K32(K33( the carrier of S, the carrier of T))
x is non empty monotone NetStr over S
f * x is non empty strict NetStr over T
S is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
K32( the carrier of S) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is non empty directed Element of K32( the carrier of S)
f .: x is non empty Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"\/" ((f .: x),T) is Element of the carrier of T
"\/" (x,S) is Element of the carrier of S
f . ("\/" (x,S)) is Element of the carrier of T
(S,x) is non empty reflexive transitive strict directed monotone eventually-directed NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 x is Relation-like x -defined x -valued Element of K32(K33(x,x))
K33(x,x) is non empty set
K32(K33(x,x)) is non empty non empty-membered set
the InternalRel of S /\ K33(x,x) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | x is non empty Relation-like x -defined the carrier of S -valued Function-like V28(x) quasi_total Element of K32(K33(x, the carrier of S))
K33(x, the carrier of S) is non empty set
K32(K33(x, the carrier of S)) is non empty non empty-membered set
NetStr(# x,( the InternalRel of S |_2 x),((id the carrier of S) | x) #) is non empty transitive strict directed NetStr over S
lim_inf (S,x) is Element of the carrier of S
the carrier of (S,x) is non empty set
{ ("/\" ( { ((S,x) . b2) where b2 is Element of the carrier of (S,x) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,x) : verum } is set
"\/" ( { ("/\" ( { ((S,x) . b2) where b2 is Element of the carrier of (S,x) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,x) : verum } ,S) is Element of the carrier of S
f * (S,x) is non empty reflexive transitive strict directed NetStr over T
lim_inf (f * (S,x)) is Element of the carrier of T
the carrier of (f * (S,x)) is non empty set
{ ("/\" ( { ((f * (S,x)) . b2) where b2 is Element of the carrier of (f * (S,x)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,x)) : verum } is set
"\/" ( { ("/\" ( { ((f * (S,x)) . b2) where b2 is Element of the carrier of (f * (S,x)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,x)) : verum } ,T) is Element of the carrier of T
FW is non empty reflexive transitive directed monotone eventually-directed NetStr over T
sup FW is Element of the carrier of T
the mapping of FW is non empty Relation-like the carrier of FW -defined the carrier of T -valued Function-like V28( the carrier of FW) quasi_total Element of K32(K33( the carrier of FW, the carrier of T))
the carrier of FW is non empty set
K33( the carrier of FW, the carrier of T) is non empty set
K32(K33( the carrier of FW, the carrier of T)) is non empty non empty-membered set
\\/ ( the mapping of FW,T) is Element of the carrier of T
f * ((id the carrier of S) | x) is non empty Relation-like x -defined the carrier of T -valued Function-like V28(x) quasi_total Element of K32(K33(x, the carrier of T))
K33(x, the carrier of T) is non empty set
K32(K33(x, the carrier of T)) is non empty non empty-membered set
\\/ ((f * ((id the carrier of S) | x)),T) is Element of the carrier of T
rng (f * ((id the carrier of S) | x)) is Element of K32( the carrier of T)
"\/" ((rng (f * ((id the carrier of S) | x))),T) is Element of the carrier of T
id x is non empty Relation-like x -defined x -valued Function-like one-to-one V28(x) quasi_total Element of K32(K33(x,x))
f * (id x) is Relation-like x -defined the carrier of T -valued Function-like Element of K32(K33(x, the carrier of T))
rng (f * (id x)) is Element of K32( the carrier of T)
f | x is non empty Relation-like x -defined the carrier of T -valued Function-like V28(x) quasi_total Element of K32(K33(x, the carrier of T))
rng (f | x) is Element of K32( the carrier of T)
S is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
K32( the carrier of S) is non empty non empty-membered set
x is Element of K32( the carrier of S)
FW is non empty directed Element of K32( the carrier of S)
f .: FW is non empty Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
"\/" ((f .: FW),T) is Element of the carrier of T
"\/" (FW,S) is Element of the carrier of S
f . ("\/" (FW,S)) is Element of the carrier of T
(S,FW) is non empty reflexive transitive strict directed monotone eventually-directed NetStr over S
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K32(K33( the carrier of S, the carrier of S))
K33( the carrier of S, the carrier of S) is non empty set
K32(K33( the carrier of S, the carrier of S)) is non empty non empty-membered set
the InternalRel of S |_2 FW is Relation-like FW -defined FW -valued Element of K32(K33(FW,FW))
K33(FW,FW) is non empty set
K32(K33(FW,FW)) is non empty non empty-membered set
the InternalRel of S /\ K33(FW,FW) is set
id the carrier of S is non empty Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of S))
(id the carrier of S) | FW is non empty Relation-like FW -defined the carrier of S -valued Function-like V28(FW) quasi_total Element of K32(K33(FW, the carrier of S))
K33(FW, the carrier of S) is non empty set
K32(K33(FW, the carrier of S)) is non empty non empty-membered set
NetStr(# FW,( the InternalRel of S |_2 FW),((id the carrier of S) | FW) #) is non empty transitive strict directed NetStr over S
lim_inf (S,FW) is Element of the carrier of S
the carrier of (S,FW) is non empty set
{ ("/\" ( { ((S,FW) . b2) where b2 is Element of the carrier of (S,FW) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,FW) : verum } is set
"\/" ( { ("/\" ( { ((S,FW) . b2) where b2 is Element of the carrier of (S,FW) : b1 <= b2 } ,S)) where b1 is Element of the carrier of (S,FW) : verum } ,S) is Element of the carrier of S
f * (S,FW) is non empty reflexive transitive strict directed NetStr over T
lim_inf (f * (S,FW)) is Element of the carrier of T
the carrier of (f * (S,FW)) is non empty set
{ ("/\" ( { ((f * (S,FW)) . b2) where b2 is Element of the carrier of (f * (S,FW)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,FW)) : verum } is set
"\/" ( { ("/\" ( { ((f * (S,FW)) . b2) where b2 is Element of the carrier of (f * (S,FW)) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * (S,FW)) : verum } ,T) is Element of the carrier of T
FX is non empty reflexive transitive directed monotone eventually-directed NetStr over T
sup FX is Element of the carrier of T
the mapping of FX is non empty Relation-like the carrier of FX -defined the carrier of T -valued Function-like V28( the carrier of FX) quasi_total Element of K32(K33( the carrier of FX, the carrier of T))
the carrier of FX is non empty set
K33( the carrier of FX, the carrier of T) is non empty set
K32(K33( the carrier of FX, the carrier of T)) is non empty non empty-membered set
\\/ ( the mapping of FX,T) is Element of the carrier of T
f * ((id the carrier of S) | FW) is non empty Relation-like FW -defined the carrier of T -valued Function-like V28(FW) quasi_total Element of K32(K33(FW, the carrier of T))
K33(FW, the carrier of T) is non empty set
K32(K33(FW, the carrier of T)) is non empty non empty-membered set
\\/ ((f * ((id the carrier of S) | FW)),T) is Element of the carrier of T
rng (f * ((id the carrier of S) | FW)) is Element of K32( the carrier of T)
"\/" ((rng (f * ((id the carrier of S) | FW))),T) is Element of the carrier of T
id FW is non empty Relation-like FW -defined FW -valued Function-like one-to-one V28(FW) quasi_total Element of K32(K33(FW,FW))
f * (id FW) is Relation-like FW -defined the carrier of T -valued Function-like Element of K32(K33(FW, the carrier of T))
rng (f * (id FW)) is Element of K32( the carrier of T)
f | FW is non empty Relation-like FW -defined the carrier of T -valued Function-like V28(FW) quasi_total Element of K32(K33(FW, the carrier of T))
rng (f | FW) is Element of K32( the carrier of T)
S is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is non empty transitive directed NetStr over S
the carrier of x is non empty set
f * x is non empty transitive strict directed NetStr over T
the carrier of (f * x) is non empty set
FW is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : FW <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : FW <= b1 } ,S) is Element of the carrier of S
f . ("/\" ( { (x . b1) where b1 is Element of the carrier of x : FW <= b1 } ,S)) is Element of the carrier of T
FX is Element of the carrier of (f * x)
{ ((f * x) . b1) where b1 is Element of the carrier of (f * x) : FX <= b1 } is set
"/\" ( { ((f * x) . b1) where b1 is Element of the carrier of (f * x) : FX <= b1 } ,T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
the InternalRel of (f * x) is Relation-like the carrier of (f * x) -defined the carrier of (f * x) -valued Element of K32(K33( the carrier of (f * x), the carrier of (f * x)))
K33( the carrier of (f * x), the carrier of (f * x)) is non empty set
K32(K33( the carrier of (f * x), the carrier of (f * x))) is non empty non empty-membered set
RelStr(# the carrier of (f * x), the InternalRel of (f * x) #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K32(K33( the carrier of x, the carrier of x))
K33( the carrier of x, the carrier of x) is non empty set
K32(K33( the carrier of x, the carrier of x)) is non empty non empty-membered set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
the mapping of x is non empty Relation-like the carrier of x -defined the carrier of S -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of S))
K33( the carrier of x, the carrier of S) is non empty set
K32(K33( the carrier of x, the carrier of S)) is non empty non empty-membered set
dom the mapping of x is Element of K32( the carrier of x)
K32( the carrier of x) is non empty non empty-membered set
f .: { (x . b1) where b1 is Element of the carrier of x : FW <= b1 } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
fx is set
b is Element of the carrier of (f * x)
(f * x) . b is Element of the carrier of T
the mapping of (f * x) is non empty Relation-like the carrier of (f * x) -defined the carrier of T -valued Function-like V28( the carrier of (f * x)) quasi_total Element of K32(K33( the carrier of (f * x), the carrier of T))
K33( the carrier of (f * x), the carrier of T) is non empty set
K32(K33( the carrier of (f * x), the carrier of T)) is non empty non empty-membered set
the mapping of (f * x) . b is Element of the carrier of T
ww is Element of the carrier of x
[FX,ww] is Element of K33( the carrier of (f * x), the carrier of x)
K33( the carrier of (f * x), the carrier of x) is non empty set
{FX,ww} is non empty set
{FX} is non empty set
{{FX,ww},{FX}} is non empty set
f * the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of T))
K33( the carrier of x, the carrier of T) is non empty set
K32(K33( the carrier of x, the carrier of T)) is non empty non empty-membered set
(f * the mapping of x) . ww is Element of the carrier of T
x . ww is Element of the carrier of S
the mapping of x . ww is Element of the carrier of S
f . (x . ww) is Element of the carrier of T
fx is set
b is set
f . b is set
ww is Element of the carrier of x
x . ww is Element of the carrier of S
the mapping of x . ww is Element of the carrier of S
f * the mapping of x is non empty Relation-like the carrier of x -defined the carrier of T -valued Function-like V28( the carrier of x) quasi_total Element of K32(K33( the carrier of x, the carrier of T))
K33( the carrier of x, the carrier of T) is non empty set
K32(K33( the carrier of x, the carrier of T)) is non empty non empty-membered set
(f * the mapping of x) . ww is Element of the carrier of T
u is Element of the carrier of (f * x)
(f * x) . u is Element of the carrier of T
the mapping of (f * x) is non empty Relation-like the carrier of (f * x) -defined the carrier of T -valued Function-like V28( the carrier of (f * x)) quasi_total Element of K32(K33( the carrier of (f * x), the carrier of T))
K33( the carrier of (f * x), the carrier of T) is non empty set
K32(K33( the carrier of (f * x), the carrier of T)) is non empty non empty-membered set
the mapping of (f * x) . u is Element of the carrier of T
[FW,ww] is Element of K33( the carrier of x, the carrier of x)
{FW,ww} is non empty set
{FW} is non empty set
{{FW,ww},{FW}} is non empty set
b is set
ww is Element of the carrier of x
x . ww is Element of the carrier of S
the mapping of x . ww is Element of the carrier of S
b is Element of K32( the carrier of S)
f .: b is Element of K32( the carrier of T)
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total continuous monotone Element of K32(K33( the carrier of S, the carrier of T))
x is non empty transitive directed NetStr over S
lim_inf x is Element of the carrier of S
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } ,S) is Element of the carrier of S
f . (lim_inf x) is Element of the carrier of T
f * x is non empty transitive strict directed NetStr over T
lim_inf (f * x) is Element of the carrier of T
the carrier of (f * x) is non empty set
{ ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } is set
"\/" ( { ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } ,T) is Element of the carrier of T
[#] T is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
downarrow (lim_inf (f * x)) is non empty directed lower property(S) Element of K32( the carrier of T)
{(lim_inf (f * x))} is non empty Element of K32( the carrier of T)
downarrow {(lim_inf (f * x))} is non empty lower property(S) Element of K32( the carrier of T)
(downarrow (lim_inf (f * x))) ` is closed_under_directed_sups Element of K32( the carrier of T)
the carrier of T \ (downarrow (lim_inf (f * x))) is set
f " ((downarrow (lim_inf (f * x))) `) is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
ww is set
u is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : u <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : u <= b1 } ,S) is Element of the carrier of S
ww is Element of K32( the carrier of S)
u is non empty directed Element of K32( the carrier of S)
w is Element of the carrier of S
h is Element of the carrier of x
{ (x . b1) where b1 is Element of the carrier of x : h <= b1 } is set
"/\" ( { (x . b1) where b1 is Element of the carrier of x : h <= b1 } ,S) is Element of the carrier of S
the InternalRel of (f * x) is Relation-like the carrier of (f * x) -defined the carrier of (f * x) -valued Element of K32(K33( the carrier of (f * x), the carrier of (f * x)))
K33( the carrier of (f * x), the carrier of (f * x)) is non empty set
K32(K33( the carrier of (f * x), the carrier of (f * x))) is non empty non empty-membered set
RelStr(# the carrier of (f * x), the InternalRel of (f * x) #) is strict RelStr
the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of K32(K33( the carrier of x, the carrier of x))
K33( the carrier of x, the carrier of x) is non empty set
K32(K33( the carrier of x, the carrier of x)) is non empty non empty-membered set
RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr
dom f is Element of K32( the carrier of S)
z is Element of the carrier of (f * x)
{ ((f * x) . b1) where b1 is Element of the carrier of (f * x) : z <= b1 } is set
"/\" ( { ((f * x) . b1) where b1 is Element of the carrier of (f * x) : z <= b1 } ,T) is Element of the carrier of T
fD is set
c17 is Element of the carrier of (f * x)
{ ((f * x) . b1) where b1 is Element of the carrier of (f * x) : c17 <= b1 } is set
"/\" ( { ((f * x) . b1) where b1 is Element of the carrier of (f * x) : c17 <= b1 } ,T) is Element of the carrier of T
f . w is Element of the carrier of T
fD is Element of K32( the carrier of T)
"\/" (fD,T) is Element of the carrier of T
f " (downarrow (lim_inf (f * x))) is Element of K32( the carrier of S)
f " ([#] T) is Element of K32( the carrier of S)
(f " ([#] T)) \ (f " (downarrow (lim_inf (f * x)))) is Element of K32( the carrier of S)
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of K32( the carrier of S)
([#] S) \ (f " (downarrow (lim_inf (f * x)))) is Element of K32( the carrier of S)
(f " (downarrow (lim_inf (f * x)))) ` is Element of K32( the carrier of S)
the carrier of S \ (f " (downarrow (lim_inf (f * x)))) is set
(f " ((downarrow (lim_inf (f * x))) `)) ` is Element of K32( the carrier of S)
the carrier of S \ (f " ((downarrow (lim_inf (f * x))) `)) is set
(f " ((downarrow (lim_inf (f * x))) `)) /\ ((f " ((downarrow (lim_inf (f * x))) `)) `) is Element of K32( the carrier of S)
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is Element of the carrier of S
f is Element of K32( the carrier of S)
waybelow T is non empty directed lower Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : b1 is_way_below T } is set
"\/" ((waybelow T),S) is Element of the carrier of S
(waybelow T) /\ f is Element of K32( the carrier of S)
x is set
FW is Element of the carrier of S
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
T is Element of the carrier of S
wayabove T is upper Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ b1 where b1 is Element of the carrier of S : T is_way_below b1 } is set
x is non empty directed Element of K32( the carrier of S)
"\/" (x,S) is Element of the carrier of S
FW is Element of the carrier of S
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
K32(K32( the carrier of S)) is non empty non empty-membered set
T is Element of the carrier of S
{ (wayabove b1) where b1 is Element of the carrier of S : b1 is_way_below T } is set
bool the carrier of S is non empty non empty-membered Element of K32(K32( the carrier of S))
x is set
FW is Element of the carrier of S
wayabove FW is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : FW is_way_below b1 } is set
x is Element of K32(K32( the carrier of S))
FW is Element of K32( the carrier of S)
FX is Element of the carrier of S
wayabove FX is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : FX is_way_below b1 } is set
FW is set
FX is Element of the carrier of S
wayabove FX is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : FX is_way_below b1 } is set
Intersect x is Element of K32( the carrier of S)
FW is Element of K32( the carrier of S)
FX is Element of the carrier of S
wayabove FX is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : FX is_way_below b1 } is set
fx is upper Element of K32( the carrier of S)
uparrow FX is non empty filtered upper Element of K32( the carrier of S)
{FX} is non empty Element of K32( the carrier of S)
uparrow {FX} is non empty upper Element of K32( the carrier of S)
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
{ (wayabove b1) where b1 is Element of the carrier of S : verum } is set
K32( the carrier of S) is non empty non empty-membered set
K32(K32( the carrier of S)) is non empty non empty-membered set
the topology of S is non empty Element of K32(K32( the carrier of S))
f is set
x is Element of the carrier of S
wayabove x is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : x is_way_below b1 } is set
f is Element of K32(K32( the carrier of S))
x is Element of the carrier of S
FW is Element of the carrier of S
{ (wayabove b1) where b1 is Element of the carrier of S : b1 is_way_below FW } is set
FX is x -quasi_basis open Element of K32(K32( the carrier of S))
fx is set
b is Element of the carrier of S
wayabove b is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : b is_way_below b1 } is set
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
K32( the carrier of S) is non empty non empty-membered set
T is Element of K32( the carrier of S)
Int T is open Element of K32( the carrier of S)
{ (wayabove b1) where b1 is Element of the carrier of S : wayabove b1 c= T } is set
union { (wayabove b1) where b1 is Element of the carrier of S : wayabove b1 c= T } is set
{ (wayabove b1) where b1 is Element of the carrier of S : verum } is set
{ b1 where b1 is Element of K32( the carrier of S) : ( b1 in { (wayabove b1) where b2 is Element of the carrier of S : verum } & b1 c= T ) } is set
FX is set
fx is Element of K32( the carrier of S)
b is Element of the carrier of S
wayabove b is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : b is_way_below b1 } is set
FX is set
fx is Element of the carrier of S
wayabove fx is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : fx is_way_below b1 } is set
K32(K32( the carrier of S)) is non empty non empty-membered set
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
[#] T is non empty non proper open closed dense non boundary directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
x is Element of K32( the carrier of T)
K32( the carrier of S) is non empty non empty-membered set
f " x is Element of K32( the carrier of S)
FX is Element of K32( the carrier of S)
Int FX is open Element of K32( the carrier of S)
fx is set
b is Element of the carrier of S
f . b is Element of the carrier of T
ww is Element of the carrier of T
u is Element of the carrier of T
w is Element of the carrier of S
f . w is Element of the carrier of T
wayabove w is upper Element of K32( the carrier of S)
{ b1 where b1 is Element of the carrier of S : w is_way_below b1 } is set
f .: (wayabove w) is Element of K32( the carrier of T)
h is set
dom f is Element of K32( the carrier of S)
z is set
f . z is set
z is Element of the carrier of S
f . z is Element of the carrier of T
f " (f .: (wayabove w)) is Element of K32( the carrier of S)
{ (wayabove b1) where b1 is Element of the carrier of S : wayabove b1 c= FX } is set
union { (wayabove b1) where b1 is Element of the carrier of S : wayabove b1 c= FX } is set
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
FW is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of FW is non empty set
FX is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of FX is non empty set
K33( the carrier of FW, the carrier of FX) is non empty set
K32(K33( the carrier of FW, the carrier of FX)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is non empty transitive directed NetStr over S
lim_inf x is Element of the carrier of S
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } ,S) is Element of the carrier of S
f . (lim_inf x) is Element of the carrier of T
f * x is non empty transitive strict directed NetStr over T
lim_inf (f * x) is Element of the carrier of T
the carrier of (f * x) is non empty set
{ ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } is set
"\/" ( { ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } ,T) is Element of the carrier of T
fx is non empty Relation-like the carrier of FW -defined the carrier of FX -valued Function-like V28( the carrier of FW) quasi_total Element of K32(K33( the carrier of FW, the carrier of FX))
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is non empty transitive directed NetStr over S
lim_inf x is Element of the carrier of S
the carrier of x is non empty set
{ ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } is set
"\/" ( { ("/\" ( { (x . b2) where b2 is Element of the carrier of x : b1 <= b2 } ,S)) where b1 is Element of the carrier of x : verum } ,S) is Element of the carrier of S
f . (lim_inf x) is Element of the carrier of T
f * x is non empty transitive strict directed NetStr over T
lim_inf (f * x) is Element of the carrier of T
the carrier of (f * x) is non empty set
{ ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } is set
"\/" ( { ("/\" ( { ((f * x) . b2) where b2 is Element of the carrier of (f * x) : b1 <= b2 } ,T)) where b1 is Element of the carrier of (f * x) : verum } ,T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
FW is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
b is Element of the carrier of S
FX is Element of the carrier of S
fx is Element of the carrier of T
f . b is Element of the carrier of T
f . FX is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
FW is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
b is Element of the carrier of S
FX is Element of the carrier of S
fx is Element of the carrier of T
f . b is Element of the carrier of T
f . FX is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete satisfying_axiom_of_approximation continuous Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
CompactSublatt T is strict full SubRelStr of T
the carrier of (CompactSublatt T) is set
CompactSublatt S is strict full SubRelStr of S
the carrier of (CompactSublatt S) is set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
FW is Element of the carrier of T
FX is Element of the carrier of S
f . FX is Element of the carrier of T
fx is Element of the carrier of S
b is Element of the carrier of S
f . b is Element of the carrier of T
FX is Element of the carrier of S
f . FX is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
CompactSublatt T is strict full SubRelStr of T
the carrier of (CompactSublatt T) is set
CompactSublatt S is strict full SubRelStr of S
the carrier of (CompactSublatt S) is set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
FW is Element of the carrier of T
FX is Element of the carrier of T
fx is Element of the carrier of S
f . fx is Element of the carrier of T
b is Element of the carrier of S
f . b is Element of the carrier of T
FX is Element of the carrier of S
f . FX is Element of the carrier of T
fx is Element of the carrier of T
b is Element of the carrier of S
f . b is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } ,T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
{ (f . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
{ b1 where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is set
f .: { b1 where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is Element of K32( the carrier of T)
compactbelow x is Element of K32( the carrier of S)
f .: (compactbelow x) is Element of K32( the carrier of T)
FW is non empty directed Element of K32( the carrier of S)
"\/" (FW,S) is Element of the carrier of S
f . ("\/" (FW,S)) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete RelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
FW is Element of the carrier of S
f . x is Element of the carrier of T
f . FW is Element of the carrier of T
compactbelow x is Element of K32( the carrier of S)
K32( the carrier of S) is non empty non empty-membered set
compactbelow FW is Element of K32( the carrier of S)
{ (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } ,T) is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : ( b1 <= FW & b1 is compact ) } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : ( b1 <= FW & b1 is compact ) } ,T) is Element of the carrier of T
dom f is Element of K32( the carrier of S)
{ H1(b1) where b1 is Element of the carrier of S : S1[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S1[b1] } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
{ (f . H1(b1)) where b1 is Element of the carrier of S : S1[b1] } is set
f .: (compactbelow x) is Element of K32( the carrier of T)
"\/" ((f .: (compactbelow x)),T) is Element of the carrier of T
{ H1(b1) where b1 is Element of the carrier of S : S2[b1] } is set
f .: { H1(b1) where b1 is Element of the carrier of S : S2[b1] } is Element of K32( the carrier of T)
{ (f . H1(b1)) where b1 is Element of the carrier of S : S2[b1] } is set
f .: (compactbelow FW) is Element of K32( the carrier of T)
"\/" ((f .: (compactbelow FW)),T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } ,T) is Element of the carrier of T
b is set
ww is Element of the carrier of S
f . ww is Element of the carrier of T
b is Element of the carrier of T
ww is Element of the carrier of S
f . ww is Element of the carrier of T
b is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
CompactSublatt T is strict full SubRelStr of T
the carrier of (CompactSublatt T) is set
CompactSublatt S is strict full SubRelStr of S
the carrier of (CompactSublatt S) is set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
FW is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
b is Element of the carrier of S
FX is Element of the carrier of S
fx is Element of the carrier of T
f . b is Element of the carrier of T
f . FX is Element of the carrier of T
FW is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
FX is Element of the carrier of S
f . FX is Element of the carrier of T
FW is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
b is Element of the carrier of S
FX is Element of the carrier of S
fx is Element of the carrier of T
f . b is Element of the carrier of T
f . FX is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded up-complete /\-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : ( b1 <= x & b1 is compact ) } ,T) is Element of the carrier of T
x is Element of the carrier of S
f . x is Element of the carrier of T
{ (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } is set
"\/" ( { (f . b1) where b1 is Element of the carrier of S : b1 is_way_below x } ,T) is Element of the carrier of T
S is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
the carrier of S is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
the carrier of T is non empty set
K33( the carrier of S, the carrier of T) is non empty set
K32(K33( the carrier of S, the carrier of T)) is non empty non empty-membered set
f is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V28( the carrier of S) quasi_total Element of K32(K33( the carrier of S, the carrier of T))