:: 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
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is set
bool [:COMPLEX,REAL:] 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 complex V18() integer set
A is ext-real complex V18() integer set
2 * A is ext-real complex V18() integer set
n 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 complex V18() integer set
2 * A is ext-real complex V18() integer set
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
n is ext-real complex V18() integer set
2 * n is ext-real complex V18() integer set
n is ext-real complex V18() integer set
A 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 complex V18() integer set
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
- f is ext-real complex V18() integer set
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
A 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
f is ext-real complex V18() integer set
2 * f is ext-real complex V18() integer set
f - A 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 * n is ext-real complex V18() integer set
n is ext-real complex V18() integer () set
n + 1 is ext-real complex V18() integer set
A is ext-real complex V18() integer set
2 * A is ext-real complex V18() integer () set
n is ext-real complex V18() integer () set
n + 1 is ext-real complex V18() integer set
A 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
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
n - 1 is ext-real complex V18() integer set
A is ext-real complex V18() integer set
2 * A is ext-real complex V18() integer () set
A - 1 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
n - 1 is ext-real complex V18() integer set
A 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
A is ext-real complex V18() integer set
n * A is ext-real complex V18() integer set
f is ext-real complex V18() integer set
2 * f is ext-real complex V18() integer () set
f * A 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
n * A is ext-real complex V18() integer set
f 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
x 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 * 1 is ext-real complex V18() integer set
(x * (2 * f)) + (x * 1) is ext-real complex V18() integer set
f * 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
n + A is ext-real complex V18() integer set
f is ext-real complex V18() integer set
2 * f is ext-real complex V18() integer () set
x is ext-real complex V18() integer set
2 * x is ext-real complex V18() integer () set
x + f 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
n + A is ext-real complex V18() integer set
f 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
x is ext-real complex V18() integer set
2 * x is ext-real complex V18() integer () set
x + f 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
n + A is ext-real complex V18() integer set
f 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
x 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
A + n is ext-real complex V18() integer set
x + f 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
n - A is ext-real complex V18() integer set
f 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
x is ext-real complex V18() integer set
2 * x is ext-real complex V18() integer () set
x - f 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
f 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
x is ext-real complex V18() integer set
2 * x is ext-real complex V18() integer () set
f - 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
n - A is ext-real complex V18() integer set
f 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
x 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 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
n + 2 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
n + 2 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 (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field A)) . 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 (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field A)) . (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 (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field A)) . ((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 Relation-like n -defined {f} -valued Function-like V33(n,{f}) Element of bool [:n,{f}:]
{f} is non empty with_non-empty_elements non empty-membered finite 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
f is Relation-like non-empty n -defined A -valued Function-like V33(n,A) Element of bool [:n,A:]
x is Element of n
f . x is Element of A
dom f is set
rng f is with_non-empty_elements 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
{ b₁ where b₁ is Element of x : S₂[b₁] } is set
bool x is non empty non empty-membered set
{ b₁ where b₁ is Element of x : S₃[b₁] } 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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(cc) . E1c is Element of n
dom H<sub>1</sub>(cc) is set
dom H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(x1) * A is Relation-like Function-like set
(H<sub>1</sub>(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:]
H<sub>1</sub>(k1) . E1c is Element of n
A . (H<sub>1</sub>(k1) . E1c) is Element of n
H<sub>1</sub>(k1) * A is Relation-like Function-like set
(H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(x1) * A is Relation-like Function-like set
(H<sub>1</sub>(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:]
H<sub>1</sub>(k1) . E1c is Element of n
A . (H<sub>1</sub>(k1) . E1c) is Element of n
H<sub>1</sub>(k1) * A is Relation-like Function-like set
(H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(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 H<sub>1</sub>(k1) is set
(n,A,l1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H<sub>1</sub>(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 H<sub>1</sub>(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:]
H<sub>1</sub>(r + 1) . YY is Element of n
A * H<sub>1</sub>(r) is Relation-like Function-like set
(A * H<sub>1</sub>(r)) . YY is set
A . YY is Element of n
H<sub>1</sub>(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 H<sub>1</sub>(k) is set
H<sub>1</sub>(r) * A is Relation-like Function-like set
(H<sub>1</sub>(r) * A) . YY is set
H<sub>1</sub>(r) . YY is Element of n
A . (H<sub>1</sub>(r) . YY) is Element of n
H<sub>1</sub>(k1) * A is Relation-like Function-like set
(H<sub>1</sub>(k1) * A) . YY is set
A . ((H<sub>1</sub>(k1) * A) . YY) is set
H<sub>1</sub>(l1) . E1c is Element of n
A . (H<sub>1</sub>(l1) . E1c) is Element of n
A . (A . (H<sub>1</sub>(l1) . E1c)) is Element of n
H<sub>1</sub>(l1) * A is Relation-like Function-like set
(H<sub>1</sub>(l1) * A) . E1c is set
A . ((H<sub>1</sub>(l1) * A) . E1c) is set
H<sub>1</sub>(k) . E1c is Element of n
A . (H<sub>1</sub>(k) . E1c) is Element of n
H<sub>1</sub>(k) * A is Relation-like Function-like set
(H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H₁(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:]
H₁(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 H₁(l1) is set
(n,A,k1) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
dom H₁(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 H₁(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:]
H₁(r + 1) . YY is Element of n
A * H₁(r) is Relation-like Function-like set
(A * H₁(r)) . YY is set
A . YY is Element of n
H₁(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 H₁(k) is set
H₁(r) * A is Relation-like Function-like set
(H₁(r) * A) . YY is set
H₁(r) . YY is Element of n
A . (H₁(r) . YY) is Element of n
H₁(l1) * A is Relation-like Function-like set
(H₁(l1) * A) . YY is set
A . ((H₁(l1) * A) . YY) is set
H₁(k1) . E1c is Element of n
A . (H₁(k1) . E1c) is Element of n
A . (A . (H₁(k1) . E1c)) is Element of n
H₁(k1) * A is Relation-like Function-like set
(H₁(k1) * A) . E1c is set
A . ((H₁(k1) * A) . E1c) is set
H₁(k) . E1c is Element of n
A . (H₁(k) . E1c) is Element of n
H₁(k) * A is Relation-like Function-like set
(H₁(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:]
H₁(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(l1) . E1c is Element of n
dom H<sub>1</sub>(k1) is set
dom H<sub>1</sub>(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
H<sub>1</sub>(cc + k1) . x1 is Element of n
H<sub>1</sub>(k1) * H<sub>1</sub>(cc) is Relation-like Function-like set
(H<sub>1</sub>(k1) * H<sub>1</sub>(cc)) . x1 is set
H<sub>1</sub>(cc) . (H<sub>1</sub>(l1) . E1c) is Element of n
H<sub>1</sub>(l1) * H<sub>1</sub>(cc) is Relation-like Function-like set
(H<sub>1</sub>(l1) * H<sub>1</sub>(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:]
H<sub>1</sub>(l1 + cc) . E1c is Element of n
dom H<sub>1</sub>(cc) is set
dom H<sub>1</sub>(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:]
H<sub>1</sub>(l1 + YY) . x1 is Element of n
H<sub>1</sub>(YY) * H<sub>1</sub>(l1) is Relation-like Function-like set
(H<sub>1</sub>(YY) * H<sub>1</sub>(l1)) . x1 is set
H<sub>1</sub>(l1) . (H<sub>1</sub>(cc) . E1c) is Element of n
H<sub>1</sub>(cc) * H<sub>1</sub>(l1) is Relation-like Function-like set
(H<sub>1</sub>(cc) * H<sub>1</sub>(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 H<sub>1</sub>(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 H<sub>1</sub>(r + r) is set
(r + r) - (k + Odl) is ext-real complex V18() integer () set
H<sub>1</sub>(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:]
H<sub>1</sub>(c1) . odl is Element of n
H<sub>1</sub>(c1) . (H<sub>1</sub>(k + Odl) . x1) is Element of n
H<sub>1</sub>(k + Odl) * H<sub>1</sub>(c1) is Relation-like Function-like set
(H<sub>1</sub>(k + Odl) * H<sub>1</sub>(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:]
H<sub>1</sub>(c1 + (k + Odl)) . x1 is Element of n
(k + Odl) - (r + r) is ext-real complex V18() integer () set
H<sub>1</sub>(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:]
H<sub>1</sub>(c1) . odl is Element of n
H<sub>1</sub>(c1) . (H<sub>1</sub>(r + r) . x1) is Element of n
H<sub>1</sub>(r + r) * H<sub>1</sub>(c1) is Relation-like Function-like set
(H<sub>1</sub>(r + r) * H<sub>1</sub>(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:]
H<sub>1</sub>(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
H<sub>1</sub>(k) . r is Element of n
r is Element of x
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . a<sub>1</sub> = r } is set
bool NAT is non empty non empty-membered Element of bool (bool NAT)
bool (bool NAT) is non empty non empty-membered set
Odl is Element of x
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . Odl = r } is set
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : S<sub>4</sub>[b<sub>1</sub>] } is set
[:x,(bool NAT):] is non empty set
bool [:x,(bool NAT):] is non empty non empty-membered set
Odl is Relation-like x -defined bool NAT -valued Function-like V33(x, bool NAT) Element of bool [:x,(bool NAT):]
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
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . 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:]
H<sub>1</sub>(k * c1) . r is Element of n
dom H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>((k * c1) + (k * 1)) . r is Element of n
H<sub>1</sub>(k) * H<sub>1</sub>(k * c1) is Relation-like Function-like set
(H<sub>1</sub>(k) * H<sub>1</sub>(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:]
H<sub>1</sub>(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 H<sub>1</sub>(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 H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(c1) * H<sub>1</sub>(d2) is Relation-like Function-like set
(H<sub>1</sub>(c1) * H<sub>1</sub>(d2)) . odl is set
H<sub>1</sub>(d1) . r is Element of n
H<sub>1</sub>(d2) . (H<sub>1</sub>(d1) . r) is Element of n
H<sub>1</sub>(d1) * H<sub>1</sub>(d2) is Relation-like Function-like set
(H<sub>1</sub>(d1) * H<sub>1</sub>(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:]
H<sub>1</sub>(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
Odl is Relation-like non-empty x -defined bool NAT -valued Function-like V33(x, bool NAT) Element of bool [:x,(bool NAT):]
[:x,NAT:] is non empty set
bool [:x,NAT:] is non empty non empty-membered set
odl is Relation-like x -defined NAT -valued Function-like V33(x, NAT ) Element of bool [:x,NAT:]
{ b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] } is set
{r} is non empty finite Element of bool x
{ b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] } \ {r} is Element of bool { b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] }
bool { b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] } is non empty set
(n,A,0) is Relation-like n -defined n -valued Function-like V33(n,n) Element of bool [:n,n:]
H<sub>1</sub>( 0 ) . r is Element of n
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . 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
{ b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>5</sub>[b<sub>1</sub>] } 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
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . 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
x - 1 is ext-real complex V18() integer set
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:]
H<sub>1</sub>(xx) . b is Element of n
A * H<sub>1</sub>(xx) is Relation-like Function-like set
(A * H<sub>1</sub>(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:]
H<sub>1</sub>(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:]
H<sub>1</sub>(x) . d3 is Element of n
{ b<sub>1</sub> where b<sub>1</sub> is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT : H<sub>1</sub>(b<sub>1</sub>) . 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:]
H<sub>1</sub>(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 * H<sub>1</sub>(y) is Relation-like Function-like set
(A * H<sub>1</sub>(y)) . d3 is set
H<sub>1</sub>(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
{ b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] } \/ 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() V59() V60() V61() V62() V63() V76() Element of NAT
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
d3 is Element of bool n
[d1,d2,d3] is Element of [:(bool n),(bool n),(bool n):]
b is Element of [:(bool n),(bool n),(bool n):]
b `1_3 is Element of bool n
b `2_3 is Element of bool n
(b `1_3) \/ (b `2_3) is Element of bool n
b `3_3 is Element of bool n
((b `1_3) \/ (b `2_3)) \/ (b `3_3) is Element of bool n
A .: (b `1_3) is set
A .: (b `2_3) is set
A .: (b `3_3) is set
b `1_3 is Element of bool n
b `2_3 is Element of bool n
b `3_3 is Element of bool n
d1 \/ d3 is Element of bool n
{ b<sub>1</sub> where b<sub>1</sub> is Element of x : S<sub>4</sub>[b<sub>1</sub>] } \/ d3 is set
(b `1_3) \/ (b `2_3) is Element of bool n
((b `1_3) \/ (b `2_3)) \/ (b `3_3) is Element of bool n
y is set
x is Element of x
odl . x 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
A .: (b `1_3) is set
A .: d2 is set
y is set
dom A is set
x is set
A . x is set
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
yc is Element of x
odl . yc is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
ox is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() () Element of NAT
ox - 1 is ext-real complex V18() integer () set
A .: (b `2_3) is set
A .: (b `3_3) is set
y is set
dom A is set
x is set
A . x is set
E2 is Element of bool n
x is Element of bool n
[:(Class (n,A)),[:(bool n),(bool n),(bool n):]:] is non empty set
bool [:(Class (n,A)),[:(bool n),(bool n),(bool n):]:] is non empty non empty-membered set
f is Relation-like Class (n,A) -defined [:(bool n),(bool n),(bool n):] -valued Function-like V33( Class (n,A),[:(bool n),(bool n),(bool n):]) Element of bool [:(Class (n,A)),[:(bool n),(bool n),(bool n):]:]
{ ((f . b<sub>1</sub>) `3_3) where b₁ is non empty Element of Class (n,A) : verum } is set
{ ((f . b₁) `2_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } is set
{ ((f . b<sub>1</sub>) `1_3) where b₁ is non empty Element of Class (n,A) : verum } is set
union { ((f . b₁) `1_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } is set
union { ((f . b<sub>1</sub>) `2_3) where b₁ is non empty Element of Class (n,A) : verum } is set
union { ((f . b₁) `3_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } is set
A .: (union { ((f . b<sub>1</sub>) `1_3) where b₁ is non empty Element of Class (n,A) : verum } ) is set
(union { ((f . b₁) `1_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } ) \/ (union { ((f . b<sub>1</sub>) `2_3) where b₁ is non empty Element of Class (n,A) : verum } ) is set
A .: (union { ((f . b₁) `2_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } ) is set
((union { ((f . b<sub>1</sub>) `1_3) where b₁ is non empty Element of Class (n,A) : verum } ) \/ (union { ((f . b₁) `2_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } )) \/ (union { ((f . b<sub>1</sub>) `3_3) where b₁ is non empty Element of Class (n,A) : verum } ) is set
A .: (union { ((f . b₁) `3_3) where b<sub>1</sub> is non empty Element of Class (n,A) : verum } ) is set
x is set
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `1_3 is Element of bool n
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `2_3 is Element of bool n
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `3_3 is Element of bool n
x is set
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `1_3 is Element of bool n
(f . c) `2_3 is Element of bool n
((f . c) `1_3) \/ ((f . c) `2_3) is Element of bool n
(f . c) `3_3 is Element of bool n
(((f . c) `1_3) \/ ((f . c) `2_3)) \/ ((f . c) `3_3) is Element of bool n
x is set
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `1_3 is Element of bool n
(f . c) `2_3 is Element of bool n
((f . c) `1_3) \/ ((f . c) `2_3) is Element of bool n
(f . c) `3_3 is Element of bool n
(((f . c) `1_3) \/ ((f . c) `2_3)) \/ ((f . c) `3_3) is Element of bool n
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
xx is set
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
xx is set
A . xx is set
YY is set
cc is non empty Element of Class (n,A)
f . cc is Element of [:(bool n),(bool n),(bool n):]
(f . cc) `1_3 is Element of bool n
(f . cc) `2_3 is Element of bool n
((f . cc) `1_3) \/ ((f . cc) `2_3) is Element of bool n
(f . cc) `3_3 is Element of bool n
(((f . cc) `1_3) \/ ((f . cc) `2_3)) \/ ((f . cc) `3_3) is Element of bool n
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
x1 is set
Class ((n,A),x1) is Element of bool n
{x1} is non empty finite set
(n,A) .: {x1} 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) . xx is set
field A is set
id (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field 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) . x is set
[x,xx] is set
{x,xx} is non empty finite set
{{x,xx},{x}} is non empty with_non-empty_elements non empty-membered finite V69() set
A .: YY is set
x is set
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `2_3 is Element of bool n
(f . c) `1_3 is Element of bool n
((f . c) `1_3) \/ ((f . c) `2_3) is Element of bool n
(f . c) `3_3 is Element of bool n
(((f . c) `1_3) \/ ((f . c) `2_3)) \/ ((f . c) `3_3) is Element of bool n
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
xx is set
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
xx is set
A . xx is set
YY is set
cc is non empty Element of Class (n,A)
f . cc is Element of [:(bool n),(bool n),(bool n):]
(f . cc) `2_3 is Element of bool n
(f . cc) `1_3 is Element of bool n
((f . cc) `1_3) \/ ((f . cc) `2_3) is Element of bool n
(f . cc) `3_3 is Element of bool n
(((f . cc) `1_3) \/ ((f . cc) `2_3)) \/ ((f . cc) `3_3) is Element of bool n
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
x1 is set
Class ((n,A),x1) is Element of bool n
{x1} is non empty finite set
(n,A) .: {x1} 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) . xx is set
field A is set
id (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field 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) . x is set
[x,xx] is set
{x,xx} is non empty finite set
{{x,xx},{x}} is non empty with_non-empty_elements non empty-membered finite V69() set
A .: YY is set
x is set
Y is set
c is non empty Element of Class (n,A)
f . c is Element of [:(bool n),(bool n),(bool n):]
(f . c) `3_3 is Element of bool n
(f . c) `1_3 is Element of bool n
(f . c) `2_3 is Element of bool n
((f . c) `1_3) \/ ((f . c) `2_3) is Element of bool n
(((f . c) `1_3) \/ ((f . c) `2_3)) \/ ((f . c) `3_3) is Element of bool n
Class ((n,A),x) is Element of bool n
{x} is non empty finite set
(n,A) .: {x} is set
xx is set
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
xx is set
A . xx is set
YY is set
cc is non empty Element of Class (n,A)
f . cc is Element of [:(bool n),(bool n),(bool n):]
(f . cc) `3_3 is Element of bool n
(f . cc) `1_3 is Element of bool n
(f . cc) `2_3 is Element of bool n
((f . cc) `1_3) \/ ((f . cc) `2_3) is Element of bool n
(((f . cc) `1_3) \/ ((f . cc) `2_3)) \/ ((f . cc) `3_3) is Element of bool n
Class ((n,A),xx) is Element of bool n
{xx} is non empty finite set
(n,A) .: {xx} is set
x1 is set
Class ((n,A),x1) is Element of bool n
{x1} is non empty finite set
(n,A) .: {x1} 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) . xx is set
field A is set
id (field A) is Relation-like Function-like one-to-one V38() V40() V41() V45() set
(id (field 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) . x is set
[x,xx] is set
{x,xx} is non empty finite set
{{x,xx},{x}} is non empty with_non-empty_elements non empty-membered finite V69() set
A .: YY is set
n is ext-real V10() V11() V12() V16() complex V18() integer set
A 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 * 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
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
(2 * x) + 1 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 * A) + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() 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
n + 1 is ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() Element of NAT
A is non empty set
[:A,A:] is non empty set
bool [:A,A:] is non empty non empty-membered set
f is Relation-like A -defined A -valued Function-like V33(A,A) Element of bool [:A,A:]
(A,f,(n + 1)) is Relation-like A -defined A -valued Function-like V33(A,A) Element of bool [:A,A:]
(A,f,n) is Relation-like A -defined A -valued Function-like V33(A,A) Element of bool [:A,A:]
x is Element of A
(A,f,(n + 1)) . x is Element of A
(A,f,n) . x is Element of A
f . ((A,f,n) . x) is Element of A
(A,f,n) * f is Relation-like Function-like set
((A,f,n) * f) . x is set
n is ext-real complex V18() integer set
A is ext-real complex V18() integer set
f is ext-real complex V18() integer set
2 * f is ext-real complex V18() integer () 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
(2 * 0) + 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
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 () 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
0 + 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
n is ext-real complex V18() integer set