:: WAYBEL18 semantic presentation

K108() is non finite countable denumerable Element of K19(K104())

K104() is set

K19(K104()) is non empty set

{} is Relation-like non-empty empty-yielding empty set

the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set

1 is non empty set

{{},1} is non empty set

K103() is non finite countable denumerable set

K19(K103()) is non empty set

K19(K108()) is non empty set

I[01] is non empty strict TopSpace-like TopStruct

the carrier of I[01] is non empty set

K105() is set

K106() is set

K107() is set

K20(K104(),K104()) is Relation-like set

K19(K20(K104(),K104())) is non empty set

K472() is non empty V147() L13()

the carrier of K472() is non empty set

<REAL,+> is non empty V147() V169() V170() V171() V173() left-invertible right-invertible V225() left-cancelable right-cancelable V228() L13()

K478() is non empty V147() V171() V173() left-cancelable right-cancelable V228() SubStr of <REAL,+>

<NAT,+> is non empty V147() V169() V171() V173() left-cancelable right-cancelable V228() uniquely-decomposable SubStr of K478()

<REAL,*> is non empty V147() V169() V171() V173() L13()

<NAT,*> is non empty V147() V169() V171() V173() uniquely-decomposable SubStr of <REAL,*>

K523() is set

{{}} is non empty set

K443({{}}) is M23({{}})

K20(K443({{}}),{{}}) is Relation-like set

K19(K20(K443({{}}),{{}})) is non empty set

PFuncs (K443({{}}),{{}}) is set

K20(1,1) is Relation-like non empty set

K19(K20(1,1)) is non empty set

K20(K20(1,1),1) is Relation-like non empty set

K19(K20(K20(1,1),1)) is non empty set

union {} is set

T is set

K19(T) is non empty set

K19(K19(T)) is non empty set

J is Element of K19(K19(T))

M is Element of K19(K19(T))

M \ {{}} is Element of K19(K19(T))

J \/ {{}} is non empty set

UniCl M is Element of K19(K19(T))

UniCl J is Element of K19(K19(T))

PP is set

f is Element of K19(K19(T))

union f is Element of K19(T)

f \ {{}} is Element of K19(K19(T))

f is set

f is Element of K19(K19(T))

f \/ {{}} is non empty set

f \/ {{}} is non empty set

union (f \/ {{}}) is set

union {{}} is set

(union f) \/ (union {{}}) is set

(union f) \/ {} is set

union f is Element of K19(T)

(union f) \/ (union {{}}) is set

(union f) \/ {} is set

T is TopSpace-like TopStruct

the carrier of T is set

K19( the carrier of T) is non empty set

K19(K19( the carrier of T)) is non empty set

M is Element of K19(K19( the carrier of T))

M \ {{}} is Element of K19(K19( the carrier of T))

J is Element of K19(K19( the carrier of T))

UniCl J is Element of K19(K19( the carrier of T))

UniCl M is Element of K19(K19( the carrier of T))

the topology of T is non empty Element of K19(K19( the carrier of T))

PP is set

T is Relation-like Function-like set

M is set

dom T is set

T . M is set

rng T is set

T is set

the TopSpace-like TopStruct is TopSpace-like TopStruct

T --> the TopSpace-like TopStruct is Relation-like T -defined { the TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the TopSpace-like TopStruct }))

{ the TopSpace-like TopStruct } is non empty set

K20(T,{ the TopSpace-like TopStruct }) is Relation-like set

K19(K20(T,{ the TopSpace-like TopStruct })) is non empty set

J is set

rng (T --> the TopSpace-like TopStruct ) is set

rng (T --> the TopSpace-like TopStruct ) is Element of K19({ the TopSpace-like TopStruct })

K19({ the TopSpace-like TopStruct }) is non empty set

T is set

the non empty TopSpace-like TopStruct is non empty TopSpace-like TopStruct

{ the non empty TopSpace-like TopStruct } is non empty set

K20(T,{ the non empty TopSpace-like TopStruct }) is Relation-like set

K19(K20(T,{ the non empty TopSpace-like TopStruct })) is non empty set

T --> the non empty TopSpace-like TopStruct is Relation-like T -defined { the non empty TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the non empty TopSpace-like TopStruct }))

J is Relation-like T -defined { the non empty TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the non empty TopSpace-like TopStruct }))

PP is set

rng J is set

rng J is Element of K19({ the non empty TopSpace-like TopStruct })

K19({ the non empty TopSpace-like TopStruct }) is non empty set

PP is 1-sorted

rng J is set

rng J is Element of K19({ the non empty TopSpace-like TopStruct })

K19({ the non empty TopSpace-like TopStruct }) is non empty set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding () set

J is Element of T

M . J is set

dom M is Element of K19(T)

K19(T) is non empty set

M . J is 1-sorted

rng M is set

T is set

M is Relation-like T -defined Function-like total 1-sorted-yielding () set

Carrier M is Relation-like T -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

K19((product (Carrier M))) is non empty set

K19(K19((product (Carrier M)))) is non empty set

J is Element of K19(K19((product (Carrier M))))

PP is Element of K19(K19((product (Carrier M))))

f is set

f is with_common_domain Element of K19((product (Carrier M)))

W is TopStruct

the carrier of W is set

K19( the carrier of W) is non empty set

V is set

Q is Element of K19( the carrier of W)

M . V is set

(Carrier M) +* (V,Q) is Relation-like Function-like set

product ((Carrier M) +* (V,Q)) is functional with_common_domain product-like set

f is set

f is with_common_domain Element of K19((product (Carrier M)))

W is TopStruct

the carrier of W is set

K19( the carrier of W) is non empty set

V is set

Q is Element of K19( the carrier of W)

M . V is set

(Carrier M) +* (V,Q) is Relation-like Function-like set

product ((Carrier M) +* (V,Q)) is functional with_common_domain product-like set

T is set

K19(T) is non empty set

K19(K19(T)) is non empty set

M is Element of K19(K19(T))

FinMeetCl M is Element of K19(K19(T))

UniCl (FinMeetCl M) is Element of K19(K19(T))

TopStruct(# T,(UniCl (FinMeetCl M)) #) is strict TopStruct

the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #) is set

the topology of TopStruct(# T,(UniCl (FinMeetCl M)) #) is Element of K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)))

K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)) is non empty set

K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))) is non empty set

PP is Element of K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)))

union PP is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))

PP is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))

f is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))

PP /\ f is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))

T is set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

Carrier M is Relation-like T -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

(T,M) is Element of K19(K19((product (Carrier M))))

K19((product (Carrier M))) is non empty set

K19(K19((product (Carrier M)))) is non empty set

PP is Element of K19(K19((product (Carrier M))))

FinMeetCl PP is Element of K19(K19((product (Carrier M))))

UniCl (FinMeetCl PP) is Element of K19(K19((product (Carrier M))))

TopStruct(# (product (Carrier M)),(UniCl (FinMeetCl PP)) #) is strict TopStruct

f is strict TopStruct

f is strict TopSpace-like TopStruct

the carrier of f is set

K19( the carrier of f) is non empty set

K19(K19( the carrier of f)) is non empty set

rng (Carrier M) is set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

V is set

(Carrier M) . V is set

M . V is set

W is 1-sorted

the carrier of W is set

dom M is Element of K19(T)

rng M is set

Q is non empty 1-sorted

the carrier of Q is non empty set

J is strict TopSpace-like TopStruct

the carrier of J is set

K19( the carrier of J) is non empty set

K19(K19( the carrier of J)) is non empty set

PP is strict TopSpace-like TopStruct

the carrier of PP is set

K19( the carrier of PP) is non empty set

K19(K19( the carrier of PP)) is non empty set

rng (Carrier M) is set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

f is set

(Carrier M) . f is set

M . f is set

f is 1-sorted

the carrier of f is set

dom M is Element of K19(T)

rng M is set

V is non empty 1-sorted

the carrier of V is non empty set

f is non empty TopSpace-like TopStruct

f is non empty TopSpace-like TopStruct

T is set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is strict TopSpace-like TopStruct

Carrier M is Relation-like T -defined Function-like total set

rng (Carrier M) is set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

J is set

(Carrier M) . J is set

M . J is set

PP is 1-sorted

the carrier of PP is set

dom M is Element of K19(T)

rng M is set

f is non empty 1-sorted

the carrier of f is non empty set

the carrier of (T,M) is set

product (Carrier M) is functional with_common_domain product-like set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

J is Element of T

M . J is set

dom M is Element of K19(T)

K19(T) is non empty set

(T,M,J) is TopStruct

rng M is set

T is set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is non empty strict TopSpace-like TopStruct

the carrier of (T,M) is non empty set

Carrier M is Relation-like T -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct

the carrier of (T,M) is non empty set

J is Relation-like Function-like Element of the carrier of (T,M)

PP is Element of T

J . PP is set

(T,M,PP) is non empty TopStruct

the carrier of (T,M,PP) is non empty set

Carrier M is Relation-like T -defined Function-like total set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

(Carrier M) . PP is set

product (Carrier M) is functional with_common_domain product-like set

f is 1-sorted

the carrier of f is set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

Carrier M is Relation-like T -defined Function-like total set

J is Element of T

proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct

the carrier of (T,M) is non empty set

(T,M,J) is non empty TopStruct

the carrier of (T,M,J) is non empty set

K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set

PP is Relation-like Function-like set

dom PP is set

rng PP is set

f is set

f is set

PP . f is set

V is Relation-like Function-like Element of the carrier of (T,M)

PP . V is set

(T,M,V,J) is Element of the carrier of (T,M,J)

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct

the carrier of (T,M) is non empty set

Carrier M is Relation-like T -defined Function-like total set

J is Element of T

(T,M,J) is non empty TopStruct

the carrier of (T,M,J) is non empty set

K19( the carrier of (T,M,J)) is non empty set

(T,M,J) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,J)))

K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set

proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

PP is Element of K19( the carrier of (T,M,J))

(T,M,J) " PP is Element of K19( the carrier of (T,M))

K19( the carrier of (T,M)) is non empty set

(Carrier M) +* (J,PP) is Relation-like Function-like set

product ((Carrier M) +* (J,PP)) is functional with_common_domain product-like set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

dom ((Carrier M) +* (J,PP)) is set

f is set

V is Relation-like Function-like set

dom V is set

W is set

V . W is set

(Carrier M) . W is set

M . W is set

((Carrier M) +* (J,PP)) . J is set

Q is 1-sorted

the carrier of Q is set

((Carrier M) +* (J,PP)) . W is set

dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))

K19((product (Carrier M))) is non empty set

((Carrier M) +* (J,PP)) . J is set

V . J is set

(proj ((Carrier M),J)) . V is set

dom (T,M,J) is non empty Element of K19( the carrier of (T,M))

f is set

dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))

K19((product (Carrier M))) is non empty set

V is Relation-like Function-like set

dom V is set

W is set

V . W is set

((Carrier M) +* (J,PP)) . W is set

(Carrier M) . W is set

(proj ((Carrier M),J)) . f is set

V . J is set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct

J is Element of T

(T,M,J) is non empty TopStruct

(T,M,J) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,J)))

the carrier of (T,M) is non empty set

the carrier of (T,M,J) is non empty set

K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set

Carrier M is Relation-like T -defined Function-like total set

proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

K19( the carrier of (T,M,J)) is non empty set

PP is Element of K19( the carrier of (T,M,J))

(T,M,J) " PP is Element of K19( the carrier of (T,M))

K19( the carrier of (T,M)) is non empty set

f is set

dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))

K19((product (Carrier M))) is non empty set

K19((product (Carrier M))) is non empty set

(T,M) is Element of K19(K19((product (Carrier M))))

K19(K19((product (Carrier M)))) is non empty set

K19(K19( the carrier of (T,M))) is non empty set

the topology of (T,M) is non empty Element of K19(K19( the carrier of (T,M)))

f is with_common_domain Element of K19((product (Carrier M)))

(Carrier M) +* (J,PP) is Relation-like Function-like set

product ((Carrier M) +* (J,PP)) is functional with_common_domain product-like set

[#] (T,M,J) is non empty non proper Element of K19( the carrier of (T,M,J))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

M is non empty set

J is Relation-like M -defined Function-like total 1-sorted-yielding non-Empty () set

(M,J) is non empty strict TopSpace-like constituted-Functions TopStruct

the carrier of (M,J) is non empty set

K20( the carrier of T, the carrier of (M,J)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (M,J))) is non empty set

PP is Relation-like the carrier of T -defined the carrier of (M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J)))

(M,J) is Element of K19(K19((product (Carrier J))))

Carrier J is Relation-like M -defined Function-like total set

product (Carrier J) is functional with_common_domain product-like set

K19((product (Carrier J))) is non empty set

K19(K19((product (Carrier J)))) is non empty set

f is Element of M

(M,J,f) is non empty TopStruct

(M,J,f) is Relation-like the carrier of (M,J) -defined the carrier of (M,J,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,J), the carrier of (M,J,f)))

the carrier of (M,J,f) is non empty set

K20( the carrier of (M,J), the carrier of (M,J,f)) is Relation-like non empty set

K19(K20( the carrier of (M,J), the carrier of (M,J,f))) is non empty set

proj ((Carrier J),f) is Relation-like product (Carrier J) -defined Function-like total set

(M,J,f) * PP is Relation-like the carrier of T -defined the carrier of (M,J,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J,f)))

K20( the carrier of T, the carrier of (M,J,f)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (M,J,f))) is non empty set

K19( the carrier of (M,J)) is non empty set

f is Element of K19( the carrier of (M,J))

PP " f is Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

V is with_common_domain Element of K19((product (Carrier J)))

Q is TopStruct

the carrier of Q is set

K19( the carrier of Q) is non empty set

W is set

x is Element of K19( the carrier of Q)

J . W is set

(Carrier J) +* (W,x) is Relation-like Function-like set

product ((Carrier J) +* (W,x)) is functional with_common_domain product-like set

Q is Element of M

(M,J,Q) is non empty TopStruct

the carrier of (M,J,Q) is non empty set

K19( the carrier of (M,J,Q)) is non empty set

(M,J,Q) is Relation-like the carrier of (M,J) -defined the carrier of (M,J,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,J), the carrier of (M,J,Q)))

K20( the carrier of (M,J), the carrier of (M,J,Q)) is Relation-like non empty set

K19(K20( the carrier of (M,J), the carrier of (M,J,Q))) is non empty set

proj ((Carrier J),Q) is Relation-like product (Carrier J) -defined Function-like total set

(M,J,Q) * PP is Relation-like the carrier of T -defined the carrier of (M,J,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J,Q)))

K20( the carrier of T, the carrier of (M,J,Q)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (M,J,Q))) is non empty set

[#] (M,J,Q) is non empty non proper Element of K19( the carrier of (M,J,Q))

v is Element of K19( the carrier of (M,J,Q))

((M,J,Q) * PP) " v is Element of K19( the carrier of T)

(M,J,Q) " v is Element of K19( the carrier of (M,J))

K19(K19( the carrier of (M,J))) is non empty set

T is non empty set

M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set

(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct

(T,M) is Element of K19(K19((product (Carrier M))))

Carrier M is Relation-like T -defined Function-like total set

product (Carrier M) is functional with_common_domain product-like set

K19((product (Carrier M))) is non empty set

K19(K19((product (Carrier M)))) is non empty set

PP is non empty TopSpace-like TopStruct

the carrier of PP is non empty set

the carrier of (T,M) is non empty set

K20( the carrier of PP, the carrier of (T,M)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M))) is non empty set

f is Relation-like the carrier of PP -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M)))

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K20( the carrier of f, the carrier of (T,M)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M))) is non empty set

V is set

W is Element of T

(T,M,W) is non empty TopStruct

the carrier of (T,M,W) is non empty set

(T,M,W) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,W)))

K20( the carrier of (T,M), the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,W))) is non empty set

proj ((Carrier M),W) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,W) * f is Relation-like the carrier of PP -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,W)))

K20( the carrier of PP, the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,W))) is non empty set

K20( the carrier of f, the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,W))) is non empty set

Q is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

V is Relation-like Function-like set

dom V is set

<:V:> is Relation-like Function-like set

dom <:V:> is set

W is set

Q is set

rng V is set

x is Relation-like Function-like set

dom x is set

Q is set

V . Q is set

v is Element of T

(T,M,v) is non empty TopStruct

the carrier of (T,M,v) is non empty set

K20( the carrier of f, the carrier of (T,M,v)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,v))) is non empty set

W is Relation-like the carrier of f -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,v)))

W | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,v) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,v)))

(T,M,v) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,v)))

K20( the carrier of (T,M), the carrier of (T,M,v)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,v))) is non empty set

proj ((Carrier M),v) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,v) * f is Relation-like the carrier of PP -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,v)))

K20( the carrier of PP, the carrier of (T,M,v)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,v))) is non empty set

V . Q is set

x is Element of T

(T,M,x) is non empty TopStruct

the carrier of (T,M,x) is non empty set

K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set

(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))

K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set

proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))

K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set

Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

W is set

V . W is set

Q is Element of T

(T,M,Q) is non empty TopStruct

the carrier of (T,M,Q) is non empty set

K20( the carrier of f, the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,Q))) is non empty set

x is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

x | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

(T,M,Q) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,Q)))

K20( the carrier of (T,M), the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,Q))) is non empty set

proj ((Carrier M),Q) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,Q) * f is Relation-like the carrier of PP -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,Q)))

K20( the carrier of PP, the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,Q))) is non empty set

rngs V is Relation-like Function-like set

product (rngs V) is functional with_common_domain product-like set

W is set

dom (rngs V) is set

Q is Relation-like Function-like set

dom Q is set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

x is set

Q . x is set

(Carrier M) . x is set

V . x is set

Q is Element of T

(T,M,Q) is non empty TopStruct

the carrier of (T,M,Q) is non empty set

K20( the carrier of f, the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,Q))) is non empty set

(T,M,Q) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,Q)))

K20( the carrier of (T,M), the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,Q))) is non empty set

proj ((Carrier M),Q) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,Q) * f is Relation-like the carrier of PP -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,Q)))

K20( the carrier of PP, the carrier of (T,M,Q)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,Q))) is non empty set

M . x is set

v is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

v | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

v is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

v | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))

(rngs V) . x is set

rng v is non empty Element of K19( the carrier of (T,M,Q))

K19( the carrier of (T,M,Q)) is non empty set

W is 1-sorted

the carrier of W is set

W is set

Q is set

V . Q is set

x is Element of T

(T,M,x) is non empty TopStruct

the carrier of (T,M,x) is non empty set

K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set

(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))

K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set

proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))

K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set

Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

rng V is set

dom Q is non empty Element of K19( the carrier of f)

K19( the carrier of f) is non empty set

rng <:V:> is set

W is Relation-like the carrier of f -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M)))

W | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M)))

dom (W | the carrier of PP) is Element of K19( the carrier of PP)

K19( the carrier of PP) is non empty set

dom W is non empty Element of K19( the carrier of f)

K19( the carrier of f) is non empty set

(dom W) /\ the carrier of PP is Element of K19( the carrier of f)

the carrier of f /\ the carrier of PP is set

dom f is non empty Element of K19( the carrier of PP)

Q is set

(W | the carrier of PP) . Q is set

f . Q is set

rng (W | the carrier of PP) is Element of K19( the carrier of (T,M))

K19( the carrier of (T,M)) is non empty set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

x is Relation-like Function-like set

dom x is set

rng f is non empty Element of K19( the carrier of (T,M))

Q is Relation-like Function-like set

dom Q is set

v is set

Q . v is set

x . v is set

V . v is set

W is Element of T

(T,M,W) is non empty TopStruct

the carrier of (T,M,W) is non empty set

K20( the carrier of f, the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,W))) is non empty set

(T,M,W) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,W)))

K20( the carrier of (T,M), the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,W))) is non empty set

proj ((Carrier M),W) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,W) * f is Relation-like the carrier of PP -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,W)))

K20( the carrier of PP, the carrier of (T,M,W)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,W))) is non empty set

dom (proj ((Carrier M),W)) is with_common_domain Element of K19((product (Carrier M)))

g is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

g | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

g is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

g | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))

<:V:> . Q is set

g . Q is set

((T,M,W) * f) . Q is set

(proj ((Carrier M),W)) . Q is set

K19( the carrier of (T,M)) is non empty set

Q is Relation-like the carrier of f -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M)))

x is Element of K19( the carrier of (T,M))

Q " x is Element of K19( the carrier of f)

Q is with_common_domain Element of K19((product (Carrier M)))

W is TopStruct

the carrier of W is set

K19( the carrier of W) is non empty set

v is set

g is Element of K19( the carrier of W)

M . v is set

(Carrier M) +* (v,g) is Relation-like Function-like set

product ((Carrier M) +* (v,g)) is functional with_common_domain product-like set

V . v is set

x is Element of T

(T,M,x) is non empty TopStruct

the carrier of (T,M,x) is non empty set

K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set

(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))

K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set

proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set

(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))

K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set

K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set

K19( the carrier of (T,M,x)) is non empty set

dom (T,M,x) is non empty Element of K19( the carrier of (T,M))

x9 is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

x9 | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

x9 is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

x9 | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))

dom x9 is non empty Element of K19( the carrier of f)

dom Q is non empty Element of K19( the carrier of f)

ZZ is Element of K19( the carrier of (T,M,x))

(T,M,x) " ZZ is Element of K19( the carrier of (T,M))

x9 " ZZ is Element of K19( the carrier of f)

ZZ is set

Q . ZZ is set

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

z is Relation-like Function-like set

dom z is set

(T,M,x) . (Q . ZZ) is set

z . x is set

x9 . ZZ is set

ZZ is set

Q . ZZ is set

rng Q is non empty Element of K19( the carrier of (T,M))

dom (Carrier M) is Element of K19(T)

K19(T) is non empty set

z is Relation-like Function-like set

dom z is set

dom (proj ((Carrier M),x)) is with_common_domain Element of K19((product (Carrier M)))

(T,M,x) . (Q . ZZ) is set

z . x is set

x9 . ZZ is set

[#] (T,M,x) is non empty non proper Element of K19( the carrier of (T,M,x))

Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M)))

K19(K19( the carrier of (T,M))) is non empty set

T is non empty TopSpace-like TopStruct

M is non empty TopSpace-like SubSpace of T

incl M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of T))

the carrier of M is non empty set

the carrier of T is non empty set

K20( the carrier of M, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of M, the carrier of T)) is non empty set

K20( the carrier of T, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of M)) is non empty set

PP is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of T, the carrier of M))

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K20( the carrier of f, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of M)) is non empty set

f is Relation-like the carrier of f -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of M))

K20( the carrier of f, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of T)) is non empty set

(incl M) * f is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of T))

W is non empty TopSpace-like TopStruct

the carrier of W is non empty set

K20( the carrier of W, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of W, the carrier of M)) is non empty set

K20( the carrier of W, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of W, the carrier of T)) is non empty set

V is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of T))

Q is Relation-like the carrier of W -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of T))

Q | the carrier of f is Relation-like the carrier of f -defined the carrier of W -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of W, the carrier of T))

PP * Q is Relation-like the carrier of W -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of M))

x is Relation-like the carrier of W -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of M))

x | the carrier of f is Relation-like the carrier of f -defined the carrier of W -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of W, the carrier of M))

dom f is non empty Element of K19( the carrier of f)

K19( the carrier of f) is non empty set

Q is set

f . Q is set

x . Q is set

Q . Q is set

V . Q is set

rng f is non empty Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

v is Element of the carrier of T

(incl M) . v is set

PP . v is Element of the carrier of M

dom x is non empty Element of K19( the carrier of W)

K19( the carrier of W) is non empty set

(dom x) /\ the carrier of f is Element of K19( the carrier of W)

the carrier of W /\ the carrier of f is set

T is 1-sorted

the carrier of T is set

M is TopStruct

the carrier of M is set

K20( the carrier of T, the carrier of M) is Relation-like set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of M))

rng J is Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is strict SubSpace of M

T is non empty 1-sorted

the carrier of T is non empty set

M is non empty TopStruct

the carrier of M is non empty set

K20( the carrier of T, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is SubSpace of M

rng J is non empty Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is non empty strict SubSpace of M

T is 1-sorted

the carrier of T is set

M is TopStruct

the carrier of M is set

K20( the carrier of T, the carrier of M) is Relation-like set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is SubSpace of M

rng J is Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is strict SubSpace of M

the carrier of (T,M,J) is set

[#] (M | (rng J)) is non proper Element of K19( the carrier of (M | (rng J)))

the carrier of (M | (rng J)) is set

K19( the carrier of (M | (rng J))) is non empty set

T is 1-sorted

the carrier of T is set

M is non empty TopStruct

the carrier of M is non empty set

K20( the carrier of T, the carrier of M) is Relation-like set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is SubSpace of M

rng J is Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is strict SubSpace of M

the carrier of (T,M,J) is set

K20( the carrier of T, the carrier of (T,M,J)) is Relation-like set

K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set

dom J is Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K20( the carrier of T, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is non empty TopSpace-like SubSpace of M

rng J is non empty Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is non empty strict TopSpace-like SubSpace of M

(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (T,M,J)))

the carrier of (T,M,J) is non empty set

K20( the carrier of T, the carrier of (T,M,J)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set

dom J is non empty Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

K20((dom J),(rng J)) is Relation-like non empty set

K19(K20((dom J),(rng J))) is non empty set

[#] M is non empty non proper closed Element of K19( the carrier of M)

K19( the carrier of (T,M,J)) is non empty set

[#] (T,M,J) is non empty non proper closed Element of K19( the carrier of (T,M,J))

J " ([#] (T,M,J)) is Element of K19( the carrier of T)

the topology of T is non empty Element of K19(K19( the carrier of T))

K19(K19( the carrier of T)) is non empty set

PP is Element of K19( the carrier of (T,M,J))

(T,M,J) " PP is Element of K19( the carrier of T)

the topology of (T,M,J) is non empty Element of K19(K19( the carrier of (T,M,J)))

K19(K19( the carrier of (T,M,J))) is non empty set

the topology of M is non empty Element of K19(K19( the carrier of M))

K19(K19( the carrier of M)) is non empty set

f is Element of K19( the carrier of M)

f /\ ([#] (T,M,J)) is Element of K19( the carrier of (T,M,J))

f is Element of K19( the carrier of M)

J " f is Element of K19( the carrier of T)

(J " f) /\ (J " ([#] (T,M,J))) is Element of K19( the carrier of T)

f /\ ([#] (T,M,J)) is Element of K19( the carrier of (T,M,J))

J " (f /\ ([#] (T,M,J))) is Element of K19( the carrier of T)

[#] (T,M,J) is non empty non proper closed Element of K19( the carrier of (T,M,J))

T is 1-sorted

the carrier of T is set

M is non empty TopStruct

the carrier of M is non empty set

K20( the carrier of T, the carrier of M) is Relation-like set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is SubSpace of M

rng J is Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is strict SubSpace of M

the carrier of (T,M,J) is set

(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of (T,M,J)))

K20( the carrier of T, the carrier of (T,M,J)) is Relation-like set

K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set

rng (T,M,J) is Element of K19( the carrier of (T,M,J))

K19( the carrier of (T,M,J)) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

M is non empty TopSpace-like TopStruct

the carrier of M is non empty set

K20( the carrier of T, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of M)) is non empty set

J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(T,M,J) is non empty TopSpace-like SubSpace of M

rng J is non empty Element of K19( the carrier of M)

K19( the carrier of M) is non empty set

M | (rng J) is non empty strict TopSpace-like SubSpace of M

(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total onto Element of K19(K20( the carrier of T, the carrier of (T,M,J)))

the carrier of (T,M,J) is non empty set

K20( the carrier of T, the carrier of (T,M,J)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set

K20( the carrier of (T,M,J), the carrier of T) is Relation-like non empty set

K19(K20( the carrier of (T,M,J), the carrier of T)) is non empty set

(T,M,J) " is Relation-like the carrier of (T,M,J) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of T))

PP is Relation-like the carrier of (T,M,J) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of T))

K20( the carrier of M, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of M, the carrier of T)) is non empty set

f is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of T))

f | the carrier of (T,M,J) is Relation-like the carrier of M -defined the carrier of (T,M,J) -defined the carrier of M -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of M, the carrier of T))

f * J is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))

K20( the carrier of T, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of T)) is non empty set

f is set

(f * J) . f is set

dom (T,M,J) is non empty Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

dom J is non empty Element of K19( the carrier of T)

J . f is set

f . (J . f) is set

(T,M,J) . f is set

((T,M,J) ") . ((T,M,J) . f) is set

(T,M,J) " is Relation-like Function-like set

((T,M,J) ") . ((T,M,J) . f) is set

dom (f * J) is non empty Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))

K20( the carrier of M, the carrier of M) is Relation-like non empty set

K19(K20( the carrier of M, the carrier of M)) is non empty set

J * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))

f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))

f * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))

(M,M,f) is non empty TopSpace-like SubSpace of M

rng f is non empty Element of K19( the carrier of M)

M | (rng f) is non empty strict TopSpace-like SubSpace of M

the carrier of (M,M,f) is non empty set

incl (M,M,f) is Relation-like the carrier of (M,M,f) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,M,f), the carrier of M))

K20( the carrier of (M,M,f), the carrier of M) is Relation-like non empty set

K19(K20( the carrier of (M,M,f), the carrier of M)) is non empty set

f * (incl (M,M,f)) is Relation-like the carrier of (M,M,f) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,M,f), the carrier of T))

K20( the carrier of (M,M,f), the carrier of T) is Relation-like non empty set

K19(K20( the carrier of (M,M,f), the carrier of T)) is non empty set

dom (f * (incl (M,M,f))) is non empty Element of K19( the carrier of (M,M,f))

K19( the carrier of (M,M,f)) is non empty set

[#] (M,M,f) is non empty non proper closed Element of K19( the carrier of (M,M,f))

rng f is non empty Element of K19( the carrier of T)

dom J is non empty Element of K19( the carrier of T)

W is set

dom f is non empty Element of K19( the carrier of M)

Q is set

f . Q is set

dom f is non empty Element of K19( the carrier of M)

f . Q is set

J . (f . Q) is set

W is Element of the carrier of (M,M,f)

(f * (incl (M,M,f))) . W is Element of the carrier of T

Q is Element of the carrier of (M,M,f)

(f * (incl (M,M,f))) . Q is Element of the carrier of T

dom (incl (M,M,f)) is non empty Element of K19( the carrier of (M,M,f))

v is Element of the carrier of (T,M,J)

PP . v is Element of the carrier of T

f . W is set

x is Element of the carrier of M

(incl (M,M,f)) . x is set

f . ((incl (M,M,f)) . x) is set

Q is Element of the carrier of M

(f * (incl (M,M,f))) . Q is set

(incl (M,M,f)) . Q is set

f . ((incl (M,M,f)) . Q) is set

f . Q is set

W is Element of the carrier of (T,M,J)

PP . W is Element of the carrier of T

dom (incl (M,M,f)) is non empty Element of K19( the carrier of (M,M,f))

rng (f * (incl (M,M,f))) is non empty Element of K19( the carrier of T)

[#] T is non empty non proper closed Element of K19( the carrier of T)

W is set

J . W is set

f . (J . W) is set

(J * f) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

((J * f) * J) . W is set

id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))

J * (id T) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(J * (id T)) . W is set

dom f is non empty Element of K19( the carrier of M)

(incl (M,M,f)) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of T, the carrier of M))

dom ((incl (M,M,f)) * J) is Element of K19( the carrier of T)

(f * (incl (M,M,f))) . (J . W) is set

(f * (incl (M,M,f))) * J is Relation-like the carrier of T -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of T, the carrier of T))

((f * (incl (M,M,f))) * J) . W is set

f * ((incl (M,M,f)) * J) is Relation-like the carrier of T -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of T, the carrier of T))

(f * ((incl (M,M,f)) * J)) . W is set

((incl (M,M,f)) * J) . W is set

f . (((incl (M,M,f)) * J) . W) is set

Q is Element of the carrier of M

(incl (M,M,f)) . Q is set

f . ((incl (M,M,f)) . Q) is set

f . (J . W) is set

(id T) . W is set

K20( the carrier of (T,M,J), the carrier of M) is Relation-like non empty set

K19(K20( the carrier of (T,M,J), the carrier of M)) is non empty set

incl (T,M,J) is Relation-like the carrier of (T,M,J) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of M))

[#] M is non empty non proper closed Element of K19( the carrier of M)

W is Relation-like the carrier of (T,M,J) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of M))

W * (T,M,J) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

dom (W * (T,M,J)) is non empty Element of K19( the carrier of T)

Q is Element of K19( the carrier of M)

J " Q is Element of K19( the carrier of T)

(W * (T,M,J)) " Q is Element of K19( the carrier of T)

x is set

J . x is set

(W * (T,M,J)) . x is set

W . (J . x) is set

Q is Element of the carrier of M

x is set

J . x is set

(W * (T,M,J)) . x is set

W . (J . x) is set

Q is Element of the carrier of M

(f * (incl (M,M,f))) " is Relation-like the carrier of T -defined the carrier of (M,M,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,M,f)))

K20( the carrier of T, the carrier of (M,M,f)) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of (M,M,f))) is non empty set

Q is Element of K19( the carrier of (M,M,f))

((f * (incl (M,M,f))) ") " Q is Element of K19( the carrier of T)

(incl (M,M,f)) .: Q is Element of K19( the carrier of M)

x is set

Q is set

(incl (M,M,f)) . Q is set

v is Element of the carrier of M

(incl (M,M,f)) . v is set

x is set

Q is Element of the carrier of M

(incl (M,M,f)) . x is set

(f * (incl (M,M,f))) .: Q is Element of K19( the carrier of T)

f .: Q is Element of K19( the carrier of T)

the topology of (M,M,f) is non empty Element of K19(K19( the carrier of (M,M,f)))

K19(K19( the carrier of (M,M,f))) is non empty set

the topology of M is non empty Element of K19(K19( the carrier of M))

K19(K19( the carrier of M)) is non empty set

x is Element of K19( the carrier of M)

x /\ ([#] (M,M,f)) is Element of K19( the carrier of (M,M,f))

Q is Element of K19( the carrier of M)

J " Q is Element of K19( the carrier of T)

v is set

J . v is set

f . (J . v) is set

id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))

(id T) . v is set

dom f is non empty Element of K19( the carrier of M)

dom f is non empty Element of K19( the carrier of M)

f . (J . v) is set

J . (f . (J . v)) is set

J . ((id T) . v) is set

v is set

W is set

f . W is set

J . v is set

g is Element of the carrier of (T,M,J)

PP . g is Element of the carrier of T

f . (J . v) is set

(id T) . v is set

x is Element of the carrier of (T,M,J)

PP . x is Element of the carrier of T

(W * (T,M,J)) " Q is Element of K19( the carrier of T)

Q is Element of K19( the carrier of M)

f " Q is Element of K19( the carrier of M)

(W * (T,M,J)) " Q is Element of K19( the carrier of T)

J " Q is Element of K19( the carrier of T)

f " (J " Q) is Element of K19( the carrier of M)

(J * f) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

((J * f) * J) * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))

id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))

J * (id T) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))

(J * (id T)) * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))

0 is Relation-like non-empty empty-yielding empty Element of K108()

{0,1} is non empty set

{1} is non empty set

{{},{1},{0,1}} is non empty set

bool {0,1} is non empty Element of K19(K19({0,1}))

K19({0,1}) is non empty set

K19(K19({0,1})) is non empty set

J is set

J is Element of K19(K19({0,1}))

TopStruct(# {0,1},J #) is non empty strict TopStruct

PP is non empty strict TopStruct

the carrier of PP is non empty set

the topology of PP is Element of K19(K19( the carrier of PP))

K19( the carrier of PP) is non empty set

K19(K19( the carrier of PP)) is non empty set

T is strict TopStruct

the carrier of T is set

the topology of T is Element of K19(K19( the carrier of T))

K19( the carrier of T) is non empty set

K19(K19( the carrier of T)) is non empty set

M is strict TopStruct

the carrier of M is set

the topology of M is Element of K19(K19( the carrier of M))

K19( the carrier of M) is non empty set

K19(K19( the carrier of M)) is non empty set

() is strict TopStruct

the carrier of () is set

the topology of () is Element of K19(K19( the carrier of ()))

K19( the carrier of ()) is non empty set

K19(K19( the carrier of ())) is non empty set

M is Element of K19(K19( the carrier of ()))

union M is Element of K19( the carrier of ())

{{1}} is non empty set

{{0,1}} is non empty set

{{},{1}} is non empty set

{} \/ {1} is non empty set

{{1},{0,1}} is non empty set

{1} \/ {0,1} is non empty set

{{},{0,1}} is non empty set

{} \/ {0,1} is non empty set

{{1},{0,1}} is non empty set

{{}} \/ {{1},{0,1}} is non empty set

union {{}} is set

union {{1},{0,1}} is set

(union {{}}) \/ (union {{1},{0,1}}) is set

{} \/ (union {{1},{0,1}}) is set

{1} \/ {0,1} is non empty set

{{1}} is non empty set

{{0,1}} is non empty set

{{},{1}} is non empty set

{{1},{0,1}} is non empty set

{{},{0,1}} is non empty set

M is Element of K19( the carrier of ())

J is Element of K19( the carrier of ())

M /\ J is Element of K19( the carrier of ())

the carrier of () is non empty set

K19( the carrier of ()) is non empty set

J is Element of the carrier of ()

PP is Element of the carrier of ()

the topology of () is non empty Element of K19(K19( the carrier of ()))

K19(K19( the carrier of ())) is non empty set

f is Element of K19( the carrier of ())

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

the carrier of () is non empty set

K20( the carrier of T, the carrier of ()) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of ())) is non empty set

J is Relation-like the carrier of T -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of ()))

[#] () is non empty non proper closed Element of K19( the carrier of ())

K19( the carrier of ()) is non empty set

PP is Element of K19( the carrier of ())

the topology of () is non empty Element of K19(K19( the carrier of ()))

K19(K19( the carrier of ())) is non empty set

J " PP is Element of K19( the carrier of T)

K19( the carrier of T) is non empty set

the topology of T is non empty Element of K19(K19( the carrier of T))

K19(K19( the carrier of T)) is non empty set

f is non empty TopSpace-like TopStruct

the carrier of f is non empty set

K20( the carrier of f, the carrier of ()) is Relation-like non empty set

K19(K20( the carrier of f, the carrier of ())) is non empty set

K19( the carrier of f) is non empty set

the topology of f is non empty Element of K19(K19( the carrier of f))

K19(K19( the carrier of f)) is non empty set

[#] T is non empty non proper closed Element of K19( the carrier of T)

f is Element of K19( the carrier of f)

f /\ ([#] T) is Element of K19( the carrier of T)

V is Element of K19( the carrier of f)

chi (V, the carrier of f) is Relation-like the carrier of f -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f,{{},1}))

K20( the carrier of f,{{},1}) is Relation-like non empty set

K19(K20( the carrier of f,{{},1})) is non empty set

dom (chi (V, the carrier of f)) is non empty Element of K19( the carrier of f)

dom J is non empty Element of K19( the carrier of T)

Q is Relation-like the carrier of f -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of ()))

x is set

J . x is set

Q . x is set

rng J is non empty Element of K19( the carrier of ())

J " {1} is Element of K19( the carrier of T)

Q | the carrier of T is Relation-like the carrier of T -defined the carrier of f -defined the carrier of () -valued Function-like Element of K19(K20( the carrier of f, the carrier of ()))

x is Element of K19( the carrier of ())

Q " x is Element of K19( the carrier of f)

Q is set

Q . Q is set

Q is set

Q . Q is set

dom Q is non empty Element of K19( the carrier of f)

(dom Q) /\ the carrier of T is Element of K19( the carrier of f)

the carrier of f /\ the carrier of T is set

T is set

M is non empty 1-sorted

T --> M is Relation-like T -defined {M} -valued Function-like constant total quasi_total Element of K19(K20(T,{M}))

{M} is non empty set

K20(T,{M}) is Relation-like set

K19(K20(T,{M})) is non empty set

J is 1-sorted

rng (T --> M) is set

rng (T --> M) is Element of K19({M})

K19({M}) is non empty set

T is set

M is TopStruct

T --> M is Relation-like T -defined {M} -valued Function-like constant total quasi_total Element of K19(K20(T,{M}))

{M} is non empty set

K20(T,{M}) is Relation-like set

K19(K20(T,{M})) is non empty set

J is set

rng (T --> M) is set

rng (T --> M) is Element of K19({M})

K19({M}) is non empty set

T is non empty set

M is non empty antisymmetric RelStr

T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty Element of K19(K20(T,{M}))

{M} is non empty set

K20(T,{M}) is Relation-like non empty set

K19(K20(T,{M})) is non empty set

product (T --> M) is non empty strict constituted-Functions RelStr

J is Element of T

(T --> M) . J is non empty RelStr

T is non empty set

M is non empty transitive RelStr

T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty Element of K19(K20(T,{M}))

{M} is non empty set

K20(T,{M}) is Relation-like non empty set

K19(K20(T,{M})) is non empty set

product (T --> M) is non empty strict constituted-Functions RelStr

J is Element of T

(T --> M) . J is non empty RelStr

BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr

the topology of () is non empty Element of K19(K19( the carrier of ()))

the carrier of () is non empty set

K19( the carrier of ()) is non empty set

K19(K19( the carrier of ())) is non empty set

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott TopAugmentation of BoolePoset 1

the topology of T is non empty Element of K19(K19( the carrier of T))

the carrier of T is non empty set

K19( the carrier of T) is non empty set

K19(K19( the carrier of T)) is non empty set

BooleLatt 1 is non empty V100() V107() V114() complete L10()

LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr

the carrier of (BooleLatt 1) is non empty set

LattRel (BooleLatt 1) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)))

K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)) is Relation-like non empty set

K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1))) is non empty set

RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) is strict RelStr

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K19(K20( the carrier of T, the carrier of T))

K20( the carrier of T, the carrier of T) is Relation-like non empty set

K19(K20( the carrier of T, the carrier of T)) is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr

the carrier of (LattPOSet (BooleLatt 1)) is non empty set

bool 1 is non empty Element of K19(K19(1))

K19(1) is non empty set

K19(K19(1)) is non empty set

the carrier of (BoolePoset 1) is non empty set

PP is set

f is Element of K19( the carrier of T)

f is Element of the carrier of T

V is Element of the carrier of T

[f,V] is Element of the carrier of [:T,T:]

[:T,T:] is non empty strict TopSpace-like TopStruct

the carrier of [:T,T:] is non empty set

{f,V} is non empty set

{f} is non empty set

{{f,V},{f}} is non empty set

M is Element of the carrier of (BoolePoset 1)

J is Element of the carrier of (BoolePoset 1)

f is non empty directed Element of K19( the carrier of T)

sup f is Element of the carrier of T

{0} is non empty set

J is Element of the carrier of (BoolePoset 1)

{J} is non empty Element of K19( the carrier of (BoolePoset 1))

K19( the carrier of (BoolePoset 1)) is non empty set

sup {J} is Element of the carrier of (BoolePoset 1)

J is Element of the carrier of (BoolePoset 1)

{J} is non empty Element of K19( the carrier of (BoolePoset 1))

K19( the carrier of (BoolePoset 1)) is non empty set

PP is Element of K19( the carrier of T)

V is set

W is Element of K19( the carrier of T)

{0} is non empty set

T is non empty set

T --> () is Relation-like T -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(T,{()}))

{()} is non empty set

K20(T,{()}) is Relation-like non empty set

K19(K20(T,{()})) is non empty set

Carrier (T --> ()) is Relation-like T -defined Function-like total set

{ (product ((Carrier (T --> ())) +* (b

(T,(T --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct

the carrier of (T,(T --> ())) is non empty set

K19( the carrier of (T,(T --> ()))) is non empty set

K19(K19( the carrier of (T,(T --> ())))) is non empty set

(T,(T --> ())) is Element of K19(K19((product (Carrier (T --> ())))))

product (Carrier (T --> ())) is functional with_common_domain product-like set

K19((product (Carrier (T --> ())))) is non empty set

K19(K19((product (Carrier (T --> ()))))) is non empty set

the topology of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))

bool the carrier of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))

f is set

f is Element of T

(Carrier (T --> ())) +* (f,{1}) is Relation-like Function-like set

product ((Carrier (T --> ())) +* (f,{1})) is functional with_common_domain product-like set

V is set

dom ((Carrier (T --> ())) +* (f,{1})) is set

W is Relation-like Function-like set

dom W is set

dom (Carrier (T --> ())) is Element of K19(T)

K19(T) is non empty set

Q is set

W . Q is set

(Carrier (T --> ())) . Q is set

(T --> ()) . Q is set

x is 1-sorted

the carrier of x is set

((Carrier (T --> ())) +* (f,{1})) . Q is set

f is Element of K19(K19( the carrier of (T,(T --> ()))))

f is Element of K19(K19( the carrier of (T,(T --> ()))))

W is set

Q is Element of T

(Carrier (T --> ())) +* (Q,{1}) is Relation-like Function-like set

product ((Carrier (T --> ())) +* (Q,{1})) is functional with_common_domain product-like set

V is Element of K19( the carrier of ())

(T,(T --> ()),Q) is non empty TopStruct

x is with_common_domain Element of K19((product (Carrier (T --> ()))))

(Carrier (T --> ())) +* (Q,V) is Relation-like Function-like set

product ((Carrier (T --> ())) +* (Q,V)) is functional with_common_domain product-like set

V is Element of K19(K19( the carrier of (T,(T --> ()))))

W is Element of K19(K19( the carrier of (T,(T --> ()))))

FinMeetCl W is Element of K19(K19( the carrier of (T,(T --> ()))))

(FinMeetCl W) \ {{}} is Element of K19(K19( the carrier of (T,(T --> ()))))

Q is open quasi_basis Element of K19(K19( the carrier of (T,(T --> ()))))

FinMeetCl f is Element of K19(K19( the carrier of (T,(T --> ()))))

x is set

Q is Element of K19( the carrier of (T,(T --> ())))

v is Element of K19(K19( the carrier of (T,(T --> ()))))

Intersect v is Element of K19( the carrier of (T,(T --> ())))

v /\ f is Element of K19(K19( the carrier of (T,(T --> ()))))

W is Element of K19(K19( the carrier of (T,(T --> ()))))

Intersect W is Element of K19( the carrier of (T,(T --> ())))

g is set

x is set

ZZ is with_common_domain Element of K19((product (Carrier (T --> ()))))

ZZ is TopStruct

the carrier of ZZ is set

K19( the carrier of ZZ) is non empty set

x9 is set

z is Element of K19( the carrier of ZZ)

(T --> ()) . x9 is set