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