:: ABIAN semantic presentation

REAL is V58() V59() V60() V64() V76() V77() V79() set
NAT is non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() Element of bool REAL
bool REAL is non empty set
COMPLEX is V58() V64() set
RAT is V58() V59() V60() V61() V64() set
INT is V58() V59() V60() V61() V62() V64() set
NAT is non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() set
bool NAT is non empty set
bool NAT is non empty set

bool is non empty set

bool is non empty set
{} is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() set
the empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() set is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() set
0 is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() Element of NAT
1 is non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() Element of NAT
K57(1) is ext-real non positive complex V18() integer Element of REAL
2 is non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() Element of NAT

n is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT

f is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
A is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * A is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * 0 is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() Element of NAT
n is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * n is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * 0 is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() Element of NAT

A is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT

f is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
2 * f is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(2 * f) + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT

2 * (- f) is ext-real complex V18() integer set
f + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
- (f + 1) is ext-real complex V18() integer set
2 * (- (f + 1)) is ext-real complex V18() integer set
(2 * (- (f + 1))) + 1 is ext-real complex V18() integer set

(2 * A) + 1 is ext-real complex V18() integer set

2 * (f - A) is ext-real complex V18() integer set

n is ext-real complex V18() integer () set

2 * A is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * A is ext-real complex V18() integer () set
(2 * A) + 1 is ext-real complex V18() integer () set

2 * (A + 1) is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * A is ext-real complex V18() integer () set

2 * (A - 1) is ext-real complex V18() integer () set
(2 * (A - 1)) + 1 is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * A is ext-real complex V18() integer () set
(2 * A) + 1 is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set

2 * (f * A) is ext-real complex V18() integer () set
A * n is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set
(2 * x) + 1 is ext-real complex V18() integer () set
x * (2 * f) is ext-real complex V18() integer () set

(x * (2 * f)) + (x * 1) is ext-real complex V18() integer set

((x * (2 * f)) + (x * 1)) + (f * 1) is ext-real complex V18() integer set
2 * (((x * (2 * f)) + (x * 1)) + (f * 1)) is ext-real complex V18() integer () set
(2 * (((x * (2 * f)) + (x * 1)) + (f * 1))) + 1 is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set

2 * (x + f) is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set

2 * (x + f) is ext-real complex V18() integer () set
(2 * (x + f)) + 1 is ext-real complex V18() integer () set
A + n is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set
(2 * x) + 1 is ext-real complex V18() integer () set

(x + f) + 1 is ext-real complex V18() integer set
2 * ((x + f) + 1) is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set

2 * (x - f) is ext-real complex V18() integer () set
(2 * (x - f)) - 1 is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set

2 * (f - x) is ext-real complex V18() integer () set
(2 * (f - x)) + 1 is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
A is ext-real complex V18() integer () set

2 * f is ext-real complex V18() integer () set
(2 * f) + 1 is ext-real complex V18() integer () set

2 * x is ext-real complex V18() integer () set
(2 * x) + 1 is ext-real complex V18() integer () set

2 * (x - f) is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * 1 is ext-real non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
A is ext-real complex V18() integer () set
n + A is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set

2 * 1 is ext-real non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
A is ext-real complex V18() integer () set
n + A is ext-real complex V18() integer () set
n is set
[:n,n:] is set
bool [:n,n:] is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
f is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
iter (A,f) is Relation-like set
n is non empty V58() V59() V60() V61() V62() V63() V74() V76() Element of bool NAT
min n is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
n is non empty set
[:n,n:] is non empty set
bool [:n,n:] is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
f is Element of n
(n,A,0) . f is Element of n
dom A is set
rng A is set
(dom A) \/ (rng A) is set
field A is set

(id ()) . f is set
n is non empty set
[:n,n:] is non empty set
bool [:n,n:] is non empty set
A is Element of n
f is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
f . A is Element of n
dom f is set
f . A is set
n is set
n is set
bool n is non empty set
bool (bool n) is non empty set
A is Element of bool (bool n)
union A is Element of bool n
bool n is non empty Element of bool (bool n)
bool (bool n) is non empty Element of bool (bool (bool n))
bool (bool n) is non empty set
bool (bool (bool n)) is non empty set
union (bool (bool n)) is Element of bool (bool n)
union (union (bool (bool n))) is Element of bool n
union (bool n) is Element of bool n
n is set
bool n is non empty set
bool (bool n) is non empty set
{n} is non empty finite set
A is Element of bool (bool n)
union A is Element of bool n
n is set
[:n,n:] is set
bool [:n,n:] is non empty set
bool n is non empty set
bool (bool n) is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
f is non empty ( bool (bool n)) Element of bool (bool n)
x is set
A . x is set
dom A is set
union f is Element of bool n
E2c is set
A .: E2c is set
n is set
[:n,n:] is set
bool [:n,n:] is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
f is set
(n,A,0) . f is set
f is set
x is set
E2c is set
E1c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1c) . f is set
E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1) . x is set
E1c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1c) . f is set
E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1) . x is set
E2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2) . x is set
E3 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E3) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E3) . E2c is set
E2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2) . x is set
E3 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E3) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E3) . E2c is set
dom (n,A,E2) is set
dom (n,A,E1) is set
dom (n,A,E1c) is set
dom (n,A,E3) is set
E1c + E2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(E1c + E2)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,(E1c + E2)) . f is set
(n,A,E1c) * (n,A,E2) is Relation-like Function-like set
((n,A,E1c) * (n,A,E2)) . f is set
(n,A,E2) . ((n,A,E1) . x) is set
(n,A,E1) * (n,A,E2) is Relation-like Function-like set
((n,A,E1) * (n,A,E2)) . x is set
E2 + E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(E2 + E1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,(E2 + E1)) . x is set
(n,A,E2) * (n,A,E1) is Relation-like Function-like set
((n,A,E2) * (n,A,E1)) . x is set
(n,A,E1) . ((n,A,E3) . E2c) is set
(n,A,E3) * (n,A,E1) is Relation-like Function-like set
((n,A,E3) * (n,A,E1)) . E2c is set
E1 + E3 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(E1 + E3)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,(E1 + E3)) . E2c is set
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x) . f is set
Y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,Y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,Y) . x is set
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x) . f is set
Y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,Y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,Y) . x is set
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x) . f is set
Y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,Y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,Y) . x is set
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x) . x is set
Y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,Y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,Y) . E2c is set
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x) . f is set
Y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,Y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,Y) . x is set
c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,c) . x is set
xx is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,xx) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,xx) . E2c is set
f is set
x is set
E2c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2c) . f is set
E1c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1c) . x is set
f is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
x is set
E2c is set
[x,E2c] is set
{x,E2c} is non empty finite set
{x} is non empty finite set
{{x,E2c},{x}} is non empty with_non-empty_elements non empty-membered finite V69() set
E1c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1c) . x is set
E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1) . E2c is set
f is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
x is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
E2c is set
E1c is set
[E2c,E1c] is set
{E2c,E1c} is non empty finite set
{E2c} is non empty finite set
{{E2c,E1c},{E2c}} is non empty with_non-empty_elements non empty-membered finite V69() set
E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1) . E2c is set
E2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2) . E1c is set
E1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E1) . E2c is set
E2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2) . E1c is set
n is non empty set
[:n,n:] is non empty set
bool [:n,n:] is non empty set
bool n is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A) is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
Class (n,A) is non empty with_non-empty_elements non empty-membered a_partition of n
f is non empty Element of Class (n,A)
x is Element of f
A . x is Element of n
dom A is set
rng A is set
(dom A) \/ (rng A) is set
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
E2c is set
Class ((n,A),E2c) is Element of bool n
{E2c} is non empty finite set
(n,A) .: {E2c} is set
(n,A,1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,1) . x is Element of n
field A is set

(id ()) . (A . x) is set
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,0) . (A . x) is Element of n
[(A . x),x] is Element of [:n,f:]
[:n,f:] is non empty set
{(A . x),x} is non empty finite set
{(A . x)} is non empty finite set
{{(A . x),x},{(A . x)}} is non empty with_non-empty_elements non empty-membered finite V69() set
n is non empty set
[:n,n:] is non empty set
bool [:n,n:] is non empty set
bool n is non empty set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A) is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
Class (n,A) is non empty with_non-empty_elements non empty-membered a_partition of n
f is non empty Element of Class (n,A)
x is Element of f
E2c is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,E2c) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,E2c) . x is Element of n
dom A is set
rng A is set
(dom A) \/ (rng A) is set
field A is set

(id ()) . ((n,A,E2c) . x) is set
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,0) . ((n,A,E2c) . x) is Element of n
[((n,A,E2c) . x),x] is Element of [:n,f:]
[:n,f:] is non empty set
{((n,A,E2c) . x),x} is non empty finite set
{((n,A,E2c) . x)} is non empty finite set
{{((n,A,E2c) . x),x},{((n,A,E2c) . x)}} is non empty with_non-empty_elements non empty-membered finite V69() set
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
E1c is set
Class ((n,A),E1c) is Element of bool n
{E1c} is non empty finite set
(n,A) .: {E1c} is set
n is set
n is set
A is non empty non empty-membered set
[:n,A:] is set
bool [:n,A:] is non empty set
f is non empty set

[:n,{f}:] is set
bool [:n,{f}:] is non empty set
x is Relation-like n -defined A -valued Function-like V33(n,A) Element of bool [:n,A:]
E2c is set
dom x is set
x . E2c is set
n is non empty set
A is non empty non empty-membered set
[:n,A:] is non empty set
bool [:n,A:] is non empty set

x is Element of n
f . x is Element of A
dom f is set

n is non empty set
bool n is non empty Element of bool (bool n)
bool n is non empty set
bool (bool n) is non empty set
n is non empty set
[:n,n:] is non empty set
bool [:n,n:] is non empty non empty-membered set
A is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
bool n is non empty non empty-membered Element of bool (bool n)
bool n is non empty non empty-membered set
bool (bool n) is non empty non empty-membered set
[:(bool n),(bool n),(bool n):] is non empty set
(n,A) is Relation-like n -defined n -valued V29(n) V38() V40() V45() Element of bool [:n,n:]
Class (n,A) is non empty with_non-empty_elements non empty-membered a_partition of n
[:(bool n),(bool n),(bool n):] is non empty set
[:(bool n),(bool n),(bool n):] is non empty Element of bool [:(bool n),(bool n),(bool n):]
bool [:(bool n),(bool n),(bool n):] is non empty non empty-membered set
x is non empty Element of Class (n,A)
E2c is set
Class ((n,A),E2c) is Element of bool n
{E2c} is non empty finite set
(n,A) .: {E2c} is set
E1c is Element of x
{ b1 where b1 is Element of x : S2[b1] } is set
bool x is non empty non empty-membered set
{ b1 where b1 is Element of x : S3[b1] } is set
E2 is Element of bool n
x is Element of bool n
f is Element of bool n
[E2,x,f] is Element of [:(bool n),(bool n),(bool n):]
Y is Element of [:(bool n),(bool n),(bool n):]
Y `1_3 is Element of bool n
Y `2_3 is Element of bool n
(Y `1_3) \/ (Y `2_3) is Element of bool n
Y `3_3 is Element of bool n
((Y `1_3) \/ (Y `2_3)) \/ (Y `3_3) is Element of bool n
A .: (Y `1_3) is set
A .: (Y `2_3) is set
A .: (Y `3_3) is set
Y `2_3 is Element of bool n
Y `3_3 is Element of bool n
Y `1_3 is Element of bool n
(Y `1_3) \/ (Y `2_3) is Element of bool n
((Y `1_3) \/ (Y `2_3)) \/ (Y `3_3) is Element of bool n
c is set
xx is Element of x
YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,YY) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,YY) . xx is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,cc) . E1c is Element of n
xx is Element of x
YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,YY) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,YY) . xx is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,cc) . E1c is Element of n
c is set
xx is Element of x
[xx,E1c] is Element of [:x,x:]
[:x,x:] is non empty set
{xx,E1c} is non empty finite set
{xx} is non empty finite set
{{xx,E1c},{xx}} is non empty with_non-empty_elements non empty-membered finite V69() set
YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,YY) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(YY) . xx is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(cc) . E1c is Element of n
dom H1(cc) is set
dom H1(YY) is set
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
x1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(x1 + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1 + 1) . xx is Element of n
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1) * A is Relation-like Function-like set
(H1(x1) * A) . xx is set
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k1) . E1c is Element of n
A . (H1(k1) . E1c) is Element of n
H1(k1) * A is Relation-like Function-like set
(H1(k1) * A) . E1c is set
k1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(k1 + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k1 + 1) . E1c is Element of n
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
x1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(x1 + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1 + 1) . xx is Element of n
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1) * A is Relation-like Function-like set
(H1(x1) * A) . xx is set
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k1) . E1c is Element of n
A . (H1(k1) . E1c) is Element of n
H1(k1) * A is Relation-like Function-like set
(H1(k1) * A) . E1c is set
k1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(k1 + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k1 + 1) . E1c is Element of n
A .: E2 is set
c is set
dom A is set
xx is set
A . xx is set
YY is Element of x
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,cc) . YY is Element of n
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x1) . E1c is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(cc) . YY is Element of n
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1) . E1c is Element of n
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
l1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
l1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(k1) is set
(n,A,l1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(l1) is set
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,r) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(r) is set
r + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(r + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(r + 1) . YY is Element of n
A * H1(r) is Relation-like Function-like set
(A * H1(r)) . YY is set
A . YY is Element of n
H1(r) . (A . YY) is Element of n
(n,A,k) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(k) is set
H1(r) * A is Relation-like Function-like set
(H1(r) * A) . YY is set
H1(r) . YY is Element of n
A . (H1(r) . YY) is Element of n
H1(k1) * A is Relation-like Function-like set
(H1(k1) * A) . YY is set
A . ((H1(k1) * A) . YY) is set
H1(l1) . E1c is Element of n
A . (H1(l1) . E1c) is Element of n
A . (A . (H1(l1) . E1c)) is Element of n
H1(l1) * A is Relation-like Function-like set
(H1(l1) * A) . E1c is set
A . ((H1(l1) * A) . E1c) is set
H1(k) . E1c is Element of n
A . (H1(k) . E1c) is Element of n
H1(k) * A is Relation-like Function-like set
(H1(k) * A) . E1c is set
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,r) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(r) . E1c is Element of n
Odl is Element of x
A .: (Y `1_3) is set
A .: x is set
c is set
dom A is set
xx is set
A . xx is set
YY is Element of x
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,cc) . YY is Element of n
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,x1) . E1c is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(cc) . YY is Element of n
x1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,x1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x1) . E1c is Element of n
l1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
l1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,l1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(l1) is set
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(k1) is set
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,r) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(r) is set
r + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(r + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(r + 1) . YY is Element of n
A * H1(r) is Relation-like Function-like set
(A * H1(r)) . YY is set
A . YY is Element of n
H1(r) . (A . YY) is Element of n
(n,A,k) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(k) is set
H1(r) * A is Relation-like Function-like set
(H1(r) * A) . YY is set
H1(r) . YY is Element of n
A . (H1(r) . YY) is Element of n
H1(l1) * A is Relation-like Function-like set
(H1(l1) * A) . YY is set
A . ((H1(l1) * A) . YY) is set
H1(k1) . E1c is Element of n
A . (H1(k1) . E1c) is Element of n
A . (A . (H1(k1) . E1c)) is Element of n
H1(k1) * A is Relation-like Function-like set
(H1(k1) * A) . E1c is set
A . ((H1(k1) * A) . E1c) is set
H1(k) . E1c is Element of n
A . (H1(k) . E1c) is Element of n
H1(k) * A is Relation-like Function-like set
(H1(k) * A) . E1c is set
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,r) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(r) . E1c is Element of n
Odl is Element of x
A .: (Y `2_3) is set
E2 is Element of bool n
x is Element of bool n
Y is set
c is Element of x
xx is Element of x
YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,YY) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,YY) . xx is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,cc) . E1c is Element of n
YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,YY) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(YY) . xx is Element of n
cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,cc) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(cc) . E1c is Element of n
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,k1) . c is Element of n
l1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,l1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,l1) . E1c is Element of n
k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k1) . c is Element of n
l1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,l1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(l1) . E1c is Element of n
dom H1(k1) is set
dom H1(l1) is set
cc + k1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(cc + k1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
x1 is Element of x
H1(cc + k1) . x1 is Element of n
H1(k1) * H1(cc) is Relation-like Function-like set
(H1(k1) * H1(cc)) . x1 is set
H1(cc) . (H1(l1) . E1c) is Element of n
H1(l1) * H1(cc) is Relation-like Function-like set
(H1(l1) * H1(cc)) . E1c is set
l1 + cc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(l1 + cc)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(l1 + cc) . E1c is Element of n
dom H1(cc) is set
dom H1(YY) is set
l1 + YY is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(l1 + YY)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(l1 + YY) . x1 is Element of n
H1(YY) * H1(l1) is Relation-like Function-like set
(H1(YY) * H1(l1)) . x1 is set
H1(l1) . (H1(cc) . E1c) is Element of n
H1(cc) * H1(l1) is Relation-like Function-like set
(H1(cc) * H1(l1)) . E1c is set
k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
Odl is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
k + Odl is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(k + Odl)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(k + Odl) is set
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
r + r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(r + r)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H1(r + r) is set
(r + r) - (k + Odl) is ext-real complex V18() integer () set
H1(k + Odl) . x1 is Element of n
odl is Element of n
Odl is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,c1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(c1) . odl is Element of n
H1(c1) . (H1(k + Odl) . x1) is Element of n
H1(k + Odl) * H1(c1) is Relation-like Function-like set
(H1(k + Odl) * H1(c1)) . x1 is set
c1 + (k + Odl) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(c1 + (k + Odl))) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(c1 + (k + Odl)) . x1 is Element of n
(k + Odl) - (r + r) is ext-real complex V18() integer () set
H1(r + r) . x1 is Element of n
odl is Element of n
Odl is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,c1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(c1) . odl is Element of n
H1(c1) . (H1(r + r) . x1) is Element of n
H1(r + r) * H1(c1) is Relation-like Function-like set
(H1(r + r) * H1(c1)) . x1 is set
c1 + (r + r) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,(c1 + (r + r))) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(c1 + (r + r)) . x1 is Element of n
k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,k) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
r is Element of n
(n,A,k) . r is Element of n
k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
(n,A,k) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
r is Element of n
H1(k) . r is Element of n
r is Element of x
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . a1 = r } is set
bool NAT is non empty non empty-membered Element of bool ()
bool () is non empty non empty-membered set
Odl is Element of x
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . Odl = r } is set
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : S4[b1] } is set
[:x,():] is non empty set
bool [:x,():] is non empty non empty-membered set

Odl is set
dom Odl is set
odl is Element of x
Odl . odl is V58() V59() V60() V61() V62() V63() V76() Element of bool NAT
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . odl = r } is set
c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
k * c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(k * c1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k * c1) . r is Element of n
dom H1(k) is set
c1 + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
k * (c1 + 1) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(k * (c1 + 1))) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k * (c1 + 1)) . r is Element of n
k * 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(k * c1) + (k * 1) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,((k * c1) + (k * 1))) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1((k * c1) + (k * 1)) . r is Element of n
H1(k) * H1(k * c1) is Relation-like Function-like set
(H1(k) * H1(k * c1)) . r is set
k * 0 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(k * 0)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k * 0) . r is Element of n
[odl,r] is Element of [:x,x:]
[:x,x:] is non empty set
{odl,r} is non empty finite set
{odl} is non empty finite set
{{odl,r},{odl}} is non empty with_non-empty_elements non empty-membered finite V69() set
c1 is set
Class ((n,A),c1) is Element of bool n
{c1} is non empty finite set
(n,A) .: {c1} is set
c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,c1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,c1) . odl is Element of n
d1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,d1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,d1) . r is Element of n
dom H1(d1) is set
d1 mod k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
d1 div k is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
d1 / k is ext-real complex V18() set
[\(d1 / k)/] is ext-real complex V18() integer set
dom H1(c1) is set
2 * 0 is empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() () Element of NAT
k - (d1 mod k) is ext-real complex V18() integer set
k * (d1 div k) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(k * (d1 div k)) + (d1 mod k) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
d2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
d1 + d2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(d1 div k) + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
k * ((d1 div k) + 1) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
d2 + c1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(d2 + c1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(d2 + c1) . odl is Element of n
(n,A,d2) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(c1) * H1(d2) is Relation-like Function-like set
(H1(c1) * H1(d2)) . odl is set
H1(d1) . r is Element of n
H1(d2) . (H1(d1) . r) is Element of n
H1(d1) * H1(d2) is Relation-like Function-like set
(H1(d1) * H1(d2)) . r is set
(n,A,(k * ((d1 div k) + 1))) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(k * ((d1 div k) + 1)) . r is Element of n
c1 + d2 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
Odl . Odl is set

[:x,NAT:] is non empty set
bool [:x,NAT:] is non empty non empty-membered set

{ b1 where b1 is Element of x : S4[b1] } is set
{r} is non empty finite Element of bool x
{ b1 where b1 is Element of x : S4[b1] } \ {r} is Element of bool { b1 where b1 is Element of x : S4[b1] }
bool { b1 where b1 is Element of x : S4[b1] } is non empty set
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1( 0 ) . r is Element of n
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . r = r } is set
Odl . r is non empty V58() V59() V60() V61() V62() V63() V74() V76() Element of bool NAT
min (Odl . r) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
odl . r is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
{ b1 where b1 is Element of x : S5[b1] } is set
d3 is Element of x
A . d3 is Element of n
odl . (A . d3) is set
odl . d3 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(odl . d3) - 1 is ext-real complex V18() integer set
b is Element of x
odl . b is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
Odl . d3 is non empty V58() V59() V60() V61() V62() V63() V74() V76() Element of bool NAT
min (Odl . d3) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . d3 = r } is set
xx is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,xx) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,xx) . d3 is Element of n
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT

dom A is set
xx is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,xx) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(xx) . b is Element of n
A * H1(xx) is Relation-like Function-like set
(A * H1(xx)) . d3 is set
xx + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(xx + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(xx + 1) . d3 is Element of n
(n,A,x) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(x) . d3 is Element of n
{ b1 where b1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H1(b1) . b = r } is set
ox is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,ox) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,ox) . d3 is Element of n
Odl . b is non empty V58() V59() V60() V61() V62() V63() V74() V76() Element of bool NAT
y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
min (Odl . b) is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
y + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,(y + 1)) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H1(y + 1) . d3 is Element of n
(n,A,y) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
A * H1(y) is Relation-like Function-like set
(A * H1(y)) . d3 is set
H1(y) . b is Element of n
ox is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
(n,A,ox) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
(n,A,ox) . b is Element of n
d1 is Element of bool n
A .: d1 is set
d2 is Element of bool n
d3 is set
dom A is set
b is set
A . b is set
y is Element of x
odl . y is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
xx is Element of x
odl . xx is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
x is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
x - 1 is ext-real complex V18() integer () set
{ b1 where b1 is Element of x : S4[b1] } \/ d2 is set
d3 is set
b is Element of x
odl . b is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
b is Element of x
odl . b is ext-real V10() V11() V12() V16() complex V18() integer V57() V58()