:: HILBERT3 semantic presentation

REAL is non empty V43() set
NAT is non empty V7() V8() V9() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V43() set
NAT is non empty V7() V8() V9() set
bool NAT is non empty set
bool NAT is non empty set

1 is ext-real non empty V7() V8() V9() V13() complex V15() integer Element of NAT
{{},1} is non empty set
K314() is set
is non empty trivial functional set
K292() is M18()

bool is non empty set
PFuncs (K292(),) is non empty functional set

bool HP-WFF is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set

INT is non empty V43() set
2 is ext-real non empty V7() V8() V9() V13() complex V15() integer Element of NAT

b is ext-real non empty V7() V8() V9() V13() complex V15() integer set
a is ext-real non empty V7() V8() V9() V13() complex V15() integer set
(0,b) --> (a,0) is Relation-like Function-like set
X is set
dom ((0,b) --> (a,0)) is set
A is set
((0,b) --> (a,0)) . X is set
((0,b) --> (a,0)) . A is set
{0,b} is non empty set
((0,b) --> (a,0)) . 0 is set
(b,0) --> (0,a) is Relation-like Function-like set
X is set
dom ((b,0) --> (0,a)) is set
A is set
((b,0) --> (0,a)) . X is set
((b,0) --> (0,a)) . A is set
{0,b} is non empty set
((b,0) --> (0,a)) . 0 is set

a is trivial set
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
b is set
A is set
{A} is non empty trivial set

dom X is set
X . b is set
rng X is set

rng a is set
SubFuncs (rng a) is set
b is set
dom a is set
A is set

b is set
A is set
A is set
a is set
b is set
Funcs (a,b) is functional set

X . A is set
[:a,b:] is Relation-like set
bool [:a,b:] is non empty set
A is set
b is set
a is set
Funcs (b,A) is functional set
[:a,(Funcs (b,A)):] is Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set

{b} is non empty trivial set

bool [:a,{b}:] is non empty set

p1 is set

(doms A) . p1 is set
dom (A . p1) is set
(a --> b) . p1 is set
a is set

{0,1} is non empty set

[:{0,1},NAT:] is non empty Relation-like set
bool [:{0,1},NAT:] is non empty set
a is set
bool a is non empty set
b is Element of bool a

[:a,{{},1}:] is Relation-like set
bool [:a,{{},1}:] is non empty set
((0,1) --> (1,0)) * (chi (b,a)) is Relation-like a -defined NAT -valued Function-like total quasi_total Element of bool [:a,NAT:]

bool [:a,NAT:] is non empty set
b ` is Element of bool a
a \ b is set

dom (chi (b,a)) is set
X is set
(((0,1) --> (1,0)) * (chi (b,a))) . X is set
(chi (b,a)) . X is set
((0,1) --> (1,0)) . 0 is set
(chi (b,a)) . X is set
((0,1) --> (1,0)) . 1 is set
dom ((0,1) --> (1,0)) is non empty set
rng (chi (b,a)) is set
dom (((0,1) --> (1,0)) * (chi (b,a))) is set
a is set
bool a is non empty set
b is Element of bool a
b ` is Element of bool a
a \ b is set

[:a,{{},1}:] is Relation-like set
bool [:a,{{},1}:] is non empty set
((0,1) --> (1,0)) * (chi ((b `),a)) is Relation-like a -defined NAT -valued Function-like total quasi_total Element of bool [:a,NAT:]

bool [:a,NAT:] is non empty set

(b `) ` is Element of bool a
a \ (b `) is set
a is set
b is set
A is set
X is set
(a,b) --> (A,X) is Relation-like Function-like set
A is set
p1 is set
(a,b) --> (A,p1) is Relation-like Function-like set
((a,b) --> (A,X)) . a is set
((a,b) --> (A,X)) . b is set
a is set
b is set
A is set
A is set
X is set
p1 is set
(a,b) --> (A,X) is Relation-like Function-like set
(a,b) --> (A,p1) is Relation-like Function-like set
product ((a,b) --> (A,p1)) is set
{A} is non empty trivial set
{X} is non empty trivial set
(a,b) --> ({A},{X}) is Relation-like Function-like set
product ((a,b) --> ({A},{X})) is set
{((a,b) --> (A,X))} is non empty trivial functional set
a is non empty set
[:2,a:] is non empty Relation-like set
bool [:2,a:] is non empty set

b . 0 is set
b . 1 is set
A is Element of a
X is Element of a
(0,1) --> (A,X) is non empty Relation-like NAT -defined {0,1} -defined a -valued Function-like total quasi_total Element of bool [:{0,1},a:]
[:{0,1},a:] is non empty Relation-like set
bool [:{0,1},a:] is non empty set
dom b is non empty set
a is set
b is set
(a,b) --> (b,a) is Relation-like Function-like set
A is set
X is set
(a,b) --> (A,X) is Relation-like Function-like set
((a,b) --> (b,a)) * ((a,b) --> (A,X)) is Relation-like Function-like set
(a,b) --> (X,A) is Relation-like Function-like set
dom ((a,b) --> (b,a)) is set
{a,b} is non empty set
(((a,b) --> (b,a)) * ((a,b) --> (A,X))) . b is set
((a,b) --> (b,a)) . b is set
((a,b) --> (A,X)) . (((a,b) --> (b,a)) . b) is set
((a,b) --> (A,X)) . a is set
(((a,b) --> (b,a)) * ((a,b) --> (A,X))) . a is set
((a,b) --> (b,a)) . a is set
((a,b) --> (A,X)) . (((a,b) --> (b,a)) . a) is set
((a,b) --> (A,X)) . b is set
rng ((a,b) --> (b,a)) is set
dom ((a,b) --> (A,X)) is set
dom (((a,b) --> (b,a)) * ((a,b) --> (A,X))) is set
a is set
b is set
A is set
X is set
(a,b) --> (A,X) is Relation-like Function-like set

dom A is set
((a,b) --> (A,X)) * A is Relation-like Function-like set
A . A is set
A . X is set
(a,b) --> ((A . A),(A . X)) is Relation-like Function-like set
dom ((a,b) --> (A,X)) is set
{a,b} is non empty set
(((a,b) --> (A,X)) * A) . a is set
((a,b) --> (A,X)) . a is set
A . (((a,b) --> (A,X)) . a) is set
(((a,b) --> (A,X)) * A) . b is set
((a,b) --> (A,X)) . b is set
A . (((a,b) --> (A,X)) . b) is set
rng ((a,b) --> (A,X)) is set
{A,X} is non empty set
dom (((a,b) --> (A,X)) * A) is set
[:2,2:] is non empty Relation-like set
bool [:2,2:] is non empty set
rng ((0,1) --> (1,0)) is non empty set
dom ((0,1) --> (1,0)) is non empty set

A is set
dom [:a,b:] is set
X is set
[:a,b:] . A is set
[:a,b:] . X is set
dom a is set
dom b is set
[:(dom a),(dom b):] is Relation-like set
A is set
p1 is set
[A,p1] is non empty set
{A,p1} is non empty set
{A} is non empty trivial set
{{A,p1},{A}} is non empty set
[:a,b:] . (A,p1) is set
[:a,b:] . [A,p1] is set
a . A is set
b . p1 is set
[(a . A),(b . p1)] is non empty set
{(a . A),(b . p1)} is non empty set
{(a . A)} is non empty trivial set
{{(a . A),(b . p1)},{(a . A)}} is non empty set
p1 is set
V is set
[p1,V] is non empty set
{p1,V} is non empty set
{p1} is non empty trivial set
{{p1,V},{p1}} is non empty set
[:a,b:] . (p1,V) is set
[:a,b:] . [p1,V] is set
a . p1 is set
b . V is set
[(a . p1),(b . V)] is non empty set
{(a . p1),(b . V)} is non empty set
{(a . p1)} is non empty trivial set
{{(a . p1),(b . V)},{(a . p1)}} is non empty set
a is non empty set
b is non empty set
[:a,b:] is non empty Relation-like set
pr1 (a,b) is non empty Relation-like [:a,b:] -defined a -valued Function-like total quasi_total Element of bool [:[:a,b:],a:]
[:[:a,b:],a:] is non empty Relation-like set
bool [:[:a,b:],a:] is non empty set
A is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
X is set
[:X,b:] is Relation-like set
bool [:X,b:] is non empty set
[:A,X:] is Relation-like set

[:[:A,X:],A:] is Relation-like set
bool [:[:A,X:],A:] is non empty set

A * (pr1 (A,X)) is Relation-like [:A,X:] -defined a -valued Function-like Element of bool [:[:A,X:],a:]
[:[:A,X:],a:] is Relation-like set
bool [:[:A,X:],a:] is non empty set

[:[:A,X:],[:a,b:]:] is Relation-like set
bool [:[:A,X:],[:a,b:]:] is non empty set
(pr1 (a,b)) * [:A,p1:] is Relation-like [:A,X:] -defined a -valued Function-like total quasi_total Element of bool [:[:A,X:],a:]
[:[:A,X:],b:] is Relation-like set
bool [:[:A,X:],b:] is non empty set

[:[:A,X:],X:] is Relation-like set
bool [:[:A,X:],X:] is non empty set
p1 * (pr2 (A,X)) is Relation-like [:A,X:] -defined b -valued Function-like Element of bool [:[:A,X:],b:]

(pr1 (a,b)) * <:p1,V:> is Relation-like [:A,X:] -defined a -valued Function-like total quasi_total Element of bool [:[:A,X:],a:]
a is non empty set
b is non empty set
[:a,b:] is non empty Relation-like set
pr2 (a,b) is non empty Relation-like [:a,b:] -defined b -valued Function-like total quasi_total Element of bool [:[:a,b:],b:]
[:[:a,b:],b:] is non empty Relation-like set
bool [:[:a,b:],b:] is non empty set
A is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
X is set
[:X,b:] is Relation-like set
bool [:X,b:] is non empty set
[:A,X:] is Relation-like set

[:[:A,X:],X:] is Relation-like set
bool [:[:A,X:],X:] is non empty set

[:[:A,X:],[:a,b:]:] is Relation-like set
bool [:[:A,X:],[:a,b:]:] is non empty set
(pr2 (a,b)) * [:A,p1:] is Relation-like [:A,X:] -defined b -valued Function-like total quasi_total Element of bool [:[:A,X:],b:]
[:[:A,X:],b:] is Relation-like set
bool [:[:A,X:],b:] is non empty set
p1 * (pr2 (A,X)) is Relation-like [:A,X:] -defined b -valued Function-like Element of bool [:[:A,X:],b:]
[:[:A,X:],a:] is Relation-like set
bool [:[:A,X:],a:] is non empty set

[:[:A,X:],A:] is Relation-like set
bool [:[:A,X:],A:] is non empty set
A * (pr1 (A,X)) is Relation-like [:A,X:] -defined a -valued Function-like Element of bool [:[:A,X:],a:]

(pr2 (a,b)) * <:p1,V:> is Relation-like [:A,X:] -defined b -valued Function-like total quasi_total Element of bool [:[:A,X:],b:]

dom ({} .. a) is set

A * (a .. b) is Relation-like Function-like set

(A * a) .. (A * b) is Relation-like Function-like set
dom (A * a) is set
X is set
(A * (a .. b)) . X is set
(A * a) . X is Relation-like Function-like set
(A * b) . X is set
((A * a) . X) . ((A * b) . X) is set
dom A is set
A . X is set
dom a is set
(a .. b) . (A . X) is set
a . (A . X) is Relation-like Function-like set
b . (A . X) is set
(a . (A . X)) . (b . (A . X)) is set
((A * a) . X) . (b . (A . X)) is set
dom (a .. b) is set
dom a is set
dom (A * (a .. b)) is set
a is set
Funcs ({},a) is functional set
b is non empty set
[:b,(Funcs ({},a)):] is Relation-like set
bool [:b,(Funcs ({},a)):] is non empty set

bool [:b,{}:] is non empty set

rng (A .. X) is set
the Element of b is Element of b
dom A is set
dom (A .. X) is set
p1 is set
rng A is set
p1 is set
(A .. X) . p1 is set

(A . p1) . (X . p1) is set
A . the Element of b is Relation-like Function-like Element of Funcs ({},a)
(A .. X) . the Element of b is set

b is set
a is set
A is set
Funcs (b,A) is functional set
[:a,(Funcs (b,A)):] is Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set
[:a,b:] is Relation-like set
bool [:a,b:] is non empty set

rng (X .. A) is set
p1 is set
dom (X .. A) is set
p1 is set
(X .. A) . p1 is set
dom X is set
[:b,A:] is Relation-like set
bool [:b,A:] is non empty set

A . p1 is set

V . (A . p1) is set
A is set
b is set
a is set
Funcs (b,A) is functional set
[:a,(Funcs (b,A)):] is Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set
Funcs (a,b) is functional set

product (doms X) is set
dom () is set

{b} is non empty trivial set

bool [:a,{b}:] is non empty set
product (a --> b) is set
A is set
b is set
a is set
Funcs (b,A) is functional set
[:a,(Funcs (b,A)):] is Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set
Funcs (a,A) is functional set

product (doms X) is set
rng () is set
rng X is set
SubFuncs (rng X) is set

dom (rngs X) is set
X " (rng X) is set
dom X is set

{A} is non empty trivial set

bool [:a,{A}:] is non empty set
A is set
(rngs X) . A is set
(a --> A) . A is set

rng (X . A) is set
dom (a --> A) is set
product (rngs X) is set
product (a --> A) is set
A is set
b is set
a is set
Funcs (b,A) is functional set
[:a,(Funcs (b,A)):] is Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set
Funcs (a,b) is functional set
Funcs (a,A) is functional set
[:(Funcs (a,b)),(Funcs (a,A)):] is Relation-like set
bool [:(Funcs (a,b)),(Funcs (a,A)):] is non empty set

product (doms X) is set
dom () is set
rng () is set
a is set
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
b is set
[:b,b:] is Relation-like set
bool [:b,b:] is non empty set
[:a,b:] is Relation-like set
[:[:a,b:],[:a,b:]:] is Relation-like set
bool [:[:a,b:],[:a,b:]:] is non empty set

rng A is set
rng X is set

a is set
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
b is set
[:b,b:] is Relation-like set
bool [:b,b:] is non empty set
[:a,b:] is Relation-like set

[:[:a,b:],[:a,b:]:] is Relation-like set
bool [:[:a,b:],[:a,b:]:] is non empty set
a is non empty set
[:a,a:] is non empty Relation-like set
bool [:a,a:] is non empty set
b is non empty set
[:b,b:] is non empty Relation-like set
bool [:b,b:] is non empty set
Funcs (a,b) is non empty functional FUNCTION_DOMAIN of a,b
[:(Funcs (a,b)),(Funcs (a,b)):] is non empty Relation-like set
bool [:(Funcs (a,b)),(Funcs (a,b)):] is non empty set
[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set

(X * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
A is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]

(X * p1) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
A is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
p1 is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
A . p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)

(X * p1) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
p1 . p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
a is non empty set
[:a,a:] is non empty Relation-like set
bool [:a,a:] is non empty set
b is non empty set
[:b,b:] is non empty Relation-like set
bool [:b,b:] is non empty set
Funcs (a,b) is non empty functional FUNCTION_DOMAIN of a,b

(a,b,A,X) is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
[:(Funcs (a,b)),(Funcs (a,b)):] is non empty Relation-like set
bool [:(Funcs (a,b)),(Funcs (a,b)):] is non empty set
A is set
dom (a,b,A,X) is non empty set
p1 is set
(a,b,A,X) . A is Relation-like Function-like set
(a,b,A,X) . p1 is Relation-like Function-like set

p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)

[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set
(X * p1) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(a,b,A,X) . V is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)

(X * V) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(X * p1) * (id a) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(X * p1) * ((A ") * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X * V) * (A ")) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * V) * ((A ") * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * V) * (id a) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(id b) * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

((X ") * X) * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X ") * (X * V) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X ") * X) * V is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(id b) * V is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
rng (a,b,A,X) is non empty set
K451((Funcs (a,b)),(a,b,A,X)) is non empty functional Element of bool (Funcs (a,b))
bool (Funcs (a,b)) is non empty set
A is set
[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set
dom (a,b,A,X) is non empty set

(X ") * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X ") * p1) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(a,b,A,X) . (((X ") * p1) * A) is Relation-like Function-like set

X * (((X ") * p1) * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * (((X ") * p1) * A)) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X * ((X ") * p1) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * ((X ") * p1)) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X * ((X ") * p1)) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(X * (X ")) * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X * (X ")) * p1) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(((X * (X ")) * p1) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(id b) * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((id b) * p1) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(((id b) * p1) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(p1 * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

p1 * (A * (A ")) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

p1 * (id a) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
a is non empty set
[:a,a:] is non empty Relation-like set
bool [:a,a:] is non empty set
b is non empty set
[:b,b:] is non empty Relation-like set
bool [:b,b:] is non empty set
[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set
Funcs (a,b) is non empty functional FUNCTION_DOMAIN of a,b

(a,b,A,X) is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
[:(Funcs (a,b)),(Funcs (a,b)):] is non empty Relation-like set
bool [:(Funcs (a,b)),(Funcs (a,b)):] is non empty set
(a,b,A,X) " is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]

((a,b,A,X) ") . A is Relation-like Function-like set
(X ") * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X ") * A) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((a,b,A,X) ") " is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
(((a,b,A,X) ") ") . (((a,b,A,X) ") . A) is Relation-like Function-like set

A * (id a) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

A * (A * (A ")) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(A * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(id b) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((id b) * A) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(((id b) * A) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(X * (X ")) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X * (X ")) * A) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(((X * (X ")) * A) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X * ((X ") * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * ((X ") * A)) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((X * ((X ") * A)) * A) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X * (((X ") * A) * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * (((X ") * A) * A)) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

(a,b,A,X) . p1 is Relation-like Function-like set
(((a,b,A,X) ") ") . (((X ") * A) * A) is Relation-like Function-like set
p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
((a,b,A,X) ") . p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
a is non empty set
[:a,a:] is non empty Relation-like set
bool [:a,a:] is non empty set
b is non empty set
[:b,b:] is non empty Relation-like set
bool [:b,b:] is non empty set
Funcs (a,b) is non empty functional FUNCTION_DOMAIN of a,b

(a,b,A,X) is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]
[:(Funcs (a,b)),(Funcs (a,b)):] is non empty Relation-like set
bool [:(Funcs (a,b)),(Funcs (a,b)):] is non empty set
(a,b,A,X) " is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]

(a,b,(A "),(X ")) is non empty Relation-like Funcs (a,b) -defined Funcs (a,b) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (a,b)),(Funcs (a,b)):]

((a,b,A,X) ") . A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
(X ") * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set
((X ") * A) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]

((X ") * A) * ((A ") ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(a,b,(A "),(X ")) . A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
a is non empty set
b is non empty set
A is non empty set
Funcs (b,A) is non empty functional FUNCTION_DOMAIN of b,A
[:a,(Funcs (b,A)):] is non empty Relation-like set
bool [:a,(Funcs (b,A)):] is non empty set
[:a,b:] is non empty Relation-like set
bool [:a,b:] is non empty set
[:b,b:] is non empty Relation-like set
bool [:b,b:] is non empty set
[:A,A:] is non empty Relation-like set
bool [:A,A:] is non empty set
X is non empty Relation-like a -defined Funcs (b,A) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]

(b,A,p1,p1) is non empty Relation-like Funcs (b,A) -defined Funcs (b,A) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs (b,A)),(Funcs (b,A)):]
[:(Funcs (b,A)),(Funcs (b,A)):] is non empty Relation-like set
bool [:(Funcs (b,A)),(Funcs (b,A)):] is non empty set
(b,A,p1,p1) * X is non empty Relation-like a -defined Funcs (b,A) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
((b,A,p1,p1) * X) .. (p1 * A) is Relation-like Function-like set
(X .. A) * p1 is Relation-like A -valued Function-like set
dom ((b,A,p1,p1) * X) is non empty set
dom p1 is non empty set
rng (X .. A) is set
dom X is non empty set
dom (X .. A) is set
dom ((X .. A) * p1) is set
V is set
((X .. A) * p1) . V is set
((b,A,p1,p1) * X) . V is Relation-like Function-like set
(p1 * A) . V is set
(((b,A,p1,p1) * X) . V) . ((p1 * A) . V) is set
[:b,A:] is non empty Relation-like set
bool [:b,A:] is non empty set

A . V is set

dom V is non empty set

dom (p1 ") is non empty set
(X .. A) . V is set
p1 . ((X .. A) . V) is set
V . (A . V) is set
p1 . (V . (A . V)) is set

(p1 * V) . (A . V) is set

(id b) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((id b) * A) . V is set
(p1 * V) . (((id b) * A) . V) is set

((p1 ") * p1) * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(((p1 ") * p1) * A) . V is set
(p1 * V) . ((((p1 ") * p1) * A) . V) is set
(p1 ") * (p1 * A) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
((p1 ") * (p1 * A)) . V is set
(p1 * V) . (((p1 ") * (p1 * A)) . V) is set
(p1 ") . ((p1 * A) . V) is set
(p1 * V) . ((p1 ") . ((p1 * A) . V)) is set
(p1 * V) * (p1 ") is non empty Relation-like b -defined A -valued Function-like total quasi_total Element of bool [:b,A:]
((p1 * V) * (p1 ")) . ((p1 * A) . V) is set
(b,A,p1,p1) . V is Relation-like Function-like set
((b,A,p1,p1) . V) . ((p1 * A) . V) is set

b . VERUM is set
A is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT

b . (prop A) is set
a . A is non empty set

K155(K160(NAT,2),X) is Relation-like Function-like V51() set
K155(K155(K160(NAT,2),X),A) is Relation-like Function-like V51() set
b . (X '&' A) is set
b . X is set
b . A is set
[:(b . X),(b . A):] is Relation-like set

K155(K160(NAT,1),p1) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),p1),p1) is Relation-like Function-like V51() set
b . (p1 => p1) is set
b . p1 is set
b . p1 is set
Funcs ((b . p1),(b . p1)) is functional set

b . VERUM is set

A . VERUM is set

b . X is set
A . X is set

b . A is set
A . A is set

K155(K160(NAT,2),X) is Relation-like Function-like V51() set
K155(K155(K160(NAT,2),X),A) is Relation-like Function-like V51() set
b . (X '&' A) is set
A . (X '&' A) is set

K155(K160(NAT,1),X) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),X),A) is Relation-like Function-like V51() set
b . (X => A) is set
A . (X => A) is set
[:(A . X),(A . A):] is Relation-like set
Funcs ((A . X),(A . A)) is functional set
X is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT

b . (prop X) is set
A . (prop X) is set
a . X is non empty set
X is set
b . X is set
A . X is set

(a) . b is set

(a,b) is set

(a) . b is set
A is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT

(a) . (prop A) is set
a . A is non empty set

(a) . A is set

(a) . X is set

K155(K160(NAT,2),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,2),A),X) is Relation-like Function-like V51() set
(a) . (A '&' X) is set

K155(K160(NAT,1),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),A),X) is Relation-like Function-like V51() set
(a) . (A => X) is set
[:((a) . A),((a) . X):] is Relation-like set
Funcs (((a) . A),((a) . X)) is functional set
(a) . VERUM is set

(a,VERUM) is non empty set

(a) . VERUM is set

a is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT

(b,(prop a)) is non empty set

(b) . (prop a) is set
b . a is non empty set

K155(K160(NAT,2),a) is Relation-like Function-like V51() set
K155(K155(K160(NAT,2),a),b) is Relation-like Function-like V51() set
(A,(a '&' b)) is non empty set

(A) . (a '&' b) is set
(A,a) is non empty set
(A) . a is set
(A,b) is non empty set
(A) . b is set
[:(A,a),(A,b):] is non empty Relation-like set

K155(K160(NAT,1),a) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),a),b) is Relation-like Function-like V51() set
(A,(a => b)) is non empty set

(A) . (a => b) is set
(A,a) is non empty set
(A) . a is set
(A,b) is non empty set
(A) . b is set
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)

K155(K160(NAT,1),b) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),b),A) is Relation-like Function-like V51() set
(a,(b => A)) is non empty set

(a) . (b => A) is set
X is set
(a,b) is non empty set
(a) . b is set
(a,A) is non empty set
(a) . A is set
Funcs ((a,b),(a,A)) is non empty functional FUNCTION_DOMAIN of (a,b),(a,A)

K155(K160(NAT,1),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),A),X) is Relation-like Function-like V51() set
b => (A => X) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),b) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),b),(A => X)) is Relation-like Function-like V51() set
(a,(b => (A => X))) is non empty functional set

(a) . (b => (A => X)) is set
A is Relation-like Function-like Element of (a,(b => (A => X)))
p1 is set
dom A is set
A . p1 is set
(a,b) is non empty set
(a) . b is set
(a,(A => X)) is non empty functional set
(a) . (A => X) is set
Funcs ((a,b),(a,(A => X))) is non empty functional FUNCTION_DOMAIN of (a,b),(a,(A => X))
[:(a,b),(a,(A => X)):] is non empty Relation-like set
bool [:(a,b),(a,(A => X)):] is non empty set

K155(K160(NAT,1),b) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),b),A) is Relation-like Function-like V51() set
(a,(b => A)) is non empty functional set

(a) . (b => A) is set

K155(K155(K160(NAT,1),b),X) is Relation-like Function-like V51() set
(a,(b => X)) is non empty functional set
(a) . (b => X) is set
[:(a,(b => A)),(a,(b => X)):] is non empty Relation-like set
bool [:(a,(b => A)),(a,(b => X)):] is non empty set
the non empty Relation-like (a,(b => A)) -defined (a,(b => X)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(a,(b => A)),(a,(b => X)):] is non empty Relation-like (a,(b => A)) -defined (a,(b => X)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(a,(b => A)),(a,(b => X)):]

K155(K160(NAT,1),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),A),X) is Relation-like Function-like V51() set
b => (A => X) is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),b),(A => X)) is Relation-like Function-like V51() set
(a,(b => (A => X))) is non empty functional set
(a) . (b => (A => X)) is set
the Relation-like Function-like Function-yielding V55() Element of (a,(b => (A => X))) is Relation-like Function-like Function-yielding V55() Element of (a,(b => (A => X)))

dom (id a) is non empty set
b is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT

a . b is non empty set
[:(a . b),(a . b):] is non empty Relation-like set
bool [:(a . b),(a . b):] is non empty set
(id a) . b is non empty Relation-like a . b -defined a . b -valued Function-like total quasi_total Element of bool [:(a . b),(a . b):]
id (a . b) is non empty Relation-like a . b -defined a . b -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(a . b),(a . b):]

(a,A) is non empty set
(a) . A is set
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set

(a,X) is non empty set
(a) . X is set
[:(a,X),(a,X):] is non empty Relation-like set
bool [:(a,X),(a,X):] is non empty set
A is set
p1 is set
V is non empty Relation-like (a,A) -defined (a,A) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,A),(a,A):]
p1 is non empty Relation-like (a,X) -defined (a,X) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,X),(a,X):]
[:V,p1:] is non empty Relation-like [:(a,A),(a,X):] -defined [:(a,A),(a,X):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,A),(a,X):],[:(a,A),(a,X):]:]
[:(a,A),(a,X):] is non empty Relation-like set
[:[:(a,A),(a,X):],[:(a,A),(a,X):]:] is non empty Relation-like set
bool [:[:(a,A),(a,X):],[:(a,A),(a,X):]:] is non empty set

(a,A) is non empty set
(a) . A is set
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set

(a,X) is non empty set
(a) . X is set
[:(a,X),(a,X):] is non empty Relation-like set
bool [:(a,X),(a,X):] is non empty set
A is set
p1 is set
V is non empty Relation-like (a,A) -defined (a,A) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,A),(a,A):]
p1 is non empty Relation-like (a,X) -defined (a,X) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,X),(a,X)