REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V65() set
NAT is non trivial V6() non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non trivial V6() non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V65() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V65() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V65() set
[:REAL,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:REAL,REAL:] is non empty non trivial non finite set
{} is set
the empty V6() V10() V11() V12() ext-real non positive non negative Function-like functional finite V39() cardinal {} -element FinSequence-membered V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set is empty V6() V10() V11() V12() ext-real non positive non negative Function-like functional finite V39() cardinal {} -element FinSequence-membered V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set
1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{{},1} is finite set
[:COMPLEX,COMPLEX:] is non empty non trivial non finite V49() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V49() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial RAT -valued non finite V49() V50() V51() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial RAT -valued non finite V49() V50() V51() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial RAT -valued INT -valued non finite V49() V50() V51() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial RAT -valued INT -valued non finite V49() V50() V51() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is RAT -valued INT -valued V49() V50() V51() V52() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued V49() V50() V51() V52() set
bool [:[:NAT,NAT:],NAT:] is non empty set
2 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
3 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card {} is V6() cardinal set
D is non empty set
C is complex-membered ext-real-membered real-membered set
[:D,C:] is V49() V50() V51() set
bool [:D,C:] is non empty set
F is Relation-like D -defined C -valued Function-like V49() V50() V51() Element of bool [:D,C:]
A is V11() V12() ext-real Element of REAL
A (#) F is Relation-like Function-like set
PFuncs (D,REAL) is non empty functional PartFunc-set of D, REAL
B is Relation-like D -defined C -valued Function-like V49() V50() V51() Element of bool [:D,C:]
A (#) B is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
D is Relation-like Function-like set
rng D is set
C is set
{C} is non empty trivial finite 1 -element set
D " {C} is set
(rng D) /\ {C} is finite set
the Element of (rng D) /\ {C} is Element of (rng D) /\ {C}
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . F is set
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . (len C) is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
F is finite set
card F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bool F is non empty finite V39() set
the Element of F is Element of F
{ the Element of F} is non empty trivial finite 1 -element set
F \ { the Element of F} is finite Element of bool F
card (F \ { the Element of F}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card { the Element of F} is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card F) - (card { the Element of F}) is V11() V12() ext-real V47() set
(C + 1) - 1 is V11() V12() ext-real V47() Element of REAL
<*F*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len <*F*> is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng <*F*> is trivial finite set
{F} is non empty trivial finite V39() 1 -element set
c is set
c is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
mi is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
len mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(len mi) - 1 is V11() V12() ext-real V47() Element of REAL
mi . m1 is set
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mi . (m1 + 1) is set
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
mi . m1 is set
d is finite set
card d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{F} is non empty trivial finite V39() 1 -element set
b is non empty finite set
bool b is non empty finite V39() set
card b is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c is Relation-like NAT -defined bool b -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool b
len c is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*F*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
c ^ <*F*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng <*F*> is trivial finite set
rng (c ^ <*F*>) is finite set
rng c is finite V39() Element of bool (bool b)
bool (bool b) is non empty finite V39() set
(rng c) \/ (rng <*F*>) is finite set
(bool F) \/ (bool F) is finite V39() set
m1 is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
len <*F*> is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
len d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len c) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(len d) - 1 is V11() V12() ext-real V47() Element of REAL
d . x is set
x + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d . (x + 1) is set
dom c is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c . x is set
mi is finite set
c . (x + 1) is set
(len c) - 1 is V11() V12() ext-real V47() Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
d . x is set
mi is finite set
card mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom c is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c . x is set
b is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
len b is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F
len c is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bool C is non empty finite V39() set
D is set
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
union (bool D) is finite set
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
union (bool D) is finite set
F is finite set
card F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
union (bool D) is finite set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom D is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . C is set
C + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . (C + 1) is set
F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . F is set
len D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len D) - 1 is V11() V12() ext-real V47() Element of REAL
C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . C is set
F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . F is set
D . 0 is set
A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . A is set
C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
len D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len D) - 1 is V11() V12() ext-real V47() Element of REAL
D . C is set
C + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D . (C + 1) is set
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () ( bool D) FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . (len C) is set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like ( bool D) FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () FinSequence of bool D
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . F is set
A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . A is set
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B is finite set
card B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len C) - 1 is V11() V12() ext-real V47() Element of REAL
F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . F is set
F + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . (F + 1) is set
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
F is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool C
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
F . D is set
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
F is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of bool C
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
F . D is set
len F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
F is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () FinSequence of bool C
len F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len F) - 1 is V11() V12() ext-real V47() Element of REAL
F . (D + 1) is set
F . D is set
(F . (D + 1)) \ (F . D) is Element of bool (F . (D + 1))
bool (F . (D + 1)) is non empty set
A is finite set
card A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B is finite set
card B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D - D is V11() V12() ext-real V47() set
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () ( bool D) FinSequence of bool D
C . 1 is set
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is finite set
card F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is set
{A} is non empty trivial finite 1 -element set
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
B is Element of D
{B} is non empty trivial finite 1 -element set
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
F is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () FinSequence of bool C
len F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len F) - 1 is V11() V12() ext-real V47() Element of REAL
F . (D + 1) is set
F . D is set
(F . (D + 1)) \ (F . D) is Element of bool (F . (D + 1))
bool (F . (D + 1)) is non empty set
B is finite set
card B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is finite set
card A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A \ B is finite Element of bool A
bool A is non empty finite V39() set
card (A \ B) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(D + 1) - D is V11() V12() ext-real V47() Element of REAL
b is set
{b} is non empty trivial finite 1 -element set
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c is Element of C
{c} is non empty trivial finite 1 -element set
(F . D) \/ {c} is set
(F . (D + 1)) \ {c} is Element of bool (F . (D + 1))
(F . (D + 1)) \/ (F . D) is set
(F . D) \ {c} is Element of bool (F . D)
bool (F . D) is non empty set
{c} \ {c} is trivial finite Element of bool {c}
bool {c} is non empty finite V39() set
((F . D) \ {c}) \/ ({c} \ {c}) is set
((F . D) \ {c}) \/ {} is set
D is non empty finite set
bool D is non empty finite V39() set
C is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len C is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card D) - 1 is V11() V12() ext-real V47() Element of REAL
max (0,((card D) - 1)) is V11() V12() ext-real set
B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len b is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom b is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg B is finite B -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
rng b is finite set
c is set
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
b . mi is set
(len C) - mi is V11() V12() ext-real V47() Element of REAL
C . ((len C) - mi) is set
D \ (C . ((len C) - mi)) is finite Element of bool D
c is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
A is finite Element of bool D
<*A*> is non empty trivial Relation-like NAT -defined bool D -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool D
c ^ <*A*> is non empty Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool D
len (c ^ <*A*>) is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len c is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len <*A*> is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len c) + (len <*A*>) is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len c) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(c ^ <*A*>) . m1 is set
(len (c ^ <*A*>)) - m1 is V11() V12() ext-real V47() Element of REAL
max (0,((len (c ^ <*A*>)) - m1)) is V11() V12() ext-real set
x is finite set
card x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom C is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
C . d is set
(len (c ^ <*A*>)) - 1 is V11() V12() ext-real V47() Element of REAL
dom c is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c . m1 is set
D \ (C . d) is finite Element of bool D
mi is finite set
card mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card D) - (card mi) is V11() V12() ext-real V47() set
(len C) - d is V11() V12() ext-real V47() Element of REAL
(len (c ^ <*A*>)) - 1 is V11() V12() ext-real V47() Element of REAL
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(c ^ <*A*>) . m1 is set
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c ^ <*A*>) . (m1 + 1) is set
dom c is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c . m1 is set
(len C) - m1 is V11() V12() ext-real V47() Element of REAL
C . ((len C) - m1) is set
D \ (C . ((len C) - m1)) is finite Element of bool D
(len C) - (m1 + 1) is V11() V12() ext-real V47() Element of REAL
max (0,((len C) - (m1 + 1))) is V11() V12() ext-real set
c . (m1 + 1) is set
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . d is set
D \ (C . d) is finite Element of bool D
(m1 + 1) + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len C) - 1 is V11() V12() ext-real V47() Element of REAL
d + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C . (d + 1) is set
m1 is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len m1) - 1 is V11() V12() ext-real V47() Element of REAL
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
m1 . d is set
(len C) - d is V11() V12() ext-real V47() Element of REAL
C . ((len C) - d) is set
D \ (C . ((len C) - d)) is finite Element of bool D
dom c is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c . d is set
F is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len F) - 1 is V11() V12() ext-real V47() Element of REAL
A is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len A) - 1 is V11() V12() ext-real V47() Element of REAL
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom F is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len C) is finite len C -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
F . B is set
A . B is set
B + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len C) - 1 is V11() V12() ext-real V47() Element of REAL
b is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F . b is set
(len C) - b is V11() V12() ext-real V47() Element of REAL
C . ((len C) - b) is set
D \ (C . ((len C) - b)) is finite Element of bool D
F . B is set
A . B is set
F is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len F is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len F) - 1 is V11() V12() ext-real V47() Element of REAL
A is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len A) - 1 is V11() V12() ext-real V47() Element of REAL
B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
A . B is set
(len F) - B is V11() V12() ext-real V47() Element of REAL
F . ((len F) - B) is set
D \ (F . ((len F) - B)) is finite Element of bool D
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len A) - B is V11() V12() ext-real V47() Element of REAL
b is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(len A) - b is V11() V12() ext-real V47() Element of REAL
B + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom A is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
A . ((len A) - b) is set
D /\ (A . ((len A) - b)) is finite set
D \ (A . ((len A) - b)) is finite Element of bool D
D \ (D \ (A . ((len A) - b))) is finite Element of bool D
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
len (CHI (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom F is finite Element of bool D
bool D is non empty finite V39() set
b is Relation-like Function-like finite set
dom b is finite set
c is Relation-like Function-like finite set
dom c is finite set
F | D is Relation-like D -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:D,REAL:]
(dom F) /\ D is finite Element of bool D
dom (F | D) is finite Element of bool D
dom (FinS (F,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (FinS (F,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (FinS (F,D))) is finite len (FinS (F,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
mi is finite set
card mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 is finite set
card m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
F is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI (F,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
A is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (A,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,D))) (#) (CHI (F,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (A,D))) (#) (CHI (F,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,F) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,F),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
(MIM (FinS (A,D))) (#) (CHI ((C,F),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (A,D))) (#) (CHI ((C,F),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
dom (D,C,A,F) is finite Element of bool C
len (CHI (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B is set
len ((MIM (FinS (F,D))) (#) (CHI (A,C))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
min ((len (MIM (FinS (F,D)))),(len (CHI (A,C)))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is Element of C
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Element of D
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
B is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
B . 1 is set
CHI (B,D) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
PFuncs (D,REAL) is non empty functional PartFunc-set of D, REAL
(MIM (FinS (A,C))) (#) (CHI (B,D)) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
((MIM (FinS (A,C))) (#) (CHI (B,D))) # F is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom B is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len B) is finite len B -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom ((MIM (FinS (A,C))) (#) (CHI (B,D))) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len ((MIM (FinS (A,C))) (#) (CHI (B,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len ((MIM (FinS (A,C))) (#) (CHI (B,D)))) is finite len ((MIM (FinS (A,C))) (#) (CHI (B,D))) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (CHI (B,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (A,C))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (((MIM (FinS (A,C))) (#) (CHI (B,D))) # F)) is finite len (((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
min ((len (MIM (FinS (A,C)))),(len (CHI (B,D)))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (CHI (B,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (CHI (B,D))) is finite len (CHI (B,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . d is set
Seg (len (MIM (FinS (A,C)))) is finite len (MIM (FinS (A,C))) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (A,C)) . d is V11() V12() ext-real Element of REAL
(CHI (B,D)) . d is Relation-like Function-like set
B . d is set
chi ((B . d),D) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
dom (MIM (FinS (A,C))) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(MIM (FinS (A,C))) . d is V11() V12() ext-real Element of REAL
mi is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) (#) (CHI (B,D))) . d is Relation-like Function-like set
(D,REAL,(chi ((B . d),D)),mi) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . d is V11() V12() ext-real Element of REAL
(D,REAL,(chi ((B . d),D)),mi) . F is V11() V12() ext-real Element of REAL
dom (D,REAL,(chi ((B . d),D)),mi) is finite Element of bool D
dom (chi ((B . d),D)) is finite Element of bool D
(chi ((B . d),D)) . F is V11() V12() ext-real Element of REAL
mi * ((chi ((B . d),D)) . F) is V11() V12() ext-real Element of REAL
mi * 1 is V11() V12() ext-real Element of REAL
d + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (A,C)) . (d + 1) is V11() V12() ext-real Element of REAL
(len (MIM (FinS (A,C)))) - 1 is V11() V12() ext-real V47() Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . x is V11() V12() ext-real Element of REAL
mi is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
mi - r is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) (#) (CHI (B,D))) . d is Relation-like Function-like set
(D,REAL,(chi ((B . d),D)),(mi - r)) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . d is V11() V12() ext-real Element of REAL
(D,REAL,(chi ((B . d),D)),(mi - r)) . F is V11() V12() ext-real Element of REAL
dom (D,REAL,(chi ((B . d),D)),(mi - r)) is finite Element of bool D
dom (chi ((B . d),D)) is finite Element of bool D
(chi ((B . d),D)) . F is V11() V12() ext-real Element of REAL
(mi - r) * ((chi ((B . d),D)) . F) is V11() V12() ext-real Element of REAL
(mi - r) * 1 is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . d is V11() V12() ext-real Element of REAL
(MIM (FinS (A,C))) . d is V11() V12() ext-real Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . x is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . d is V11() V12() ext-real Element of REAL
(MIM (FinS (A,C))) . d is V11() V12() ext-real Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . x is V11() V12() ext-real Element of REAL
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . (d + 1) is set
B . d is set
(B . (d + 1)) \ (B . d) is Element of bool (B . (d + 1))
bool (B . (d + 1)) is non empty set
d |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V49() V50() V51() Element of d -tuples_on REAL
d -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = d } is set
Seg d is finite d -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K134((Seg d),0) is Relation-like Seg d -defined RAT -valued INT -valued {0} -valued Function-like V30( Seg d,{0}) finite FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg d),{0}:]
{0} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:(Seg d),{0}:] is RAT -valued INT -valued finite V49() V50() V51() V52() set
bool [:(Seg d),{0}:] is non empty finite V39() set
(FinS (A,C)) /^ d is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
MIM ((FinS (A,C)) /^ d) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(d |-> 0) ^ (MIM ((FinS (A,C)) /^ d)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) /^ d is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len ((MIM (FinS (A,C))) /^ d) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (MIM (FinS (A,C)))) - d is V11() V12() ext-real V47() Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . x is set
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . x is set
len (MIM ((FinS (A,C)) /^ d)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len ((FinS (A,C)) /^ d) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (d |-> 0) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (FinS (A,C))) - d is V11() V12() ext-real V47() Element of REAL
len ((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d + ((len (FinS (A,C))) - d) is V11() V12() ext-real V47() Element of REAL
dom ((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (MIM (FinS (A,C)))) is finite len (MIM (FinS (A,C))) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (d |-> 0) is finite d -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (d |-> 0)) is finite len (d |-> 0) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (A,C)) . m1 is V11() V12() ext-real Element of REAL
dom (MIM (FinS (A,C))) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(CHI (B,D)) . m1 is Relation-like Function-like set
B . m1 is set
chi ((B . m1),D) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (A,C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
(len (MIM (FinS (A,C)))) - 1 is V11() V12() ext-real V47() Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . ma is V11() V12() ext-real Element of REAL
bma is V11() V12() ext-real Element of REAL
bm1 is V11() V12() ext-real Element of REAL
bma - bm1 is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) (#) (CHI (B,D))) . m1 is Relation-like Function-like set
(D,REAL,(chi ((B . m1),D)),(bma - bm1)) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
(D,REAL,(chi ((B . m1),D)),(bma - bm1)) . F is V11() V12() ext-real Element of REAL
(chi ((B . m1),D)) . F is V11() V12() ext-real Element of REAL
(d |-> 0) . m1 is empty V6() V10() V11() V12() ext-real non positive non negative Function-like functional finite V39() cardinal {} -element FinSequence-membered V47() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() Element of REAL
dom (D,REAL,(chi ((B . m1),D)),(bma - bm1)) is finite Element of bool D
dom (chi ((B . m1),D)) is finite Element of bool D
(bma - bm1) * ((chi ((B . m1),D)) . F) is V11() V12() ext-real Element of REAL
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
m1 - d is V11() V12() ext-real V47() set
max (0,(m1 - d)) is V11() V12() ext-real set
(chi ((B . m1),D)) . F is V11() V12() ext-real Element of REAL
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . m1 is V11() V12() ext-real Element of REAL
bma is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) (#) (CHI (B,D))) . m1 is Relation-like Function-like set
(D,REAL,(chi ((B . m1),D)),bma) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
(D,REAL,(chi ((B . m1),D)),bma) . F is V11() V12() ext-real Element of REAL
dom ((MIM (FinS (A,C))) /^ d) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
(MIM ((FinS (A,C)) /^ d)) . (m1 - d) is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) /^ d) . bm1 is V11() V12() ext-real Element of REAL
bm1 + d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . (bm1 + d) is V11() V12() ext-real Element of REAL
dom (D,REAL,(chi ((B . m1),D)),bma) is finite Element of bool D
dom (chi ((B . m1),D)) is finite Element of bool D
bma * ((chi ((B . m1),D)) . F) is V11() V12() ext-real Element of REAL
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (A,C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
(len (MIM (FinS (A,C)))) - 1 is V11() V12() ext-real V47() Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . ma is V11() V12() ext-real Element of REAL
bma is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
bma - y is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) (#) (CHI (B,D))) . m1 is Relation-like Function-like set
(D,REAL,(chi ((B . m1),D)),(bma - y)) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
(D,REAL,(chi ((B . m1),D)),(bma - y)) . F is V11() V12() ext-real Element of REAL
dom ((MIM (FinS (A,C))) /^ d) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
(MIM ((FinS (A,C)) /^ d)) . (m1 - d) is V11() V12() ext-real Element of REAL
((MIM (FinS (A,C))) /^ d) . bm1 is V11() V12() ext-real Element of REAL
bm1 + d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(MIM (FinS (A,C))) . (bm1 + d) is V11() V12() ext-real Element of REAL
dom (D,REAL,(chi ((B . m1),D)),(bma - y)) is finite Element of bool D
dom (chi ((B . m1),D)) is finite Element of bool D
(bma - y) * ((chi ((B . m1),D)) . F) is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
(((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) . m1 is V11() V12() ext-real Element of REAL
((d |-> 0) ^ (MIM ((FinS (A,C)) /^ d))) . m1 is V11() V12() ext-real Element of REAL
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Element of D
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
B . 1 is set
(C,D,B,A) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
CHI (B,D) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
PFuncs (D,REAL) is non empty functional PartFunc-set of D, REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,D)) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,D))) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(C,D,B,A) . F is V11() V12() ext-real Element of REAL
len B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((MIM (FinS (A,C))) (#) (CHI (B,D))) # F is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
Sum (((MIM (FinS (A,C))) (#) (CHI (B,D))) # F) is V11() V12() ext-real Element of REAL
len (CHI (B,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (A,C))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum (MIM (FinS (A,C))) is V11() V12() ext-real Element of REAL
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . (m1 + 1) is set
B . m1 is set
(B . (m1 + 1)) \ (B . m1) is Element of bool (B . (m1 + 1))
bool (B . (m1 + 1)) is non empty set
(FinS (A,C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
(FinS (A,C)) /^ m1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
MIM ((FinS (A,C)) /^ m1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
m1 |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m1 -element FinSequence-like FinSubsequence-like V49() V50() V51() Element of m1 -tuples_on REAL
m1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m1 } is set
Seg m1 is finite m1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K134((Seg m1),0) is Relation-like Seg m1 -defined RAT -valued INT -valued {0} -valued Function-like V30( Seg m1,{0}) finite FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg m1),{0}:]
{0} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:(Seg m1),{0}:] is RAT -valued INT -valued finite V49() V50() V51() V52() set
bool [:(Seg m1),{0}:] is non empty finite V39() set
(m1 |-> 0) ^ (MIM ((FinS (A,C)) /^ m1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
Sum (m1 |-> 0) is V11() V12() ext-real Element of REAL
Sum (MIM ((FinS (A,C)) /^ m1)) is V11() V12() ext-real Element of REAL
(Sum (m1 |-> 0)) + (Sum (MIM ((FinS (A,C)) /^ m1))) is V11() V12() ext-real Element of REAL
0 + (Sum (MIM ((FinS (A,C)) /^ m1))) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
rng (FinS (F,D)) is finite complex-membered ext-real-membered real-membered Element of bool REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
rng (D,C,A,F) is complex-membered ext-real-membered real-membered Element of bool REAL
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (CHI (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom F is finite Element of bool D
bool D is non empty finite V39() set
m1 is Relation-like Function-like finite set
dom m1 is finite set
d is Relation-like Function-like finite set
dom d is finite set
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (F,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (D,C,A,F) is finite Element of bool C
dom (FinS (F,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (FinS (F,D))) is finite len (FinS (F,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom A is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len A) is finite len A -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
F | D is Relation-like D -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:D,REAL:]
x is finite set
card x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mi is finite set
card mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
r is set
m1 is Element of C
(D,C,A,F) . m1 is V11() V12() ext-real Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . ma is set
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
A . ma is set
ma - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(ma - 1)) is V11() V12() ext-real set
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . bma is set
bma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (bma + 1) is set
(A . (bma + 1)) \ (A . bma) is Element of bool (A . (bma + 1))
bool (A . (bma + 1)) is non empty set
(FinS (F,D)) . (bma + 1) is V11() V12() ext-real Element of REAL
r is set
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . m1 is V11() V12() ext-real Element of REAL
m1 - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(m1 - 1)) is V11() V12() ext-real set
A . 1 is set
the Element of A . 1 is Element of A . 1
bm1 is Element of C
(D,C,A,F) . bm1 is V11() V12() ext-real Element of REAL
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (ma + 1) is set
A . ma is set
(A . (ma + 1)) \ (A . ma) is Element of bool (A . (ma + 1))
bool (A . (ma + 1)) is non empty set
the Element of (A . (ma + 1)) \ (A . ma) is Element of (A . (ma + 1)) \ (A . ma)
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (FinS (F,D))) - 1 is V11() V12() ext-real V47() Element of REAL
A . m1 is set
bm1 is Element of C
(D,C,A,F) . bm1 is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (ma + 1) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
dom (D,C,A,F) is finite Element of bool C
len (CHI (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len A is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (F,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (FinS (F,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (FinS (F,D))) is finite len (FinS (F,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom A is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len A) is finite len A -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
m1 is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom m1 is finite Element of bool C
rng m1 is finite complex-membered ext-real-membered real-membered Element of bool REAL
rng (FinS (F,D)) is finite complex-membered ext-real-membered real-membered Element of bool REAL
d is set
{d} is non empty trivial finite 1 -element set
(FinS (F,D)) " {d} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 " {d} is finite Element of bool C
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is set
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . x is V11() V12() ext-real Element of REAL
x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . x is V11() V12() ext-real Element of REAL
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . mi is V11() V12() ext-real Element of REAL
mi - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(mi - 1)) is V11() V12() ext-real set
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg x is finite x -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg m1 is finite m1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(Seg x) \ (Seg m1) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{d} is non empty trivial finite 1 -element set
(FinS (F,D)) " {d} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
ma is set
bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (F,D)) . bma is V11() V12() ext-real Element of REAL
bma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bm1 is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
bm1 is V11() V12() ext-real Element of REAL
ma is set
bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (F,D)) . ma is V11() V12() ext-real Element of REAL
(FinS (F,D)) . bma is V11() V12() ext-real Element of REAL
bma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card ((FinS (F,D)) " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (Seg x) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (Seg m1) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card (Seg x)) - (card (Seg m1)) is V11() V12() ext-real V47() set
x - (card (Seg m1)) is V11() V12() ext-real V47() set
x - m1 is V11() V12() ext-real V47() set
A . x is set
m1 " {d} is finite Element of bool C
ma is set
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . bm1 is set
bm1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (bm1 + 1) is set
(len A) - 1 is V11() V12() ext-real V47() Element of REAL
y is Element of C
m1 . y is V11() V12() ext-real Element of REAL
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(A . (bm1 + 1)) \/ (A . bm1) is set
(A . (bm1 + 1)) \ (A . bm1) is Element of bool (A . (bm1 + 1))
bool (A . (bm1 + 1)) is non empty set
((A . (bm1 + 1)) \ (A . bm1)) \/ (A . bm1) is set
m1 . y is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (bm1 + 1) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
A . 0 is set
bm1 is Element of C
bma is Element of C
ma is set
bma is Element of C
m1 . bma is V11() V12() ext-real Element of REAL
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . bm1 is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
A . bm1 is set
bm1 - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(bm1 - 1)) is V11() V12() ext-real set
x + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bm1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (y + 1) is set
A . y is set
(A . (y + 1)) \ (A . y) is Element of bool (A . (y + 1))
bool (A . (y + 1)) is non empty set
(FinS (F,D)) . bm1 is V11() V12() ext-real Element of REAL
A . y is set
bm1 - y is V11() V12() ext-real V47() set
y + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (y + 1) is set
(A . (y + 1)) \ (A . y) is Element of bool (A . (y + 1))
bool (A . (y + 1)) is non empty set
(FinS (F,D)) . bm1 is V11() V12() ext-real Element of REAL
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . m1 is set
A . x is set
(A . x) \ (A . m1) is Element of bool (A . x)
bool (A . x) is non empty set
m1 " {d} is finite Element of bool C
bm1 is set
y is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . y is set
(A . y) \ (A . m1) is Element of bool (A . y)
bool (A . y) is non empty set
y + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (y + 1) is set
(A . (y + 1)) \ (A . m1) is Element of bool (A . (y + 1))
bool (A . (y + 1)) is non empty set
cy is Element of C
m1 . cy is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (y + 1) is V11() V12() ext-real Element of REAL
(A . (y + 1)) \/ (A . y) is set
((A . (y + 1)) \/ (A . y)) \ (A . m1) is Element of bool ((A . (y + 1)) \/ (A . y))
bool ((A . (y + 1)) \/ (A . y)) is non empty set
(A . (y + 1)) \ (A . y) is Element of bool (A . (y + 1))
((A . (y + 1)) \ (A . y)) \/ (A . y) is set
(((A . (y + 1)) \ (A . y)) \/ (A . y)) \ (A . m1) is Element of bool (((A . (y + 1)) \ (A . y)) \/ (A . y))
bool (((A . (y + 1)) \ (A . y)) \/ (A . y)) is non empty set
((A . (y + 1)) \ (A . y)) \ (A . m1) is Element of bool (A . (y + 1))
(((A . (y + 1)) \ (A . y)) \ (A . m1)) \/ ((A . y) \ (A . m1)) is set
m1 . cy is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (y + 1) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
A . 0 is set
(A . 0) \ (A . m1) is Element of bool (A . 0)
bool (A . 0) is non empty set
y is Element of C
y is Element of C
bm1 is set
y is Element of C
m1 . y is V11() V12() ext-real Element of REAL
cy is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . cy is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cy is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
A . cy is set
cy - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(cy - 1)) is V11() V12() ext-real set
x + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cy + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (mm + 1) is set
A . mm is set
(A . (mm + 1)) \ (A . mm) is Element of bool (A . (mm + 1))
bool (A . (mm + 1)) is non empty set
(FinS (F,D)) . cy is V11() V12() ext-real Element of REAL
A . mm is set
cy - mm is V11() V12() ext-real V47() set
mm + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (mm + 1) is set
(A . (mm + 1)) \ (A . mm) is Element of bool (A . (mm + 1))
bool (A . (mm + 1)) is non empty set
(FinS (F,D)) . cy is V11() V12() ext-real Element of REAL
cy is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
A . cy is set
cy - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(cy - 1)) is V11() V12() ext-real set
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cy + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . mm is set
mm + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A . (mm + 1) is set
(A . (mm + 1)) \ (A . mm) is Element of bool (A . (mm + 1))
bool (A . (mm + 1)) is non empty set
(FinS (F,D)) . (mm + 1) is V11() V12() ext-real Element of REAL
m1 - m1 is V11() V12() ext-real V47() set
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ma is finite set
card ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bma is finite set
card bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card ma) - (card bma) is V11() V12() ext-real V47() set
x - (card bma) is V11() V12() ext-real V47() set
m1 " {d} is finite Element of bool C
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 " {d} is finite Element of bool C
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is set
{d} is non empty trivial finite 1 -element set
(FinS (F,D)) " {d} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 " {d} is finite Element of bool C
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is set
{d} is non empty trivial finite 1 -element set
(FinS (F,D)) " {d} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 " {d} is finite Element of bool C
card (m1 " {d}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Coim ((FinS (F,D)),d) is set
(FinS (F,D)) " {d} is finite set
card (Coim ((FinS (F,D)),d)) is V6() cardinal set
Coim (m1,d) is set
m1 " {d} is finite set
card (Coim (m1,d)) is V6() cardinal set
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
dom (D,C,A,F) is finite Element of bool C
(D,C,A,F) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
Sum (F,D) is V11() V12() ext-real Element of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
Sum ((D,C,A,F),C) is V11() V12() ext-real Element of REAL
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum (FinS (F,D)) is V11() V12() ext-real Element of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((A - D),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((A - D),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
CHI (B,F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS (((C,F,B,A) - D),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum (((C,F,B,A) - D),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom ((C,F,B,A) - D) is finite Element of bool F
dom (C,F,B,A) is finite Element of bool F
((C,F,B,A) - D) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (A - D) is finite Element of bool C
(A - D) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((A - D),C)) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
dom (D,C,A,F) is finite Element of bool C
len (CHI ((C,A),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (C,A) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
min ((len (MIM (FinS (F,D)))),(len (CHI ((C,A),C)))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is set
c is Element of C
D is non empty finite set
bool D is non empty finite V39() set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Element of D
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
(D,B) is Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool D) FinSequence of bool D
(D,B) . 1 is set
(C,D,B,A) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
CHI ((D,B),D) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
PFuncs (D,REAL) is non empty functional PartFunc-set of D, REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((D,B),D)) is Relation-like NAT -defined PFuncs (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (D,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((D,B),D))) is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (D,REAL)
(C,D,B,A) . F is V11() V12() ext-real Element of REAL
len (D,B) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((MIM (FinS (A,C))) (#) (CHI ((D,B),D))) # F is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
Sum (((MIM (FinS (A,C))) (#) (CHI ((D,B),D))) # F) is V11() V12() ext-real Element of REAL
len (CHI ((D,B),D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (A,C))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (A,C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum (MIM (FinS (A,C))) is V11() V12() ext-real Element of REAL
d is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(D,B) . (d + 1) is set
(D,B) . d is set
((D,B) . (d + 1)) \ ((D,B) . d) is Element of bool ((D,B) . (d + 1))
bool ((D,B) . (d + 1)) is non empty set
(FinS (A,C)) . (d + 1) is V11() V12() ext-real Element of REAL
(FinS (A,C)) /^ d is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
MIM ((FinS (A,C)) /^ d) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
d |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V49() V50() V51() Element of d -tuples_on REAL
d -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = d } is set
Seg d is finite d -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K134((Seg d),0) is Relation-like Seg d -defined RAT -valued INT -valued {0} -valued Function-like V30( Seg d,{0}) finite FinSequence-like FinSubsequence-like V49() V50() V51() V52() Element of bool [:(Seg d),{0}:]
{0} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
[:(Seg d),{0}:] is RAT -valued INT -valued finite V49() V50() V51() V52() set
bool [:(Seg d),{0}:] is non empty finite V39() set
(d |-> 0) ^ (MIM ((FinS (A,C)) /^ d)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
Sum (d |-> 0) is V11() V12() ext-real Element of REAL
Sum (MIM ((FinS (A,C)) /^ d)) is V11() V12() ext-real Element of REAL
(Sum (d |-> 0)) + (Sum (MIM ((FinS (A,C)) /^ d))) is V11() V12() ext-real Element of REAL
0 + (Sum (MIM ((FinS (A,C)) /^ d))) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
rng (FinS (F,D)) is finite complex-membered ext-real-membered real-membered Element of bool REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
rng (D,C,A,F) is complex-membered ext-real-membered real-membered Element of bool REAL
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (CHI ((C,A),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom F is finite Element of bool D
bool D is non empty finite V39() set
dom (FinS (F,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (FinS (F,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (FinS (F,D))) is finite len (FinS (F,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (D,C,A,F) is finite Element of bool C
dom (C,A) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (C,A) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (C,A)) is finite len (C,A) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
d is Relation-like Function-like finite set
dom d is finite set
F | D is Relation-like D -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:D,REAL:]
x is finite set
card x is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mi is finite set
card mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
r is set
m1 is Element of C
(D,C,A,F) . m1 is V11() V12() ext-real Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . ma is set
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(C,A) . ma is set
ma - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(ma - 1)) is V11() V12() ext-real set
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . bma is set
bma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (bma + 1) is set
((C,A) . (bma + 1)) \ ((C,A) . bma) is Element of bool ((C,A) . (bma + 1))
bool ((C,A) . (bma + 1)) is non empty set
(FinS (F,D)) . (bma + 1) is V11() V12() ext-real Element of REAL
r is set
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . m1 is V11() V12() ext-real Element of REAL
m1 - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(m1 - 1)) is V11() V12() ext-real set
(C,A) . 1 is set
the Element of (C,A) . 1 is Element of (C,A) . 1
bm1 is Element of C
(D,C,A,F) . bm1 is V11() V12() ext-real Element of REAL
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (ma + 1) is set
(C,A) . ma is set
((C,A) . (ma + 1)) \ ((C,A) . ma) is Element of bool ((C,A) . (ma + 1))
bool ((C,A) . (ma + 1)) is non empty set
the Element of ((C,A) . (ma + 1)) \ ((C,A) . ma) is Element of ((C,A) . (ma + 1)) \ ((C,A) . ma)
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (FinS (F,D))) - 1 is V11() V12() ext-real V47() Element of REAL
(C,A) . m1 is set
bm1 is Element of C
(D,C,A,F) . bm1 is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (ma + 1) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
len (CHI ((C,A),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (C,A) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (MIM (FinS (F,D))) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (FinS (F,D)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng (D,C,A,F) is complex-membered ext-real-membered real-membered Element of bool REAL
rng (FinS (F,D)) is finite complex-membered ext-real-membered real-membered Element of bool REAL
dom (D,C,A,F) is finite Element of bool C
dom (FinS (F,D)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (FinS (F,D))) is finite len (FinS (F,D)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (C,A) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (C,A)) is finite len (C,A) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
x is set
{x} is non empty trivial finite 1 -element set
(FinS (F,D)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is set
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . mi is V11() V12() ext-real Element of REAL
mi - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(mi - 1)) is V11() V12() ext-real set
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . ma is V11() V12() ext-real Element of REAL
ma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(FinS (F,D)) . ma is V11() V12() ext-real Element of REAL
Seg ma is finite ma -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg m1 is finite m1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(Seg ma) \ (Seg m1) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{x} is non empty trivial finite 1 -element set
(FinS (F,D)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
bma is set
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (F,D)) . bm1 is V11() V12() ext-real Element of REAL
bm1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
bma is set
bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS (F,D)) . bma is V11() V12() ext-real Element of REAL
(FinS (F,D)) . bm1 is V11() V12() ext-real Element of REAL
bm1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card ((FinS (F,D)) " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (Seg ma) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (Seg m1) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card (Seg ma)) - (card (Seg m1)) is V11() V12() ext-real V47() set
ma - (card (Seg m1)) is V11() V12() ext-real V47() set
ma - m1 is V11() V12() ext-real V47() set
(C,A) . ma is set
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
bma is set
y is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . y is set
y + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (y + 1) is set
(len (C,A)) - 1 is V11() V12() ext-real V47() Element of REAL
cy is Element of C
d . cy is V11() V12() ext-real Element of REAL
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((C,A) . (y + 1)) \/ ((C,A) . y) is set
((C,A) . (y + 1)) \ ((C,A) . y) is Element of bool ((C,A) . (y + 1))
bool ((C,A) . (y + 1)) is non empty set
(((C,A) . (y + 1)) \ ((C,A) . y)) \/ ((C,A) . y) is set
d . cy is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (y + 1) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
(C,A) . 0 is set
y is Element of C
bm1 is Element of C
bma is set
bm1 is Element of C
d . bm1 is V11() V12() ext-real Element of REAL
y is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . y is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(C,A) . y is set
y - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(y - 1)) is V11() V12() ext-real set
ma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cy is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
cy + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (cy + 1) is set
(C,A) . cy is set
((C,A) . (cy + 1)) \ ((C,A) . cy) is Element of bool ((C,A) . (cy + 1))
bool ((C,A) . (cy + 1)) is non empty set
(FinS (F,D)) . y is V11() V12() ext-real Element of REAL
(C,A) . cy is set
y - cy is V11() V12() ext-real V47() set
cy + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (cy + 1) is set
((C,A) . (cy + 1)) \ ((C,A) . cy) is Element of bool ((C,A) . (cy + 1))
bool ((C,A) . (cy + 1)) is non empty set
(FinS (F,D)) . y is V11() V12() ext-real Element of REAL
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . m1 is set
(C,A) . ma is set
((C,A) . ma) \ ((C,A) . m1) is Element of bool ((C,A) . ma)
bool ((C,A) . ma) is non empty set
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
y is set
cy is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . cy is set
((C,A) . cy) \ ((C,A) . m1) is Element of bool ((C,A) . cy)
bool ((C,A) . cy) is non empty set
cy + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (cy + 1) is set
((C,A) . (cy + 1)) \ ((C,A) . m1) is Element of bool ((C,A) . (cy + 1))
bool ((C,A) . (cy + 1)) is non empty set
mm is Element of C
d . mm is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (cy + 1) is V11() V12() ext-real Element of REAL
((C,A) . (cy + 1)) \/ ((C,A) . cy) is set
(((C,A) . (cy + 1)) \/ ((C,A) . cy)) \ ((C,A) . m1) is Element of bool (((C,A) . (cy + 1)) \/ ((C,A) . cy))
bool (((C,A) . (cy + 1)) \/ ((C,A) . cy)) is non empty set
((C,A) . (cy + 1)) \ ((C,A) . cy) is Element of bool ((C,A) . (cy + 1))
(((C,A) . (cy + 1)) \ ((C,A) . cy)) \/ ((C,A) . cy) is set
((((C,A) . (cy + 1)) \ ((C,A) . cy)) \/ ((C,A) . cy)) \ ((C,A) . m1) is Element of bool ((((C,A) . (cy + 1)) \ ((C,A) . cy)) \/ ((C,A) . cy))
bool ((((C,A) . (cy + 1)) \ ((C,A) . cy)) \/ ((C,A) . cy)) is non empty set
(((C,A) . (cy + 1)) \ ((C,A) . cy)) \ ((C,A) . m1) is Element of bool ((C,A) . (cy + 1))
((((C,A) . (cy + 1)) \ ((C,A) . cy)) \ ((C,A) . m1)) \/ (((C,A) . cy) \ ((C,A) . m1)) is set
d . mm is V11() V12() ext-real Element of REAL
(FinS (F,D)) . (cy + 1) is V11() V12() ext-real Element of REAL
r is V11() V12() ext-real Element of REAL
(C,A) . 0 is set
((C,A) . 0) \ ((C,A) . m1) is Element of bool ((C,A) . 0)
bool ((C,A) . 0) is non empty set
cy is Element of C
cy is Element of C
y is set
cy is Element of C
d . cy is V11() V12() ext-real Element of REAL
mm is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . mm is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(C,A) . mm is set
mm - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(mm - 1)) is V11() V12() ext-real set
ma + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1m is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1m + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (1m + 1) is set
(C,A) . 1m is set
((C,A) . (1m + 1)) \ ((C,A) . 1m) is Element of bool ((C,A) . (1m + 1))
bool ((C,A) . (1m + 1)) is non empty set
(FinS (F,D)) . mm is V11() V12() ext-real Element of REAL
(C,A) . 1m is set
mm - 1m is V11() V12() ext-real V47() set
1m + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (1m + 1) is set
((C,A) . (1m + 1)) \ ((C,A) . 1m) is Element of bool ((C,A) . (1m + 1))
bool ((C,A) . (1m + 1)) is non empty set
(FinS (F,D)) . mm is V11() V12() ext-real Element of REAL
mm is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(C,A) . mm is set
mm - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(mm - 1)) is V11() V12() ext-real set
(FinS (F,D)) . 1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1m is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mm + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . 1m is set
1m + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(C,A) . (1m + 1) is set
((C,A) . (1m + 1)) \ ((C,A) . 1m) is Element of bool ((C,A) . (1m + 1))
bool ((C,A) . (1m + 1)) is non empty set
(FinS (F,D)) . (1m + 1) is V11() V12() ext-real Element of REAL
m1 - m1 is V11() V12() ext-real V47() set
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bma is finite set
card bma is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bm1 is finite set
card bm1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card bma) - (card bm1) is V11() V12() ext-real V47() set
ma - (card bm1) is V11() V12() ext-real V47() set
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is set
{x} is non empty trivial finite 1 -element set
(FinS (F,D)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is set
{x} is non empty trivial finite 1 -element set
(FinS (F,D)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card ((FinS (F,D)) " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
d is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
d " {x} is finite Element of bool C
card (d " {x}) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Coim ((FinS (F,D)),x) is set
(FinS (F,D)) " {x} is finite set
card (Coim ((FinS (F,D)),x)) is V6() cardinal set
Coim (d,x) is set
d " {x} is finite set
card (Coim (d,x)) is V6() cardinal set
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
dom (D,C,A,F) is finite Element of bool C
(D,C,A,F) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
Sum (F,D) is V11() V12() ext-real Element of REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
Sum ((D,C,A,F),C) is V11() V12() ext-real Element of REAL
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum (FinS (F,D)) is V11() V12() ext-real Element of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((A - D),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((A - D),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
(F,B) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
CHI ((F,B),F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS (((C,F,B,A) - D),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum (((C,F,B,A) - D),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom ((C,F,B,A) - D) is finite Element of bool F
dom (C,F,B,A) is finite Element of bool F
((C,F,B,A) - D) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (A - D) is finite Element of bool C
(A - D) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((A - D),C)) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((D,C,A,F),C) is V11() V12() ext-real Element of REAL
Sum ((D,C,A,F),C) is V11() V12() ext-real Element of REAL
Sum (F,D) is V11() V12() ext-real Element of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
max+ (A - D) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((max+ (A - D)),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max+ (A - D)),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
CHI (B,F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
max+ ((C,F,B,A) - D) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS ((max+ ((C,F,B,A) - D)),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max+ ((C,F,B,A) - D)),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom (max+ ((C,F,B,A) - D)) is finite Element of bool F
dom ((C,F,B,A) - D) is finite Element of bool F
(max+ ((C,F,B,A) - D)) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (max+ (A - D)) is finite Element of bool C
dom (A - D) is finite Element of bool C
(max+ (A - D)) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((max+ (A - D)),C)) is V11() V12() ext-real Element of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
max- (A - D) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((max- (A - D)),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max- (A - D)),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
CHI (B,F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
max- ((C,F,B,A) - D) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS ((max- ((C,F,B,A) - D)),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max- ((C,F,B,A) - D)),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom (max- ((C,F,B,A) - D)) is finite Element of bool F
dom ((C,F,B,A) - D) is finite Element of bool F
(max- ((C,F,B,A) - D)) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (max- (A - D)) is finite Element of bool C
dom (A - D) is finite Element of bool C
(max- (A - D)) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((max- (A - D)),C)) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
len (FinS ((D,C,A,F),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (D,C,A,F) is finite Element of bool C
(D,C,A,F) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
dom B is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
CHI (B,F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
FinS ((C,F,B,A),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(FinS ((C,F,B,A),F)) | D is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
B . D is set
FinS ((C,F,B,A),(B . D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
len (FinS ((C,F,B,A),F)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len B) is finite len B -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (FinS ((C,F,B,A),F)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (FinS ((C,F,B,A),F))) is finite len (FinS ((C,F,B,A),F)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS ((C,F,B,A),F)) | mi is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
B . mi is set
FinS ((C,F,B,A),(B . mi)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
mi + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS ((C,F,B,A),F)) | (mi + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
B . (mi + 1) is set
FinS ((C,F,B,A),(B . (mi + 1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Seg (mi + 1) is non empty finite mi + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (C,F,B,A) is finite Element of bool F
(len B) - 1 is V11() V12() ext-real V47() Element of REAL
len ((FinS ((C,F,B,A),F)) | (mi + 1)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . 1 is set
m1 is Element of F
{m1} is non empty trivial finite 1 -element set
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((FinS ((C,F,B,A),F)) | (mi + 1)) . 1 is V11() V12() ext-real Element of REAL
(FinS ((C,F,B,A),F)) . 1 is V11() V12() ext-real Element of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,A) . m1 is V11() V12() ext-real Element of REAL
<*((C,F,B,A) . m1)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
Seg mi is finite mi -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((FinS ((C,F,B,A),F)) | (mi + 1)) | mi is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((FinS ((C,F,B,A),F)) | (mi + 1)) | (Seg mi) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V49() V50() V51() set
bool [:NAT,REAL:] is non empty non trivial non finite set
(FinS ((C,F,B,A),F)) | (Seg (mi + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
((FinS ((C,F,B,A),F)) | (Seg (mi + 1))) | (Seg mi) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
(Seg (mi + 1)) /\ (Seg mi) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(FinS ((C,F,B,A),F)) | ((Seg (mi + 1)) /\ (Seg mi)) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
(FinS ((C,F,B,A),F)) | (Seg mi) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(B . (mi + 1)) \ (B . mi) is Element of bool (B . (mi + 1))
bool (B . (mi + 1)) is non empty set
m1 is Element of F
{m1} is non empty trivial finite 1 -element set
(B . mi) \/ {m1} is set
(B . (mi + 1)) \ {m1} is Element of bool (B . (mi + 1))
(C,F,B,A) . m1 is V11() V12() ext-real Element of REAL
(FinS (A,C)) . (mi + 1) is V11() V12() ext-real Element of REAL
(FinS ((C,F,B,A),F)) . (mi + 1) is V11() V12() ext-real Element of REAL
((FinS ((C,F,B,A),F)) | (mi + 1)) . (mi + 1) is V11() V12() ext-real Element of REAL
<*((C,F,B,A) . m1)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
((FinS ((C,F,B,A),F)) | mi) ^ <*((C,F,B,A) . m1)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(dom (C,F,B,A)) /\ (B . (mi + 1)) is finite Element of bool F
(C,F,B,A) | (B . (mi + 1)) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
dom ((C,F,B,A) | (B . (mi + 1))) is finite Element of bool F
(FinS ((C,F,B,A),F)) | 0 is empty V6() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() V49() V50() V51() V52() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() FinSequence of REAL
B . 0 is set
FinS ((C,F,B,A),(B . 0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,(A - D)) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
CHI (B,F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS ((A - D),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS ((A - D),C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS ((A - D),C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS ((A - D),C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI (B,F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI (B,F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
dom (C,F,B,A) is finite Element of bool F
dom A is finite Element of bool C
bool C is non empty finite V39() set
dom (A - D) is finite Element of bool C
(A - D) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
len (FinS ((A - D),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
(card C) |-> D is Relation-like NAT -defined REAL -valued Function-like finite card C -element FinSequence-like FinSubsequence-like V49() V50() V51() Element of (card C) -tuples_on REAL
(card C) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = card C } is set
Seg (card C) is non empty finite card C -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K134((Seg (card C)),D) is Relation-like Seg (card C) -defined {D} -valued Function-like V30( Seg (card C),{D}) finite FinSequence-like FinSubsequence-like V49() V50() V51() Element of bool [:(Seg (card C)),{D}:]
{D} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg (card C)),{D}:] is non empty finite V49() V50() V51() set
bool [:(Seg (card C)),{D}:] is non empty finite V39() set
(FinS (A,C)) - ((card C) |-> D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
b is Element of F
dom (C,F,B,(A - D)) is finite Element of bool F
dom B is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
B . (len B) is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
B . c is set
c - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(c - 1)) is V11() V12() ext-real set
c + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (FinS ((A - D),C)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((card C) |-> D) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . b is V11() V12() ext-real Element of REAL
(FinS ((A - D),C)) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,A) . b is V11() V12() ext-real Element of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
((C,F,B,A) . b) - D is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . b is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . mi is set
mi + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
B . (mi + 1) is set
(B . (mi + 1)) \ (B . mi) is Element of bool (B . (mi + 1))
bool (B . (mi + 1)) is non empty set
(C,F,B,(A - D)) . b is V11() V12() ext-real Element of REAL
(FinS ((A - D),C)) . (mi + 1) is V11() V12() ext-real Element of REAL
(C,F,B,A) . b is V11() V12() ext-real Element of REAL
(FinS (A,C)) . (mi + 1) is V11() V12() ext-real Element of REAL
((card C) |-> D) . (mi + 1) is V11() V12() ext-real Element of REAL
dom (FinS ((A - D),C)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((C,F,B,A) . b) - D is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . b is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . b is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . b is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . b is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . b is V11() V12() ext-real Element of REAL
dom ((C,F,B,A) - D) is finite Element of bool F
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
max+ (A - D) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((max+ (A - D)),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max+ (A - D)),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
(F,B) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
CHI ((F,B),F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
max+ ((C,F,B,A) - D) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS ((max+ ((C,F,B,A) - D)),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max+ ((C,F,B,A) - D)),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom (max+ ((C,F,B,A) - D)) is finite Element of bool F
dom ((C,F,B,A) - D) is finite Element of bool F
(max+ ((C,F,B,A) - D)) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (max+ (A - D)) is finite Element of bool C
dom (A - D) is finite Element of bool C
(max+ (A - D)) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((max+ (A - D)),C)) is V11() V12() ext-real Element of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
max- (A - D) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
FinS ((max- (A - D)),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max- (A - D)),C) is V11() V12() ext-real Element of REAL
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
(F,B) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
CHI ((F,B),F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
max- ((C,F,B,A) - D) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS ((max- ((C,F,B,A) - D)),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Sum ((max- ((C,F,B,A) - D)),F) is V11() V12() ext-real Element of REAL
dom A is finite Element of bool C
bool C is non empty finite V39() set
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
dom (max- ((C,F,B,A) - D)) is finite Element of bool F
dom ((C,F,B,A) - D) is finite Element of bool F
(max- ((C,F,B,A) - D)) | F is Relation-like F -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:F,REAL:]
dom (max- (A - D)) is finite Element of bool C
dom (A - D) is finite Element of bool C
(max- (A - D)) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
Sum (FinS ((max- (A - D)),C)) is V11() V12() ext-real Element of REAL
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
FinS ((D,C,A,F),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
len (FinS ((D,C,A,F),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (D,C,A,F) is finite Element of bool C
(D,C,A,F) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
D is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
dom B is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
(F,B) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
CHI ((F,B),F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
FinS ((C,F,B,A),F) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(FinS ((C,F,B,A),F)) | D is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(F,B) . D is set
FinS ((C,F,B,A),((F,B) . D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
len (FinS ((C,F,B,A),F)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (F,B) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
len (F,B) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (F,B)) is finite len (F,B) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (FinS ((C,F,B,A),F)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg (len (FinS ((C,F,B,A),F))) is finite len (FinS ((C,F,B,A),F)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS ((C,F,B,A),F)) | m1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(F,B) . m1 is set
FinS ((C,F,B,A),((F,B) . m1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(FinS ((C,F,B,A),F)) | (m1 + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(F,B) . (m1 + 1) is set
FinS ((C,F,B,A),((F,B) . (m1 + 1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
Seg (m1 + 1) is non empty finite m1 + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
dom (C,F,B,A) is finite Element of bool F
(len (F,B)) - 1 is V11() V12() ext-real V47() Element of REAL
len ((FinS ((C,F,B,A),F)) | (m1 + 1)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(F,B) . 1 is set
d is Element of F
{d} is non empty trivial finite 1 -element set
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((FinS ((C,F,B,A),F)) | (m1 + 1)) . 1 is V11() V12() ext-real Element of REAL
(FinS ((C,F,B,A),F)) . 1 is V11() V12() ext-real Element of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,A) . d is V11() V12() ext-real Element of REAL
<*((C,F,B,A) . d)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
Seg m1 is finite m1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((FinS ((C,F,B,A),F)) | (m1 + 1)) | m1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((FinS ((C,F,B,A),F)) | (m1 + 1)) | (Seg m1) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V49() V50() V51() set
bool [:NAT,REAL:] is non empty non trivial non finite set
(FinS ((C,F,B,A),F)) | (Seg (m1 + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
((FinS ((C,F,B,A),F)) | (Seg (m1 + 1))) | (Seg m1) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
(Seg (m1 + 1)) /\ (Seg m1) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(FinS ((C,F,B,A),F)) | ((Seg (m1 + 1)) /\ (Seg m1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
(FinS ((C,F,B,A),F)) | (Seg m1) is Relation-like NAT -defined REAL -valued Function-like finite FinSubsequence-like V49() V50() V51() Element of bool [:NAT,REAL:]
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((F,B) . (m1 + 1)) \ ((F,B) . m1) is Element of bool ((F,B) . (m1 + 1))
bool ((F,B) . (m1 + 1)) is non empty set
d is Element of F
{d} is non empty trivial finite 1 -element set
((F,B) . m1) \/ {d} is set
((F,B) . (m1 + 1)) \ {d} is Element of bool ((F,B) . (m1 + 1))
(C,F,B,A) . d is V11() V12() ext-real Element of REAL
(FinS (A,C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
(FinS ((C,F,B,A),F)) . (m1 + 1) is V11() V12() ext-real Element of REAL
((FinS ((C,F,B,A),F)) | (m1 + 1)) . (m1 + 1) is V11() V12() ext-real Element of REAL
<*((C,F,B,A) . d)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
((FinS ((C,F,B,A),F)) | m1) ^ <*((C,F,B,A) . d)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(dom (C,F,B,A)) /\ ((F,B) . (m1 + 1)) is finite Element of bool F
(C,F,B,A) | ((F,B) . (m1 + 1)) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
dom ((C,F,B,A) | ((F,B) . (m1 + 1))) is finite Element of bool F
len B is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len B) is finite len B -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(FinS ((C,F,B,A),F)) | 0 is empty V6() V10() V11() V12() ext-real non positive non negative Relation-like NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() V49() V50() V51() V52() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() FinSequence of REAL
(F,B) . 0 is set
FinS ((C,F,B,A),((F,B) . 0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
D is V11() V12() ext-real Element of REAL
C is non empty finite set
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is non empty finite set
bool F is non empty finite V39() set
card F is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
A - D is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
B is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
(C,F,B,(A - D)) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
[:F,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:F,REAL:] is non empty non trivial non finite set
(F,B) is Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool F) FinSequence of bool F
CHI ((F,B),F) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
PFuncs (F,REAL) is non empty functional PartFunc-set of F, REAL
FinS ((A - D),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS ((A - D),C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS ((A - D),C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS ((A - D),C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
FinS (A,C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (A,C)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (A,C))) (#) (CHI ((F,B),F)) is Relation-like NAT -defined PFuncs (F,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (F,REAL)
Sum ((MIM (FinS (A,C))) (#) (CHI ((F,B),F))) is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (F,REAL)
(C,F,B,A) - D is Relation-like F -defined REAL -valued Function-like V49() V50() V51() Element of bool [:F,REAL:]
dom (C,F,B,A) is finite Element of bool F
len (F,B) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom A is finite Element of bool C
bool C is non empty finite V39() set
dom (A - D) is finite Element of bool C
(A - D) | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
len (FinS ((A - D),C)) is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
A | C is Relation-like C -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:C,REAL:]
(card C) |-> D is Relation-like NAT -defined REAL -valued Function-like finite card C -element FinSequence-like FinSubsequence-like V49() V50() V51() Element of (card C) -tuples_on REAL
(card C) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = card C } is set
Seg (card C) is non empty finite card C -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
K134((Seg (card C)),D) is Relation-like Seg (card C) -defined {D} -valued Function-like V30( Seg (card C),{D}) finite FinSequence-like FinSubsequence-like V49() V50() V51() Element of bool [:(Seg (card C)),{D}:]
{D} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered set
[:(Seg (card C)),{D}:] is non empty finite V49() V50() V51() set
bool [:(Seg (card C)),{D}:] is non empty finite V39() set
(FinS (A,C)) - ((card C) |-> D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
c is Element of F
dom (C,F,B,(A - D)) is finite Element of bool F
dom (F,B) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(F,B) . (len (F,B)) is set
0 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
mi is V6() V10() V11() V12() ext-real non negative finite cardinal V47() set
(F,B) . mi is set
mi - 1 is V11() V12() ext-real V47() Element of REAL
max (0,(mi - 1)) is V11() V12() ext-real set
mi + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m1 is V6() V10() V11() V12() ext-real non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (FinS ((A - D),C)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((card C) |-> D) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . c is V11() V12() ext-real Element of REAL
(FinS ((A - D),C)) . 1 is V11() V12() ext-real Element of REAL
(C,F,B,A) . c is V11() V12() ext-real Element of REAL
(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL
((C,F,B,A) . c) - D is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . c is V11() V12() ext-real Element of REAL
1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(F,B) . m1 is set
m1 + 1 is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(F,B) . (m1 + 1) is set
((F,B) . (m1 + 1)) \ ((F,B) . m1) is Element of bool ((F,B) . (m1 + 1))
bool ((F,B) . (m1 + 1)) is non empty set
(C,F,B,(A - D)) . c is V11() V12() ext-real Element of REAL
(FinS ((A - D),C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
(C,F,B,A) . c is V11() V12() ext-real Element of REAL
(FinS (A,C)) . (m1 + 1) is V11() V12() ext-real Element of REAL
((card C) |-> D) . (m1 + 1) is V11() V12() ext-real Element of REAL
dom (FinS ((A - D),C)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
((C,F,B,A) . c) - D is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . c is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . c is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . c is V11() V12() ext-real Element of REAL
(C,F,B,(A - D)) . c is V11() V12() ext-real Element of REAL
((C,F,B,A) - D) . c is V11() V12() ext-real Element of REAL
dom ((C,F,B,A) - D) is finite Element of bool F
D is non empty finite set
[:D,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:D,REAL:] is non empty non trivial non finite set
card D is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
C is non empty finite set
bool C is non empty finite V39() set
card C is non empty V6() V10() V11() V12() ext-real positive non negative finite cardinal V47() V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
F is Relation-like D -defined REAL -valued Function-like V49() V50() V51() Element of bool [:D,REAL:]
rng F is complex-membered ext-real-membered real-membered Element of bool REAL
A is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
[:C,REAL:] is non empty non trivial non finite V49() V50() V51() set
bool [:C,REAL:] is non empty non trivial non finite set
CHI (A,C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL
FinS (F,D) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
MIM (FinS (F,D)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(MIM (FinS (F,D))) (#) (CHI (A,C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
(D,C,A,F) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of bool [:C,REAL:]
(C,A) is Relation-like NAT -defined bool C -valued Function-like finite FinSequence-like FinSubsequence-like () () ( bool C) FinSequence of bool C
CHI ((C,A),C) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
(MIM (FinS (F,D))) (#) (CHI ((C,A),C)) is Relation-like NAT -defined PFuncs (C,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PFuncs (C,REAL)
Sum ((MIM (FinS (F,D))) (#) (CHI ((C,A),C))) is Relation-like C -defined REAL -valued Function-like V49() V50() V51() Element of PFuncs (C,REAL)
rng (D,C,A,F) is complex-membered ext-real-membered real-membered Element of bool REAL
rng (D,C,A,F) is complex-membered ext-real-membered real-membered Element of bool REAL
dom F is finite Element of bool D
bool D is non empty finite V39() set
F | D is Relation-like D -defined REAL -valued Function-like finite V49() V50() V51() Element of bool [:D,REAL:]
dom (F | D) is finite Element of bool D
(dom F) /\ D is finite Element of bool D