:: WAYBEL24 semantic presentation

K92() is Element of bool K88()

K88() is set

bool K88() is non empty set

K47() is set

bool K47() is non empty set

bool K92() is non empty set

K235() is TopStruct

the carrier of K235() is set

K89() is set

K90() is set

K91() is set

[:K88(),K88():] is Relation-like set

bool [:K88(),K88():] is non empty set

K391() is non empty V104() L9()

the carrier of K391() is non empty set

<REAL,+> is non empty V104() V126() V127() V128() V130() left-invertible right-invertible V182() left-cancelable right-cancelable V185() L9()

K397() is non empty V104() V128() V130() left-cancelable right-cancelable V185() SubStr of <REAL,+>

<NAT,+> is non empty V104() V126() V128() V130() left-cancelable right-cancelable V185() uniquely-decomposable SubStr of K397()

<REAL,*> is non empty V104() V126() V128() V130() L9()

<NAT,*> is non empty V104() V126() V128() V130() uniquely-decomposable SubStr of <REAL,*>

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

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

1 is non empty set

{{},1} is non empty set

[:1,1:] is non empty Relation-like set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty Relation-like set

bool [:[:1,1:],1:] is non empty set

S is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima Scott non void TopRelStr

T is non empty TopSpace-like reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima Scott non void TopRelStr

SCMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of MonMaps (S,T)

MonMaps (S,T) is non empty strict reflexive transitive antisymmetric full non void SubRelStr of T |^ the carrier of S

the carrier of S is non empty set

T |^ the carrier of S is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of (SCMaps (S,T)) is non empty set

bool the carrier of (SCMaps (S,T)) is non empty set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

Sm is Element of bool the carrier of (SCMaps (S,T))

"\/" (Sm,(SCMaps (S,T))) is Element of the carrier of (SCMaps (S,T))

the carrier of (MonMaps (S,T)) is non empty set

S is non empty RelStr

the carrier of S is non empty set

T is non empty reflexive non void RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

SC is Element of the carrier of S

a is Element of the carrier of S

Sm . SC is Element of the carrier of T

Sm . a is Element of the carrier of T

dom Sm is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

T is non empty reflexive non void RelStr

the carrier of T is non empty set

S is non empty RelStr

Sm is Element of the carrier of T

S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

the carrier of S is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the carrier of S --> Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

a is Element of the carrier of S

f is Element of the carrier of S

(S --> Sm) . a is Element of the carrier of T

(S --> Sm) . f is Element of the carrier of T

( the carrier of S --> Sm) . a is Element of the carrier of T

( the carrier of S --> Sm) . f is Element of the carrier of T

S is non empty RelStr

T is non empty reflexive antisymmetric lower-bounded non void RelStr

MonMaps (S,T) is non empty strict reflexive antisymmetric full non void SubRelStr of T |^ the carrier of S

the carrier of S is non empty set

T |^ the carrier of S is non empty strict reflexive antisymmetric non void RelStr

Bottom (MonMaps (S,T)) is Element of the carrier of (MonMaps (S,T))

the carrier of (MonMaps (S,T)) is non empty set

Bottom T is Element of the carrier of T

the carrier of T is non empty set

S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the carrier of S --> (Bottom T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

SC is Element of the carrier of (MonMaps (S,T))

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

the carrier of (T |^ the carrier of S) is non empty set

b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

g9 is Element of the carrier of S

a . g9 is Element of the carrier of T

b9 . g9 is Element of the carrier of T

( the carrier of S --> (Bottom T)) . g9 is Element of the carrier of T

g1 is Element of the carrier of (T |^ the carrier of S)

i is Element of the carrier of (T |^ the carrier of S)

"\/" ({},(MonMaps (S,T))) is Element of the carrier of (MonMaps (S,T))

S is non empty RelStr

T is non empty reflexive antisymmetric upper-bounded non void RelStr

MonMaps (S,T) is non empty strict reflexive antisymmetric full non void SubRelStr of T |^ the carrier of S

the carrier of S is non empty set

T |^ the carrier of S is non empty strict reflexive antisymmetric non void RelStr

Top (MonMaps (S,T)) is Element of the carrier of (MonMaps (S,T))

the carrier of (MonMaps (S,T)) is non empty set

Top T is Element of the carrier of T

the carrier of T is non empty set

S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the carrier of S --> (Top T) is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

SC is Element of the carrier of (MonMaps (S,T))

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

the carrier of (T |^ the carrier of S) is non empty set

b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

g9 is Element of the carrier of S

b9 . g9 is Element of the carrier of T

a . g9 is Element of the carrier of T

( the carrier of S --> (Top T)) . g9 is Element of the carrier of T

i is Element of the carrier of (T |^ the carrier of S)

g1 is Element of the carrier of (T |^ the carrier of S)

"/\" ({},(MonMaps (S,T))) is Element of the carrier of (MonMaps (S,T))

F

the carrier of F

F

dom F

F

the carrier of F

{ F

F

{ (F

T is set

Sm is set

F

SC is Element of the carrier of F

F

T is set

Sm is Element of the carrier of F

F

F

F

the carrier of F

{ F

{ F

S is set

T is Element of the carrier of F

F

S is set

T is Element of the carrier of F

F

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of S is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

SC is Element of the carrier of S

Sm . SC is Element of the carrier of T

downarrow SC is non empty directed lower Element of bool the carrier of S

bool the carrier of S is non empty set

{SC} is non empty Element of bool the carrier of S

downarrow {SC} is non empty lower Element of bool the carrier of S

Sm .: (downarrow SC) is Element of bool the carrier of T

bool the carrier of T is non empty set

"\/" ((Sm .: (downarrow SC)),T) is Element of the carrier of T

a is Element of the carrier of T

dom Sm is non empty Element of bool the carrier of S

"\/" ((downarrow SC),S) is Element of the carrier of S

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of S is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

SC is Element of the carrier of S

Sm . SC is Element of the carrier of T

{ (Sm . b

"\/" ( { (Sm . b

{SC} is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

dom Sm is non empty Element of bool the carrier of S

{ H

Sm .: { H

bool the carrier of T is non empty set

{ (Sm . H

a is Element of the carrier of S

f is Element of the carrier of S

{ H

downarrow SC is non empty directed lower Element of bool the carrier of S

downarrow {SC} is non empty lower Element of bool the carrier of S

{ b

Sm .: (downarrow SC) is Element of bool the carrier of T

"\/" ((Sm .: (downarrow SC)),T) is Element of the carrier of T

"\/" ((downarrow SC),S) is Element of the carrier of S

Sm . ("\/" ((downarrow SC),S)) is Element of the carrier of T

S is RelStr

the carrier of S is set

T is non empty RelStr

T |^ the carrier of S is non empty strict RelStr

the carrier of (T |^ the carrier of S) is non empty set

bool the carrier of (T |^ the carrier of S) is non empty set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is Relation-like set

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

Sm is Element of bool the carrier of (T |^ the carrier of S)

"\/" (Sm,(T |^ the carrier of S)) is Element of the carrier of (T |^ the carrier of S)

Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T

a is Relation-like Function-like set

dom a is set

rng a is set

S is non empty RelStr

T is non empty RelStr

[:S,T:] is non empty strict RelStr

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

Sm is non empty RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

curry SC is Relation-like Function-like set

a is Element of the carrier of S

(curry SC) . a is set

the carrier of T is non empty set

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

[: the carrier of S, the carrier of T:] is non empty Relation-like set

Funcs ( the carrier of T, the carrier of Sm) is non empty functional FUNCTION_DOMAIN of the carrier of T, the carrier of Sm

[: the carrier of S,(Funcs ( the carrier of T, the carrier of Sm)):] is non empty Relation-like set

bool [: the carrier of S,(Funcs ( the carrier of T, the carrier of Sm)):] is non empty set

S is non empty RelStr

the carrier of S is non empty set

T is non empty RelStr

the carrier of T is non empty set

Sm is non empty RelStr

[:T,Sm:] is non empty strict RelStr

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

[: the carrier of [:T,Sm:], the carrier of S:] is non empty Relation-like set

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

the carrier of Sm is non empty set

SC is non empty Relation-like the carrier of [:T,Sm:] -defined the carrier of S -valued Function-like V14( the carrier of [:T,Sm:]) quasi_total Element of bool [: the carrier of [:T,Sm:], the carrier of S:]

a is Element of the carrier of T

(T,Sm,S,SC,a) is non empty Relation-like the carrier of Sm -defined the carrier of S -valued Function-like V14( the carrier of Sm) quasi_total Element of bool [: the carrier of Sm, the carrier of S:]

[: the carrier of Sm, the carrier of S:] is non empty Relation-like set

bool [: the carrier of Sm, the carrier of S:] is non empty set

curry SC is Relation-like Function-like set

(curry SC) . a is set

f is Element of the carrier of Sm

(T,Sm,S,SC,a) . f is Element of the carrier of S

SC . (a,f) is set

[a,f] is set

{a,f} is non empty set

{a} is non empty set

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

SC . [a,f] is set

dom SC is non empty Element of bool the carrier of [:T,Sm:]

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

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

[a,f] is Element of the carrier of [:T,Sm:]

S is non empty RelStr

T is non empty RelStr

[:S,T:] is non empty strict RelStr

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

Sm is non empty RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

curry' SC is Relation-like Function-like set

a is Element of the carrier of T

(curry' SC) . a is set

the carrier of S is non empty set

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

Funcs ( the carrier of S, the carrier of Sm) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of Sm

[: the carrier of T,(Funcs ( the carrier of S, the carrier of Sm)):] is non empty Relation-like set

bool [: the carrier of T,(Funcs ( the carrier of S, the carrier of Sm)):] is non empty set

S is non empty RelStr

the carrier of S is non empty set

T is non empty RelStr

the carrier of T is non empty set

Sm is non empty RelStr

[:Sm,T:] is non empty strict RelStr

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

[: the carrier of [:Sm,T:], the carrier of S:] is non empty Relation-like set

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

the carrier of Sm is non empty set

SC is non empty Relation-like the carrier of [:Sm,T:] -defined the carrier of S -valued Function-like V14( the carrier of [:Sm,T:]) quasi_total Element of bool [: the carrier of [:Sm,T:], the carrier of S:]

a is Element of the carrier of T

(Sm,T,S,SC,a) is non empty Relation-like the carrier of Sm -defined the carrier of S -valued Function-like V14( the carrier of Sm) quasi_total Element of bool [: the carrier of Sm, the carrier of S:]

[: the carrier of Sm, the carrier of S:] is non empty Relation-like set

bool [: the carrier of Sm, the carrier of S:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . a is set

f is Element of the carrier of Sm

(Sm,T,S,SC,a) . f is Element of the carrier of S

SC . (f,a) is set

[f,a] is set

{f,a} is non empty set

{f} is non empty set

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

SC . [f,a] is set

dom SC is non empty Element of bool the carrier of [:Sm,T:]

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

[: the carrier of Sm, the carrier of T:] is non empty Relation-like set

[f,a] is Element of the carrier of [:Sm,T:]

S is non empty RelStr

T is non empty RelStr

[:S,T:] is non empty strict RelStr

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

Sm is non empty RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

f is Element of the carrier of T

(S,T,Sm,SC,a) . f is Element of the carrier of Sm

(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . f is set

(S,T,Sm,SC,f) . a is Element of the carrier of Sm

SC . (a,f) is set

[a,f] is set

{a,f} is non empty set

{a} is non empty set

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

SC . [a,f] is set

S is non empty RelStr

the carrier of S is non empty set

T is non empty reflexive non void RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the Element of the carrier of T is Element of the carrier of T

S --> the Element of the carrier of T is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

the carrier of S --> the Element of the carrier of T is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total monotone Element of bool [: the carrier of S, the carrier of T:]

a is Element of the carrier of S

f is Element of the carrier of S

SC . a is set

SC . f is set

[a,f] is Element of the carrier of [:S,S:]

[:S,S:] is non empty strict RelStr

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

{a,f} is non empty set

{a} is non empty set

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

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

b9 is Element of the carrier of T

i is Element of the carrier of T

SC . a is Element of the carrier of T

SC . f is Element of the carrier of T

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

f is Element of the carrier of T

(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . f is set

i is Element of the carrier of T

(S,T,Sm,SC,i) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

(curry' SC) . i is set

b9 is Element of the carrier of S

(S,T,Sm,SC,b9) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

(curry SC) . b9 is set

L is Element of the carrier of S

(S,T,Sm,SC,i) . L is Element of the carrier of Sm

SC . (L,i) is set

[L,i] is set

{L,i} is non empty set

{L} is non empty set

{{L,i},{L}} is non empty set

SC . [L,i] is set

P is Element of the carrier of S

(S,T,Sm,SC,i) . P is Element of the carrier of Sm

SC . (P,i) is set

[P,i] is set

{P,i} is non empty set

{P} is non empty set

{{P,i},{P}} is non empty set

SC . [P,i] is set

[L,i] is Element of the carrier of [:S,T:]

[P,i] is Element of the carrier of [:S,T:]

L is Element of the carrier of T

(S,T,Sm,SC,b9) . L is Element of the carrier of Sm

SC . (b9,L) is set

[b9,L] is set

{b9,L} is non empty set

{b9} is non empty set

{{b9,L},{b9}} is non empty set

SC . [b9,L] is set

P is Element of the carrier of T

(S,T,Sm,SC,b9) . P is Element of the carrier of Sm

SC . (b9,P) is set

[b9,P] is set

{b9,P} is non empty set

{{b9,P},{b9}} is non empty set

SC . [b9,P] is set

[b9,L] is Element of the carrier of [:S,T:]

[b9,P] is Element of the carrier of [:S,T:]

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

f is Element of the carrier of T

(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . f is set

g9 is Element of the carrier of T

L is Element of the carrier of S

(S,T,Sm,SC,f) . L is Element of the carrier of Sm

SC . (L,f) is set

[L,f] is set

{L,f} is non empty set

{L} is non empty set

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

SC . [L,f] is set

P is Element of the carrier of S

(S,T,Sm,SC,f) . P is Element of the carrier of Sm

SC . (P,f) is set

[P,f] is set

{P,f} is non empty set

{P} is non empty set

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

SC . [P,f] is set

[L,g9] is Element of the carrier of [:S,T:]

{L,g9} is non empty set

{{L,g9},{L}} is non empty set

[P,g9] is Element of the carrier of [:S,T:]

{P,g9} is non empty set

{{P,g9},{P}} is non empty set

b9 is Element of the carrier of S

g9 is Element of the carrier of T

(S,T,Sm,SC,a) . g9 is Element of the carrier of Sm

SC . (a,g9) is set

[a,g9] is set

{a,g9} is non empty set

{a} is non empty set

{{a,g9},{a}} is non empty set

SC . [a,g9] is set

L is Element of the carrier of T

(S,T,Sm,SC,a) . L is Element of the carrier of Sm

SC . (a,L) is set

[a,L] is set

{a,L} is non empty set

{{a,L},{a}} is non empty set

SC . [a,L] is set

[b9,g9] is Element of the carrier of [:S,T:]

{b9,g9} is non empty set

{b9} is non empty set

{{b9,g9},{b9}} is non empty set

[b9,L] is Element of the carrier of [:S,T:]

{b9,L} is non empty set

{{b9,L},{b9}} is non empty set

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

the carrier of T is non empty set

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of T

(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

the carrier of S is non empty set

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . a is set

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total antitone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

the carrier of T is non empty set

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

S is non empty reflexive non void RelStr

T is non empty reflexive non void RelStr

[:S,T:] is non empty strict reflexive non void RelStr

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

Sm is non empty reflexive non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total antitone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of T

(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

the carrier of S is non empty set

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . a is set

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of [:S,T:]

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

a `1 is Element of the carrier of S

f `1 is Element of the carrier of S

a `2 is Element of the carrier of T

f `2 is Element of the carrier of T

SC . ((a `1),(f `2)) is set

[(a `1),(f `2)] is set

{(a `1),(f `2)} is non empty set

{(a `1)} is non empty set

{{(a `1),(f `2)},{(a `1)}} is non empty set

SC . [(a `1),(f `2)] is set

(S,T,Sm,SC,(a `1)) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . (a `1) is set

(S,T,Sm,SC,(a `1)) . (f `2) is Element of the carrier of Sm

SC . ((a `1),(a `2)) is set

[(a `1),(a `2)] is set

{(a `1),(a `2)} is non empty set

{{(a `1),(a `2)},{(a `1)}} is non empty set

SC . [(a `1),(a `2)] is set

(S,T,Sm,SC,(a `1)) . (a `2) is Element of the carrier of Sm

[(a `1),(a `2)] is Element of the carrier of [:S,T:]

SC . [(a `1),(a `2)] is Element of the carrier of Sm

[(a `1),(f `2)] is Element of the carrier of [:S,T:]

SC . [(a `1),(f `2)] is Element of the carrier of Sm

SC . ((f `1),(f `2)) is set

[(f `1),(f `2)] is set

{(f `1),(f `2)} is non empty set

{(f `1)} is non empty set

{{(f `1),(f `2)},{(f `1)}} is non empty set

SC . [(f `1),(f `2)] is set

(S,T,Sm,SC,(f `2)) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . (f `2) is set

(S,T,Sm,SC,(f `2)) . (f `1) is Element of the carrier of Sm

(S,T,Sm,SC,(f `2)) . (a `1) is Element of the carrier of Sm

[(f `1),(f `2)] is Element of the carrier of [:S,T:]

SC . [(f `1),(f `2)] is Element of the carrier of Sm

[: the carrier of S, the carrier of T:] is non empty Relation-like set

SC . f is Element of the carrier of Sm

SC . a is Element of the carrier of Sm

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of [:S,T:]

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

a `1 is Element of the carrier of S

f `1 is Element of the carrier of S

a `2 is Element of the carrier of T

f `2 is Element of the carrier of T

SC . ((a `1),(f `2)) is set

[(a `1),(f `2)] is set

{(a `1),(f `2)} is non empty set

{(a `1)} is non empty set

{{(a `1),(f `2)},{(a `1)}} is non empty set

SC . [(a `1),(f `2)] is set

(S,T,Sm,SC,(a `1)) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . (a `1) is set

(S,T,Sm,SC,(a `1)) . (f `2) is Element of the carrier of Sm

SC . ((a `1),(a `2)) is set

[(a `1),(a `2)] is set

{(a `1),(a `2)} is non empty set

{{(a `1),(a `2)},{(a `1)}} is non empty set

SC . [(a `1),(a `2)] is set

(S,T,Sm,SC,(a `1)) . (a `2) is Element of the carrier of Sm

[(a `1),(f `2)] is Element of the carrier of [:S,T:]

SC . [(a `1),(f `2)] is Element of the carrier of Sm

[(a `1),(a `2)] is Element of the carrier of [:S,T:]

SC . [(a `1),(a `2)] is Element of the carrier of Sm

SC . ((f `1),(f `2)) is set

[(f `1),(f `2)] is set

{(f `1),(f `2)} is non empty set

{(f `1)} is non empty set

{{(f `1),(f `2)},{(f `1)}} is non empty set

SC . [(f `1),(f `2)] is set

(S,T,Sm,SC,(f `2)) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . (f `2) is set

(S,T,Sm,SC,(f `2)) . (f `1) is Element of the carrier of Sm

(S,T,Sm,SC,(f `2)) . (a `1) is Element of the carrier of Sm

[(f `1),(f `2)] is Element of the carrier of [:S,T:]

SC . [(f `1),(f `2)] is Element of the carrier of Sm

[: the carrier of S, the carrier of T:] is non empty Relation-like set

SC . f is Element of the carrier of Sm

SC . a is Element of the carrier of Sm

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of T is non empty set

the carrier of S is non empty set

bool the carrier of S is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of T

(S,T,Sm,SC,a) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . a is set

{a} is non empty Element of bool the carrier of T

bool the carrier of T is non empty set

f is Element of bool the carrier of S

(S,T,Sm,SC,a) .: f is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

[:f,{a}:] is Relation-like Element of bool the carrier of [:S,T:]

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

SC .: [:f,{a}:] is Element of bool the carrier of Sm

b9 is set

dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of S

i is set

(S,T,Sm,SC,a) . i is set

[i,a] is set

{i,a} is non empty set

{i} is non empty set

{{i,a},{i}} is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

dom SC is non empty Element of bool the carrier of [:S,T:]

SC . (i,a) is set

SC . [i,a] is set

b9 is set

dom SC is non empty Element of bool the carrier of [:S,T:]

i is set

SC . i is set

g1 is set

g9 is set

[g1,g9] is set

{g1,g9} is non empty set

{g1} is non empty set

{{g1,g9},{g1}} is non empty set

SC . (g1,g9) is set

SC . [g1,g9] is set

dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of S

(S,T,Sm,SC,a) . g1 is set

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

bool the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

{a} is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

f is Element of bool the carrier of T

(S,T,Sm,SC,a) .: f is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

[:{a},f:] is Relation-like Element of bool the carrier of [:S,T:]

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

SC .: [:{a},f:] is Element of bool the carrier of Sm

b9 is set

dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of T

i is set

(S,T,Sm,SC,a) . i is set

[a,i] is set

{a,i} is non empty set

{a} is non empty set

{{a,i},{a}} is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

dom SC is non empty Element of bool the carrier of [:S,T:]

SC . (a,i) is set

SC . [a,i] is set

b9 is set

dom SC is non empty Element of bool the carrier of [:S,T:]

i is set

SC . i is set

g1 is set

g9 is set

[g1,g9] is set

{g1,g9} is non empty set

{g1} is non empty set

{{g1,g9},{g1}} is non empty set

SC . (g1,g9) is set

SC . [g1,g9] is set

dom (S,T,Sm,SC,a) is non empty Element of bool the carrier of T

(S,T,Sm,SC,a) . g9 is set

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

(S,T,Sm,SC,a) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . a is set

f is Element of the carrier of T

(S,T,Sm,SC,f) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . f is set

bool the carrier of T is non empty set

bool the carrier of S is non empty set

{a} is non empty Element of bool the carrier of S

i is Element of bool the carrier of T

b9 is non empty directed Element of bool the carrier of S

"\/" (b9,S) is Element of the carrier of S

g1 is non empty directed Element of bool the carrier of T

[:b9,g1:] is non empty Relation-like directed Element of bool the carrier of [:S,T:]

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

(S,T,Sm,SC,a) .: i is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

SC .: [:b9,g1:] is Element of bool the carrier of Sm

"\/" (((S,T,Sm,SC,a) .: i),Sm) is Element of the carrier of Sm

"\/" (i,T) is Element of the carrier of T

(S,T,Sm,SC,a) . ("\/" (i,T)) is Element of the carrier of Sm

"\/" ((SC .: [:b9,g1:]),Sm) is Element of the carrier of Sm

"\/" ([:b9,g1:],[:S,T:]) is Element of the carrier of [:S,T:]

SC . ("\/" ([:b9,g1:],[:S,T:])) is Element of the carrier of Sm

"\/" (g1,T) is Element of the carrier of T

SC . (("\/" (b9,S)),("\/" (g1,T))) is set

[("\/" (b9,S)),("\/" (g1,T))] is set

{("\/" (b9,S)),("\/" (g1,T))} is non empty set

{("\/" (b9,S))} is non empty set

{{("\/" (b9,S)),("\/" (g1,T))},{("\/" (b9,S))}} is non empty set

SC . [("\/" (b9,S)),("\/" (g1,T))] is set

bool the carrier of S is non empty set

{f} is non empty Element of bool the carrier of T

i is Element of bool the carrier of S

b9 is non empty directed Element of bool the carrier of T

"\/" (b9,T) is Element of the carrier of T

g1 is non empty directed Element of bool the carrier of S

[:g1,b9:] is non empty Relation-like directed Element of bool the carrier of [:S,T:]

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

(S,T,Sm,SC,f) .: i is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

SC .: [:g1,b9:] is Element of bool the carrier of Sm

"\/" (((S,T,Sm,SC,f) .: i),Sm) is Element of the carrier of Sm

"\/" (i,S) is Element of the carrier of S

(S,T,Sm,SC,f) . ("\/" (i,S)) is Element of the carrier of Sm

"\/" ((SC .: [:g1,b9:]),Sm) is Element of the carrier of Sm

"\/" ([:g1,b9:],[:S,T:]) is Element of the carrier of [:S,T:]

SC . ("\/" ([:g1,b9:],[:S,T:])) is Element of the carrier of Sm

"\/" (g1,S) is Element of the carrier of S

SC . (("\/" (g1,S)),("\/" (b9,T))) is set

[("\/" (g1,S)),("\/" (b9,T))] is set

{("\/" (g1,S)),("\/" (b9,T))} is non empty set

{("\/" (g1,S))} is non empty set

{{("\/" (g1,S)),("\/" (b9,T))},{("\/" (g1,S))}} is non empty set

SC . [("\/" (g1,S)),("\/" (b9,T))] is set

S is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

T is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima non void RelStr

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

Sm is non empty reflexive transitive antisymmetric with_suprema with_infima non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

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

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total monotone Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

a is Element of the carrier of S

f is Element of the carrier of T

[a,f] is Element of the carrier of [:S,T:]

{a,f} is non empty set

{a} is non empty set

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

SC . [a,f] is Element of the carrier of Sm

b9 is directed Element of bool the carrier of [:S,T:]

SC .: b9 is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

proj1 b9 is Element of bool the carrier of S

bool the carrier of S is non empty set

proj2 b9 is Element of bool the carrier of T

bool the carrier of T is non empty set

"\/" ((SC .: b9),Sm) is Element of the carrier of Sm

i is set

[i,f] is set

{i,f} is non empty set

{i} is non empty set

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

g9 is set

[a,g9] is set

{a,g9} is non empty set

{{a,g9},{a}} is non empty set

L is Element of the carrier of T

[a,L] is Element of the carrier of [:S,T:]

{a,L} is non empty set

{{a,L},{a}} is non empty set

g1 is Element of the carrier of S

[g1,f] is Element of the carrier of [:S,T:]

{g1,f} is non empty set

{g1} is non empty set

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

P is Element of the carrier of [:S,T:]

[a,L] "\/" [g1,f] is Element of the carrier of [:S,T:]

P "\/" P is Element of the carrier of [:S,T:]

a "\/" g1 is Element of the carrier of S

L "\/" f is Element of the carrier of T

[(a "\/" g1),(L "\/" f)] is Element of the carrier of [:S,T:]

{(a "\/" g1),(L "\/" f)} is non empty set

{(a "\/" g1)} is non empty set

{{(a "\/" g1),(L "\/" f)},{(a "\/" g1)}} is non empty set

SC . [(a "\/" g1),(L "\/" f)] is Element of the carrier of Sm

SC . P is Element of the carrier of Sm

dom SC is non empty Element of bool the carrier of [:S,T:]

S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

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

Sm is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of Sm is non empty set

[: the carrier of [:S,T:], the carrier of Sm:] is non empty Relation-like set

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

the carrier of S is non empty set

the carrier of T is non empty set

SC is non empty Relation-like the carrier of [:S,T:] -defined the carrier of Sm -valued Function-like V14( the carrier of [:S,T:]) quasi_total Element of bool [: the carrier of [:S,T:], the carrier of Sm:]

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

a is Element of bool the carrier of [:S,T:]

b9 is Element of the carrier of S

(S,T,Sm,SC,b9) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . b9 is set

i is Element of the carrier of T

(S,T,Sm,SC,i) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . i is set

f is non empty directed Element of bool the carrier of [:S,T:]

proj1 f is Element of bool the carrier of S

bool the carrier of S is non empty set

proj2 f is Element of bool the carrier of T

bool the carrier of T is non empty set

"\/" ((proj2 f),T) is Element of the carrier of T

(S,T,Sm,SC,("\/" ((proj2 f),T))) is non empty Relation-like the carrier of S -defined the carrier of Sm -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of Sm:]

[: the carrier of S, the carrier of Sm:] is non empty Relation-like set

bool [: the carrier of S, the carrier of Sm:] is non empty set

curry' SC is Relation-like Function-like set

(curry' SC) . ("\/" ((proj2 f),T)) is set

(S,T,Sm,SC,("\/" ((proj2 f),T))) .: (proj1 f) is Element of bool the carrier of Sm

bool the carrier of Sm is non empty set

SC .: f is Element of bool the carrier of Sm

"\/" ((SC .: f),Sm) is Element of the carrier of Sm

"\/" (f,[:S,T:]) is Element of the carrier of [:S,T:]

SC . ("\/" (f,[:S,T:])) is Element of the carrier of Sm

b9 is Element of the carrier of Sm

dom (S,T,Sm,SC,("\/" ((proj2 f),T))) is non empty Element of bool the carrier of S

i is set

(S,T,Sm,SC,("\/" ((proj2 f),T))) . i is set

g1 is Element of the carrier of S

(S,T,Sm,SC,g1) is non empty Relation-like the carrier of T -defined the carrier of Sm -valued Function-like V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of Sm:]

[: the carrier of T, the carrier of Sm:] is non empty Relation-like set

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

curry SC is Relation-like Function-like set

(curry SC) . g1 is set

(S,T,Sm,SC,g1) .: (proj2 f) is Element of bool the carrier of Sm

g9 is Element of the carrier of Sm

dom (S,T,Sm,SC,g1) is non empty Element of bool the carrier of T

L is set

(S,T,Sm,SC,g1) . L is set

P is Element of the carrier of T

SC . (g1,P) is set

[g1,P] is set

{g1,P} is non empty set

{g1} is non empty set

{{g1,P},{g1}} is non empty set

SC . [g1,P] is set

(S,T,Sm,SC,g1) . ("\/" ((proj2 f),T)) is Element of the carrier of Sm

"\/" (((S,T,Sm,SC,g1) .: (proj2 f)),Sm) is Element of the carrier of Sm

"\/" ((proj1 f),S) is Element of the carrier of S

SC . (("\/" ((proj1 f),S)),("\/" ((proj2 f),T))) is set

[("\/" ((proj1 f),S)),("\/" ((proj2 f),T))] is set

{("\/" ((proj1 f),S)),("\/" ((proj2 f),T))} is non empty set

{("\/" ((proj1 f),S))} is non empty set

{{("\/" ((proj1 f),S)),("\/" ((proj2 f),T))},{("\/" ((proj1 f),S))}} is non empty set

SC . [("\/" ((proj1 f),S)),("\/" ((proj2 f),T))] is set

(S,T,Sm,SC,("\/" ((proj2 f),T))) . ("\/" ((proj1 f),S)) is Element of the carrier of Sm

"\/" (((S,T,Sm,SC,("\/" ((proj2 f),T))) .: (proj1 f)),Sm) is Element of the carrier of Sm

S is set

T is non empty RelStr

T |^ S is non empty strict RelStr

the carrier of (T |^ S) is non empty set

the carrier of T is non empty set

[:S, the carrier of T:] is Relation-like set

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

Sm is set

Funcs (S, the carrier of T) is non empty functional FUNCTION_DOMAIN of S, the carrier of T

SC is Relation-like Function-like set

dom SC is set

rng SC is set

S is TopStruct

the carrier of S is set

T is non empty TopRelStr

T |^ the carrier of S is non empty strict RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is Relation-like set

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

the carrier of (T |^ the carrier of S) is non empty set

Sm is set

SC is set

bool the carrier of (T |^ the carrier of S) is non empty set

SC is Element of bool the carrier of (T |^ the carrier of S)

subrelstr SC is strict full SubRelStr of T |^ the carrier of S

a is strict full SubRelStr of T |^ the carrier of S

the carrier of a is set

f is set

b9 is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

i is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

b9 is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

Funcs ( the carrier of S, the carrier of T) is non empty functional FUNCTION_DOMAIN of the carrier of S, the carrier of T

Sm is strict RelStr

the carrier of Sm is set

SC is strict RelStr

the carrier of SC is set

a is set

f is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

a is set

f is Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like TopRelStr

(S,T) is strict RelStr

the carrier of S is non empty set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

the non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:] is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total continuous Element of bool [: the carrier of S, the carrier of T:]

the carrier of (S,T) is set

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like TopRelStr

(S,T) is non empty strict RelStr

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

Sm is Element of the carrier of (S,T)

the carrier of S is non empty set

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like reflexive non void TopRelStr

(S,T) is non empty constituted-Functions strict RelStr

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

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

the carrier of T is non empty set

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

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

Sm is Relation-like Function-like Element of the carrier of (S,T)

SC is Relation-like Function-like Element of the carrier of (S,T)

T |^ the carrier of S is non empty strict reflexive non void RelStr

the carrier of (T |^ the carrier of S) is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

a is Element of the carrier of (T |^ the carrier of S)

f is Element of the carrier of (T |^ the carrier of S)

b9 is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

i is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

g1 is Element of the carrier of S

b9 . g1 is Element of the carrier of T

i . g1 is Element of the carrier of T

Sm . g1 is set

SC . g1 is set

[(Sm . g1),(SC . g1)] is set

{(Sm . g1),(SC . g1)} is non empty set

{(Sm . g1)} is non empty set

{{(Sm . g1),(SC . g1)},{(Sm . g1)}} is non empty set

g9 is Element of the carrier of T

L is Element of the carrier of T

g1 is set

g9 is Element of the carrier of S

b9 . g9 is Element of the carrier of T

i . g9 is Element of the carrier of T

L is Element of the carrier of T

P is Element of the carrier of T

b is Element of the carrier of T

b9 . g1 is set

i9 is Element of the carrier of T

i . g1 is set

[b,i9] is Element of the carrier of [:T,T:]

[:T,T:] is non empty strict reflexive non void RelStr

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

{b,i9} is non empty set

{b} is non empty set

{{b,i9},{b}} is non empty set

S is non empty TopSpace-like TopStruct

the carrier of S is non empty set

T is non empty TopSpace-like reflexive non void TopRelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

(S,T) is non empty constituted-Functions strict RelStr

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

Sm is set

SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like reflexive non void TopRelStr

(S,T) is non empty constituted-Functions strict RelStr

the carrier of S is non empty set

T |^ the carrier of S is non empty strict reflexive non void RelStr

Sm is reflexive full SubRelStr of T |^ the carrier of S

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like transitive TopRelStr

(S,T) is non empty constituted-Functions strict RelStr

the carrier of S is non empty set

T |^ the carrier of S is non empty strict transitive RelStr

Sm is transitive full SubRelStr of T |^ the carrier of S

S is non empty TopSpace-like TopStruct

T is non empty TopSpace-like antisymmetric TopRelStr

(S,T) is non empty constituted-Functions strict RelStr

the carrier of S is non empty set

T |^ the carrier of S is non empty strict antisymmetric RelStr

Sm is antisymmetric full SubRelStr of T |^ the carrier of S

S is set

T is non empty RelStr

T |^ S is non empty strict RelStr

the carrier of (T |^ S) is non empty set

Sm is Element of the carrier of (T |^ S)

S is non empty 1-sorted

the carrier of S is non empty set

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

the carrier of T is non empty set

[: the carrier of S, the carrier of T:] is non empty Relation-like set

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

T |^ the carrier of S is non empty constituted-Functions strict reflexive transitive antisymmetric lower-bounded upper-bounded V250() up-complete /\-complete with_suprema with_infima complete non void RelStr

a is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

Sm is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

SC is non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of T:]

{Sm,SC} is non empty Element of bool (bool [: the carrier of S, the carrier of T:])

bool (bool [: the carrier of S, the carrier of T:]) is non empty set

"\/" ({Sm,SC},(T |^ the carrier of S)) is Relation-like Function-like Element of the carrier of (T |^ the carrier of S)

the carrier of (T |^ the carrier of S) is non empty set

f is Element of the carrier of S

a . f is Element of the carrier of T

Sm . f is Element of the carrier of T

SC . f is Element of the carrier of T

{(Sm . f),(SC . f)} is non empty Element of bool the carrier of T

bool the carrier of T is non empty set

"\/" ({(Sm . f),(SC . f)},T) is Element of the carrier of T

the carrier of S --> T is non empty Relation-like the carrier of S -defined {T} -valued Function-like V14( the carrier of S) quasi_total RelStr-yielding non-Empty reflexive-yielding Element of bool [: the carrier of S,{T}:]

{T} is non empty set

[: the carrier of S,{T}:] is non empty Relation-like