:: FUZZY_1 semantic presentation

REAL is non empty V43() V44() V45() V49() V53() set

NAT is V43() V44() V45() V46() V47() V48() V49() Element of K6(REAL)

K6(REAL) is set

COMPLEX is non empty V43() V49() V53() set

{} is empty V43() V44() V45() V46() V47() V48() V49() set

1 is non empty V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V71() V72() Element of NAT

{{},1} is non empty set

NAT is V43() V44() V45() V46() V47() V48() V49() set

K6(NAT) is set

K6(NAT) is set

ExtREAL is non empty V44() set

RAT is non empty V43() V44() V45() V46() V49() V53() set

INT is non empty V43() V44() V45() V46() V47() V49() V53() set

K7(COMPLEX,COMPLEX) is complex-valued set

K6(K7(COMPLEX,COMPLEX)) is set

K7(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(COMPLEX,REAL)) is set

0 is empty V10() V11() V12() ext-real non positive non negative V43() V44() V45() V46() V47() V48() V49() V71() V72() Element of NAT

2 is non empty V10() V11() V12() ext-real positive non negative V43() V44() V45() V46() V47() V48() V71() V72() Element of NAT

[.0,1.] is V43() V44() V45() Element of K6(REAL)

C is set

h is set

chi (C,h) is Relation-like h -defined REAL -valued Function-like total V30(h, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(h,REAL))

K7(h,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(h,REAL)) is set

rng (chi (C,h)) is V43() V44() V45() set

{0,1} is non empty V43() V44() V45() V46() V47() V48() set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

rng (chi (C,C)) is V43() V44() V45() set

C is non empty set

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom g is set

G is set

F is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom F is set

F . G is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is Element of C

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

dom h is Element of K6(C)

K6(C) is set

dom g is Element of K6(C)

K6(C) is set

dom h is Element of K6(C)

F is set

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is Element of C

h . c is V11() V12() ext-real Element of REAL

g . c is V11() V12() ext-real Element of REAL

dom h is Element of K6(C)

K6(C) is set

dom g is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

F is non empty set

K7(F,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(F,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like F -defined REAL -valued [.0,1.] -valued Function-like total V30(F, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(F,REAL))

c is non empty Relation-like F -defined REAL -valued [.0,1.] -valued Function-like total V30(F, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(F,REAL))

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is set

G is set

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

c is set

F is set

G is set

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

F is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom F is Element of K6(C)

K6(C) is set

G is set

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

min ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

c is set

G is Element of C

F . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

min ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

rng h is V43() V44() V45() set

rng g is V43() V44() V45() set

rng F is V43() V44() V45() set

c is set

x is Element of C

F . x is V11() V12() ext-real Element of REAL

h . x is V11() V12() ext-real Element of REAL

g . x is V11() V12() ext-real Element of REAL

min ((h . x),(g . x)) is V11() V12() ext-real Element of REAL

G is non empty V43() V44() V45() V50() closed_interval V81() V82() Element of K6(REAL)

lower_bound G is V11() V12() ext-real Element of REAL

upper_bound G is V11() V12() ext-real Element of REAL

[.(lower_bound G),(upper_bound G).] is V43() V44() V45() Element of K6(REAL)

dom h is Element of K6(C)

dom g is Element of K6(C)

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is Element of C

F . c is V11() V12() ext-real Element of REAL

G . c is V11() V12() ext-real Element of REAL

h . c is V11() V12() ext-real Element of REAL

g . c is V11() V12() ext-real Element of REAL

min ((h . c),(g . c)) is V11() V12() ext-real Element of REAL

dom F is Element of K6(C)

K6(C) is set

dom G is Element of K6(C)

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

F . G is V11() V12() ext-real Element of REAL

min ((F . G),(F . G)) is V11() V12() ext-real Element of REAL

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

x is Element of C

F . x is V11() V12() ext-real Element of REAL

c . x is V11() V12() ext-real Element of REAL

G . x is V11() V12() ext-real Element of REAL

min ((c . x),(G . x)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is set

G is set

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

c is set

F is set

G is set

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

F is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom F is Element of K6(C)

K6(C) is set

G is set

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

max ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

c is set

G is Element of C

F . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

max ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

rng h is V43() V44() V45() set

rng g is V43() V44() V45() set

rng F is V43() V44() V45() set

c is set

x is Element of C

F . x is V11() V12() ext-real Element of REAL

G is non empty V43() V44() V45() V50() closed_interval V81() V82() Element of K6(REAL)

lower_bound G is V11() V12() ext-real Element of REAL

upper_bound G is V11() V12() ext-real Element of REAL

[.(lower_bound G),(upper_bound G).] is V43() V44() V45() Element of K6(REAL)

dom h is Element of K6(C)

h . x is V11() V12() ext-real Element of REAL

g . x is V11() V12() ext-real Element of REAL

max ((h . x),(g . x)) is V11() V12() ext-real Element of REAL

dom g is Element of K6(C)

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is Element of C

F . c is V11() V12() ext-real Element of REAL

G . c is V11() V12() ext-real Element of REAL

h . c is V11() V12() ext-real Element of REAL

g . c is V11() V12() ext-real Element of REAL

max ((h . c),(g . c)) is V11() V12() ext-real Element of REAL

dom F is Element of K6(C)

K6(C) is set

dom G is Element of K6(C)

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

F . G is V11() V12() ext-real Element of REAL

max ((F . G),(F . G)) is V11() V12() ext-real Element of REAL

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

x is Element of C

F . x is V11() V12() ext-real Element of REAL

c . x is V11() V12() ext-real Element of REAL

G . x is V11() V12() ext-real Element of REAL

max ((c . x),(G . x)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom h is Element of K6(C)

K6(C) is set

g is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom g is Element of K6(C)

F is set

F is Element of C

g . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

1 - (h . F) is V11() V12() ext-real Element of REAL

rng h is V43() V44() V45() set

rng g is V43() V44() V45() set

G is set

c is Element of C

g . c is V11() V12() ext-real Element of REAL

F is non empty V43() V44() V45() V50() closed_interval V81() V82() Element of K6(REAL)

lower_bound F is V11() V12() ext-real Element of REAL

upper_bound F is V11() V12() ext-real Element of REAL

[.(lower_bound F),(upper_bound F).] is V43() V44() V45() Element of K6(REAL)

h . c is V11() V12() ext-real Element of REAL

0 + 1 is V11() V12() ext-real Element of REAL

1 + (h . c) is V11() V12() ext-real Element of REAL

1 - (h . c) is V11() V12() ext-real Element of REAL

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

1 - (h . G) is V11() V12() ext-real Element of REAL

dom g is Element of K6(C)

K6(C) is set

dom F is Element of K6(C)

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

F . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

1 - (g . G) is V11() V12() ext-real Element of REAL

1 - (F . G) is V11() V12() ext-real Element of REAL

1 - (1 - (F . G)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

G is non empty set

K7(G,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(G,REAL)) is set

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is Element of C

g . h is V11() V12() ext-real Element of REAL

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F . h is V11() V12() ext-real Element of REAL

min ((g . h),(F . h)) is V11() V12() ext-real Element of REAL

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) . h is V11() V12() ext-real Element of REAL

x is non empty Relation-like G -defined REAL -valued [.0,1.] -valued Function-like total V30(G, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(G,REAL))

c is Element of G

x . c is V11() V12() ext-real Element of REAL

c

c

max ((x . c),(c

(G,x,c

(G,x,c

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

g is non empty set

K7(g,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(g,REAL)) is set

G is non empty set

K7(G,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(G,REAL)) is set

x is non empty set

K7(x,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(x,REAL)) is set

c

K7(c

K6(K7(c

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,h) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like g -defined REAL -valued [.0,1.] -valued Function-like total V30(g, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(g,REAL))

(g,F,F) is non empty Relation-like g -defined REAL -valued [.0,1.] -valued Function-like total V30(g, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(g,REAL))

c is non empty Relation-like G -defined REAL -valued [.0,1.] -valued Function-like total V30(G, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(G,REAL))

(G,c,c) is non empty Relation-like G -defined REAL -valued [.0,1.] -valued Function-like total V30(G, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(G,REAL))

(G,c,c) is non empty Relation-like G -defined REAL -valued [.0,1.] -valued Function-like total V30(G, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(G,REAL))

c

c

(x,c

(x,c

c

c

(c

(c

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g),F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,g,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g),F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,g,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom (C,(C,h,g),F) is Element of K6(C)

K6(C) is set

dom (C,h,(C,g,F)) is Element of K6(C)

G is Element of C

(C,(C,h,g),F) . G is V11() V12() ext-real Element of REAL

(C,h,(C,g,F)) . G is V11() V12() ext-real Element of REAL

(C,h,g) . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

max (((C,h,g) . G),(F . G)) is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

max ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

max ((max ((h . G),(g . G))),(F . G)) is V11() V12() ext-real Element of REAL

max ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

max ((h . G),(max ((g . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

max ((h . G),((C,g,F) . G)) is V11() V12() ext-real Element of REAL

G is Element of C

(C,(C,h,g),F) . G is V11() V12() ext-real Element of REAL

(C,h,(C,g,F)) . G is V11() V12() ext-real Element of REAL

(C,h,g) . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

min (((C,h,g) . G),(F . G)) is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

min ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

min ((min ((h . G),(g . G))),(F . G)) is V11() V12() ext-real Element of REAL

min ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

min ((h . G),(min ((g . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

min ((h . G),((C,g,F) . G)) is V11() V12() ext-real Element of REAL

dom (C,(C,h,g),F) is Element of K6(C)

dom (C,h,(C,g,F)) is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,h,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,h,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom (C,h,(C,h,g)) is Element of K6(C)

K6(C) is set

F is Element of C

(C,h,(C,h,g)) . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

max ((h . F),((C,h,g) . F)) is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

max ((h . F),(min ((h . F),(g . F)))) is V11() V12() ext-real Element of REAL

F is Element of C

(C,h,(C,h,g)) . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

min ((h . F),((C,h,g) . F)) is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

min ((h . F),(max ((h . F),(g . F)))) is V11() V12() ext-real Element of REAL

dom (C,h,(C,h,g)) is Element of K6(C)

dom h is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,g,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g),(C,h,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C,g,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g),(C,h,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom (C,h,(C,g,F)) is Element of K6(C)

K6(C) is set

dom (C,(C,h,g),(C,h,F)) is Element of K6(C)

G is Element of C

(C,h,(C,g,F)) . G is V11() V12() ext-real Element of REAL

(C,(C,h,g),(C,h,F)) . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

min ((h . G),((C,g,F) . G)) is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

max ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

min ((h . G),(max ((g . G),(F . G)))) is V11() V12() ext-real Element of REAL

min ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

min ((h . G),(F . G)) is V11() V12() ext-real Element of REAL

max ((min ((h . G),(g . G))),(min ((h . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,h,g) . G is V11() V12() ext-real Element of REAL

max (((C,h,g) . G),(min ((h . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,h,F) . G is V11() V12() ext-real Element of REAL

max (((C,h,g) . G),((C,h,F) . G)) is V11() V12() ext-real Element of REAL

G is Element of C

(C,h,(C,g,F)) . G is V11() V12() ext-real Element of REAL

(C,(C,h,g),(C,h,F)) . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

max ((h . G),((C,g,F) . G)) is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

min ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

max ((h . G),(min ((g . G),(F . G)))) is V11() V12() ext-real Element of REAL

max ((h . G),(g . G)) is V11() V12() ext-real Element of REAL

max ((h . G),(F . G)) is V11() V12() ext-real Element of REAL

min ((max ((h . G),(g . G))),(max ((h . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,h,g) . G is V11() V12() ext-real Element of REAL

min (((C,h,g) . G),(max ((h . G),(F . G)))) is V11() V12() ext-real Element of REAL

(C,h,F) . G is V11() V12() ext-real Element of REAL

min (((C,h,g) . G),((C,h,F) . G)) is V11() V12() ext-real Element of REAL

dom (C,h,(C,g,F)) is Element of K6(C)

dom (C,(C,h,g),(C,h,F)) is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h),(C,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h),(C,g)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom (C,(C,h,g)) is Element of K6(C)

K6(C) is set

dom (C,(C,h),(C,g)) is Element of K6(C)

F is Element of C

(C,(C,h,g)) . F is V11() V12() ext-real Element of REAL

(C,(C,h),(C,g)) . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

1 - ((C,h,g) . F) is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

1 - (max ((h . F),(g . F))) is V11() V12() ext-real Element of REAL

(h . F) + (g . F) is V11() V12() ext-real Element of REAL

(h . F) - (g . F) is V11() V12() ext-real Element of REAL

abs ((h . F) - (g . F)) is V11() V12() ext-real Element of REAL

((h . F) + (g . F)) + (abs ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

(((h . F) + (g . F)) + (abs ((h . F) - (g . F)))) / 2 is V11() V12() ext-real Element of REAL

1 - ((((h . F) + (g . F)) + (abs ((h . F) - (g . F)))) / 2) is V11() V12() ext-real Element of REAL

(C,h) . F is V11() V12() ext-real Element of REAL

(C,g) . F is V11() V12() ext-real Element of REAL

min (((C,h) . F),((C,g) . F)) is V11() V12() ext-real Element of REAL

1 - (h . F) is V11() V12() ext-real Element of REAL

min ((1 - (h . F)),((C,g) . F)) is V11() V12() ext-real Element of REAL

1 - (g . F) is V11() V12() ext-real Element of REAL

min ((1 - (h . F)),(1 - (g . F))) is V11() V12() ext-real Element of REAL

(1 - (h . F)) + (1 - (g . F)) is V11() V12() ext-real Element of REAL

(1 - (h . F)) - (1 - (g . F)) is V11() V12() ext-real Element of REAL

abs ((1 - (h . F)) - (1 - (g . F))) is V11() V12() ext-real Element of REAL

((1 - (h . F)) + (1 - (g . F))) - (abs ((1 - (h . F)) - (1 - (g . F)))) is V11() V12() ext-real Element of REAL

(((1 - (h . F)) + (1 - (g . F))) - (abs ((1 - (h . F)) - (1 - (g . F))))) / 2 is V11() V12() ext-real Element of REAL

2 - (h . F) is V11() V12() ext-real Element of REAL

(2 - (h . F)) - (g . F) is V11() V12() ext-real Element of REAL

- ((h . F) - (g . F)) is V11() V12() ext-real Element of REAL

abs (- ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

((2 - (h . F)) - (g . F)) - (abs (- ((h . F) - (g . F)))) is V11() V12() ext-real Element of REAL

(((2 - (h . F)) - (g . F)) - (abs (- ((h . F) - (g . F))))) / 2 is V11() V12() ext-real Element of REAL

2 - ((h . F) + (g . F)) is V11() V12() ext-real Element of REAL

(2 - ((h . F) + (g . F))) - (abs ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

((2 - ((h . F) + (g . F))) - (abs ((h . F) - (g . F)))) / 2 is V11() V12() ext-real Element of REAL

F is Element of C

(C,(C,h,g)) . F is V11() V12() ext-real Element of REAL

(C,(C,h),(C,g)) . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

1 - ((C,h,g) . F) is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

1 - (min ((h . F),(g . F))) is V11() V12() ext-real Element of REAL

(h . F) + (g . F) is V11() V12() ext-real Element of REAL

(h . F) - (g . F) is V11() V12() ext-real Element of REAL

abs ((h . F) - (g . F)) is V11() V12() ext-real Element of REAL

((h . F) + (g . F)) - (abs ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

(((h . F) + (g . F)) - (abs ((h . F) - (g . F)))) / 2 is V11() V12() ext-real Element of REAL

1 - ((((h . F) + (g . F)) - (abs ((h . F) - (g . F)))) / 2) is V11() V12() ext-real Element of REAL

(C,h) . F is V11() V12() ext-real Element of REAL

(C,g) . F is V11() V12() ext-real Element of REAL

max (((C,h) . F),((C,g) . F)) is V11() V12() ext-real Element of REAL

1 - (h . F) is V11() V12() ext-real Element of REAL

max ((1 - (h . F)),((C,g) . F)) is V11() V12() ext-real Element of REAL

1 - (g . F) is V11() V12() ext-real Element of REAL

max ((1 - (h . F)),(1 - (g . F))) is V11() V12() ext-real Element of REAL

(1 - (h . F)) + (1 - (g . F)) is V11() V12() ext-real Element of REAL

(1 - (h . F)) - (1 - (g . F)) is V11() V12() ext-real Element of REAL

abs ((1 - (h . F)) - (1 - (g . F))) is V11() V12() ext-real Element of REAL

((1 - (h . F)) + (1 - (g . F))) + (abs ((1 - (h . F)) - (1 - (g . F)))) is V11() V12() ext-real Element of REAL

(((1 - (h . F)) + (1 - (g . F))) + (abs ((1 - (h . F)) - (1 - (g . F))))) / 2 is V11() V12() ext-real Element of REAL

2 - (h . F) is V11() V12() ext-real Element of REAL

(2 - (h . F)) - (g . F) is V11() V12() ext-real Element of REAL

- ((h . F) - (g . F)) is V11() V12() ext-real Element of REAL

abs (- ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

((2 - (h . F)) - (g . F)) + (abs (- ((h . F) - (g . F)))) is V11() V12() ext-real Element of REAL

(((2 - (h . F)) - (g . F)) + (abs (- ((h . F) - (g . F))))) / 2 is V11() V12() ext-real Element of REAL

2 - ((h . F) + (g . F)) is V11() V12() ext-real Element of REAL

(2 - ((h . F) + (g . F))) + (abs ((h . F) - (g . F))) is V11() V12() ext-real Element of REAL

((2 - ((h . F) + (g . F))) + (abs ((h . F) - (g . F)))) / 2 is V11() V12() ext-real Element of REAL

dom (C,(C,h,g)) is Element of K6(C)

dom (C,(C,h),(C,g)) is Element of K6(C)

C is non empty set

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

C is non empty set

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

C is non empty set

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is V11() V12() ext-real Element of REAL

g is V11() V12() ext-real Element of REAL

[.h,g.] is V43() V44() V45() Element of K6(REAL)

F is Relation-like C -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

rng F is V43() V44() V45() set

dom F is Element of K6(C)

K6(C) is set

c is Element of C

F . c is V11() V12() ext-real Element of REAL

G is non empty V43() V44() V45() V50() closed_interval V81() V82() Element of K6(REAL)

lower_bound G is V11() V12() ext-real Element of REAL

upper_bound G is V11() V12() ext-real Element of REAL

[.(lower_bound G),(upper_bound G).] is V43() V44() V45() Element of K6(REAL)

G is Element of C

F . G is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is Element of C

(C) . g is V11() V12() ext-real Element of REAL

h . g is V11() V12() ext-real Element of REAL

rng h is V43() V44() V45() set

dom h is Element of K6(C)

K6(C) is set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is Element of C

h . g is V11() V12() ext-real Element of REAL

(C) . g is V11() V12() ext-real Element of REAL

rng h is V43() V44() V45() set

dom h is Element of K6(C)

K6(C) is set

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is Element of C

(C) . h is V11() V12() ext-real Element of REAL

(C) . h is V11() V12() ext-real Element of REAL

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g . h is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is Element of C

(C,h,g) . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

F is Element of C

h . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi (C,C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,(C)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

dom (C,h,(C)) is Element of K6(C)

K6(C) is set

dom (C,h,(C)) is Element of K6(C)

g is Element of C

(C,h,(C)) . g is V11() V12() ext-real Element of REAL

h . g is V11() V12() ext-real Element of REAL

(C) . g is V11() V12() ext-real Element of REAL

min ((h . g),((C) . g)) is V11() V12() ext-real Element of REAL

g is Element of C

(C,h,(C)) . g is V11() V12() ext-real Element of REAL

(C) . g is V11() V12() ext-real Element of REAL

h . g is V11() V12() ext-real Element of REAL

min ((h . g),((C) . g)) is V11() V12() ext-real Element of REAL

g is Element of C

(C,h,(C)) . g is V11() V12() ext-real Element of REAL

h . g is V11() V12() ext-real Element of REAL

(C) . g is V11() V12() ext-real Element of REAL

max ((h . g),((C) . g)) is V11() V12() ext-real Element of REAL

dom (C) is Element of K6(C)

dom (C,h,(C)) is Element of K6(C)

dom h is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

(C,h,F) . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

max ((h . G),(F . G)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

(C,h,F) . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

max ((h . G),(F . G)) is V11() V12() ext-real Element of REAL

max ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,G) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is Element of C

(C,h,F) . c is V11() V12() ext-real Element of REAL

(C,g,G) . c is V11() V12() ext-real Element of REAL

h . c is V11() V12() ext-real Element of REAL

g . c is V11() V12() ext-real Element of REAL

F . c is V11() V12() ext-real Element of REAL

G . c is V11() V12() ext-real Element of REAL

max ((h . c),(F . c)) is V11() V12() ext-real Element of REAL

max ((g . c),(G . c)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is Element of C

(C,h,g) . F is V11() V12() ext-real Element of REAL

(C,h,g) . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

max ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

h . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

min ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

(C,h,F) . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

h . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

min ((h . G),(F . G)) is V11() V12() ext-real Element of REAL

min ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,G) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

c is Element of C

(C,h,F) . c is V11() V12() ext-real Element of REAL

(C,g,G) . c is V11() V12() ext-real Element of REAL

h . c is V11() V12() ext-real Element of REAL

g . c is V11() V12() ext-real Element of REAL

F . c is V11() V12() ext-real Element of REAL

G . c is V11() V12() ext-real Element of REAL

min ((h . c),(F . c)) is V11() V12() ext-real Element of REAL

min ((g . c),(G . c)) is V11() V12() ext-real Element of REAL

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is Element of C

(C,h,g) . F is V11() V12() ext-real Element of REAL

h . F is V11() V12() ext-real Element of REAL

g . F is V11() V12() ext-real Element of REAL

min ((h . F),(g . F)) is V11() V12() ext-real Element of REAL

dom (C,h,g) is Element of K6(C)

K6(C) is set

dom h is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

(C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

chi ({},C) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

h . G is V11() V12() ext-real Element of REAL

(C) . G is V11() V12() ext-real Element of REAL

g . G is V11() V12() ext-real Element of REAL

F . G is V11() V12() ext-real Element of REAL

min ((g . G),(F . G)) is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

dom h is Element of K6(C)

K6(C) is set

dom (C) is Element of K6(C)

C is non empty set

K7(C,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(C,REAL)) is set

h is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

g is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,g) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

F is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,h,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,(C,h,g),(C,h,F)) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

(C,g,F) is non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(C,REAL))

G is Element of C

h . G is V11() V12() ext-real Element of REAL

(C,g,F) . G is V11() V12() ext-real Element of REAL

(C,(C,h,g),(C,h,F)) . G is V11() V12() ext-real Element of REAL

(C,h,g)