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
c8 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))
c8 . c is V11() V12() ext-real Element of REAL
max ((x . c),(c8 . c)) is V11() V12() ext-real Element of REAL
(G,x,c8) 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,x,c8) . 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
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
c10 is non empty set
K7(c10,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(c10,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,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))
c8 is non empty Relation-like x -defined REAL -valued [.0,1.] -valued Function-like total V30(x, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(x,REAL))
c9 is non empty Relation-like x -defined REAL -valued [.0,1.] -valued Function-like total V30(x, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(x,REAL))
(x,c8,c9) is non empty Relation-like x -defined REAL -valued [.0,1.] -valued Function-like total V30(x, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(x,REAL))
(x,c9,c8) is non empty Relation-like x -defined REAL -valued [.0,1.] -valued Function-like total V30(x, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(x,REAL))
c11 is non empty Relation-like c10 -defined REAL -valued [.0,1.] -valued Function-like total V30(c10, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(c10,REAL))
c12 is non empty Relation-like c10 -defined REAL -valued [.0,1.] -valued Function-like total V30(c10, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(c10,REAL))
(c10,c11,c12) is non empty Relation-like c10 -defined REAL -valued [.0,1.] -valued Function-like total V30(c10, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(c10,REAL))
(c10,c12,c11) is non empty Relation-like c10 -defined REAL -valued [.0,1.] -valued Function-like total V30(c10, REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(c10,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 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) . 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
F . G is V11() V12() ext-real Element of REAL
min ((h . G),(F . 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
g . G is V11() V12() ext-real Element of REAL
min ((h . G),(g . 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
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
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))
(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
(C) . 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,g,F) . G is V11() V12() ext-real Element of REAL
dom (C,h,F) 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
(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 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))
(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
h . F is V11() V12() ext-real Element of REAL
(C) . 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 Element of C
g . F is V11() V12() ext-real Element of REAL
(C) . F is V11() V12() ext-real Element of REAL
h . F is V11() V12() ext-real Element of REAL
max ((h . F),(g . F)) 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)
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
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 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
g . c is V11() V12() ext-real Element of REAL
F . c is V11() V12() ext-real Element of REAL
max ((g . c),(F . 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))
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 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
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
min ((g . c),(F . 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
(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))
(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
h . G is V11() V12() ext-real Element of REAL
g . G is V11() V12() ext-real Element of 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,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),(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))
min ((h . G),(g . 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))
(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,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,g) . F is V11() V12() ext-real Element of REAL
(C,h) . 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
1 - (g . F) is V11() V12() ext-real Element of REAL
1 - (h . 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))
(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,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)) 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,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))
(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,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)) 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))
(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 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 is non empty 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))
K7(C,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(C,REAL)) is 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))
(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,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,(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,(C)) . h is V11() V12() ext-real Element of REAL
(C) . h is V11() V12() ext-real Element of REAL
(C) . h is V11() V12() ext-real Element of REAL
1 - ((C) . h) is V11() V12() ext-real Element of REAL
1 - 0 is V11() V12() ext-real Element of REAL
dom (C,(C)) is Element of K6(C)
K6(C) is set
dom (C) is Element of K6(C)
h is Element of C
(C,(C)) . h is V11() V12() ext-real Element of REAL
(C) . h is V11() V12() ext-real Element of REAL
(C) . h is V11() V12() ext-real Element of REAL
1 - ((C) . h) is V11() V12() ext-real Element of REAL
1 - 1 is V11() V12() ext-real Element of REAL
dom (C,(C)) is Element of K6(C)
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,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,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) 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)),(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))
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))
(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,G,(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,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,G),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,(C,G,(C,c)),(C,(C,G),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,c,(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,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,c,(C,G)),(C,(C,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 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))
(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,(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,(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) 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)) 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,(C))),(C,(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) 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,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,(C,h,(C)),(C,(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,(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 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))
(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,(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,(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) 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)) 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,(C))),(C,(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) 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,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,(C,h,(C)),(C,(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,(C),(C,(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 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,(C,h,g),(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,F,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,(C,(C,h,g),(C,g,F)),(C,F,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,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),(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,F,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,(C,(C,h,g),(C,g,F)),(C,F,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,(C,(C,h,g),(C,g,F)),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,(C,h,g),(C,g,F)),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,(C,(C,(C,h,g),(C,g,F)),F),(C,(C,(C,h,g),(C,g,F)),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,(C,g,F),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,(C,g,F),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,(C,h,g),(C,(C,g,F),F)),(C,(C,(C,h,g),(C,g,F)),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,F,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,F,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),(C,(C,F,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),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,(C,(C,h,g),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,(C,h,g),(C,(C,F,g),F)),(C,(C,(C,h,g),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,(C,(C,h,g),F),(C,(C,(C,h,g),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,(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,(C,h,g),F),(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,F,(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,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,(C,F,(C,h,g)),(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,F,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,F,h),(C,F,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,(C,h,g),(C,h,F)),(C,(C,F,h),(C,F,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,(C,h,g),(C,h,F)),(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,(C,(C,h,g),(C,h,F)),(C,h,F)),(C,F,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,F),(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,(C,h,F),(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,(C,h,g),(C,(C,h,F),(C,h,F))),(C,F,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))
(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,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,(C,h,g),(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,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,(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)),(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,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,(C,h,g),(C,(C,h),(C,g))) . c is V11() V12() ext-real Element of REAL
(C,(C,h,g)) . c is V11() V12() ext-real Element of 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,(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,(C,h,(C,g))),(C,(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,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,(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,(C,h),(C,(C,g))),(C,(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),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)) 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,(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,(C,(C,h),g),(C,(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,(C,(C,h),g),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,(C,(C,h),g),(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,(C,(C,h),g),h),(C,(C,(C,h),g),(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,(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,(C,h,(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,(C,(C,h,(C,h)),(C,h,g)),(C,(C,(C,h),g),(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,g),(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,(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,(C,(C,g),(C,h)),(C,(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,(C,(C,h,(C,h)),(C,h,g)),(C,(C,(C,g),(C,h)),(C,(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,(C,h,g),(C,h,(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,(C,(C,h,g),(C,h,(C,h))),(C,(C,g),(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,(C,(C,(C,h,g),(C,h,(C,h))),(C,(C,g),(C,h))),(C,(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,(C,(C,g),(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,(C,(C,(C,g),(C,h)),(C,h,g)),(C,h,(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,(C,(C,(C,(C,g),(C,h)),(C,h,g)),(C,h,(C,h))),(C,(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,(C,h,(C,h)),(C,(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,(C,(C,(C,g),(C,h)),(C,h,g)),(C,(C,h,(C,h)),(C,(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,(C,h,(C,h)),(C,(C,g),g)) . c is V11() V12() ext-real Element of REAL
max (((C,(C,h,g),(C,(C,h),(C,g))) . c),((C,(C,h,(C,h)),(C,(C,g),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,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,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) 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)),(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,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),(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 is Element of C
(C,(C,h,g),(C,h,g)) . c is V11() V12() ext-real Element of REAL
(C,h,g) . c is V11() V12() ext-real Element of REAL
(C,(C,(C,h),g),(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)),(C,(C,(C,h),g),(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,(C,h),g),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,g,(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,(C,(C,h),g),h),(C,g,(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)),(C,(C,(C,(C,h),g),h),(C,g,(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,(C,(C,h),g),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)),(C,(C,(C,(C,h),g),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,(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)),(C,h,(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)),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,(C,h,(C,g)),(C,h,(C,(C,h),g))),(C,(C,h,(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,h,(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,(C,h,(C,h,(C,g))),(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,(C,h,(C,h,(C,g))),(C,(C,h),g)),(C,(C,h,(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,(C,h,(C,(C,h),g)),(C,(C,h,(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,h,(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,(C,h,(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,g,(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,(C,(C,h,(C,h)),(C,h,g)),(C,g,(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,g,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,g,(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,g,h),(C,g,(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,(C,h,(C,h)),(C,h,g)),(C,(C,g,h),(C,g,(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,(C,h,(C,h)),(C,h,g)),(C,g,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,(C,(C,(C,h,(C,h)),(C,h,g)),(C,g,h)),(C,g,(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,g),(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,h)),(C,(C,h,g),(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,(C,h,(C,h)),(C,(C,h,g),(C,h,g))),(C,g,(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,h)),(C,g,(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,g),(C,(C,h,(C,h)),(C,g,(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,h)),(C,g,(C,g))) . c is V11() V12() ext-real Element of REAL
min (((C,h,g) . c),((C,(C,h,(C,h)),(C,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))
(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))
(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,(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,(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))
(C,(C,h,(C,h)),(C,(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))
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
(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
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
(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
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
(h . G) - (g . G) is V11() V12() ext-real Element of REAL
abs ((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
(h . G) - (g . G) is V11() V12() ext-real Element of REAL
abs ((h . G) - (g . G)) is V11() V12() ext-real Element of REAL
rng g is V43() V44() V45() set
rng h 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
(h . x) - (g . x) is V11() V12() ext-real Element of REAL
abs ((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)
1 - (g . x) is V11() V12() ext-real Element of REAL
1 - 0 is V11() V12() ext-real Element of REAL
- 1 is V11() V12() ext-real Element of REAL
- (g . x) is V11() V12() ext-real Element of REAL
0 - (g . x) 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 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
(h . c) - (g . c) is V11() V12() ext-real Element of REAL
abs ((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)