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