:: REARRAN1 semantic presentation

bool REAL is non empty non trivial non finite 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

is non empty non trivial non finite V49() V50() V51() set
bool is non empty non trivial non finite set
{} is set

{{},1} is finite set
is non empty non trivial non finite V49() set
bool is non empty non trivial non finite set
is non empty non trivial non finite V49() set
bool is non empty non trivial non finite set
is non empty non trivial non finite V49() V50() V51() set
bool is non empty non trivial non finite set
is non empty non trivial RAT -valued non finite V49() V50() V51() set
bool is non empty non trivial non finite set
is non empty non trivial RAT -valued non finite V49() V50() V51() set
bool is non empty non trivial non finite set
is non empty non trivial RAT -valued INT -valued non finite V49() V50() V51() set
bool is non empty non trivial non finite set
is non empty non trivial RAT -valued INT -valued non finite V49() V50() V51() set
bool is non empty non trivial non finite set

bool is non empty set

D is non empty set

[:D,C:] is V49() V50() V51() set
bool [:D,C:] is non empty set

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

PFuncs (D,REAL) is non empty functional PartFunc-set of 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

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 . F is set

D is non empty finite set
bool D is non empty finite V39() set

C . (len C) is set

F is finite set

D is non empty finite set
bool D is non empty finite V39() set

F is non empty finite set

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) - (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 finite V39() 1 -element set
c is set

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

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

{F} is non empty trivial finite V39() 1 -element set
b is non empty finite set
bool b is non empty finite V39() 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) \/ () is finite set
(bool F) \/ (bool F) is finite V39() set

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

d . (x + 1) is set

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

c . x is set

C is non empty finite set

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

union (bool D) is finite set
D is non empty finite set
bool D is non empty finite V39() set

union (bool D) is finite set
F is finite set

union (bool D) is finite set

D . C is set

D . (C + 1) is set

D . F is set

(len D) - 1 is V11() V12() ext-real V47() Element of REAL

D . C is set

D . F is set
D . 0 is set

D . A is set
C 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 . C is set

D . (C + 1) is set
D is non empty finite set
bool D is non empty finite V39() set

C . (len C) is set

D is non empty finite set
bool D is non empty finite V39() set

D is non empty finite set
bool D is non empty finite V39() set

C . F is set

C . A is set

B is finite set

D is non empty finite set
bool D is non empty finite V39() set

(len C) - 1 is V11() V12() ext-real V47() Element of REAL

C . F is set

C . (F + 1) is set

C is non empty finite set
bool C is non empty finite V39() set

F . D is set

C is non empty finite set
bool C is non empty finite V39() set

F . D is set

C is non empty finite set
bool C is non empty finite V39() set

(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

B is finite set

D - D is V11() V12() ext-real V47() set
D is non empty finite set
bool D is non empty finite V39() set

C . 1 is set

F is finite set

A is set
{A} is non empty trivial finite 1 -element set

B is Element of D
{B} is non empty trivial finite 1 -element set

C is non empty finite set
bool C is non empty finite V39() set

(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

A is finite set

A \ B is finite Element of bool A
bool A is non empty finite V39() set

(D + 1) - D is V11() V12() ext-real V47() Element of REAL
b is set
{b} is non empty trivial finite 1 -element set

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

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

(card D) - 1 is V11() V12() ext-real V47() Element of REAL
max (0,((card D) - 1)) is V11() V12() ext-real set

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

A is finite Element of bool D

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

C . d is set
(len (c ^ <*A*>)) - 1 is V11() V12() ext-real V47() Element of REAL

c . m1 is set
D \ (C . d) is finite Element of bool D
mi is finite set

(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

(c ^ <*A*>) . (m1 + 1) is set

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

C . d is set
D \ (C . d) is finite Element of bool D

(len C) - 1 is V11() V12() ext-real V47() Element of REAL

C . (d + 1) is set

(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

c . d is set

(len F) - 1 is V11() V12() ext-real V47() Element of REAL

(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
F . B is set
A . B is set

(len C) - 1 is V11() V12() ext-real V47() Element of REAL

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

(len F) - 1 is V11() V12() ext-real V47() Element of REAL

(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

(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

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

C is non empty finite set
bool C is non empty finite V39() set

PFuncs (C,REAL) is non empty functional PartFunc-set of C, REAL

dom F is finite Element of bool D
bool D is non empty finite V39() set

dom b is finite set

dom c is finite set

(dom F) /\ D is finite Element of bool D
dom (F | D) is finite Element of bool D

mi is finite set

m1 is finite set

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

PFuncs (C,REAL) is non empty functional PartFunc-set of 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

(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

C is non empty finite set
bool C is non empty finite V39() set

(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

PFuncs (C,REAL) is non empty functional PartFunc-set of 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

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

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

F is Element of D

B . 1 is set

PFuncs (D,REAL) is non empty functional PartFunc-set of 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 ((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 (((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

B . d is set

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

(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

(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

(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

(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

(MIM (FinS (A,C))) . x is V11() V12() ext-real Element of REAL

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

{ } is set

[:(Seg d),:] is RAT -valued INT -valued finite V49() V50() V51() V52() set
bool [:(Seg d),:] is non empty finite V39() set

(len (MIM (FinS (A,C)))) - d is V11() V12() ext-real V47() Element of REAL

B . x is set

B . x is set

(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

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

(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

(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

(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

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

(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

((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

(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

(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

(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

((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

(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

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

F is Element of D

(FinS (A,C)) . 1 is V11() V12() ext-real Element of REAL

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

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