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

the carrier of F

F

dom F

F

the carrier of F

{ F

F

{ (F

T is set

f is set

F

x is Element of the carrier of F

F

T is set

f is Element of the carrier of F

F

F

F

the carrier of F

F

dom F

F

the carrier of F

{ F

F

{ (F

T is set

f is set

F

x is Element of the carrier of F

F

T is set

f is Element of the carrier of F

F

F

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

"\/" ( { ("/\" ( { ((S,T,f) . b

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

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

FW is Element of the carrier of (S,T,f)

{ ((S,T,f) . b

"/\" (H

"/\" (H

{ H

{ H

{ (T "/\" f) where b

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

"\/" ( { ("/\" ( { ((S,T,f) . b

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

"\/" ( { ("/\" ( { ((FW * (S,f,x)) . b

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

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

b is Element of the carrier of (FW * (S,f,x))

{ ((FW * (S,f,x)) . b

"/\" (H

"/\" (H

{ H

{ H

{ ((FW . f) "/\" (FW . x)) where b

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

"\/" ( { ("/\" ( { (T . b

sup T is Element of the carrier of S

{ (T . b

"/\" ( { (T . b

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

"/\" ( { (T . b

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

{ H

\\/ ( 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

"\/" ( { ("/\" ( { ((S,T) . b

"\/" (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

"\/" ( { ("/\" ( { ((S,x,FW) . b

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

"\/" ( { ("/\" ( { ((f * (S,x,FW)) . b

f . FW is Element of the carrier of T

(f . x) "/\" (f . FW) is Element of the carrier of T

F

the carrier of F

F

dom F

F

the carrier of F

F

the carrier of F

{ F

F

{ (F

T is set

f is set

F

x is Element of the carrier of F

F

FW is Element of the carrier of F

F

F

T is set

f is Element of the carrier of F

F

F

x is Element of the carrier of F

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

"\/" ( { (f . b

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

dom f is Element of K32( the carrier of S)

{ H

f .: { H

K32( the carrier of T) is non empty non empty-membered set

{ (f . H

"\/" ((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