:: 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)