:: ARROW semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of bool REAL

NAT is non empty V24() V25() V26() set

{} is ext-real non negative empty V24() V25() V26() V28() V29() V30() V31() V32() finite V37() V44() set
1 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() Element of NAT
2 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() Element of NAT

N is non empty set
bool N is set
A is non empty set
f is non empty Element of bool N
[:A,f:] is set
bool [:A,f:] is set

f9 is Element of A
o . f9 is set
o . f9 is Element of f
A is finite set
card A is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
f is Element of A
{f} is non empty finite set
N is non empty finite set
N \ {f} is finite Element of bool N
bool N is finite V37() set
card (N \ {f}) is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
card N is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
card {f} is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
(card N) - () is ext-real V31() V32() V44() set
(card N) - 1 is ext-real V31() V32() V44() set
0 is ext-real non negative empty V24() V25() V26() V28() V29() V30() V31() V32() finite V37() V44() Element of NAT
o is set
f9 is Element of A
3 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() Element of NAT
A is finite set
card A is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
f is Element of A
o is Element of A
{f,o} is non empty finite set
N is non empty finite set
N \ {f,o} is finite Element of bool N
bool N is finite V37() set
card (N \ {f,o}) is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
card N is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
card {f,o} is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
(card N) - (card {f,o}) is ext-real V31() V32() V44() set
3 - 2 is ext-real V31() V32() V44() set
0 is ext-real non negative empty V24() V25() V26() V28() V29() V30() V31() V32() finite V37() V44() Element of NAT
f9 is set
n is Element of A
A is non empty set
[:A,A:] is set
bool [:A,A:] is set
N is set
f is set
o is Element of A
f9 is Element of A
[o,f9] is set
[f9,o] is set
n is Element of A
p is Element of A
[n,p] is set
q is Element of A
[p,q] is set
[n,q] is set
N is set
f is set
o is set
f9 is Element of A
n is Element of A
[f9,n] is set
[n,f9] is set
p is Element of A
q is Element of A
[p,q] is set
a is Element of A
[q,a] is set
[p,a] is set
f9 is Element of A
n is Element of A
[f9,n] is set
[n,f9] is set
p is Element of A
q is Element of A
[p,q] is set
a is Element of A
[q,a] is set
[p,a] is set
A is non empty set
(A) is set
[:A,A:] is set
bool [:A,A:] is set

f is Element of A
o is Element of A
[f,o] is set
[o,f] is set
f9 is Element of A
n is Element of A
[f9,n] is set
p is Element of A
[n,p] is set
[f9,p] is set
A is non empty set
(A) is non empty set
bool (A) is set
N is set
f is set
f is Element of bool (A)
o is Element of (A)
f9 is Element of A
n is Element of A
[f9,n] is set
[n,f9] is set
N is Element of bool (A)
f is Element of bool (A)
o is Element of (A)
f9 is Element of A
n is Element of A
[f9,n] is set
[n,f9] is set
f9 is Element of A
n is Element of A
[f9,n] is set
[n,f9] is set
A is set
[:A,A:] is set
bool [:A,A:] is set

N /\ [:A,A:] is set
f9 is set
[f9,f9] is set

dom o is Element of bool A
bool A is set

A is non empty set
(A) is non empty set
bool (A) is set
(A) is Element of bool (A)
[:A,A:] is set
bool [:A,A:] is set
N is set
o is set
[o,o] is set

dom f is Element of bool A
bool A is set
o is set
[o,o] is set
rng f is Element of bool A
field f is set
dom f is set
rng f is set
(dom f) \/ (rng f) is set
A \/ A is non empty set
o is set
f9 is set
[o,f9] is set
[f9,o] is set
o is set
[o,o] is set
o is set
f9 is set
[o,f9] is set
[f9,o] is set
o is set
f9 is set
n is set
[o,f9] is set
[f9,n] is set
[o,n] is set
N is set

dom f is Element of bool A
rng f is Element of bool A
(dom f) \/ (rng f) is Element of bool A
field f is set
dom f is set
rng f is set
(dom f) \/ (rng f) is set
o is Element of A
f9 is Element of A
[o,f9] is set
[f9,o] is set
o is Element of A
f9 is Element of A
[o,f9] is set
n is Element of A
[f9,n] is set
[o,n] is set
o is Element of A
f9 is Element of A
[o,f9] is set
[f9,o] is set
N is Element of bool (A)
f is set
o is set
f is set
A is non empty set
(A) is Element of bool (A)
(A) is non empty set
bool (A) is set
[:A,A:] is set
bool [:A,A:] is set

A is non empty set
(A) is non empty set
N is Element of (A)
(A) is non empty Element of bool (A)
bool (A) is set
N is Element of (A)
A is non empty set
(A) is non empty set
N is Element of A
f is Relation-like Element of (A)
[N,N] is set
A is non empty set
(A) is non empty set
N is Element of A
f is Element of A
o is Relation-like Element of (A)
[N,f] is set
[f,N] is set
A is non empty set
(A) is non empty set
N is Element of A
f is Element of A
o is Element of A
f9 is Relation-like Element of (A)
[N,f] is set
[f,o] is set
[N,o] is set
A is non empty set
(A) is non empty set
(A) is non empty Element of bool (A)
bool (A) is set
N is Element of A
f is Element of A
o is Relation-like Element of (A)
[N,f] is set
[f,N] is set
A is non empty set
(A) is non empty set
N is Element of A
f is Element of A
o is Element of A
[:A,A:] is set
bool [:A,A:] is set
f9 is Relation-like A -defined A -valued Element of bool [:A,A:]
n is Element of A
p is Element of A
[n,p] is set
[p,n] is set
n is Element of A
p is Element of A
[n,p] is set
q is Element of A
[p,q] is set
[n,q] is set
n is Relation-like Element of (A)
[f,N] is set
[o,f] is set
A is non empty set
(A) is non empty set
N is Element of A
[:A,A:] is set
bool [:A,A:] is set

o is Element of A
f9 is Element of A
[o,f9] is set
[f9,o] is set
o is Element of A
f9 is Element of A
[o,f9] is set
n is Element of A
[f9,n] is set
[o,n] is set
o is Relation-like Element of (A)
f9 is Element of A
[f9,N] is set
A is non empty set
(A) is non empty set
N is Element of A
[:A,A:] is set
bool [:A,A:] is set

o is Element of A
f9 is Element of A
[o,f9] is set
[f9,o] is set
o is Element of A
f9 is Element of A
[o,f9] is set
n is Element of A
[f9,n] is set
[o,n] is set
o is Relation-like Element of (A)
f9 is Element of A
[N,f9] is set
A is non empty set
(A) is non empty set
N is Element of A
f is Element of A
o is Element of A
f9 is Relation-like Element of (A)
[:A,A:] is set
bool [:A,A:] is set

p is Element of A
q is Element of A
[p,q] is set
[q,p] is set
p is Element of A
q is Element of A
[p,q] is set
a is Element of A
[q,a] is set
[p,a] is set
p is Relation-like Element of (A)
[f,N] is set
[o,N] is set
[o,f] is set
[f,o] is set
A is non empty set
(A) is non empty set
N is Element of A
f is Element of A
o is Element of A
f9 is Relation-like Element of (A)
[:A,A:] is set
bool [:A,A:] is set

p is Element of A
q is Element of A
[p,q] is set
[q,p] is set
p is Element of A
q is Element of A
[p,q] is set
a is Element of A
[q,a] is set
[p,a] is set
p is Relation-like Element of (A)
[N,f] is set
[N,o] is set
[o,f] is set
[f,o] is set
A is non empty set
(A) is non empty set
(A) is non empty Element of bool (A)
bool (A) is set
N is Element of A
f is Element of A
o is Relation-like Element of (A)
f9 is Relation-like Element of (A)
A is non empty set
(A) is non empty set
(A) is non empty Element of bool (A)
bool (A) is set
N is Relation-like Element of (A)
f is Relation-like Element of (A)
f9 is Element of A
o is Element of A
o is Element of A
f9 is Element of A
o is Element of A
f9 is Element of A
f9 is Element of A
o is Element of A
f9 is Element of A
o is Element of A
A is non empty finite set
(A) is non empty set
card A is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
N is non empty finite set
Funcs (N,(A)) is non empty FUNCTION_DOMAIN of N,(A)
[:(Funcs (N,(A))),(A):] is set
bool [:(Funcs (N,(A))),(A):] is set
f is Relation-like Funcs (N,(A)) -defined (A) -valued Function-like quasi_total Element of bool [:(Funcs (N,(A))),(A):]
f9 is Element of A
o is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
n is Element of A
f . o is Relation-like Element of (A)
p is Element of A
f9 is Element of A
o is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . o is Relation-like Element of (A)
n is Element of A
n is Element of A
p is Element of A
p is Element of A
q is Element of A
q is Element of A
a is Element of A
q is Element of A
a is Element of A
b is Element of N
o . b is Relation-like Element of (A)
b is Relation-like Element of (A)
b is Relation-like Element of (A)
b is Element of A
i is Element of A
[:N,(A):] is set
bool [:N,(A):] is set

b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . b is Relation-like Element of (A)

rng o is set
n is Element of A
p is Relation-like Element of (A)
q is Relation-like Element of (A)

dom f9 is Element of bool NAT
a is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
b is Element of N
b is set
f9 . b is set
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
[:N,(A):] is set
bool [:N,(A):] is set

b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
f9 . i is set
b . (f9 . i) is set
pI9 is Element of N
b . pI9 is Relation-like Element of (A)
pII9 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
f9 . pII9 is set
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
f9 . i is set
b . (f9 . i) is set
pI9 is Element of N
b . pI9 is Relation-like Element of (A)
pII9 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
f9 . pII9 is set
len f9 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
(len f9) + 1 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() set
a is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . b is Relation-like Element of (A)
b is Element of A
i is Element of N
b . i is Relation-like Element of (A)
pI9 is set
f9 . pI9 is set
pII9 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
0 is ext-real non negative empty V24() V25() V26() V28() V29() V30() V31() V32() finite V37() V44() Element of NAT
pII9 + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
b is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
i is Element of A
pI9 is Element of N
b . pI9 is Relation-like Element of (A)
pII9 is set
f9 . pII9 is set
pI is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
f . b is Relation-like Element of (A)
b - 1 is ext-real V31() V32() V44() set
i is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
pI9 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
pI9 + 1 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() set
1 - 1 is ext-real V31() V32() V44() set
0 is ext-real non negative empty V24() V25() V26() V28() V29() V30() V31() V32() finite V37() V44() Element of NAT
0 + 1 is ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() set
a - 1 is ext-real V31() V32() V44() set
f9 . pI9 is set
pI9 + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
pI is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . pI is Relation-like Element of (A)
pII9 is Element of N
pI . pII9 is Relation-like Element of (A)
b . pII9 is Relation-like Element of (A)
f . b is Relation-like Element of (A)
i is Element of N
pI . i is Relation-like Element of (A)
b . i is Relation-like Element of (A)
k is set
f9 . k is set
k is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
k + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
k is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
k is ext-real non negative V24() V25() V26() V30() V31() V32() V44() set
i is Element of N
pI . i is Relation-like Element of (A)
k is set
f9 . k is set
k is Element of A
k is Element of A
i is Element of N
b . i is Relation-like Element of (A)
k is set
f9 . k is set
k is Element of A
k is Element of A
i is Element of A
i is Element of A
i is Element of A
k is Element of A
i is Element of A
o is Element of A
f9 is Element of N
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
n . f9 is Relation-like Element of (A)
p . f9 is Relation-like Element of (A)
f . n is Relation-like Element of (A)
f . p is Relation-like Element of (A)
q is Element of N
n . q is Relation-like Element of (A)
p . q is Relation-like Element of (A)
b is Element of A
a is Element of N
n . a is Relation-like Element of (A)
b is Element of A
i is Element of A
pI9 is Element of A
q is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
q . f9 is Relation-like Element of (A)
f . q is Relation-like Element of (A)
a is Element of A
b is Element of A
b is Element of N
q . b is Relation-like Element of (A)
p . b is Relation-like Element of (A)
i is Relation-like Element of (A)
i is Relation-like Element of (A)
i is Relation-like Element of (A)
i is Element of A
pI9 is Element of A
[:N,(A):] is set
bool [:N,(A):] is set

i is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
pI9 is Element of N
p . pI9 is Relation-like Element of (A)
i . pI9 is Relation-like Element of (A)
pII9 is Element of A
pI is Element of A
f . i is Relation-like Element of (A)
pI9 is Element of N
n . pI9 is Relation-like Element of (A)
i . pI9 is Relation-like Element of (A)
p . pI9 is Relation-like Element of (A)
p . pI9 is Relation-like Element of (A)
p . pI9 is Relation-like Element of (A)
pII9 is Element of A
pI is Element of A
the Element of A is Element of A
f9 is Element of N
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . n is Relation-like Element of (A)
f . p is Relation-like Element of (A)
q is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
q . f9 is Relation-like Element of (A)
f . q is Relation-like Element of (A)
a is Element of A
b is Element of A
b is Element of A
i is Element of N
pI9 is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
pII9 is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . pI9 is Relation-like Element of (A)
f . pII9 is Relation-like Element of (A)
n . i is Relation-like Element of (A)
p . i is Relation-like Element of (A)
n . i is Relation-like Element of (A)
p . i is Relation-like Element of (A)
A is non empty finite set
(A) is non empty Element of bool (A)
(A) is non empty set
bool (A) is set
card A is ext-real non negative V24() V25() V26() V30() V31() V32() V44() Element of NAT
N is non empty finite set
Funcs (N,(A)) is non empty FUNCTION_DOMAIN of N,(A)
[:(Funcs (N,(A))),(A):] is set
bool [:(Funcs (N,(A))),(A):] is set
f is Relation-like Funcs (N,(A)) -defined (A) -valued Function-like quasi_total Element of bool [:(Funcs (N,(A))),(A):]
the Relation-like Element of (A) is Relation-like Element of (A)
f9 is Relation-like Element of (A)
[:A,A:] is finite set
bool [:A,A:] is finite V37() set

p is Element of A
q is Element of A
[p,q] is set
[q,p] is set
p is Element of A
q is Element of A
a is Element of A
[p,q] is set
[q,a] is set
[p,a] is set
q is Element of A
a is Element of A
[q,a] is set
p is Relation-like Element of (A)
[a,q] is set
q is Relation-like Element of (A)
a is Element of A
b is Element of A
[a,b] is set
Funcs (N,(A)) is non empty FUNCTION_DOMAIN of N,(A)
f9 is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
q is Element of N
n . q is set
p . q is set
[:A,A:] is finite set
bool [:A,A:] is finite V37() set
(N,(A),(A),n,q) is Relation-like Element of (A)
(N,(A),(A),p,q) is Relation-like Element of (A)
f9 . q is Relation-like Element of (A)
b is Element of A
i is Element of A
[b,i] is set

f9 is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
n is Element of N
f9 . n is Relation-like Element of (A)
[:N,(A):] is set
bool [:N,(A):] is set

p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
q is Element of N
f9 . q is Relation-like Element of (A)
a is Element of A
b is Element of A
(N,(A),(A),p,q) is Relation-like Element of (A)
b is Element of N
(N,(A),(A),p,b) is Relation-like Element of (A)
i is Element of A
pI9 is Element of A
f9 . b is Relation-like Element of (A)
f9 is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . n is Relation-like Element of (A)
[:(Funcs (N,(A))),(A):] is set
bool [:(Funcs (N,(A))),(A):] is set
f9 is Relation-like Funcs (N,(A)) -defined (A) -valued Function-like quasi_total Element of bool [:(Funcs (N,(A))),(A):]
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f9 . n is Relation-like Element of (A)
p is Element of A
q is Element of A
a is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . a is Relation-like Element of (A)
b is Element of N
n . b is Relation-like Element of (A)
(N,(A),(A),a,b) is Relation-like Element of (A)
n is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
a is Element of A
q is Element of A
p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f9 . n is Relation-like Element of (A)
b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . b is Relation-like Element of (A)
f9 . p is Relation-like Element of (A)
b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . b is Relation-like Element of (A)
i is Element of N
(N,(A),(A),b,i) is Relation-like Element of (A)
(N,(A),(A),b,i) is Relation-like Element of (A)
n . i is Relation-like Element of (A)
p . i is Relation-like Element of (A)
n is Element of N
p is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
(N,(A),(A),p,n) is Relation-like Element of (A)
f . p is Relation-like Element of (A)
rng p is set
dom p is finite Element of bool N
bool N is finite V37() set
q is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
a is Element of N
q . a is Relation-like Element of (A)
(N,(A),(A),p,a) is Relation-like Element of (A)
b is Element of A
b is Element of A
f9 . q is Relation-like Element of (A)
b is Element of A
a is Element of A
b is Relation-like N -defined (A) -valued Function-like quasi_total Element of Funcs (N,(A))
f . b is Relation-like Element of (A)
a is Element of A
q is Element of A
b is Element of A
b is Element of A