:: ARROW semantic presentation

REAL is set

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

bool REAL is set

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

bool NAT is set

bool NAT is 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

card {} is cardinal set

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

o is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

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) - (card {f}) 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

N is Relation-like A -defined A -valued Element of bool [:A,A:]

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 is Relation-like set

N |_2 A is Relation-like set

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

f9 is set

[f9,f9] is set

o is Relation-like A -defined A -valued Element of bool [:A,A:]

dom o is Element of bool A

bool A is set

f9 is Relation-like A -defined A -valued V17(A) reflexive antisymmetric transitive Element of bool [:A,A:]

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

f is Relation-like A -defined A -valued Element of bool [:A,A:]

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

f is Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive Element of bool [:A,A:]

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

the Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive Element of bool [:A,A:] is Relation-like A -defined A -valued V17(A) reflexive antisymmetric connected transitive Element of bool [:A,A:]

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

f is Relation-like A -defined A -valued Element of bool [:A,A:]

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

f is Relation-like A -defined A -valued Element of bool [:A,A:]

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

n is Relation-like A -defined A -valued Element of bool [:A,A:]

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

n is Relation-like A -defined A -valued Element of bool [:A,A:]

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 finite Element of bool [:N,(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)

o is Relation-like Function-like FinSequence-like set

rng o is set

n is Element of A

p is Relation-like Element of (A)

q is Relation-like Element of (A)

f9 is Relation-like NAT -defined N -valued Function-like FinSequence-like FinSequence of N

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 finite Element of bool [:N,(A):]

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

b is Relation-like N -defined (A) -valued Function-like quasi_total finite Element of bool [:N,(A):]

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

n is Relation-like A -defined A -valued finite Element of bool [:A,A:]

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

a is Relation-like A -defined A -valued finite Element of bool [:A,A:]

b is Relation-like A -defined A -valued finite Element of bool [:A,A:]

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

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

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