:: WAYBEL17 semantic presentation

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
F₂() is non empty TopRelStr
the carrier of F₂() is non empty set
F₄() is Relation-like Function-like set
dom F₄() is set
F₁() is non empty TopRelStr
the carrier of F₁() is non empty set
{ F₃(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
F₄() .: { F₃(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
{ (F₄() . F₃(b₁)) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
T is set
f is set
F₄() . f is set
x is Element of the carrier of F₁()
F₃(x) is Element of the carrier of F₂()
T is set
f is Element of the carrier of F₁()
F₃(f) is Element of the carrier of F₂()
F₄() . F₃(f) is set
F₂() is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of F₂() is non empty set
F₄() is Relation-like Function-like set
dom F₄() is set
F₁() is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of F₁() is non empty set
{ F₃(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
F₄() .: { F₃(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
{ (F₄() . F₃(b₁)) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
T is set
f is set
F₄() . f is set
x is Element of the carrier of F₁()
F₃(x) is Element of the carrier of F₂()
T is set
f is Element of the carrier of F₁()
F₃(f) is Element of the carrier of F₂()
F₄() . F₃(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) . b₂) where b₂ is Element of the carrier of (S,T,f) : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of (S,T,f) : verum } is set
"\/" ( { ("/\" ( { ((S,T,f) . b₂) where b₂ is Element of the carrier of (S,T,f) : b₁ <= b₂ } ,S)) where b₁ 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) . b₁) where b₁ is Element of the carrier of (S,T,f) : FW <= b₁ } 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) . b₁) where b₁ is Element of the carrier of (S,T,f) : S₁[b₁,a₁] } is set
FW is Element of the carrier of (S,T,f)
{ ((S,T,f) . b₁) where b₁ is Element of the carrier of (S,T,f) : S₁[b₁,FW] } is set
"/\" (H₁(FW),S) is Element of the carrier of S
"/\" (H₂(FW),S) is Element of the carrier of S
{ H₃(b₁) where b₁ is Element of the carrier of (S,T,f) : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of (S,T,f) : S₂[b₁] } is set
{ (T "/\" f) where b₁ is Element of the carrier of (S,T,f) : S₂[b₁] } 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) . b₂) where b₂ is Element of the carrier of (S,T,f) : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of (S,T,f) : verum } is set
"\/" ( { ("/\" ( { ((S,T,f) . b₂) where b₂ is Element of the carrier of (S,T,f) : b₁ <= b₂ } ,S)) where b₁ 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)) . b₂) where b₂ is Element of the carrier of (FW * (S,f,x)) : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of (FW * (S,f,x)) : verum } is set
"\/" ( { ("/\" ( { ((FW * (S,f,x)) . b₂) where b₂ is Element of the carrier of (FW * (S,f,x)) : b₁ <= b₂ } ,T)) where b₁ 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)) . b₁) where b₁ is Element of the carrier of (FW * (S,f,x)) : b <= b₁ } 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)) . b₁) where b₁ is Element of the carrier of (FW * (S,f,x)) : S₁[b₁,a₁] } is set
b is Element of the carrier of (FW * (S,f,x))
{ ((FW * (S,f,x)) . b₁) where b₁ is Element of the carrier of (FW * (S,f,x)) : S₁[b₁,b] } is set
"/\" (H₁(b),T) is Element of the carrier of T
"/\" (H₂(b),T) is Element of the carrier of T
{ H₃(b₁) where b₁ is Element of the carrier of (FW * (S,f,x)) : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of (FW * (S,f,x)) : S₂[b₁] } is set
{ ((FW . f) "/\" (FW . x)) where b₁ is Element of the carrier of (FW * (S,f,x)) : S₂[b₁] } 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 . b₂) where b₂ is Element of the carrier of T : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of T : verum } is set
"\/" ( { ("/\" ( { (T . b₂) where b₂ is Element of the carrier of T : b₁ <= b₂ } ,S)) where b₁ 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 . b₁) where b₁ is Element of the carrier of T : a₁ <= b₁ } is set
"/\" ( { (T . b₁) where b₁ is Element of the carrier of T : a₁ <= b₁ } ,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 . b₁) where b₁ is Element of the carrier of T : f <= b₁ } is set
"/\" ( { (T . b₁) where b₁ is Element of the carrier of T : f <= b₁ } ,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
{ H₁(b₁) where b₁ is Element of the carrier of T : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Element of the carrier of T : S₁[b₁] } 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) . b₂) where b₂ is Element of the carrier of (S,T) : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of (S,T) : verum } is set
"\/" ( { ("/\" ( { ((S,T) . b₂) where b₂ is Element of the carrier of (S,T) : b₁ <= b₂ } ,S)) where b₁ 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) . b₂) where b₂ is Element of the carrier of (S,x,FW) : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of (S,x,FW) : verum } is set
"\/" ( { ("/\" ( { ((S,x,FW) . b₂) where b₂ is Element of the carrier of (S,x,FW) : b₁ <= b₂ } ,S)) where b₁ 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)) . b₂) where b₂ is Element of the carrier of (f * (S,x,FW)) : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of (f * (S,x,FW)) : verum } is set
"\/" ( { ("/\" ( { ((f * (S,x,FW)) . b₂) where b₂ is Element of the carrier of (f * (S,x,FW)) : b₁ <= b₂ } ,T)) where b₁ 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
F₃() is non empty TopRelStr
the carrier of F₃() is non empty set
F₅() is Relation-like Function-like set
dom F₅() is set
F₁() is non empty TopRelStr
the carrier of F₁() is non empty set
F₂() is non empty TopRelStr
the carrier of F₂() is non empty set
{ F₄(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
F₅() .: { F₄(b₁) where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
{ (F₅() . F₄(b₁)) where b₁ is Element of the carrier of F₂() : P₁[b₁] } is set
T is set
f is set
F₅() . f is set
x is Element of the carrier of F₁()
F₄(x) is Element of the carrier of F₃()
FW is Element of the carrier of F₂()
F₄(FW) is Element of the carrier of F₃()
F₅() . F₄(FW) is set
T is set
f is Element of the carrier of F₂()
F₄(f) is Element of the carrier of F₃()
F₅() . F₄(f) is set
x is Element of the carrier of F₁()
F₄(x) is Element of the carrier of F₃()
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 . b₁) where b₁ is Element of the carrier of S : b₁ is_way_below x } is set
"\/" ( { (f . b₁) where b₁ is Element of the carrier of S : b₁ 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
{ b₁ where b₁ is Element of the carrier of S : b₁ is_way_below x } is set
dom f is Element of K32( the carrier of S)
{ H₁(b₁) where b₁ is Element of the carrier of S : S₁[b₁] } is set
f .: { H₁(b₁) where b₁ is Element of the carrier of S : S₁[b₁] } is Element of K32( the carrier of T)
K32( the carrier of T) is non empty non empty-membered set
{ (f . H₁(b₁)) where b₁ is Element of the carrier of S : S₁[b₁] } 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 carr