:: 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
{} is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() set
the ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() set is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() 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({{}})
[:K292({{}}),{{}}:] is Relation-like set
bool [:K292({{}}),{{}}:] is non empty set
PFuncs (K292({{}}),{{}}) is non empty functional set
HP-WFF is non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed 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
HP_TAUT is functional Hilbert_theory Element of bool HP-WFF
{} HP-WFF is ext-real empty trivial proper V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() Element of bool HP-WFF
CnPos ({} HP-WFF) is functional Hilbert_theory Element of bool HP-WFF
INT is non empty V43() set
2 is ext-real non empty V7() V8() V9() V13() complex V15() integer Element of NAT
0 is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() 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 ext-real complex V15() integer set
a - 1 is ext-real complex V15() integer set
b is ext-real complex V15() integer set
b - 1 is ext-real complex V15() integer set
a is ext-real complex V15() integer set
a - 1 is ext-real complex V15() integer set
b is ext-real complex V15() integer set
b - 1 is ext-real complex V15() integer 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
X is Relation-like a -defined a -valued Function-like total quasi_total Element of bool [:a,a:]
dom X is set
X . b is set
rng X is set
a is Relation-like Function-like Function-yielding V55() set
rng a is set
SubFuncs (rng a) is set
b is set
dom a is set
A is set
a . A is Relation-like Function-like set
b is set
A is set
A is set
a is set
b is set
Funcs (a,b) is functional set
X is Relation-like Function-like 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
a --> b is Relation-like a -defined {b} -valued Function-like constant total quasi_total Element of bool [:a,{b}:]
{b} is non empty trivial set
[:a,{b}:] is Relation-like set
bool [:a,{b}:] is non empty set
X is Relation-like a -defined Funcs (b,A) -valued Function-like quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
doms X is Relation-like Function-like set
p1 is set
A is Relation-like a -defined Function-like total Function-yielding V55() set
A . p1 is Relation-like Function-like set
doms A is Relation-like a -defined Function-like total set
(doms A) . p1 is set
dom (A . p1) is set
(a --> b) . p1 is set
a is set
{} . a is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() set
{0,1} is non empty set
(0,1) --> (1,0) is non empty Relation-like NAT -defined {0,1} -defined NAT -valued Function-like one-to-one total quasi_total Element of bool [:{0,1},NAT:]
[:{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
chi (b,a) is Relation-like a -defined {{},1} -valued Function-like total quasi_total Element of bool [:a,{{},1}:]
[: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:]
[:a,NAT:] is Relation-like set
bool [:a,NAT:] is non empty set
b ` is Element of bool a
a \ b is set
chi ((b `),a) is Relation-like a -defined {{},1} -valued Function-like total quasi_total Element of bool [:a,{{},1}:]
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
chi ((b `),a) is Relation-like a -defined {{},1} -valued Function-like total quasi_total Element of bool [:a,{{},1}:]
[: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:]
[:a,NAT:] is Relation-like set
bool [:a,NAT:] is non empty set
chi (b,a) is Relation-like a -defined {{},1} -valued Function-like total quasi_total Element of bool [:a,{{},1}:]
(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 is non empty Relation-like 2 -defined a -valued Function-like total quasi_total Element of bool [:2,a:]
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
A 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 Relation-like Function-like one-to-one set
b is Relation-like Function-like one-to-one set
[:a,b:] is Relation-like Function-like 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
pr1 (A,X) is Relation-like [:A,X:] -defined A -valued Function-like quasi_total Element of bool [:[:A,X:],A:]
[:[:A,X:],A:] is Relation-like set
bool [:[:A,X:],A:] is non empty set
A is Relation-like A -defined a -valued Function-like total quasi_total Element of bool [:A,a:]
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
p1 is Relation-like X -defined b -valued Function-like total quasi_total Element of bool [:X,b:]
[:A,p1:] is Relation-like [:A,X:] -defined [:a,b:] -valued Function-like total quasi_total Element of bool [:[:A,X:],[:a,b:]:]
[:[: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
pr2 (A,X) is Relation-like [:A,X:] -defined X -valued Function-like quasi_total Element of bool [:[:A,X:],X:]
[:[: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:]
p1 is Relation-like [:A,X:] -defined a -valued Function-like total quasi_total Element of bool [:[:A,X:],a:]
V is Relation-like [:A,X:] -defined b -valued Function-like total quasi_total Element of bool [:[:A,X:],b:]
<:p1,V:> is Relation-like [:A,X:] -defined [:a,b:] -valued Function-like total quasi_total Element of bool [:[:A,X:],[:a,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
pr2 (A,X) is Relation-like [:A,X:] -defined X -valued Function-like quasi_total Element of bool [:[:A,X:],X:]
[:[:A,X:],X:] is Relation-like set
bool [:[:A,X:],X:] is non empty set
A is Relation-like A -defined a -valued Function-like total quasi_total Element of bool [:A,a:]
p1 is Relation-like X -defined b -valued Function-like total quasi_total Element of bool [:X,b:]
[:A,p1:] is Relation-like [:A,X:] -defined [:a,b:] -valued Function-like total quasi_total Element of bool [:[:A,X:],[:a,b:]:]
[:[: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
pr1 (A,X) is Relation-like [:A,X:] -defined A -valued Function-like quasi_total Element of bool [:[:A,X:],A:]
[:[: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:]
p1 is Relation-like [:A,X:] -defined a -valued Function-like total quasi_total Element of bool [:[:A,X:],a:]
V is Relation-like [:A,X:] -defined b -valued Function-like total quasi_total Element of bool [:[:A,X:],b:]
<:p1,V:> is Relation-like [:A,X:] -defined [:a,b:] -valued Function-like total quasi_total Element of bool [:[:A,X:],[:a,b:]:]
(pr2 (a,b)) * <:p1,V:> is Relation-like [:A,X:] -defined b -valued Function-like total quasi_total Element of bool [:[:A,X:],b:]
a is Relation-like Function-like set
{} .. a is Relation-like Function-like set
dom {} is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() set
dom ({} .. a) is set
a is Relation-like Function-like Function-yielding V55() set
A is Relation-like Function-like set
b is Relation-like Function-like set
a .. b is Relation-like Function-like set
A * (a .. b) is Relation-like Function-like set
A * a is Relation-like Function-like Function-yielding V55() set
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
[:b,{}:] is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() set
bool [:b,{}:] is non empty set
A is Relation-like b -defined Funcs ({},a) -valued Function-like quasi_total Function-yielding V55() Element of bool [:b,(Funcs ({},a)):]
X is ext-real empty trivial non proper V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding b -defined {} -valued Function-like one-to-one constant functional non total quasi_total Function-yielding V55() Element of bool [:b,{}:]
A .. X is Relation-like Function-like 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 is Relation-like Function-like set
X . p1 is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() 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
X . the Element of b is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() Element of {}
{} . (X . the Element of b) is ext-real empty trivial V7() V8() V9() V11() V12() V13() complex V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V55() 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
X is Relation-like a -defined Funcs (b,A) -valued Function-like quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
A is Relation-like a -defined b -valued Function-like quasi_total Element of bool [:a,b:]
X .. A is Relation-like Function-like 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
X . p1 is Relation-like Function-like set
A . p1 is set
V is Relation-like b -defined A -valued Function-like quasi_total Element of bool [:b,A:]
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
X is Relation-like a -defined Funcs (b,A) -valued Function-like quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
Frege X is Relation-like product (doms X) -defined Function-like total Function-yielding V55() set
doms X is Relation-like Function-like set
product (doms X) is set
dom (Frege X) is set
a --> b is Relation-like a -defined {b} -valued Function-like constant total quasi_total Element of bool [:a,{b}:]
{b} is non empty trivial set
[:a,{b}:] is Relation-like 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
X is Relation-like a -defined Funcs (b,A) -valued Function-like quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
Frege X is Relation-like product (doms X) -defined Function-like total Function-yielding V55() set
doms X is Relation-like Function-like set
product (doms X) is set
rng (Frege X) is set
rng X is set
SubFuncs (rng X) is set
rngs X is Relation-like Function-like set
dom (rngs X) is set
X " (rng X) is set
dom X is set
a --> A is Relation-like a -defined {A} -valued Function-like constant total quasi_total Element of bool [:a,{A}:]
{A} is non empty trivial set
[:a,{A}:] is Relation-like set
bool [:a,{A}:] is non empty set
A is set
(rngs X) . A is set
(a --> A) . A is set
X . A is Relation-like Function-like 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
X is Relation-like a -defined Funcs (b,A) -valued Function-like quasi_total Function-yielding V55() Element of bool [:a,(Funcs (b,A)):]
Frege X is Relation-like product (doms X) -defined Function-like total Function-yielding V55() set
doms X is Relation-like Function-like set
product (doms X) is set
dom (Frege X) is set
rng (Frege 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 Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
[:A,X:] is Relation-like [:a,b:] -defined [:a,b:] -valued Function-like one-to-one total quasi_total Element of bool [:[:a,b:],[:a,b:]:]
rng A is set
rng X is set
rng [:A,X:] is Relation-like set
A is Relation-like [:a,b:] -defined [:a,b:] -valued Function-like total quasi_total Element of bool [:[:a,b:],[:a,b:]:]
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 is Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
[:A,X:] is Relation-like [:a,b:] -defined [:a,b:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:a,b:],[:a,b:]:]
[:[: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
A is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
A " is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is non empty Relation-like b -defined b -valued Function-like total quasi_total Element of bool [:b,b:]
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:]
(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)):]
p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
A . p1 is Relation-like Function-like 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 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 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:]
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 is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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
A " is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (a,b)
X * p1 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 * p1) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
V is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of Funcs (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 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(X * V) * (A ") is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
id a is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:a,a:]
(X * p1) * (id a) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
(A ") * A is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
(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 is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:b,b:]
(id b) * p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X " is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
(X ") * X is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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
p1 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X " is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
(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
A " is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
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 ") is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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 is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:b,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 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:]
A * (A ") is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
p1 * (A * (A ")) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
id a is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:a,a:]
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 is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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)):]
X " is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
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 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
id a is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:a,a:]
A * (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 Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
A * (A ") is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
A * (A * (A ")) is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
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 is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:b,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 ") is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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:]
p1 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 is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
A " is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
X is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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)):]
X " is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,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 is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of 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:]
(A ") " is non empty Relation-like a -defined a -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:a,a:]
((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)):]
A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
X .. A is Relation-like Function-like set
p1 is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
p1 * A is non empty Relation-like a -defined b -valued Function-like total quasi_total Element of bool [:a,b:]
p1 is non empty Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:A,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
X . V is Relation-like Function-like set
A . V is set
V is non empty Relation-like b -defined A -valued Function-like total quasi_total Element of bool [:b,A:]
dom V is non empty set
p1 " is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
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 is non empty Relation-like b -defined A -valued Function-like total quasi_total Element of bool [:b,A:]
(p1 * V) . (A . V) is set
id b is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:b,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) . V is set
(p1 * V) . (((id b) * A) . V) is set
(p1 ") * p1 is non empty Relation-like b -defined b -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:b,b:]
((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
VERUM is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,0) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is non empty Relation-like HP-WFF -defined Function-like total set
b . VERUM is set
A is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop A is Relation-like Function-like V51() Element of HP-WFF
b . (prop A) is set
a . A is non empty set
X is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
X '&' A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
p1 is Relation-like Function-like V51() Element of HP-WFF
p1 is Relation-like Function-like V51() Element of HP-WFF
p1 => p1 is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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 is non empty Relation-like HP-WFF -defined Function-like total set
b . VERUM is set
A is non empty Relation-like HP-WFF -defined Function-like total set
A . VERUM is set
X is Relation-like Function-like V51() Element of HP-WFF
b . X is set
A . X is set
A is Relation-like Function-like V51() Element of HP-WFF
b . A is set
A . A is set
X '&' A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
X => A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
prop X is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
b is Relation-like Function-like V51() Element of HP-WFF
(a) . b is set
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is Relation-like Function-like V51() Element of HP-WFF
(a,b) is set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . b is set
A is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop A is Relation-like Function-like V51() Element of HP-WFF
(a) . (prop A) is set
a . A is non empty set
A is Relation-like Function-like V51() Element of HP-WFF
(a) . A is set
X is Relation-like Function-like V51() Element of HP-WFF
(a) . X is set
A '&' X is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
A => X is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(a,VERUM) is non empty set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . VERUM is set
b is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
a is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop a is Relation-like Function-like V51() Element of HP-WFF
(b,(prop a)) is non empty set
(b) is non empty Relation-like HP-WFF -defined Function-like total set
(b) . (prop a) is set
b . a is non empty set
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a '&' b is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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) is non empty Relation-like HP-WFF -defined Function-like total 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
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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) is non empty Relation-like HP-WFF -defined Function-like total 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)
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
b => A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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) is non empty Relation-like HP-WFF -defined Function-like total 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)
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
X is Relation-like Function-like V51() Element of HP-WFF
A => X is Relation-like Function-like V51() Element of HP-WFF
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) is non empty Relation-like HP-WFF -defined Function-like total 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
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
b => A 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) is Relation-like Function-like V51() set
(a,(b => A)) is non empty functional set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . (b => A) is set
X is Relation-like Function-like V51() Element of HP-WFF
b => X is Relation-like Function-like V51() Element of HP-WFF
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)):]
A => X is Relation-like Function-like V51() Element of HP-WFF
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)))
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
id a is non empty Relation-like NAT -defined Function-like total Function-yielding V55() ManySortedFunction of a,a
dom (id a) is non empty set
b is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
(id a) . b is Relation-like Function-like set
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
id 1 is non empty Relation-like 1 -defined 1 -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:1,1:]
b is Relation-like Function-like (a)
A is Relation-like Function-like V51() Element of HP-WFF
(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
X is Relation-like Function-like V51() Element of HP-WFF
(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 is Relation-like Function-like V51() Element of HP-WFF
(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
X is Relation-like Function-like V51() Element of HP-WFF
(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):]
((a,A),(a,X),V,p1) is non empty Relation-like Funcs ((a,A),(a,X)) -defined Funcs ((a,A),(a,X)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):]
Funcs ((a,A),(a,X)) is non empty functional FUNCTION_DOMAIN of (a,A),(a,X)
[:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):] is non empty Relation-like set
bool [:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):] is non empty set
A is Relation-like Function-like V51() Element of HP-WFF
(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
X is Relation-like Function-like V51() Element of HP-WFF
(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):]
p0 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):]
p1 is set
((a,A),(a,X),V,p0) is non empty Relation-like Funcs ((a,A),(a,X)) -defined Funcs ((a,A),(a,X)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):]
Funcs ((a,A),(a,X)) is non empty functional FUNCTION_DOMAIN of (a,A),(a,X)
[:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):] is non empty Relation-like set
bool [:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):] is non empty set
f 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):]
p0 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 is set
((a,A),(a,X),f,p0) is non empty Relation-like Funcs ((a,A),(a,X)) -defined Funcs ((a,A),(a,X)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,X))),(Funcs ((a,A),(a,X))):]
A is Relation-like Function-like V51() Element of HP-WFF
(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
X is Relation-like Function-like V51() Element of HP-WFF
(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):]
p0 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):]
p1 is set
[:V,p0:] 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
f 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):]
p0 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 is set
[:f,p0:] 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 is non empty Relation-like HP-WFF -defined Function-like total set
A . VERUM is set
X is Relation-like Function-like V51() Element of HP-WFF
A . X is set
(a) . X is set
[:((a) . X),((a) . X):] is Relation-like set
bool [:((a) . X),((a) . X):] is non empty set
A is Relation-like Function-like V51() Element of HP-WFF
A . A is set
(a) . A is set
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
X '&' A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
A . (X '&' A) is set
(a) . (X '&' A) is set
[:((a) . (X '&' A)),((a) . (X '&' A)):] is Relation-like set
bool [:((a) . (X '&' A)),((a) . (X '&' A)):] is non empty set
X => A is Relation-like Function-like V51() Element of HP-WFF
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
A . (X => A) is set
(a) . (X => A) is set
[:((a) . (X => A)),((a) . (X => A)):] is Relation-like set
bool [:((a) . (X => A)),((a) . (X => A)):] is non empty set
(a,X) is non empty set
(a,A) is non empty set
[:(a,X),(a,A):] is non empty Relation-like set
[:(a,X),(a,X):] is non empty Relation-like set
bool [:(a,X),(a,X):] is non empty set
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set
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):]
p1 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,p1:] is non empty Relation-like [:(a,X),(a,A):] -defined [:(a,X),(a,A):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:]
[:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty Relation-like set
bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty set
Funcs ((a,X),(a,A)) is non empty functional FUNCTION_DOMAIN of (a,X),(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):]
p1 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):]
((a,X),(a,A),p1,p1) is non empty Relation-like Funcs ((a,X),(a,A)) -defined Funcs ((a,X),(a,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):]
[:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty Relation-like set
bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty set
A . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
(a) . VERUM is set
[:((a) . VERUM),((a) . VERUM):] is Relation-like set
bool [:((a) . VERUM),((a) . VERUM):] is non empty set
X is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop X is Relation-like Function-like V51() Element of HP-WFF
A . (prop X) is set
(a) . (prop X) is set
[:((a) . (prop X)),((a) . (prop X)):] is Relation-like set
bool [:((a) . (prop X)),((a) . (prop X)):] is non empty set
b . X is set
a . X is non empty set
X is set
A . X is set
(a) . X is set
[:((a) . X),((a) . X):] is Relation-like set
bool [:((a) . X),((a) . X):] is non empty set
X is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop X is Relation-like Function-like V51() Element of HP-WFF
A . (prop X) is set
b . X is set
X is Relation-like Function-like V51() Element of HP-WFF
(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 . X is Relation-like (a) . X -defined (a) . X -valued Function-like total quasi_total Element of bool [:((a) . X),((a) . X):]
[:((a) . X),((a) . X):] is Relation-like set
bool [:((a) . X),((a) . X):] is non empty set
A is Relation-like Function-like V51() Element of HP-WFF
(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 . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
X '&' A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
A . (X '&' A) is Relation-like (a) . (X '&' A) -defined (a) . (X '&' A) -valued Function-like total quasi_total Element of bool [:((a) . (X '&' A)),((a) . (X '&' A)):]
(a) . (X '&' A) is set
[:((a) . (X '&' A)),((a) . (X '&' A)):] is Relation-like set
bool [:((a) . (X '&' A)),((a) . (X '&' A)):] is non empty set
X => A is Relation-like Function-like V51() Element of HP-WFF
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
A . (X => A) is Relation-like (a) . (X => A) -defined (a) . (X => A) -valued Function-like total quasi_total Element of bool [:((a) . (X => A)),((a) . (X => A)):]
(a) . (X => A) is set
[:((a) . (X => A)),((a) . (X => A)):] is Relation-like set
bool [:((a) . (X => A)),((a) . (X => A)):] is non empty set
A . X is set
A . A is set
A . (X '&' A) is set
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):]
p1 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,p1:] is non empty Relation-like [:(a,X),(a,A):] -defined [:(a,X),(a,A):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:]
[:(a,X),(a,A):] is non empty Relation-like set
[:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty Relation-like set
bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty set
((a,X),(a,A),p1,p1) is non empty Relation-like Funcs ((a,X),(a,A)) -defined Funcs ((a,X),(a,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):]
Funcs ((a,X),(a,A)) is non empty functional FUNCTION_DOMAIN of (a,X),(a,A)
[:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty Relation-like set
bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty set
A . (X => A) is set
V 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 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):]
((a,X),(a,A),V,V) is non empty Relation-like Funcs ((a,X),(a,A)) -defined Funcs ((a,X),(a,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):]
A is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
A . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
(a) . VERUM is set
[:((a) . VERUM),((a) . VERUM):] is Relation-like set
bool [:((a) . VERUM),((a) . VERUM):] is non empty set
X is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
X . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
A is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop A is Relation-like Function-like V51() Element of HP-WFF
(a) . (prop A) is set
A . (prop A) is Relation-like (a) . (prop A) -defined (a) . (prop A) -valued Function-like total quasi_total Element of bool [:((a) . (prop A)),((a) . (prop A)):]
[:((a) . (prop A)),((a) . (prop A)):] is Relation-like set
bool [:((a) . (prop A)),((a) . (prop A)):] is non empty set
X . (prop A) is Relation-like (a) . (prop A) -defined (a) . (prop A) -valued Function-like total quasi_total Element of bool [:((a) . (prop A)),((a) . (prop A)):]
b . A is set
A is Relation-like Function-like V51() Element of HP-WFF
(a) . A is set
A . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
X . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
p1 is Relation-like Function-like V51() Element of HP-WFF
(a) . p1 is set
A . p1 is Relation-like (a) . p1 -defined (a) . p1 -valued Function-like total quasi_total Element of bool [:((a) . p1),((a) . p1):]
[:((a) . p1),((a) . p1):] is Relation-like set
bool [:((a) . p1),((a) . p1):] is non empty set
X . p1 is Relation-like (a) . p1 -defined (a) . p1 -valued Function-like total quasi_total Element of bool [:((a) . p1),((a) . p1):]
A '&' p1 is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
K155(K160(NAT,2),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,2),A),p1) is Relation-like Function-like V51() set
(a) . (A '&' p1) is set
A . (A '&' p1) is Relation-like (a) . (A '&' p1) -defined (a) . (A '&' p1) -valued Function-like total quasi_total Element of bool [:((a) . (A '&' p1)),((a) . (A '&' p1)):]
[:((a) . (A '&' p1)),((a) . (A '&' p1)):] is Relation-like set
bool [:((a) . (A '&' p1)),((a) . (A '&' p1)):] is non empty set
X . (A '&' p1) is Relation-like (a) . (A '&' p1) -defined (a) . (A '&' p1) -valued Function-like total quasi_total Element of bool [:((a) . (A '&' p1)),((a) . (A '&' p1)):]
A => p1 is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),A) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),A),p1) is Relation-like Function-like V51() set
(a) . (A => p1) is set
A . (A => p1) is Relation-like (a) . (A => p1) -defined (a) . (A => p1) -valued Function-like total quasi_total Element of bool [:((a) . (A => p1)),((a) . (A => p1)):]
[:((a) . (A => p1)),((a) . (A => p1)):] is Relation-like set
bool [:((a) . (A => p1)),((a) . (A => p1)):] is non empty set
X . (A => p1) is Relation-like (a) . (A => p1) -defined (a) . (A => p1) -valued Function-like total quasi_total Element of bool [:((a) . (A => p1)),((a) . (A => p1)):]
(a,A) is non empty set
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set
(a,p1) is non empty set
[:(a,p1),(a,p1):] is non empty Relation-like set
bool [:(a,p1),(a,p1):] is non empty set
p1 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):]
V is non empty Relation-like (a,p1) -defined (a,p1) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,p1),(a,p1):]
[:p1,V:] is non empty Relation-like [:(a,A),(a,p1):] -defined [:(a,A),(a,p1):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:]
[:(a,A),(a,p1):] is non empty Relation-like set
[:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:] is non empty Relation-like set
bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:] is non empty set
((a,A),(a,p1),p1,V) is non empty Relation-like Funcs ((a,A),(a,p1)) -defined Funcs ((a,A),(a,p1)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):]
Funcs ((a,A),(a,p1)) is non empty functional FUNCTION_DOMAIN of (a,A),(a,p1)
[:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):] is non empty Relation-like set
bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):] is non empty 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):]
p0 is non empty Relation-like (a,p1) -defined (a,p1) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,p1),(a,p1):]
[:V,p0:] is non empty Relation-like [:(a,A),(a,p1):] -defined [:(a,A),(a,p1):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:]
((a,A),(a,p1),V,p0) is non empty Relation-like Funcs ((a,A),(a,p1)) -defined Funcs ((a,A),(a,p1)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):]
p1 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):]
V is non empty Relation-like (a,p1) -defined (a,p1) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,p1),(a,p1):]
[:p1,V:] is non empty Relation-like [:(a,A),(a,p1):] -defined [:(a,A),(a,p1):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:]
[:(a,A),(a,p1):] is non empty Relation-like set
[:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:] is non empty Relation-like set
bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:] is non empty set
((a,A),(a,p1),p1,V) is non empty Relation-like Funcs ((a,A),(a,p1)) -defined Funcs ((a,A),(a,p1)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):]
Funcs ((a,A),(a,p1)) is non empty functional FUNCTION_DOMAIN of (a,A),(a,p1)
[:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):] is non empty Relation-like set
bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):] is non empty 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):]
p0 is non empty Relation-like (a,p1) -defined (a,p1) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,p1),(a,p1):]
[:V,p0:] is non empty Relation-like [:(a,A),(a,p1):] -defined [:(a,A),(a,p1):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,A),(a,p1):],[:(a,A),(a,p1):]:]
((a,A),(a,p1),V,p0) is non empty Relation-like Funcs ((a,A),(a,p1)) -defined Funcs ((a,A),(a,p1)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,A),(a,p1))),(Funcs ((a,A),(a,p1))):]
A is set
A . A is Relation-like Function-like set
X . A is Relation-like Function-like set
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
b is Relation-like Function-like (a)
(a,b) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
A is Relation-like Function-like V51() Element of HP-WFF
(a,b) . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
(a) . A is set
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
(a,A) is non empty set
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(a,VERUM) is non empty set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . VERUM is set
id (a,VERUM) is non empty Relation-like (a,VERUM) -defined (a,VERUM) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(a,VERUM),(a,VERUM):]
[:(a,VERUM),(a,VERUM):] is non empty Relation-like set
bool [:(a,VERUM),(a,VERUM):] is non empty set
b is Relation-like Function-like (a)
(a,b,VERUM) is non empty Relation-like (a,VERUM) -defined (a,VERUM) -valued Function-like total quasi_total Element of bool [:(a,VERUM),(a,VERUM):]
(a,b) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
(a,b) . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
[:((a) . VERUM),((a) . VERUM):] is Relation-like set
bool [:((a) . VERUM),((a) . VERUM):] is non empty set
b is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
A is Relation-like Function-like (b)
a is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop a is Relation-like Function-like V51() Element of HP-WFF
(b,A,(prop a)) is non empty Relation-like (b,(prop a)) -defined (b,(prop a)) -valued Function-like total quasi_total Element of bool [:(b,(prop a)),(b,(prop a)):]
(b,(prop a)) is non empty set
(b) is non empty Relation-like HP-WFF -defined Function-like total set
(b) . (prop a) is set
[:(b,(prop a)),(b,(prop a)):] is non empty Relation-like set
bool [:(b,(prop a)),(b,(prop a)):] is non empty set
(b,A) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (b),(b)
(b,A) . (prop a) is Relation-like (b) . (prop a) -defined (b) . (prop a) -valued Function-like total quasi_total Element of bool [:((b) . (prop a)),((b) . (prop a)):]
[:((b) . (prop a)),((b) . (prop a)):] is Relation-like set
bool [:((b) . (prop a)),((b) . (prop a)):] is non empty set
A . a is set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a '&' b is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,(a '&' b)) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
X is Relation-like Function-like (A)
(A,X,(a '&' b)) is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
[:(A,(a '&' b)),(A,(a '&' b)):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,(a '&' b)):] is non empty set
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . (a '&' b) is Relation-like (A) . (a '&' b) -defined (A) . (a '&' b) -valued Function-like total quasi_total Element of bool [:((A) . (a '&' b)),((A) . (a '&' b)):]
[:((A) . (a '&' b)),((A) . (a '&' b)):] is Relation-like set
bool [:((A) . (a '&' b)),((A) . (a '&' b)):] is non empty set
(A,X,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,a),(A,a):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
[:(A,X,a),(A,X,b):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like total quasi_total Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty Relation-like set
bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty set
a => b is Relation-like Function-like V51() Element of HP-WFF
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,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
(A) . (a => b) is set
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
A 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,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:A,p1:] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
((A,a),(A,b),A,p1) is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
[:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty Relation-like set
bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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,b) is non empty set
(A) . b is set
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
X is Relation-like Function-like (A)
(A,X,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,a),(A,a):]
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,b),(A,b):]
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
a '&' b is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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,X) . (a '&' b) is Relation-like (A) . (a '&' b) -defined (A) . (a '&' b) -valued Function-like total quasi_total Element of bool [:((A) . (a '&' b)),((A) . (a '&' b)):]
(A) . (a '&' b) is set
[:((A) . (a '&' b)),((A) . (a '&' b)):] is Relation-like set
bool [:((A) . (a '&' b)),((A) . (a '&' b)):] is non empty set
A 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,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
((A,a),(A,b),A,p1) is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
[:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty Relation-like set
bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty set
p1 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):]
V is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:p1,V:] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:(A,a),(A,b):] is non empty Relation-like set
[:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty Relation-like set
bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty set
((A,a),(A,b),p1,V) is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
A is Relation-like Function-like V51() Element of HP-WFF
(a,A) is non empty set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . A is set
b is Relation-like Function-like (a)
(a,b,A) is non empty Relation-like (a,A) -defined (a,A) -valued Function-like total quasi_total Element of bool [:(a,A),(a,A):]
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set
(a,b) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
(a,b) . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
X is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop X is Relation-like Function-like V51() Element of HP-WFF
(a,(prop X)) is non empty set
(a) . (prop X) is set
(a,b,(prop X)) is non empty Relation-like (a,(prop X)) -defined (a,(prop X)) -valued Function-like total quasi_total Element of bool [:(a,(prop X)),(a,(prop X)):]
[:(a,(prop X)),(a,(prop X)):] is non empty Relation-like set
bool [:(a,(prop X)),(a,(prop X)):] is non empty set
(a,b) . (prop X) is Relation-like (a) . (prop X) -defined (a) . (prop X) -valued Function-like total quasi_total Element of bool [:((a) . (prop X)),((a) . (prop X)):]
[:((a) . (prop X)),((a) . (prop X)):] is Relation-like set
bool [:((a) . (prop X)),((a) . (prop X)):] is non empty set
a . X is non empty set
b . X is set
X is Relation-like Function-like V51() Element of HP-WFF
(a,X) is non empty set
(a) . X is set
(a,b,X) is non empty Relation-like (a,X) -defined (a,X) -valued Function-like total quasi_total Element of bool [:(a,X),(a,X):]
[:(a,X),(a,X):] is non empty Relation-like set
bool [:(a,X),(a,X):] is non empty set
(a,b) . X is Relation-like (a) . X -defined (a) . X -valued Function-like total quasi_total Element of bool [:((a) . X),((a) . X):]
[:((a) . X),((a) . X):] is Relation-like set
bool [:((a) . X),((a) . X):] is non empty set
A is Relation-like Function-like V51() Element of HP-WFF
(a,A) is non empty set
(a) . A is set
(a,b,A) is non empty Relation-like (a,A) -defined (a,A) -valued Function-like total quasi_total Element of bool [:(a,A),(a,A):]
[:(a,A),(a,A):] is non empty Relation-like set
bool [:(a,A),(a,A):] is non empty set
(a,b) . A is Relation-like (a) . A -defined (a) . A -valued Function-like total quasi_total Element of bool [:((a) . A),((a) . A):]
[:((a) . A),((a) . A):] is Relation-like set
bool [:((a) . A),((a) . A):] is non empty set
X '&' A is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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
(a,(X '&' A)) is non empty set
(a) . (X '&' A) is set
(a,b,(X '&' A)) is non empty Relation-like (a,(X '&' A)) -defined (a,(X '&' A)) -valued Function-like total quasi_total Element of bool [:(a,(X '&' A)),(a,(X '&' A)):]
[:(a,(X '&' A)),(a,(X '&' A)):] is non empty Relation-like set
bool [:(a,(X '&' A)),(a,(X '&' A)):] is non empty set
(a,b) . (X '&' A) is Relation-like (a) . (X '&' A) -defined (a) . (X '&' A) -valued Function-like total quasi_total Element of bool [:((a) . (X '&' A)),((a) . (X '&' A)):]
[:((a) . (X '&' A)),((a) . (X '&' A)):] is Relation-like set
bool [:((a) . (X '&' A)),((a) . (X '&' A)):] is non empty set
X => A is Relation-like Function-like V51() Element of HP-WFF
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
(a,(X => A)) is non empty functional set
(a) . (X => A) is set
(a,b,(X => A)) is non empty Relation-like (a,(X => A)) -defined (a,(X => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(a,(X => A)),(a,(X => A)):]
[:(a,(X => A)),(a,(X => A)):] is non empty Relation-like set
bool [:(a,(X => A)),(a,(X => A)):] is non empty set
(a,b) . (X => A) is Relation-like (a) . (X => A) -defined (a) . (X => A) -valued Function-like total quasi_total Element of bool [:((a) . (X => A)),((a) . (X => A)):]
[:((a) . (X => A)),((a) . (X => A)):] is Relation-like set
bool [:((a) . (X => A)),((a) . (X => A)):] is non empty set
[:(a,X),(a,A):] is non empty Relation-like set
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):]
p1 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,p1:] is non empty Relation-like [:(a,X),(a,A):] -defined [:(a,X),(a,A):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:]
[:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty Relation-like set
bool [:[:(a,X),(a,A):],[:(a,X),(a,A):]:] is non empty set
Funcs ((a,X),(a,A)) is non empty functional FUNCTION_DOMAIN of (a,X),(a,A)
((a,X),(a,A),p1,p1) is non empty Relation-like Funcs ((a,X),(a,A)) -defined Funcs ((a,X),(a,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):]
[:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty Relation-like set
bool [:(Funcs ((a,X),(a,A))),(Funcs ((a,X),(a,A))):] is non empty set
(a,VERUM) is non empty set
(a) . VERUM is set
(a,b,VERUM) is non empty Relation-like (a,VERUM) -defined (a,VERUM) -valued Function-like total quasi_total Element of bool [:(a,VERUM),(a,VERUM):]
[:(a,VERUM),(a,VERUM):] is non empty Relation-like set
bool [:(a,VERUM),(a,VERUM):] is non empty set
(a,b) . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
[:((a) . VERUM),((a) . VERUM):] is Relation-like set
bool [:((a) . VERUM),((a) . VERUM):] is non empty set
id (a,VERUM) is non empty Relation-like (a,VERUM) -defined (a,VERUM) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(a,VERUM),(a,VERUM):]
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
bool [:(A,a),(A,b):] is non empty set
X is Relation-like Function-like (A)
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
(A,X,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,a) " 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):]
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
A is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(A,X,(a => b)) . A is Relation-like Function-like set
(A,X,b) * A is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
((A,X,b) * A) * ((A,X,a) ") is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
((A,a),(A,b),(A,X,a),(A,X,b)) is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
[:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty Relation-like set
bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty set
((A,a),(A,b),(A,X,a),(A,X,b)) . A is Relation-like Function-like set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
bool [:(A,a),(A,b):] is non empty set
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
X is Relation-like Function-like (A)
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
(A,X,(a => b)) " is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,X,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,X,b) " is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
A is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
((A,X,(a => b)) ") . A is Relation-like Function-like set
((A,X,b) ") * A is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(((A,X,b) ") * A) * (A,X,a) is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
((A,a),(A,b),(A,X,a),(A,X,b)) is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
[:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty Relation-like set
bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):] is non empty set
((A,a),(A,b),(A,X,a),(A,X,b)) " is non empty Relation-like Funcs ((A,a),(A,b)) -defined Funcs ((A,a),(A,b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((A,a),(A,b))),(Funcs ((A,a),(A,b))):]
(((A,a),(A,b),(A,X,a),(A,X,b)) ") . A is Relation-like Function-like set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
bool [:(A,a),(A,b):] is non empty set
X is Relation-like Function-like (A)
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,X,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
A is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
p1 is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(A,X,(a => b)) . p1 is Relation-like Function-like set
(A,X,b) * p1 is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
A * (A,X,a) is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
id (A,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(A,a),(A,a):]
((A,X,b) * p1) * (id (A,a)) is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(A,X,a) " 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):]
((A,X,a) ") * (A,X,a) 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):]
((A,X,b) * p1) * (((A,X,a) ") * (A,X,a)) is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
((A,X,b) * p1) * ((A,X,a) ") is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(((A,X,b) * p1) * ((A,X,a) ")) * (A,X,a) is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
X is Relation-like Function-like (A)
(A,X,a) 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):]
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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 Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
(A,b) is non empty set
(A) . b is set
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
A is set
p1 is Relation-like Function-like set
p1 . A is set
dom (A,X,(a => b)) is non empty set
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
[:(A,a),(A,b):] is non empty Relation-like set
bool [:(A,a),(A,b):] is non empty set
(A,X,(a => b)) . p1 is Relation-like Function-like set
(A,X,a) " 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,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
(A,X,b) * p1 is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
((A,X,b) * p1) * ((A,X,a) ") is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
V is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
dom (A,X,a) is non empty set
dom (A,X,b) is non empty set
(A,X,b) . (p1 . A) is set
((A,X,b) * p1) . A is set
(A,X,a) * p1 is Relation-like (A,a) -defined Function-like set
((A,X,a) * p1) . A is set
(A,X,a) . A is set
p1 . ((A,X,a) . A) is set
a is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
b is Relation-like Function-like (a)
(a,b,VERUM) is non empty Relation-like (a,VERUM) -defined (a,VERUM) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(a,VERUM),(a,VERUM):]
(a,VERUM) is non empty set
(a) is non empty Relation-like HP-WFF -defined Function-like total set
(a) . VERUM is set
[:(a,VERUM),(a,VERUM):] is non empty Relation-like set
bool [:(a,VERUM),(a,VERUM):] is non empty set
(a,b) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (a),(a)
(a,b) . VERUM is Relation-like (a) . VERUM -defined (a) . VERUM -valued Function-like total quasi_total Element of bool [:((a) . VERUM),((a) . VERUM):]
[:((a) . VERUM),((a) . VERUM):] is Relation-like set
bool [:((a) . VERUM),((a) . VERUM):] is non empty set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
b => a 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) is Relation-like Function-like V51() set
a => (b => a) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),a) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),a),(b => a)) is Relation-like Function-like V51() set
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,b) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total set
(A) . b is set
(A,a) is non empty set
(A) . a is set
(A,(b => a)) is non empty functional set
(A) . (b => a) is set
X is Element of (A,a)
(A,b) --> X is non empty Relation-like (A,b) -defined (A,a) -valued {X} -valued Function-like constant total quasi_total Element of bool [:(A,b),{X}:]
{X} is non empty trivial set
[:(A,b),{X}:] is non empty Relation-like set
bool [:(A,b),{X}:] is non empty set
(A,b) --> X is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
[:(A,b),(A,a):] is non empty Relation-like set
bool [:(A,b),(A,a):] is non empty set
Funcs ((A,b),(A,a)) is non empty functional FUNCTION_DOMAIN of (A,b),(A,a)
[:(A,a),(A,(b => a)):] is non empty Relation-like set
bool [:(A,a),(A,(b => a)):] is non empty set
X is non empty Relation-like (A,a) -defined (A,(b => a)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => a)):]
A is Relation-like Function-like (A)
(A,A,(a => (b => a))) is non empty Relation-like (A,(a => (b => a))) -defined (A,(a => (b => a))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => (b => a))),(A,(a => (b => a))):]
(A,(a => (b => a))) is non empty functional set
(A) . (a => (b => a)) is set
[:(A,(a => (b => a))),(A,(a => (b => a))):] is non empty Relation-like set
bool [:(A,(a => (b => a))),(A,(a => (b => a))):] is non empty set
(A,A) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,A) . (a => (b => a)) is Relation-like (A) . (a => (b => a)) -defined (A) . (a => (b => a)) -valued Function-like total quasi_total Element of bool [:((A) . (a => (b => a))),((A) . (a => (b => a))):]
[:((A) . (a => (b => a))),((A) . (a => (b => a))):] is Relation-like set
bool [:((A) . (a => (b => a))),((A) . (a => (b => a))):] is non empty set
Funcs ((A,a),(A,(b => a))) is non empty functional FUNCTION_DOMAIN of (A,a),(A,(b => a))
dom (A,A,(a => (b => a))) is non empty set
(A,A,(a => (b => a))) . X is Relation-like Function-like set
[:(A,b),(A,a):] is non empty Relation-like set
bool [:(A,b),(A,a):] is non empty set
(A,A,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,A) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,A,a) " 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 Element of (A,a)
((A,A,a) ") . p1 is Element of (A,a)
(A,b) --> (((A,A,a) ") . p1) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
{(((A,A,a) ") . p1)} is non empty trivial set
[:(A,b),{(((A,A,a) ") . p1)}:] is non empty Relation-like set
rng (A,A,a) is non empty set
dom (A,A,a) is non empty set
X . p1 is Relation-like Function-like Element of (A,(b => a))
(A,b) --> p1 is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
{p1} is non empty trivial set
[:(A,b),{p1}:] is non empty Relation-like set
id (A,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(A,a),(A,a):]
(id (A,a)) . p1 is Element of (A,a)
(A,b) --> ((id (A,a)) . p1) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
{((id (A,a)) . p1)} is non empty trivial set
[:(A,b),{((id (A,a)) . p1)}:] is non empty Relation-like set
(A,A,a) * ((A,A,a) ") 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):]
((A,A,a) * ((A,A,a) ")) . p1 is Element of (A,a)
(A,b) --> (((A,A,a) * ((A,A,a) ")) . p1) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
{(((A,A,a) * ((A,A,a) ")) . p1)} is non empty trivial set
[:(A,b),{(((A,A,a) * ((A,A,a) ")) . p1)}:] is non empty Relation-like set
(A,A,a) . (((A,A,a) ") . p1) is Element of (A,a)
(A,b) --> ((A,A,a) . (((A,A,a) ") . p1)) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(A,b),(A,a):]
{((A,A,a) . (((A,A,a) ") . p1))} is non empty trivial set
[:(A,b),{((A,A,a) . (((A,A,a) ") . p1))}:] is non empty Relation-like set
(A,A,a) * ((A,b) --> (((A,A,a) ") . p1)) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
(A,A,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,A) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,A,b) " is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
((A,A,b) ") " (A,b) is set
(((A,A,b) ") " (A,b)) --> (((A,A,a) ") . p1) is Relation-like ((A,A,b) ") " (A,b) -defined (A,a) -valued Function-like constant total quasi_total Element of bool [:(((A,A,b) ") " (A,b)),(A,a):]
[:(((A,A,b) ") " (A,b)),(A,a):] is Relation-like set
bool [:(((A,A,b) ") " (A,b)),(A,a):] is non empty set
[:(((A,A,b) ") " (A,b)),{(((A,A,a) ") . p1)}:] is Relation-like set
(A,A,a) * ((((A,A,b) ") " (A,b)) --> (((A,A,a) ") . p1)) is Relation-like ((A,A,b) ") " (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(((A,A,b) ") " (A,b)),(A,a):]
p1 is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
p1 * ((A,A,b) ") is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
(A,A,a) * (p1 * ((A,A,b) ")) is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
(A,A,a) * p1 is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
((A,A,a) * p1) * ((A,A,b) ") is non empty Relation-like (A,b) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,b),(A,a):]
(A,A,(b => a)) is non empty Relation-like (A,(b => a)) -defined (A,(b => a)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(b => a)),(A,(b => a)):]
[:(A,(b => a)),(A,(b => a)):] is non empty Relation-like set
bool [:(A,(b => a)),(A,(b => a)):] is non empty set
(A,A) . (b => a) is Relation-like (A) . (b => a) -defined (A) . (b => a) -valued Function-like total quasi_total Element of bool [:((A) . (b => a)),((A) . (b => a)):]
[:((A) . (b => a)),((A) . (b => a)):] is Relation-like set
bool [:((A) . (b => a)),((A) . (b => a)):] is non empty set
(A,A,(b => a)) . p1 is Relation-like Function-like set
X . (((A,A,a) ") . p1) is Relation-like Function-like Element of (A,(b => a))
(A,A,(b => a)) . (X . (((A,A,a) ") . p1)) is Relation-like Function-like Element of (A,(b => a))
(A,A,(b => a)) * X is non empty Relation-like (A,a) -defined (A,(b => a)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => a)):]
((A,A,(b => a)) * X) . (((A,A,a) ") . p1) is Relation-like Function-like Element of (A,(b => a))
((A,A,(b => a)) * X) * ((A,A,a) ") is non empty Relation-like (A,a) -defined (A,(b => a)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => a)):]
(((A,A,(b => a)) * X) * ((A,A,a) ")) . p1 is Relation-like Function-like Element of (A,(b => a))
a '&' b is Relation-like Function-like V51() Element of HP-WFF
K160(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V51() M7( NAT )
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 '&' b) => a is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(a '&' b)) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(a '&' b)),a) is Relation-like Function-like V51() set
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
[:[:(A,a),(A,b):],(A,a):] is non empty Relation-like set
bool [:[:(A,a),(A,b):],(A,a):] is non empty set
pr1 ((A,a),(A,b)) is non empty Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like total quasi_total Element of bool [:[:(A,a),(A,b):],(A,a):]
X is non empty Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like total quasi_total Element of bool [:[:(A,a),(A,b):],(A,a):]
A is Relation-like Function-like (A)
(A,A,((a '&' b) => a)) is non empty Relation-like (A,((a '&' b) => a)) -defined (A,((a '&' b) => a)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,((a '&' b) => a)),(A,((a '&' b) => a)):]
(A,((a '&' b) => a)) is non empty functional set
(A) . ((a '&' b) => a) is set
[:(A,((a '&' b) => a)),(A,((a '&' b) => a)):] is non empty Relation-like set
bool [:(A,((a '&' b) => a)),(A,((a '&' b) => a)):] is non empty set
(A,A) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,A) . ((a '&' b) => a) is Relation-like (A) . ((a '&' b) => a) -defined (A) . ((a '&' b) => a) -valued Function-like total quasi_total Element of bool [:((A) . ((a '&' b) => a)),((A) . ((a '&' b) => a)):]
[:((A) . ((a '&' b) => a)),((A) . ((a '&' b) => a)):] is Relation-like set
bool [:((A) . ((a '&' b) => a)),((A) . ((a '&' b) => a)):] is non empty set
dom (A,A,((a '&' b) => a)) is non empty set
(A,(a '&' b)) is non empty set
(A) . (a '&' b) is set
Funcs ((A,(a '&' b)),(A,a)) is non empty functional FUNCTION_DOMAIN of (A,(a '&' b)),(A,a)
Funcs ([:(A,a),(A,b):],(A,a)) is non empty functional FUNCTION_DOMAIN of [:(A,a),(A,b):],(A,a)
(A,A,((a '&' b) => a)) . X is Relation-like Function-like set
[:(A,(a '&' b)),(A,a):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,a):] is non empty set
(A,A,(a '&' b)) is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
[:(A,(a '&' b)),(A,(a '&' b)):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,(a '&' b)):] is non empty set
(A,A) . (a '&' b) is Relation-like (A) . (a '&' b) -defined (A) . (a '&' b) -valued Function-like total quasi_total Element of bool [:((A) . (a '&' b)),((A) . (a '&' b)):]
[:((A) . (a '&' b)),((A) . (a '&' b)):] is Relation-like set
bool [:((A) . (a '&' b)),((A) . (a '&' b)):] is non empty set
(A,A,(a '&' b)) " is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
p1 is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
(A,A,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,A) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,A,a) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
((A,A,a) * p1) * ((A,A,(a '&' b)) ") is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
(A,A,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,A) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
[:(A,A,a),(A,A,b):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty Relation-like set
bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty set
[:(A,A,a),(A,A,b):] " is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
((A,A,a) * p1) * ([:(A,A,a),(A,A,b):] ") is Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,a):]
(A,A,a) " 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):]
(A,A,b) " is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:((A,A,a) "),((A,A,b) "):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
((A,A,a) * p1) * [:((A,A,a) "),((A,A,b) "):] is Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,a):]
p1 * [:((A,A,a) "),((A,A,b) "):] is Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,a):]
(A,A,a) * (p1 * [:((A,A,a) "),((A,A,b) "):]) is Relation-like [:(A,a),(A,b):] -defined (A,a) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,a):]
((A,A,a) ") * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
(A,A,a) * (((A,A,a) ") * p1) is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
(A,A,a) * ((A,A,a) ") 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):]
((A,A,a) * ((A,A,a) ")) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
id (A,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(A,a),(A,a):]
(id (A,a)) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,a) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,a):]
(a '&' b) => b is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),(a '&' b)),b) is Relation-like Function-like V51() set
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
[:[:(A,a),(A,b):],(A,b):] is non empty Relation-like set
bool [:[:(A,a),(A,b):],(A,b):] is non empty set
pr2 ((A,a),(A,b)) is non empty Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like total quasi_total Element of bool [:[:(A,a),(A,b):],(A,b):]
X is non empty Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like total quasi_total Element of bool [:[:(A,a),(A,b):],(A,b):]
A is Relation-like Function-like (A)
(A,A,((a '&' b) => b)) is non empty Relation-like (A,((a '&' b) => b)) -defined (A,((a '&' b) => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,((a '&' b) => b)),(A,((a '&' b) => b)):]
(A,((a '&' b) => b)) is non empty functional set
(A) . ((a '&' b) => b) is set
[:(A,((a '&' b) => b)),(A,((a '&' b) => b)):] is non empty Relation-like set
bool [:(A,((a '&' b) => b)),(A,((a '&' b) => b)):] is non empty set
(A,A) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,A) . ((a '&' b) => b) is Relation-like (A) . ((a '&' b) => b) -defined (A) . ((a '&' b) => b) -valued Function-like total quasi_total Element of bool [:((A) . ((a '&' b) => b)),((A) . ((a '&' b) => b)):]
[:((A) . ((a '&' b) => b)),((A) . ((a '&' b) => b)):] is Relation-like set
bool [:((A) . ((a '&' b) => b)),((A) . ((a '&' b) => b)):] is non empty set
dom (A,A,((a '&' b) => b)) is non empty set
(A,(a '&' b)) is non empty set
(A) . (a '&' b) is set
Funcs ((A,(a '&' b)),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,(a '&' b)),(A,b)
Funcs ([:(A,a),(A,b):],(A,b)) is non empty functional FUNCTION_DOMAIN of [:(A,a),(A,b):],(A,b)
(A,A,((a '&' b) => b)) . X is Relation-like Function-like set
[:(A,(a '&' b)),(A,b):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,b):] is non empty set
(A,A,(a '&' b)) is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
[:(A,(a '&' b)),(A,(a '&' b)):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,(a '&' b)):] is non empty set
(A,A) . (a '&' b) is Relation-like (A) . (a '&' b) -defined (A) . (a '&' b) -valued Function-like total quasi_total Element of bool [:((A) . (a '&' b)),((A) . (a '&' b)):]
[:((A) . (a '&' b)),((A) . (a '&' b)):] is Relation-like set
bool [:((A) . (a '&' b)),((A) . (a '&' b)):] is non empty set
(A,A,(a '&' b)) " is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
p1 is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
(A,A,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,A) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,A,b) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
((A,A,b) * p1) * ((A,A,(a '&' b)) ") is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
(A,A,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,A) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
[:(A,A,a),(A,A,b):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty Relation-like set
bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty set
[:(A,A,a),(A,A,b):] " is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
((A,A,b) * p1) * ([:(A,A,a),(A,A,b):] ") is Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,b):]
(A,A,a) " 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):]
(A,A,b) " is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:((A,A,a) "),((A,A,b) "):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
((A,A,b) * p1) * [:((A,A,a) "),((A,A,b) "):] is Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,b):]
p1 * [:((A,A,a) "),((A,A,b) "):] is Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,b):]
(A,A,b) * (p1 * [:((A,A,a) "),((A,A,b) "):]) is Relation-like [:(A,a),(A,b):] -defined (A,b) -valued Function-like Element of bool [:[:(A,a),(A,b):],(A,b):]
((A,A,b) ") * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
(A,A,b) * (((A,A,b) ") * p1) is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
(A,A,b) * ((A,A,b) ") is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
((A,A,b) * ((A,A,b) ")) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(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):]
(id (A,b)) * p1 is non empty Relation-like (A,(a '&' b)) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,(a '&' b)),(A,b):]
b => (a '&' b) is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),b),(a '&' b)) is Relation-like Function-like V51() set
a => (b => (a '&' b)) is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),a),(b => (a '&' b))) is Relation-like Function-like V51() set
A is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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
Funcs ((A,b),[:(A,a),(A,b):]) is non empty functional FUNCTION_DOMAIN of (A,b),[:(A,a),(A,b):]
[:(A,a),(Funcs ((A,b),[:(A,a),(A,b):])):] is non empty Relation-like set
bool [:(A,a),(Funcs ((A,b),[:(A,a),(A,b):])):] is non empty set
id (A,a) is non empty Relation-like (A,a) -defined (A,a) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Element of bool [:(A,a),(A,a):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
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,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
[:(id (A,a)),(id (A,b)):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty Relation-like set
bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:] is non empty set
curry [:(id (A,a)),(id (A,b)):] is non empty Relation-like (A,a) -defined Funcs ((A,b),[:(A,a),(A,b):]) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(Funcs ((A,b),[:(A,a),(A,b):])):]
X is non empty Relation-like (A,a) -defined Funcs ((A,b),[:(A,a),(A,b):]) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(Funcs ((A,b),[:(A,a),(A,b):])):]
A is Relation-like Function-like (A)
(A,A,(a => (b => (a '&' b)))) is non empty Relation-like (A,(a => (b => (a '&' b)))) -defined (A,(a => (b => (a '&' b)))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => (b => (a '&' b)))),(A,(a => (b => (a '&' b)))):]
(A,(a => (b => (a '&' b)))) is non empty functional set
(A) . (a => (b => (a '&' b))) is set
[:(A,(a => (b => (a '&' b)))),(A,(a => (b => (a '&' b)))):] is non empty Relation-like set
bool [:(A,(a => (b => (a '&' b)))),(A,(a => (b => (a '&' b)))):] is non empty set
(A,A) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,A) . (a => (b => (a '&' b))) is Relation-like (A) . (a => (b => (a '&' b))) -defined (A) . (a => (b => (a '&' b))) -valued Function-like total quasi_total Element of bool [:((A) . (a => (b => (a '&' b)))),((A) . (a => (b => (a '&' b)))):]
[:((A) . (a => (b => (a '&' b)))),((A) . (a => (b => (a '&' b)))):] is Relation-like set
bool [:((A) . (a => (b => (a '&' b)))),((A) . (a => (b => (a '&' b)))):] is non empty set
Funcs ((A,a),(Funcs ((A,b),[:(A,a),(A,b):]))) is non empty functional FUNCTION_DOMAIN of (A,a), Funcs ((A,b),[:(A,a),(A,b):])
(A,(a '&' b)) is non empty set
(A) . (a '&' b) is set
Funcs ((A,b),(A,(a '&' b))) is non empty functional FUNCTION_DOMAIN of (A,b),(A,(a '&' b))
Funcs ((A,a),(Funcs ((A,b),(A,(a '&' b))))) is non empty functional FUNCTION_DOMAIN of (A,a), Funcs ((A,b),(A,(a '&' b)))
(A,(b => (a '&' b))) is non empty functional set
(A) . (b => (a '&' b)) is set
Funcs ((A,a),(A,(b => (a '&' b)))) is non empty functional FUNCTION_DOMAIN of (A,a),(A,(b => (a '&' b)))
[:(A,a),(A,(b => (a '&' b))):] is non empty Relation-like set
bool [:(A,a),(A,(b => (a '&' b))):] is non empty set
dom (A,A,(a => (b => (a '&' b)))) is non empty set
(A,A,(a => (b => (a '&' b)))) . X is Relation-like Function-like set
p1 is Element of (A,a)
X . p1 is non empty Relation-like (A,b) -defined [:(A,a),(A,b):] -valued Function-like total quasi_total Element of Funcs ((A,b),[:(A,a),(A,b):])
p1 is non empty Relation-like (A,a) -defined (A,(b => (a '&' b))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => (a '&' b))):]
p1 . p1 is Relation-like Function-like Element of (A,(b => (a '&' b)))
[:(A,b),(A,(a '&' b)):] is non empty Relation-like set
bool [:(A,b),(A,(a '&' b)):] is non empty set
(A,A,a) 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):]
(A,A) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,A,a) " 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):]
((A,A,a) ") . p1 is Element of (A,a)
p1 . (((A,A,a) ") . p1) is Relation-like Function-like Element of (A,(b => (a '&' b)))
V is non empty Relation-like (A,b) -defined (A,(a '&' b)) -valued Function-like total quasi_total Element of bool [:(A,b),(A,(a '&' b)):]
p0 is Element of (A,b)
V . p0 is Element of (A,(a '&' b))
[:(id (A,a)),(id (A,b)):] . (p1,p0) is Element of [:(A,a),(A,b):]
[p1,p0] is non empty set
{p1,p0} is non empty set
{p1} is non empty trivial set
{{p1,p0},{p1}} is non empty set
[:(id (A,a)),(id (A,b)):] . [p1,p0] is set
(id (A,a)) . p1 is Element of (A,a)
(id (A,b)) . p0 is Element of (A,b)
[((id (A,a)) . p1),((id (A,b)) . p0)] is non empty set
{((id (A,a)) . p1),((id (A,b)) . p0)} is non empty set
{((id (A,a)) . p1)} is non empty trivial set
{{((id (A,a)) . p1),((id (A,b)) . p0)},{((id (A,a)) . p1)}} is non empty set
(A,A,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
(A,A) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,A,b) " is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
(A,A,b) * ((A,A,b) ") is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
((A,A,b) * ((A,A,b) ")) . p0 is Element of (A,b)
[((id (A,a)) . p1),(((A,A,b) * ((A,A,b) ")) . p0)] is non empty set
{((id (A,a)) . p1),(((A,A,b) * ((A,A,b) ")) . p0)} is non empty set
{{((id (A,a)) . p1),(((A,A,b) * ((A,A,b) ")) . p0)},{((id (A,a)) . p1)}} is non empty set
((A,A,b) ") . p0 is Element of (A,b)
(A,A,b) . (((A,A,b) ") . p0) is Element of (A,b)
[((id (A,a)) . p1),((A,A,b) . (((A,A,b) ") . p0))] is non empty set
{((id (A,a)) . p1),((A,A,b) . (((A,A,b) ") . p0))} is non empty set
{{((id (A,a)) . p1),((A,A,b) . (((A,A,b) ") . p0))},{((id (A,a)) . p1)}} is non empty set
(A,A,a) * ((A,A,a) ") 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):]
((A,A,a) * ((A,A,a) ")) . p1 is Element of (A,a)
[(((A,A,a) * ((A,A,a) ")) . p1),((A,A,b) . (((A,A,b) ") . p0))] is non empty set
{(((A,A,a) * ((A,A,a) ")) . p1),((A,A,b) . (((A,A,b) ") . p0))} is non empty set
{(((A,A,a) * ((A,A,a) ")) . p1)} is non empty trivial set
{{(((A,A,a) * ((A,A,a) ")) . p1),((A,A,b) . (((A,A,b) ") . p0))},{(((A,A,a) * ((A,A,a) ")) . p1)}} is non empty set
(A,A,a) . (((A,A,a) ") . p1) is Element of (A,a)
[((A,A,a) . (((A,A,a) ") . p1)),((A,A,b) . (((A,A,b) ") . p0))] is non empty set
{((A,A,a) . (((A,A,a) ") . p1)),((A,A,b) . (((A,A,b) ") . p0))} is non empty set
{((A,A,a) . (((A,A,a) ") . p1))} is non empty trivial set
{{((A,A,a) . (((A,A,a) ") . p1)),((A,A,b) . (((A,A,b) ") . p0))},{((A,A,a) . (((A,A,a) ") . p1))}} is non empty set
[:(A,A,a),(A,A,b):] is non empty Relation-like [:(A,a),(A,b):] -defined [:(A,a),(A,b):] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:[:(A,a),(A,b):],[:(A,a),(A,b):]:]
[:(A,A,a),(A,A,b):] . ((((A,A,a) ") . p1),(((A,A,b) ") . p0)) is Element of [:(A,a),(A,b):]
[(((A,A,a) ") . p1),(((A,A,b) ") . p0)] is non empty set
{(((A,A,a) ") . p1),(((A,A,b) ") . p0)} is non empty set
{(((A,A,a) ") . p1)} is non empty trivial set
{{(((A,A,a) ") . p1),(((A,A,b) ") . p0)},{(((A,A,a) ") . p1)}} is non empty set
[:(A,A,a),(A,A,b):] . [(((A,A,a) ") . p1),(((A,A,b) ") . p0)] is set
(A,A,(a '&' b)) is non empty Relation-like (A,(a '&' b)) -defined (A,(a '&' b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,(a '&' b)),(A,(a '&' b)):]
[:(A,(a '&' b)),(A,(a '&' b)):] is non empty Relation-like set
bool [:(A,(a '&' b)),(A,(a '&' b)):] is non empty set
(A,A) . (a '&' b) is Relation-like (A) . (a '&' b) -defined (A) . (a '&' b) -valued Function-like total quasi_total Element of bool [:((A) . (a '&' b)),((A) . (a '&' b)):]
[:((A) . (a '&' b)),((A) . (a '&' b)):] is Relation-like set
bool [:((A) . (a '&' b)),((A) . (a '&' b)):] is non empty set
(A,A,(a '&' b)) . [(((A,A,a) ") . p1),(((A,A,b) ") . p0)] is set
(id (A,b)) . (((A,A,b) ") . p0) is Element of (A,b)
[(((A,A,a) ") . p1),((id (A,b)) . (((A,A,b) ") . p0))] is non empty set
{(((A,A,a) ") . p1),((id (A,b)) . (((A,A,b) ") . p0))} is non empty set
{{(((A,A,a) ") . p1),((id (A,b)) . (((A,A,b) ") . p0))},{(((A,A,a) ") . p1)}} is non empty set
(A,A,(a '&' b)) . [(((A,A,a) ") . p1),((id (A,b)) . (((A,A,b) ") . p0))] is set
(id (A,a)) . (((A,A,a) ") . p1) is Element of (A,a)
[((id (A,a)) . (((A,A,a) ") . p1)),((id (A,b)) . (((A,A,b) ") . p0))] is non empty set
{((id (A,a)) . (((A,A,a) ") . p1)),((id (A,b)) . (((A,A,b) ") . p0))} is non empty set
{((id (A,a)) . (((A,A,a) ") . p1))} is non empty trivial set
{{((id (A,a)) . (((A,A,a) ") . p1)),((id (A,b)) . (((A,A,b) ") . p0))},{((id (A,a)) . (((A,A,a) ") . p1))}} is non empty set
(A,A,(a '&' b)) . [((id (A,a)) . (((A,A,a) ") . p1)),((id (A,b)) . (((A,A,b) ") . p0))] is set
[:(id (A,a)),(id (A,b)):] . ((((A,A,a) ") . p1),(((A,A,b) ") . p0)) is Element of [:(A,a),(A,b):]
[:(id (A,a)),(id (A,b)):] . [(((A,A,a) ") . p1),(((A,A,b) ") . p0)] is set
(A,A,(a '&' b)) . ([:(id (A,a)),(id (A,b)):] . ((((A,A,a) ") . p1),(((A,A,b) ") . p0))) is set
f is non empty Relation-like (A,b) -defined (A,(a '&' b)) -valued Function-like total quasi_total Element of bool [:(A,b),(A,(a '&' b)):]
f . (((A,A,b) ") . p0) is Element of (A,(a '&' b))
(A,A,(a '&' b)) . (f . (((A,A,b) ") . p0)) is Element of (A,(a '&' b))
(A,A,(a '&' b)) * f is non empty Relation-like (A,b) -defined (A,(a '&' b)) -valued Function-like total quasi_total Element of bool [:(A,b),(A,(a '&' b)):]
((A,A,(a '&' b)) * f) . (((A,A,b) ") . p0) is Element of (A,(a '&' b))
((A,A,(a '&' b)) * f) * ((A,A,b) ") is non empty Relation-like (A,b) -defined (A,(a '&' b)) -valued Function-like total quasi_total Element of bool [:(A,b),(A,(a '&' b)):]
(((A,A,(a '&' b)) * f) * ((A,A,b) ")) . p0 is Element of (A,(a '&' b))
(A,A,(b => (a '&' b))) is non empty Relation-like (A,(b => (a '&' b))) -defined (A,(b => (a '&' b))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(b => (a '&' b))),(A,(b => (a '&' b))):]
[:(A,(b => (a '&' b))),(A,(b => (a '&' b))):] is non empty Relation-like set
bool [:(A,(b => (a '&' b))),(A,(b => (a '&' b))):] is non empty set
(A,A) . (b => (a '&' b)) is Relation-like (A) . (b => (a '&' b)) -defined (A) . (b => (a '&' b)) -valued Function-like total quasi_total Element of bool [:((A) . (b => (a '&' b))),((A) . (b => (a '&' b))):]
[:((A) . (b => (a '&' b))),((A) . (b => (a '&' b))):] is Relation-like set
bool [:((A) . (b => (a '&' b))),((A) . (b => (a '&' b))):] is non empty set
(A,A,(b => (a '&' b))) . (p1 . (((A,A,a) ") . p1)) is Relation-like Function-like Element of (A,(b => (a '&' b)))
(A,A,(b => (a '&' b))) * p1 is non empty Relation-like (A,a) -defined (A,(b => (a '&' b))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => (a '&' b))):]
((A,A,(b => (a '&' b))) * p1) . (((A,A,a) ") . p1) is Relation-like Function-like Element of (A,(b => (a '&' b)))
((A,A,(b => (a '&' b))) * p1) * ((A,A,a) ") is non empty Relation-like (A,a) -defined (A,(b => (a '&' b))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(A,a),(A,(b => (a '&' b))):]
(((A,A,(b => (a '&' b))) * p1) * ((A,A,a) ")) . p1 is Relation-like Function-like Element of (A,(b => (a '&' b)))
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
b => A 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) is Relation-like Function-like V51() set
a => (b => A) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),a) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),a),(b => A)) is Relation-like Function-like V51() set
a => b is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),a),b) is Relation-like Function-like V51() set
a => A is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),a),A) is Relation-like Function-like V51() set
(a => b) => (a => A) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(a => b)) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(a => b)),(a => A)) is Relation-like Function-like V51() set
(a => (b => A)) => ((a => b) => (a => A)) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(a => (b => A))) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(a => (b => A))),((a => b) => (a => A))) is Relation-like Function-like V51() set
X is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
(X,(a => b)) is non empty functional set
(X) is non empty Relation-like HP-WFF -defined Function-like total set
(X) . (a => b) is set
(X,a) is non empty set
(X) . a is set
(X,b) is non empty set
(X) . b is set
Funcs ((X,a),(X,b)) is non empty functional FUNCTION_DOMAIN of (X,a),(X,b)
(X,(a => A)) is non empty functional set
(X) . (a => A) is set
(X,A) is non empty set
(X) . A is set
Funcs ((X,a),(X,A)) is non empty functional FUNCTION_DOMAIN of (X,a),(X,A)
(X,(a => (b => A))) is non empty functional set
(X) . (a => (b => A)) is set
(X,((a => b) => (a => A))) is non empty functional set
(X) . ((a => b) => (a => A)) is set
A is Relation-like Function-like Function-yielding V55() Element of (X,(a => (b => A)))
Frege A is Relation-like Function-like set
(X,(b => A)) is non empty functional set
(X) . (b => A) is set
Funcs ((X,a),(X,(b => A))) is non empty functional FUNCTION_DOMAIN of (X,a),(X,(b => A))
Funcs ((X,b),(X,A)) is non empty functional FUNCTION_DOMAIN of (X,b),(X,A)
Funcs ((X,a),(Funcs ((X,b),(X,A)))) is non empty functional FUNCTION_DOMAIN of (X,a), Funcs ((X,b),(X,A))
Frege A is Relation-like product (doms A) -defined Function-like total Function-yielding V55() set
doms A is Relation-like Function-like set
product (doms A) is set
[:(X,(a => b)),(X,(a => A)):] is non empty Relation-like set
bool [:(X,(a => b)),(X,(a => A)):] is non empty set
Funcs ((X,(a => b)),(X,(a => A))) is non empty functional FUNCTION_DOMAIN of (X,(a => b)),(X,(a => A))
[:(X,(a => (b => A))),(X,((a => b) => (a => A))):] is non empty Relation-like set
bool [:(X,(a => (b => A))),(X,((a => b) => (a => A))):] is non empty set
A is non empty Relation-like (X,(a => (b => A))) -defined (X,((a => b) => (a => A))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => (b => A))),(X,((a => b) => (a => A))):]
p1 is Relation-like Function-like (X)
(X,p1,((a => (b => A)) => ((a => b) => (a => A)))) is non empty Relation-like (X,((a => (b => A)) => ((a => b) => (a => A)))) -defined (X,((a => (b => A)) => ((a => b) => (a => A)))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,((a => (b => A)) => ((a => b) => (a => A)))),(X,((a => (b => A)) => ((a => b) => (a => A)))):]
(X,((a => (b => A)) => ((a => b) => (a => A)))) is non empty functional set
(X) . ((a => (b => A)) => ((a => b) => (a => A))) is set
[:(X,((a => (b => A)) => ((a => b) => (a => A)))),(X,((a => (b => A)) => ((a => b) => (a => A)))):] is non empty Relation-like set
bool [:(X,((a => (b => A)) => ((a => b) => (a => A)))),(X,((a => (b => A)) => ((a => b) => (a => A)))):] is non empty set
(X,p1) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (X),(X)
(X,p1) . ((a => (b => A)) => ((a => b) => (a => A))) is Relation-like (X) . ((a => (b => A)) => ((a => b) => (a => A))) -defined (X) . ((a => (b => A)) => ((a => b) => (a => A))) -valued Function-like total quasi_total Element of bool [:((X) . ((a => (b => A)) => ((a => b) => (a => A)))),((X) . ((a => (b => A)) => ((a => b) => (a => A)))):]
[:((X) . ((a => (b => A)) => ((a => b) => (a => A)))),((X) . ((a => (b => A)) => ((a => b) => (a => A)))):] is Relation-like set
bool [:((X) . ((a => (b => A)) => ((a => b) => (a => A)))),((X) . ((a => (b => A)) => ((a => b) => (a => A)))):] is non empty set
Funcs ((X,(a => (b => A))),(X,((a => b) => (a => A)))) is non empty functional FUNCTION_DOMAIN of (X,(a => (b => A))),(X,((a => b) => (a => A)))
dom (X,p1,((a => (b => A)) => ((a => b) => (a => A)))) is non empty set
(X,p1,((a => (b => A)) => ((a => b) => (a => A)))) . A is Relation-like Function-like set
(X,(b => A)) is non empty functional set
(X) . (b => A) is set
[:(X,(b => A)),(X,(b => A)):] is non empty Relation-like set
bool [:(X,(b => A)),(X,(b => A)):] is non empty set
(X,p1,(b => A)) is non empty Relation-like (X,(b => A)) -defined (X,(b => A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(b => A)),(X,(b => A)):]
(X,p1) . (b => A) is Relation-like (X) . (b => A) -defined (X) . (b => A) -valued Function-like total quasi_total Element of bool [:((X) . (b => A)),((X) . (b => A)):]
[:((X) . (b => A)),((X) . (b => A)):] is Relation-like set
bool [:((X) . (b => A)),((X) . (b => A)):] is non empty set
(X,p1,(b => A)) " is non empty Relation-like (X,(b => A)) -defined (X,(b => A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(b => A)),(X,(b => A)):]
(X,p1,(a => (b => A))) is non empty Relation-like (X,(a => (b => A))) -defined (X,(a => (b => A))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => (b => A))),(X,(a => (b => A))):]
[:(X,(a => (b => A))),(X,(a => (b => A))):] is non empty Relation-like set
bool [:(X,(a => (b => A))),(X,(a => (b => A))):] is non empty set
(X,p1) . (a => (b => A)) is Relation-like (X) . (a => (b => A)) -defined (X) . (a => (b => A)) -valued Function-like total quasi_total Element of bool [:((X) . (a => (b => A))),((X) . (a => (b => A))):]
[:((X) . (a => (b => A))),((X) . (a => (b => A))):] is Relation-like set
bool [:((X) . (a => (b => A))),((X) . (a => (b => A))):] is non empty set
(X,p1,(a => (b => A))) " is non empty Relation-like (X,(a => (b => A))) -defined (X,(a => (b => A))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => (b => A))),(X,(a => (b => A))):]
V is Relation-like Function-like Function-yielding V55() Element of (X,(a => (b => A)))
((X,p1,(a => (b => A))) ") . V is Relation-like Function-like Function-yielding V55() Element of (X,(a => (b => A)))
Funcs ((X,b),(X,A)) is non empty functional FUNCTION_DOMAIN of (X,b),(X,A)
Funcs ((X,a),(X,(b => A))) is non empty functional FUNCTION_DOMAIN of (X,a),(X,(b => A))
[:(X,a),(X,(b => A)):] is non empty Relation-like set
bool [:(X,a),(X,(b => A)):] is non empty set
(X,p1,a) is non empty Relation-like (X,a) -defined (X,a) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(X,a),(X,a):]
[:(X,a),(X,a):] is non empty Relation-like set
bool [:(X,a),(X,a):] is non empty set
(X,p1) . a is Relation-like (X) . a -defined (X) . a -valued Function-like total quasi_total Element of bool [:((X) . a),((X) . a):]
[:((X) . a),((X) . a):] is Relation-like set
bool [:((X) . a),((X) . a):] is non empty set
p0 is non empty Relation-like (X,a) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
((X,p1,(b => A)) ") * p0 is non empty Relation-like (X,a) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
(((X,p1,(b => A)) ") * p0) * (X,p1,a) is non empty Relation-like (X,a) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
[:(X,(a => b)),(X,(a => A)):] is non empty Relation-like set
bool [:(X,(a => b)),(X,(a => A)):] is non empty set
Frege (((X,p1,(a => (b => A))) ") . V) is Relation-like product (doms (((X,p1,(a => (b => A))) ") . V)) -defined Function-like total Function-yielding V55() set
doms (((X,p1,(a => (b => A))) ") . V) is Relation-like Function-like set
product (doms (((X,p1,(a => (b => A))) ") . V)) is set
(X,p1,(a => b)) is non empty Relation-like (X,(a => b)) -defined (X,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => b)),(X,(a => b)):]
[:(X,(a => b)),(X,(a => b)):] is non empty Relation-like set
bool [:(X,(a => b)),(X,(a => b)):] is non empty set
(X,p1) . (a => b) is Relation-like (X) . (a => b) -defined (X) . (a => b) -valued Function-like total quasi_total Element of bool [:((X) . (a => b)),((X) . (a => b)):]
[:((X) . (a => b)),((X) . (a => b)):] is Relation-like set
bool [:((X) . (a => b)),((X) . (a => b)):] is non empty set
(X,p1,(a => b)) " is non empty Relation-like (X,(a => b)) -defined (X,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => b)),(X,(a => b)):]
f is non empty Relation-like (X,(a => b)) -defined (X,(a => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => b)),(X,(a => A)):]
(X,p1,(a => A)) is non empty Relation-like (X,(a => A)) -defined (X,(a => A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => A)),(X,(a => A)):]
[:(X,(a => A)),(X,(a => A)):] is non empty Relation-like set
bool [:(X,(a => A)),(X,(a => A)):] is non empty set
(X,p1) . (a => A) is Relation-like (X) . (a => A) -defined (X) . (a => A) -valued Function-like total quasi_total Element of bool [:((X) . (a => A)),((X) . (a => A)):]
[:((X) . (a => A)),((X) . (a => A)):] is Relation-like set
bool [:((X) . (a => A)),((X) . (a => A)):] is non empty set
(X,p1,(a => A)) * f is non empty Relation-like (X,(a => b)) -defined (X,(a => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => b)),(X,(a => A)):]
((X,p1,(a => A)) * f) * ((X,p1,(a => b)) ") is non empty Relation-like (X,(a => b)) -defined (X,(a => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => b)),(X,(a => A)):]
doms p0 is non empty Relation-like (X,a) -defined Function-like total set
product (doms p0) is set
(X,a) --> (X,b) is non empty Relation-like non-empty non empty-yielding (X,a) -defined {(X,b)} -valued Function-like constant total quasi_total Element of bool [:(X,a),{(X,b)}:]
{(X,b)} is non empty trivial set
[:(X,a),{(X,b)}:] is non empty Relation-like set
bool [:(X,a),{(X,b)}:] is non empty set
product ((X,a) --> (X,b)) is set
doms V is Relation-like Function-like set
product (doms V) is set
P is Relation-like product (doms V) -defined Function-like total Function-yielding V55() set
[:(X,a),(Funcs ((X,b),(X,A))):] is non empty Relation-like set
bool [:(X,a),(Funcs ((X,b),(X,A))):] is non empty set
x is Relation-like Function-like set
P . x is Relation-like Function-like set
V .. x is Relation-like Function-like set
[:(X,a),(X,b):] is non empty Relation-like set
bool [:(X,a),(X,b):] is non empty set
P is non empty Relation-like (X,a) -defined Funcs ((X,b),(X,A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(Funcs ((X,b),(X,A))):]
dom P is non empty set
x is non empty Relation-like (X,a) -defined (X,b) -valued Function-like total quasi_total Element of bool [:(X,a),(X,b):]
P .. x is Relation-like Function-like set
dom (P .. x) is set
rng (P .. x) is set
[:(X,a),(X,A):] is non empty Relation-like set
bool [:(X,a),(X,A):] is non empty set
(X,p1,b) is non empty Relation-like (X,b) -defined (X,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(X,b),(X,b):]
[:(X,b),(X,b):] is non empty Relation-like set
bool [:(X,b),(X,b):] is non empty set
(X,p1) . b is Relation-like (X) . b -defined (X) . b -valued Function-like total quasi_total Element of bool [:((X) . b),((X) . b):]
[:((X) . b),((X) . b):] is Relation-like set
bool [:((X) . b),((X) . b):] is non empty set
(X,p1,b) " is non empty Relation-like (X,b) -defined (X,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(X,b),(X,b):]
((X,p1,b) ") * x is non empty Relation-like (X,a) -defined (X,b) -valued Function-like total quasi_total Element of bool [:(X,a),(X,b):]
(((X,p1,b) ") * x) * (X,p1,a) is non empty Relation-like (X,a) -defined (X,b) -valued Function-like total quasi_total Element of bool [:(X,a),(X,b):]
x * ((X,p1,b) ") is Relation-like (X,b) -valued Function-like set
(X,p1,a) * (x * ((X,p1,b) ")) is Relation-like (X,a) -defined (X,b) -valued Function-like set
((X,p1,(a => b)) ") . x is Relation-like Function-like set
p1 is non empty Relation-like (X,(b => A)) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(b => A)),(X,(b => A)):]
(X,p1,A) is non empty Relation-like (X,A) -defined (X,A) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(X,A),(X,A):]
[:(X,A),(X,A):] is non empty Relation-like set
bool [:(X,A),(X,A):] is non empty set
(X,p1) . A is Relation-like (X) . A -defined (X) . A -valued Function-like total quasi_total Element of bool [:((X) . A),((X) . A):]
[:((X) . A),((X) . A):] is Relation-like set
bool [:((X) . A),((X) . A):] is non empty set
((X,b),(X,A),(X,p1,b),(X,p1,A)) is non empty Relation-like Funcs ((X,b),(X,A)) -defined Funcs ((X,b),(X,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((X,b),(X,A))),(Funcs ((X,b),(X,A))):]
[:(Funcs ((X,b),(X,A))),(Funcs ((X,b),(X,A))):] is non empty Relation-like set
bool [:(Funcs ((X,b),(X,A))),(Funcs ((X,b),(X,A))):] is non empty set
((X,b),(X,A),(X,p1,b),(X,p1,A)) " is non empty Relation-like Funcs ((X,b),(X,A)) -defined Funcs ((X,b),(X,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((X,b),(X,A))),(Funcs ((X,b),(X,A))):]
(X,p1,A) " is non empty Relation-like (X,A) -defined (X,A) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(X,A),(X,A):]
((X,b),(X,A),((X,p1,b) "),((X,p1,A) ")) is non empty Relation-like Funcs ((X,b),(X,A)) -defined Funcs ((X,b),(X,A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(Funcs ((X,b),(X,A))),(Funcs ((X,b),(X,A))):]
((X,p1,(a => b)) ") . x is Relation-like Function-like set
f . (((X,p1,(a => b)) ") . x) is Relation-like Function-like set
f . ((((X,p1,b) ") * x) * (X,p1,a)) is Relation-like Function-like set
(((X,p1,(a => (b => A))) ") . V) .. ((X,p1,a) * (x * ((X,p1,b) "))) is Relation-like Function-like set
p1 * p0 is non empty Relation-like (X,a) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
(p1 * p0) * (X,p1,a) is non empty Relation-like (X,a) -defined (X,(b => A)) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
((p1 * p0) * (X,p1,a)) .. ((X,p1,a) * (x * ((X,p1,b) "))) is Relation-like Function-like set
p1 * P is Relation-like (X,a) -defined (X,(b => A)) -valued Function-like Function-yielding V55() Element of bool [:(X,a),(X,(b => A)):]
(p1 * P) .. (x * ((X,p1,b) ")) is Relation-like Function-like set
(X,p1,a) * ((p1 * P) .. (x * ((X,p1,b) "))) is Relation-like (X,a) -defined Function-like set
(P .. x) * ((X,p1,A) ") is Relation-like (X,A) -valued Function-like set
(X,p1,a) * ((P .. x) * ((X,p1,A) ")) is Relation-like (X,a) -defined (X,A) -valued Function-like set
(X,p1,(a => A)) " is non empty Relation-like (X,(a => A)) -defined (X,(a => A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => A)),(X,(a => A)):]
g is non empty Relation-like (X,a) -defined (X,A) -valued Function-like total quasi_total Element of bool [:(X,a),(X,A):]
((X,p1,(a => A)) ") . g is Relation-like Function-like set
((X,p1,(a => A)) * f) . (((X,p1,(a => b)) ") . x) is Relation-like Function-like set
(X,p1,(a => A)) . (((X,p1,(a => A)) ") . g) is Relation-like Function-like set
(X,p1,(a => A)) * ((X,p1,(a => A)) ") is non empty Relation-like (X,(a => A)) -defined (X,(a => A)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,(a => A)),(X,(a => A)):]
((X,p1,(a => A)) * ((X,p1,(a => A)) ")) . g is Relation-like Function-like set
id (X,(a => A)) is non empty Relation-like (X,(a => A)) -defined (X,(a => A)) -valued Function-like one-to-one total quasi_total onto bijective V35() V37() V38() V42() Function-yielding V55() Element of bool [:(X,(a => A)),(X,(a => A)):]
(id (X,(a => A))) . g is Relation-like Function-like set
A . V is Relation-like Function-like Function-yielding V55() Element of (X,((a => b) => (a => A)))
Frege V is Relation-like product (doms V) -defined Function-like total Function-yielding V55() set
(X,p1,((a => b) => (a => A))) is non empty Relation-like (X,((a => b) => (a => A))) -defined (X,((a => b) => (a => A))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(X,((a => b) => (a => A))),(X,((a => b) => (a => A))):]
[:(X,((a => b) => (a => A))),(X,((a => b) => (a => A))):] is non empty Relation-like set
bool [:(X,((a => b) => (a => A))),(X,((a => b) => (a => A))):] is non empty set
(X,p1) . ((a => b) => (a => A)) is Relation-like (X) . ((a => b) => (a => A)) -defined (X) . ((a => b) => (a => A)) -valued Function-like total quasi_total Element of bool [:((X) . ((a => b) => (a => A))),((X) . ((a => b) => (a => A))):]
[:((X) . ((a => b) => (a => A))),((X) . ((a => b) => (a => A))):] is Relation-like set
bool [:((X) . ((a => b) => (a => A))),((X) . ((a => b) => (a => A))):] is non empty set
(X,p1,((a => b) => (a => A))) . f is Relation-like Function-like set
A . (((X,p1,(a => (b => A))) ") . V) is Relation-like Function-like Function-yielding V55() Element of (X,((a => b) => (a => A)))
(X,p1,((a => b) => (a => A))) . (A . (((X,p1,(a => (b => A))) ") . V)) is Relation-like Function-like Function-yielding V55() Element of (X,((a => b) => (a => A)))
(X,p1,((a => b) => (a => A))) * A is non empty Relation-like (X,(a => (b => A))) -defined (X,((a => b) => (a => A))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => (b => A))),(X,((a => b) => (a => A))):]
((X,p1,((a => b) => (a => A))) * A) . (((X,p1,(a => (b => A))) ") . V) is Relation-like Function-like Function-yielding V55() Element of (X,((a => b) => (a => A)))
((X,p1,((a => b) => (a => A))) * A) * ((X,p1,(a => (b => A))) ") is non empty Relation-like (X,(a => (b => A))) -defined (X,((a => b) => (a => A))) -valued Function-like total quasi_total Function-yielding V55() Element of bool [:(X,(a => (b => A))),(X,((a => b) => (a => A))):]
(((X,p1,((a => b) => (a => A))) * A) * ((X,p1,(a => (b => A))) ")) . V is Relation-like Function-like Function-yielding V55() Element of (X,((a => b) => (a => A)))
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
X is set
the Relation-like Function-like (A) is Relation-like Function-like (A)
(A, the Relation-like Function-like (A),(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) is non empty Relation-like HP-WFF -defined Function-like total set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A, the Relation-like Function-like (A)) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A, the Relation-like Function-like (A)) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
dom (A, the Relation-like Function-like (A),(a => b)) is non empty 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)
p1 is set
[:(A,a),(A,b):] is non empty Relation-like set
bool [:(A,a),(A,b):] is non empty set
p1 is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
p1 . X is set
V is Relation-like Function-like (A)
(A,V,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,V) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,V) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,V,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,V) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
(A,V,a) 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):]
[:(A,a),(A,a):] is non empty Relation-like set
bool [:(A,a),(A,a):] is non empty set
(A,V) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
a is Relation-like Function-like V51() Element of HP-WFF
{ b₁ where b₁ is Relation-like Function-like V51() Element of HP-WFF : b₁ is () } is set
A is set
X is Relation-like Function-like V51() Element of HP-WFF
A is functional Element of bool HP-WFF
X is Relation-like Function-like V51() Element of HP-WFF
A is Relation-like Function-like V51() Element of HP-WFF
A => X is Relation-like Function-like V51() Element of HP-WFF
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
X => (A => X) is Relation-like Function-like V51() () Element of HP-WFF
K155(K160(NAT,1),X) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),X),(A => X)) is Relation-like Function-like V51() set
X => A is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),X),A) is Relation-like Function-like V51() set
X '&' A is Relation-like Function-like V51() Element of HP-WFF
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
(X '&' A) => X is Relation-like Function-like V51() () Element of HP-WFF
K155(K160(NAT,1),(X '&' A)) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(X '&' A)),X) is Relation-like Function-like V51() set
(X '&' A) => A is Relation-like Function-like V51() () Element of HP-WFF
K155(K155(K160(NAT,1),(X '&' A)),A) is Relation-like Function-like V51() set
A => (X '&' A) is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),A),(X '&' A)) is Relation-like Function-like V51() set
X => (A => (X '&' A)) is Relation-like Function-like V51() () Element of HP-WFF
K155(K155(K160(NAT,1),X),(A => (X '&' A))) is Relation-like Function-like V51() set
p1 is Relation-like Function-like V51() Element of HP-WFF
A => p1 is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),A),p1) is Relation-like Function-like V51() set
X => (A => p1) is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),X),(A => p1)) is Relation-like Function-like V51() set
X => p1 is Relation-like Function-like V51() Element of HP-WFF
K155(K155(K160(NAT,1),X),p1) is Relation-like Function-like V51() set
(X => A) => (X => p1) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(X => A)) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(X => A)),(X => p1)) is Relation-like Function-like V51() set
(X => (A => p1)) => ((X => A) => (X => p1)) is Relation-like Function-like V51() () Element of HP-WFF
K155(K160(NAT,1),(X => (A => p1))) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(X => (A => p1))),((X => A) => (X => p1))) is Relation-like Function-like V51() set
p1 is Relation-like Function-like V51() Element of HP-WFF
V is Relation-like Function-like V51() Element of HP-WFF
X is Relation-like Function-like V51() Element of HP-WFF
a is Relation-like Function-like V51() Element of HP-WFF
b is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
A is set
X is Relation-like Function-like (b)
(b,X,a) is non empty Relation-like (b,a) -defined (b,a) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(b,a),(b,a):]
(b,a) is non empty set
(b) is non empty Relation-like HP-WFF -defined Function-like total set
(b) . a is set
[:(b,a),(b,a):] is non empty Relation-like set
bool [:(b,a),(b,a):] is non empty set
(b,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (b),(b)
(b,X) . a is Relation-like (b) . a -defined (b) . a -valued Function-like total quasi_total Element of bool [:((b) . a),((b) . a):]
[:((b) . a),((b) . a):] is Relation-like set
bool [:((b) . a),((b) . a):] is non empty set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
X is Relation-like Function-like (A)
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
(A,b) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total set
(A) . b is set
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
(A,X,a) 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):]
(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) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
A is set
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
p1 is set
dom (A,X,(a => b)) is non empty set
Funcs ((A,a),(A,b)) is non empty functional FUNCTION_DOMAIN of (A,a),(A,b)
[:(A,a),(A,b):] is non empty Relation-like set
bool [:(A,a),(A,b):] is non empty set
p1 is non empty Relation-like (A,a) -defined (A,b) -valued Function-like total quasi_total Element of bool [:(A,a),(A,b):]
p1 . A is set
a is Relation-like Function-like V51() Element of HP-WFF
b is Relation-like Function-like V51() Element of HP-WFF
a => b is Relation-like Function-like V51() Element of HP-WFF
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 is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
X is Relation-like Function-like (A)
(A,X,a) 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):]
(A,a) is non empty set
(A) is non empty Relation-like HP-WFF -defined Function-like total 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 Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (A),(A)
(A,X) . a is Relation-like (A) . a -defined (A) . a -valued Function-like total quasi_total Element of bool [:((A) . a),((A) . a):]
[:((A) . a),((A) . a):] is Relation-like set
bool [:((A) . a),((A) . a):] is non empty set
(A,X,b) is non empty Relation-like (A,b) -defined (A,b) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(A,b),(A,b):]
(A,b) is non empty set
(A) . b is set
[:(A,b),(A,b):] is non empty Relation-like set
bool [:(A,b),(A,b):] is non empty set
(A,X) . b is Relation-like (A) . b -defined (A) . b -valued Function-like total quasi_total Element of bool [:((A) . b),((A) . b):]
[:((A) . b),((A) . b):] is Relation-like set
bool [:((A) . b),((A) . b):] is non empty set
A is set
(A,X,(a => b)) is non empty Relation-like (A,(a => b)) -defined (A,(a => b)) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(A,(a => b)),(A,(a => b)):]
(A,(a => b)) is non empty functional set
(A) . (a => b) is set
[:(A,(a => b)),(A,(a => b)):] is non empty Relation-like set
bool [:(A,(a => b)),(A,(a => b)):] is non empty set
(A,X) . (a => b) is Relation-like (A) . (a => b) -defined (A) . (a => b) -valued Function-like total quasi_total Element of bool [:((A) . (a => b)),((A) . (a => b)):]
[:((A) . (a => b)),((A) . (a => b)):] is Relation-like set
bool [:((A) . (a => b)),((A) . (a => b)):] is non empty set
p1 is set
dom (A,X,(a => b)) is non empty set
p1 is Relation-like Function-like set
p1 . A is set
a is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
b is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
prop a is Relation-like Function-like V51() Element of HP-WFF
prop b is Relation-like Function-like V51() Element of HP-WFF
(prop a) => (prop b) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(prop a)) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(prop a)),(prop b)) is Relation-like Function-like V51() set
((prop a) => (prop b)) => (prop a) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),((prop a) => (prop b))) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),((prop a) => (prop b))),(prop a)) is Relation-like Function-like V51() set
(((prop a) => (prop b)) => (prop a)) => (prop a) is Relation-like Function-like V51() Element of HP-WFF
K155(K160(NAT,1),(((prop a) => (prop b)) => (prop a))) is Relation-like Function-like V51() set
K155(K155(K160(NAT,1),(((prop a) => (prop b)) => (prop a))),(prop a)) is Relation-like Function-like V51() set
{ ((0,1) --> (b₁,b₂)) where b₁, b₂ is ext-real complex V15() integer Element of INT : ( not b₂ <= b₁ or ( b₁ is even & b₁ = b₂ ) ) } is set
(0,1) --> (INT,INT) is Relation-like NAT -defined Function-like set
product ((0,1) --> (INT,INT)) is set
A is set
p1 is ext-real complex V15() integer Element of INT
p1 is ext-real complex V15() integer Element of INT
(0,1) --> (p1,p1) is non empty Relation-like NAT -defined {0,1} -defined INT -valued Function-like total quasi_total Element of bool [:{0,1},INT:]
[:{0,1},INT:] is non empty Relation-like set
bool [:{0,1},INT:] is non empty set
bool (product ((0,1) --> (INT,INT))) is non empty set
a .--> 2 is trivial Relation-like NAT -defined {a} -defined NAT -valued Function-like one-to-one constant set
{a} is non empty trivial set
{a} --> 2 is non empty Relation-like non-empty non empty-yielding {a} -defined NAT -valued {2} -valued Function-like constant total quasi_total Element of bool [:{a},{2}:]
{2} is non empty trivial set
[:{a},{2}:] is non empty Relation-like set
bool [:{a},{2}:] is non empty set
dom (a .--> 2) is trivial set
NAT --> INT is non empty Relation-like non-empty non empty-yielding NAT -defined {INT} -valued Function-like constant total quasi_total Element of bool [:NAT,{INT}:]
{INT} is non empty trivial set
[:NAT,{INT}:] is non empty Relation-like set
bool [:NAT,{INT}:] is non empty set
(NAT --> INT) +* (a .--> 2) is non empty Relation-like NAT -defined Function-like total set
(a .--> 2) . a is set
V is non empty Relation-like non-empty non empty-yielding NAT -defined Function-like total set
V . a is non empty set
(V,(prop a)) is non empty set
(V) is non empty Relation-like HP-WFF -defined Function-like total set
(V) . (prop a) is set
p0 is ext-real complex V15() integer Element of INT
f is ext-real complex V15() integer set
f + 1 is ext-real complex V15() integer set
p0 is ext-real complex V15() integer Element of INT
[:INT,INT:] is non empty Relation-like set
bool [:INT,INT:] is non empty set
p0 is non empty Relation-like INT -defined INT -valued Function-like total quasi_total Element of bool [:INT,INT:]
dom p0 is non empty set
f is set
p0 is ext-real complex V15() integer set
p0 - 1 is ext-real complex V15() integer set
P is set
P is set
p0 . P is set
x is ext-real complex V15() integer set
x + 1 is ext-real complex V15() integer set
p0 is set
p0 . p0 is set
P is ext-real complex V15() integer set
P + 1 is ext-real complex V15() integer set
rng p0 is non empty set
f is set
p0 is set
p0 . f is set
p0 . p0 is set
P is ext-real complex V15() integer Element of INT
p0 . P is ext-real complex V15() integer Element of INT
P is ext-real complex V15() integer Element of INT
p0 . P is ext-real complex V15() integer Element of INT
x is ext-real complex V15() integer set
x + 1 is ext-real complex V15() integer set
x is ext-real complex V15() integer set
x + 1 is ext-real complex V15() integer set
(V,(prop b)) is non empty set
(V) . (prop b) is set
V . b is non empty set
(NAT --> INT) . b is non empty Element of {INT}
2 --> INT is non empty Relation-like non-empty non empty-yielding 2 -defined {INT} -valued Function-like constant total quasi_total Element of bool [:2,{INT}:]
[:2,{INT}:] is non empty Relation-like set
bool [:2,{INT}:] is non empty set
product (2 --> INT) is set
Funcs (2,INT) is non empty functional FUNCTION_DOMAIN of 2, INT
(V,((prop a) => (prop b))) is non empty functional set
(V) . ((prop a) => (prop b)) is set
[:(V,((prop a) => (prop b))),(V,(prop a)):] is non empty Relation-like set
bool [:(V,((prop a) => (prop b))),(V,(prop a)):] is non empty set
A is Element of bool (product ((0,1) --> (INT,INT)))
chi (A,(product ((0,1) --> (INT,INT)))) is Relation-like product ((0,1) --> (INT,INT)) -defined {{},1} -valued Function-like total quasi_total Element of bool [:(product ((0,1) --> (INT,INT))),{{},1}:]
[:(product ((0,1) --> (INT,INT))),{{},1}:] is Relation-like set
bool [:(product ((0,1) --> (INT,INT))),{{},1}:] is non empty set
p1 is non empty Relation-like 2 -defined 2 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:2,2:]
a .--> p1 is trivial Relation-like NAT -defined {a} -defined bool [:2,2:] -valued Function-like one-to-one constant Function-yielding V55() set
{a} --> p1 is non empty Relation-like non-empty non empty-yielding {a} -defined bool [:2,2:] -valued {p1} -valued Function-like constant total quasi_total Function-yielding V55() Element of bool [:{a},{p1}:]
{p1} is non empty trivial functional set
[:{a},{p1}:] is non empty Relation-like set
bool [:{a},{p1}:] is non empty set
dom (a .--> p1) is trivial set
p0 is non empty Relation-like INT -defined INT -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:INT,INT:]
NAT --> p0 is non empty Relation-like non-empty non empty-yielding NAT -defined bool [:INT,INT:] -valued Function-like constant total quasi_total Function-yielding V55() Element of bool [:NAT,(bool [:INT,INT:]):]
[:NAT,(bool [:INT,INT:]):] is non empty Relation-like set
bool [:NAT,(bool [:INT,INT:]):] is non empty set
{p0} is non empty trivial functional set
[:NAT,{p0}:] is non empty Relation-like set
(NAT --> p0) +* (a .--> p1) is non empty Relation-like NAT -defined Function-like total Function-yielding V55() set
dom ((NAT --> p0) +* (a .--> p1)) is non empty set
dom (NAT --> p0) is non empty set
(dom (NAT --> p0)) \/ (dom (a .--> p1)) is non empty set
(dom (NAT --> p0)) \/ {a} is non empty set
NAT \/ {a} is non empty set
P is ext-real V7() V8() V9() V13() complex V15() integer Element of NAT
((NAT --> p0) +* (a .--> p1)) . P is Relation-like Function-like set
V . P is non empty set
[:(V . P),(V . P):] is non empty Relation-like set
bool [:(V . P),(V . P):] is non empty set
(a .--> p1) . a is Relation-like Function-like set
(NAT --> INT) . P is non empty Element of {INT}
(NAT --> p0) . P is non empty Relation-like INT -defined INT -valued Function-like Element of bool [:INT,INT:]
P is Relation-like Function-like (V)
(V,P,(prop a)) is non empty Relation-like (V,(prop a)) -defined (V,(prop a)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(V,(prop a)),(V,(prop a)):]
[:(V,(prop a)),(V,(prop a)):] is non empty Relation-like set
bool [:(V,(prop a)),(V,(prop a)):] is non empty set
(V,P) is non empty Relation-like HP-WFF -defined Function-like total Function-yielding V55() ManySortedFunction of (V),(V)
(V,P) . (prop a) is Relation-like (V) . (prop a) -defined (V) . (prop a) -valued Function-like total quasi_total Element of bool [:((V) . (prop a)),((V) . (prop a)):]
[:((V) . (prop a)),((V) . (prop a)):] is Relation-like set
bool [:((V) . (prop a)),((V) . (prop a)):] is non empty set
P . a is set
(a .--> p1) . a is Relation-like Function-like set
f is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,(prop a)) -valued Function-like total quasi_total Element of bool [:(V,((prop a) => (prop b))),(V,(prop a)):]
(V,P,(((prop a) => (prop b)) => (prop a))) is non empty Relation-like (V,(((prop a) => (prop b)) => (prop a))) -defined (V,(((prop a) => (prop b)) => (prop a))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(V,(((prop a) => (prop b)) => (prop a))),(V,(((prop a) => (prop b)) => (prop a))):]
(V,(((prop a) => (prop b)) => (prop a))) is non empty functional set
(V) . (((prop a) => (prop b)) => (prop a)) is set
[:(V,(((prop a) => (prop b)) => (prop a))),(V,(((prop a) => (prop b)) => (prop a))):] is non empty Relation-like set
bool [:(V,(((prop a) => (prop b)) => (prop a))),(V,(((prop a) => (prop b)) => (prop a))):] is non empty set
(V,P) . (((prop a) => (prop b)) => (prop a)) is Relation-like (V) . (((prop a) => (prop b)) => (prop a)) -defined (V) . (((prop a) => (prop b)) => (prop a)) -valued Function-like total quasi_total Element of bool [:((V) . (((prop a) => (prop b)) => (prop a))),((V) . (((prop a) => (prop b)) => (prop a))):]
[:((V) . (((prop a) => (prop b)) => (prop a))),((V) . (((prop a) => (prop b)) => (prop a))):] is Relation-like set
bool [:((V) . (((prop a) => (prop b)) => (prop a))),((V) . (((prop a) => (prop b)) => (prop a))):] is non empty set
Funcs ((V,((prop a) => (prop b))),(V,(prop a))) is non empty functional FUNCTION_DOMAIN of (V,((prop a) => (prop b))),(V,(prop a))
dom (V,P,(((prop a) => (prop b)) => (prop a))) is non empty set
(V,P,(((prop a) => (prop b)) => (prop a))) . f is Relation-like Function-like set
(V,P,((prop a) => (prop b))) is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,((prop a) => (prop b))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(V,((prop a) => (prop b))),(V,((prop a) => (prop b))):]
[:(V,((prop a) => (prop b))),(V,((prop a) => (prop b))):] is non empty Relation-like set
bool [:(V,((prop a) => (prop b))),(V,((prop a) => (prop b))):] is non empty set
(V,P) . ((prop a) => (prop b)) is Relation-like (V) . ((prop a) => (prop b)) -defined (V) . ((prop a) => (prop b)) -valued Function-like total quasi_total Element of bool [:((V) . ((prop a) => (prop b))),((V) . ((prop a) => (prop b))):]
[:((V) . ((prop a) => (prop b))),((V) . ((prop a) => (prop b))):] is Relation-like set
bool [:((V) . ((prop a) => (prop b))),((V) . ((prop a) => (prop b))):] is non empty set
(V,P,((prop a) => (prop b))) " is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,((prop a) => (prop b))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(V,((prop a) => (prop b))),(V,((prop a) => (prop b))):]
rng ((V,P,((prop a) => (prop b))) ") is non empty set
((V,P,((prop a) => (prop b))) ") " is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,((prop a) => (prop b))) -valued Function-like one-to-one total quasi_total onto bijective Function-yielding V55() Element of bool [:(V,((prop a) => (prop b))),(V,((prop a) => (prop b))):]
dom (((V,P,((prop a) => (prop b))) ") ") is non empty set
dom f is non empty set
f * ((V,P,((prop a) => (prop b))) ") is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,(prop a)) -valued Function-like total quasi_total Element of bool [:(V,((prop a) => (prop b))),(V,(prop a)):]
dom (f * ((V,P,((prop a) => (prop b))) ")) is non empty set
dom ((V,P,((prop a) => (prop b))) ") is non empty set
rng (V,P,((prop a) => (prop b))) is non empty set
A ` is Element of bool (product ((0,1) --> (INT,INT)))
(product ((0,1) --> (INT,INT))) \ A is set
chi ((A `),(product ((0,1) --> (INT,INT)))) is Relation-like product ((0,1) --> (INT,INT)) -defined {{},1} -valued Function-like total quasi_total Element of bool [:(product ((0,1) --> (INT,INT))),{{},1}:]
dom (chi ((A `),(product ((0,1) --> (INT,INT))))) is set
p0 " is non empty Relation-like INT -defined INT -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:INT,INT:]
dom (p0 ") is non empty set
x is set
(f * ((V,P,((prop a) => (prop b))) ")) . x is set
(chi ((A `),(product ((0,1) --> (INT,INT))))) . x is set
Funcs ((V,(prop a)),(V,(prop b))) is non empty functional FUNCTION_DOMAIN of (V,(prop a)),(V,(prop b))
[:(V,(prop a)),(V,(prop b)):] is non empty Relation-like set
bool [:(V,(prop a)),(V,(prop b)):] is non empty set
g is non empty Relation-like (V,(prop a)) -defined (V,(prop b)) -valued Function-like total quasi_total Element of bool [:(V,(prop a)),(V,(prop b)):]
i0 is ext-real complex V15() integer Element of INT
j0 is ext-real complex V15() integer Element of INT
(0,1) --> (i0,j0) is non empty Relation-like NAT -defined {0,1} -defined INT -valued Function-like total quasi_total Element of bool [:{0,1},INT:]
[:{0,1},INT:] is non empty Relation-like set
bool [:{0,1},INT:] is non empty set
j0 is ext-real complex V15() integer set
j0 - 1 is ext-real complex V15() integer set
dom p0 is non empty set
p0 . (j0 - 1) is set
i is ext-real complex V15() integer set
i + 1 is ext-real complex V15() integer set
i0 is ext-real complex V15() integer set
i0 - 1 is ext-real complex V15() integer set
p0 . (i0 - 1) is set
i is ext-real complex V15() integer set
i + 1 is ext-real complex V15() integer set
(p0 ") . i0 is set
(V,P,(prop b)) is non empty Relation-like (V,(prop b)) -defined (V,(prop b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(V,(prop b)),(V,(prop b)):]
[:(V,(prop b)),(V,(prop b)):] is non empty Relation-like set
bool [:(V,(prop b)),(V,(prop b)):] is non empty set
(V,P) . (prop b) is Relation-like (V) . (prop b) -defined (V) . (prop b) -valued Function-like total quasi_total Element of bool [:((V) . (prop b)),((V) . (prop b)):]
[:((V) . (prop b)),((V) . (prop b)):] is Relation-like set
bool [:((V) . (prop b)),((V) . (prop b)):] is non empty set
P . b is set
(NAT --> p0) . b is non empty Relation-like INT -defined INT -valued Function-like Element of bool [:INT,INT:]
(V,P,(prop b)) " is non empty Relation-like (V,(prop b)) -defined (V,(prop b)) -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(V,(prop b)),(V,(prop b)):]
((V,P,(prop b)) ") * g is non empty Relation-like (V,(prop a)) -defined (V,(prop b)) -valued Function-like total quasi_total Element of bool [:(V,(prop a)),(V,(prop b)):]
(p0 ") . j0 is set
(0,1) --> (((p0 ") . i0),((p0 ") . j0)) is Relation-like NAT -defined Function-like set
(0,1) --> ((i0 - 1),(j0 - 1)) is Relation-like NAT -defined Function-like set
((V,P,((prop a) => (prop b))) ") . x is Relation-like Function-like set
f . (((V,P,((prop a) => (prop b))) ") . x) is set
(((V,P,(prop b)) ") * g) * (V,P,(prop a)) is non empty Relation-like (V,(prop a)) -defined (V,(prop b)) -valued Function-like total quasi_total Element of bool [:(V,(prop a)),(V,(prop b)):]
f . ((((V,P,(prop b)) ") * g) * (V,P,(prop a))) is set
(0,1) --> ((j0 - 1),(i0 - 1)) is Relation-like NAT -defined Function-like set
f . ((0,1) --> ((j0 - 1),(i0 - 1))) is set
i is ext-real complex V15() integer Element of INT
j is ext-real complex V15() integer Element of INT
(0,1) --> (i,j) is non empty Relation-like NAT -defined {0,1} -defined INT -valued Function-like total quasi_total Element of bool [:{0,1},INT:]
i is ext-real complex V15() integer Element of INT
j is ext-real complex V15() integer Element of INT
(0,1) --> (i,j) is non empty Relation-like NAT -defined {0,1} -defined INT -valued Function-like total quasi_total Element of bool [:{0,1},INT:]
(A `) ` is Element of bool (product ((0,1) --> (INT,INT)))
(product ((0,1) --> (INT,INT))) \ (A `) is set
(product ((0,1) --> (INT,INT))) \ A is Element of bool (product ((0,1) --> (INT,INT)))
(product ((0,1) --> (INT,INT))) \ A is Element of bool (product ((0,1) --> (INT,INT)))
(V,P,(prop a)) * (f * ((V,P,((prop a) => (prop b))) ")) is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,(prop a)) -valued Function-like total quasi_total Element of bool [:(V,((prop a) => (prop b))),(V,(prop a)):]
(V,P,(prop a)) * f is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,(prop a)) -valued Function-like total quasi_total Element of bool [:(V,((prop a) => (prop b))),(V,(prop a)):]
((V,P,(prop a)) * f) * ((V,P,((prop a) => (prop b))) ") is non empty Relation-like (V,((prop a) => (prop b))) -defined (V,(prop a)) -valued Function-like total quasi_total Element of bool [:(V,((prop a) => (prop b))),(V,(prop a)):]
x is set
dom (V,P,(prop a)) is non empty set
(V,P,(prop a)) . x is set