:: REARRAN1 semantic presentation

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

{ b

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