:: FLANG_1 semantic presentation

REAL is set
NAT is non empty V5() V6() V7() Element of K7(REAL)
K7(REAL) is non empty set
NAT is non empty V5() V6() V7() set
K7(NAT) is non empty set
K7(NAT) is non empty set
0 is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V33() V34() V37() V51() Element of NAT
1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative Element of NAT
K157(NAT,0,1) is non empty V33() Element of K7(NAT)
K157(NAT,0,1) ^omega is non empty functional set
K7((K157(NAT,0,1) ^omega)) is non empty set
K8(NAT,REAL) is V16() set
K7(K8(NAT,REAL)) is non empty set
2 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative Element of NAT
3 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative Element of NAT
{} is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V33() V34() V37() V51() set
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
A ^ x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() set
E is set
<%> E is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() set
E ^omega is non empty functional M9(E)
E is non empty set
A is Element of E
<%A%> is non empty V9() V16() V19( NAT ) V20(E) Function-like V33() V40(1) V51() set
E ^omega is non empty functional M9(E)
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
{A} is non empty functional V33() V37() set
K7((E ^omega)) is non empty set
E is set
bool E is non empty Element of K7(K7(E))
K7(E) is non empty set
K7(K7(E)) is non empty set
K8(NAT,(bool E)) is non empty V16() set
K7(K8(NAT,(bool E))) is non empty set
A is V16() V19( NAT ) V20( bool E) Function-like V30( NAT , bool E) Element of K7(K8(NAT,(bool E)))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
A . x is set
rng A is Element of K7((bool E))
K7((bool E)) is non empty set
E is V1() V5() V6() V7() V11() V12() ext-real non negative set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
E + x is V1() V5() V6() V7() V11() V12() ext-real non negative set
A + 0 is V1() V5() V6() V7() V11() V12() ext-real non negative set
E is V1() V5() V6() V7() V11() V12() ext-real non negative set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
E + A is V1() V5() V6() V7() V11() V12() ext-real non negative set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
1 + 0 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
E is V1() V5() V6() V7() V11() V12() ext-real non negative set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
E + A is V1() V5() V6() V7() V11() V12() ext-real non negative set
E is set
<%E%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
A is set
A ^omega is non empty functional M9(A)
(A) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(A) Function-like one-to-one constant functional V33() V34() V37() V51() Element of A ^omega
x is V9() V16() V19( NAT ) V20(A) Function-like V33() V51() Element of A ^omega
b is V9() V16() V19( NAT ) V20(A) Function-like V33() V51() Element of A ^omega
(A,x,b) is V9() V16() V19( NAT ) V20(A) Function-like V33() V51() Element of A ^omega
{} ^ b is V9() V16() V19( NAT ) Function-like V33() V51() set
x ^ {} is V9() V16() V19( NAT ) Function-like V33() V51() set
len (A,x,b) is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76((A,x,b)) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
len x is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(x) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(len x) + (len b) is V1() V5() V6() V7() V11() V12() ext-real non negative set
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
x is V9() V16() V19( NAT ) Function-like V33() V51() set
b is V9() V16() V19( NAT ) Function-like V33() V51() set
x ^ b is V9() V16() V19( NAT ) Function-like V33() V51() set
E is set
<%E%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
A is set
A ^omega is non empty functional M9(A)
rng <%E%> is non empty V33() set
{E} is non empty V33() set
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
b is V9() V16() V19( NAT ) Function-like V33() V51() set
c is set
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
b ^ <%c%> is V9() V16() V19( NAT ) Function-like V33() V51() set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
e is Element of E
<%e%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
b ^ <%e%> is V9() V16() V19( NAT ) Function-like V33() V51() set
len <%c%> is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(<%c%>) is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative V33() set
(len b) + (len <%c%>) is V1() V5() V6() V7() V11() V12() ext-real non negative set
(len b) + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
E is V9() V16() V19( NAT ) Function-like V33() V51() set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
A + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
x is V9() V16() V19( NAT ) Function-like V33() V51() set
len x is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(x) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
b is V9() V16() V19( NAT ) Function-like V33() V51() set
c is set
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
b ^ <%c%> is V9() V16() V19( NAT ) Function-like V33() V51() set
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
len <%c%> is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(<%c%>) is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative V33() set
(len b) + (len <%c%>) is V1() V5() V6() V7() V11() V12() ext-real non negative set
(len b) + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
{} ^ <%c%> is V9() V16() V19( NAT ) Function-like V33() V51() set
<%c%> ^ {} is V9() V16() V19( NAT ) Function-like V33() V51() set
b is set
<%b%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
e is V9() V16() V19( NAT ) Function-like V33() V51() set
<%b%> ^ e is V9() V16() V19( NAT ) Function-like V33() V51() set
e ^ <%c%> is V9() V16() V19( NAT ) Function-like V33() V51() set
<%b%> ^ (e ^ <%c%>) is V9() V16() V19( NAT ) Function-like V33() V51() set
A is V9() V16() V19( NAT ) Function-like V33() V51() set
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
len E is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(E) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
c is set
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
b is V9() V16() V19( NAT ) Function-like V33() V51() set
<%c%> ^ b is V9() V16() V19( NAT ) Function-like V33() V51() set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
e is Element of E
<%e%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
<%e%> ^ b is V9() V16() V19( NAT ) Function-like V33() V51() set
len <%c%> is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(<%c%>) is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative V33() set
(len b) + (len <%c%>) is V1() V5() V6() V7() V11() V12() ext-real non negative set
(len b) + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
x is V9() V16() V19( NAT ) Function-like V33() V51() set
len x is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(x) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
E is V1() V5() V6() V7() V11() V12() ext-real non negative set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
E + A is V1() V5() V6() V7() V11() V12() ext-real non negative set
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
c is V9() V16() V19( NAT ) Function-like V33() V51() set
len c is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(c) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
e is V9() V16() V19( NAT ) Function-like V33() V51() set
len e is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(e) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
c ^ e is V9() V16() V19( NAT ) Function-like V33() V51() set
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len n2 is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(n2) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(E,n2,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,A,A) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(len A) + (len A) is V1() V5() V6() V7() V11() V12() ext-real non negative set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
c is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is set
(E,b,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is functional Element of K7((E ^omega))
c is functional Element of K7((E ^omega))
e is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A,(E,(E))) is functional Element of K7((E ^omega))
(E,(E,(E)),A) is functional Element of K7((E ^omega))
x is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b ^ {} is V9() V16() V19( NAT ) Function-like V33() V51() set
x is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
{} ^ b is V9() V16() V19( NAT ) Function-like V33() V51() set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
x is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,(E)) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b ^ {} is V9() V16() V19( NAT ) Function-like V33() V51() set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
x is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
{} ^ c is V9() V16() V19( NAT ) Function-like V33() V51() set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is set
b is set
e is set
b is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,c) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
{} ^ (E) is V9() V16() V19( NAT ) Function-like V33() V51() set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,x,A) is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
b is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c ^ {} is V9() V16() V19( NAT ) Function-like V33() V51() set
b is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
{} ^ c is V9() V16() V19( NAT ) Function-like V33() V51() set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
c is functional Element of K7((E ^omega))
(E,x,c) is functional Element of K7((E ^omega))
e is set
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
(E,(E,A,x),b) is functional Element of K7((E ^omega))
(E,x,b) is functional Element of K7((E ^omega))
(E,A,(E,x,b)) is functional Element of K7((E ^omega))
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c₉ is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,n2,c₉) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c₉,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,n2,(E,c₉,b)) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c₉ is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,n2,c₉) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,(E,e,n2),c₉) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
(E,x,A) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
x /\ b is functional Element of K7((E ^omega))
(E,A,(x /\ b)) is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,A,x) /\ (E,A,b) is functional Element of K7((E ^omega))
(E,(x /\ b),A) is functional Element of K7((E ^omega))
(E,b,A) is functional Element of K7((E ^omega))
(E,x,A) /\ (E,b,A) is functional Element of K7((E ^omega))
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
(E,x,A) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,A,x) \/ (E,A,b) is functional Element of K7((E ^omega))
x \/ b is functional Element of K7((E ^omega))
(E,A,(x \/ b)) is functional Element of K7((E ^omega))
(E,b,A) is functional Element of K7((E ^omega))
(E,x,A) \/ (E,b,A) is functional Element of K7((E ^omega))
(E,(x \/ b),A) is functional Element of K7((E ^omega))
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
(E,x,A) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,A,x) \ (E,A,b) is functional Element of K7((E ^omega))
x \ b is functional Element of K7((E ^omega))
(E,A,(x \ b)) is functional Element of K7((E ^omega))
(E,b,A) is functional Element of K7((E ^omega))
(E,x,A) \ (E,b,A) is functional Element of K7((E ^omega))
(E,(x \ b),A) is functional Element of K7((E ^omega))
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
(E,x,A) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,A,x) \+\ (E,A,b) is functional Element of K7((E ^omega))
x \+\ b is functional Element of K7((E ^omega))
(E,A,(x \+\ b)) is functional Element of K7((E ^omega))
(E,b,A) is functional Element of K7((E ^omega))
(E,x,A) \+\ (E,b,A) is functional Element of K7((E ^omega))
(E,(x \+\ b),A) is functional Element of K7((E ^omega))
(E,A,x) \/ (E,A,b) is functional Element of K7((E ^omega))
(E,A,x) /\ (E,A,b) is functional Element of K7((E ^omega))
((E,A,x) \/ (E,A,b)) \ ((E,A,x) /\ (E,A,b)) is functional Element of K7((E ^omega))
x \/ b is functional Element of K7((E ^omega))
(E,A,(x \/ b)) is functional Element of K7((E ^omega))
(E,A,(x \/ b)) \ ((E,A,x) /\ (E,A,b)) is functional Element of K7((E ^omega))
x /\ b is functional Element of K7((E ^omega))
(E,A,(x /\ b)) is functional Element of K7((E ^omega))
(E,A,(x \/ b)) \ (E,A,(x /\ b)) is functional Element of K7((E ^omega))
(E,x,A) \/ (E,b,A) is functional Element of K7((E ^omega))
(E,x,A) /\ (E,b,A) is functional Element of K7((E ^omega))
((E,x,A) \/ (E,b,A)) \ ((E,x,A) /\ (E,b,A)) is functional Element of K7((E ^omega))
(E,(x \/ b),A) is functional Element of K7((E ^omega))
(E,(x \/ b),A) \ ((E,x,A) /\ (E,b,A)) is functional Element of K7((E ^omega))
(E,(x /\ b),A) is functional Element of K7((E ^omega))
(E,(x \/ b),A) \ (E,(x /\ b),A) is functional Element of K7((E ^omega))
(x \/ b) \ (x /\ b) is functional Element of K7((E ^omega))
(E,((x \/ b) \ (x /\ b)),A) is functional Element of K7((E ^omega))
(E,A,((x \/ b) \ (x /\ b))) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
bool (E ^omega) is non empty Element of K7(K7((E ^omega)))
K7(K7((E ^omega))) is non empty set
K8(NAT,(bool (E ^omega))) is non empty V16() set
K7(K8(NAT,(bool (E ^omega)))) is non empty set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
c is functional Element of bool (E ^omega)
(E,c,A) is functional Element of K7((E ^omega))
b is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),b,0) is functional Element of K7((E ^omega))
((E ^omega),b,x) is functional Element of K7((E ^omega))
c is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
((E ^omega),b,(b + 1)) is functional Element of K7((E ^omega))
((E ^omega),b,b) is functional Element of K7((E ^omega))
e + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
((E ^omega),b,(e + 1)) is functional Element of K7((E ^omega))
((E ^omega),b,e) is functional Element of K7((E ^omega))
(E,((E ^omega),b,e),A) is functional Element of K7((E ^omega))
c₉ is functional Element of K7((E ^omega))
n2 is functional Element of K7((E ^omega))
(E,n2,A) is functional Element of K7((E ^omega))
b is functional Element of K7((E ^omega))
c is functional Element of K7((E ^omega))
e is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),e,x) is functional Element of K7((E ^omega))
((E ^omega),e,0) is functional Element of K7((E ^omega))
b is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),b,x) is functional Element of K7((E ^omega))
((E ^omega),b,0) is functional Element of K7((E ^omega))
n2 is V1() V5() V6() V7() V11() V12() ext-real non negative set
((E ^omega),e,n2) is functional Element of K7((E ^omega))
((E ^omega),b,n2) is functional Element of K7((E ^omega))
n2 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
((E ^omega),b,(n2 + 1)) is functional Element of K7((E ^omega))
(E,((E ^omega),b,n2),A) is functional Element of K7((E ^omega))
((E ^omega),e,(n2 + 1)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(x + 1)) is functional Element of K7((E ^omega))
(E,A,x) is functional Element of K7((E ^omega))
(E,(E,A,x),A) is functional Element of K7((E ^omega))
bool (E ^omega) is non empty Element of K7(K7((E ^omega)))
K7(K7((E ^omega))) is non empty set
K8(NAT,(bool (E ^omega))) is non empty V16() set
K7(K8(NAT,(bool (E ^omega)))) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
b is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),b,x) is functional Element of K7((E ^omega))
((E ^omega),b,0) is functional Element of K7((E ^omega))
((E ^omega),b,(x + 1)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
bool (E ^omega) is non empty Element of K7(K7((E ^omega)))
K7(K7((E ^omega))) is non empty set
K8(NAT,(bool (E ^omega))) is non empty V16() set
K7(K8(NAT,(bool (E ^omega)))) is non empty set
x is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),x,0) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A,1) is functional Element of K7((E ^omega))
bool (E ^omega) is non empty Element of K7(K7((E ^omega)))
K7(K7((E ^omega))) is non empty set
K8(NAT,(bool (E ^omega))) is non empty V16() set
K7(K8(NAT,(bool (E ^omega)))) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
x is V16() V19( NAT ) V20( bool (E ^omega)) Function-like V30( NAT , bool (E ^omega)) Element of K7(K8(NAT,(bool (E ^omega))))
((E ^omega),x,1) is functional Element of K7((E ^omega))
((E ^omega),x,0) is functional Element of K7((E ^omega))
0 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
((E ^omega),x,(0 + 1)) is functional Element of K7((E ^omega))
(E,(E,(E)),A) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A,2) is functional Element of K7((E ^omega))
(E,A,A) is functional Element of K7((E ^omega))
1 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(1 + 1)) is functional Element of K7((E ^omega))
(E,A,1) is functional Element of K7((E ^omega))
(E,(E,A,1),A) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,(E,A,b),A) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
{} (E ^omega) is V1() empty proper V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) Function-like one-to-one constant functional V33() V34() V37() V51() Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,({} (E ^omega)),(b + 1)) is functional Element of K7((E ^omega))
(E,({} (E ^omega)),b) is functional Element of K7((E ^omega))
(E,(E,({} (E ^omega)),b),({} (E ^omega))) is functional Element of K7((E ^omega))
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,A,1) is functional Element of K7((E ^omega))
0 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
E is set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
E ^omega is non empty functional M9(E)
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
K7((E ^omega)) is non empty set
A is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,(E)),A) is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,(E)),x) is functional Element of K7((E ^omega))
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,(E,(E)),(x + 1)) is functional Element of K7((E ^omega))
(E,(E,(E,(E)),x),(E,(E))) is functional Element of K7((E ^omega))
(E,(E,(E)),0) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
(E,(E,A,x),A) is functional Element of K7((E ^omega))
(E,A,(E,A,x)) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
(E,A,(E,A,b)) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,(E,A,(b + 1)),A) is functional Element of K7((E ^omega))
(E,(E,(E,A,b),A),A) is functional Element of K7((E ^omega))
(E,A,(E,(E,A,b),A)) is functional Element of K7((E ^omega))
(E,A,(E,A,(b + 1))) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E,(E,A,0),A) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E,(E)),A) is functional Element of K7((E ^omega))
(E,A,(E,(E))) is functional Element of K7((E ^omega))
(E,A,(E,A,0)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(x + b)) is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,x),(E,A,b)) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
e + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(e + b)) is functional Element of K7((E ^omega))
(E,A,e) is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,e),(E,A,b)) is functional Element of K7((E ^omega))
(E,A,(c + 1)) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E,A,(c + 1)),(E,(E))) is functional Element of K7((E ^omega))
n2 is V1() V5() V6() V7() V11() V12() ext-real non negative set
n2 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
n2 + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(n2 + b) + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,((n2 + b) + 1)) is functional Element of K7((E ^omega))
(E,A,(n2 + b)) is functional Element of K7((E ^omega))
(E,(E,A,(n2 + b)),A) is functional Element of K7((E ^omega))
(E,A,(E,A,(n2 + b))) is functional Element of K7((E ^omega))
(E,A,n2) is functional Element of K7((E ^omega))
(E,(E,A,n2),(E,A,b)) is functional Element of K7((E ^omega))
(E,A,(E,(E,A,n2),(E,A,b))) is functional Element of K7((E ^omega))
(E,A,(E,A,n2)) is functional Element of K7((E ^omega))
(E,(E,A,(E,A,n2)),(E,A,b)) is functional Element of K7((E ^omega))
(E,(E,A,n2),A) is functional Element of K7((E ^omega))
(E,(E,(E,A,n2),A),(E,A,b)) is functional Element of K7((E ^omega))
(E,A,1) is functional Element of K7((E ^omega))
(E,(E,A,n2),(E,A,1)) is functional Element of K7((E ^omega))
(E,(E,(E,A,n2),(E,A,1)),(E,A,b)) is functional Element of K7((E ^omega))
(E,(E,(E)),(E,A,(c + 1))) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
e + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(e + b)) is functional Element of K7((E ^omega))
(E,A,e) is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,e),(E,A,b)) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(c + e)) is functional Element of K7((E ^omega))
(E,A,e) is functional Element of K7((E ^omega))
(E,(E,A,c),(E,A,e)) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E,(E,A,0),(E,(E))) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,A,x),b) is functional Element of K7((E ^omega))
x * b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(x * b)) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
e + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,e) is functional Element of K7((E ^omega))
(E,(E,A,e),b) is functional Element of K7((E ^omega))
e * b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(e * b)) is functional Element of K7((E ^omega))
n2 is V1() V5() V6() V7() V11() V12() ext-real non negative set
n2 + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
e + n2 is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,A,e),n2) is functional Element of K7((E ^omega))
(E,(E,(E,A,e),n2),(E,A,e)) is functional Element of K7((E ^omega))
e * n2 is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(e * n2)) is functional Element of K7((E ^omega))
(E,(E,A,(e * n2)),(E,A,e)) is functional Element of K7((E ^omega))
(e * n2) + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,((e * n2) + e)) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E,(E)),b) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
e + b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,e) is functional Element of K7((E ^omega))
(E,(E,A,e),b) is functional Element of K7((E ^omega))
e * b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(e * b)) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,A,c),e) is functional Element of K7((E ^omega))
c * e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(c * e)) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
(E,(E,A,c),e) is functional Element of K7((E ^omega))
c * e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(c * e)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
b + c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
(E,(E,A,c),(E,A,b)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,x,b) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
(E,x,c) is functional Element of K7((E ^omega))
(E,(E,A,c),A) is functional Element of K7((E ^omega))
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(c + 1)) is functional Element of K7((E ^omega))
(E,(E,x,c),x) is functional Element of K7((E ^omega))
(E,x,(c + 1)) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,x,0) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
A \/ x is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,x,b) is functional Element of K7((E ^omega))
(E,A,b) \/ (E,x,b) is functional Element of K7((E ^omega))
(E,(A \/ x),b) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
A /\ x is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(A /\ x),b) is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
(E,x,b) is functional Element of K7((E ^omega))
(E,A,b) /\ (E,x,b) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,x,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,e) is functional Element of K7((E ^omega))
c + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(c + e)) is functional Element of K7((E ^omega))
(E,(E,A,c),(E,A,e)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
K7(K7((E ^omega))) is non empty set
{ b₁ where b₁ is functional Element of K7((E ^omega)) : S₁[b₁] } is set
x is Element of K7(K7((E ^omega)))
union x is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
b is set
{ b₁ where b₁ is functional Element of K7((E ^omega)) : S₁[b₁] } is set
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,c) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
c is functional Element of K7((E ^omega))
K7(K7((E ^omega))) is non empty set
{ b₁ where b₁ is functional Element of K7((E ^omega)) : S₁[b₁] } is set
e is Element of K7(K7((E ^omega)))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,A,1) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A,A) is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,A,2) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,x,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,e) is functional Element of K7((E ^omega))
c + e is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,(c + e)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
b is functional Element of K7((E ^omega))
(E,A,b) is functional Element of K7((E ^omega))
c is set
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is set
x is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
x is set
(E,A,0) is functional Element of K7((E ^omega))
x is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
x is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
E is set
{E} is non empty V33() set
A is set
A ^omega is non empty functional M9(A)
K7((A ^omega)) is non empty set
(A) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(A) Function-like one-to-one constant functional V33() V34() V37() V51() Element of A ^omega
x is functional Element of K7((A ^omega))
(A,x) is functional Element of K7((A ^omega))
{ b₁ where b₁ is functional Element of K7((A ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (A,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((A ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (A,x,b₂) } is set
b is V9() V16() V19( NAT ) V20(A) Function-like V33() V51() Element of A ^omega
(A,b,b) is V9() V16() V19( NAT ) V20(A) Function-like V33() V51() Element of A ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
(E,(E,x),x) is functional Element of K7((E ^omega))
(E,x,(E,x)) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,x,(b + 1)) is functional Element of K7((E ^omega))
(E,x,b) is functional Element of K7((E ^omega))
(E,(E,x,b),x) is functional Element of K7((E ^omega))
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,x,(E,x,b)) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,b,n2) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,A,(E,A)) is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(x + 1)) is functional Element of K7((E ^omega))
b is set
b is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
(E,(E,x),x) is functional Element of K7((E ^omega))
(E,x,(E,x)) is functional Element of K7((E ^omega))
b is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
(E,x,1) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,x,(b + 1)) is functional Element of K7((E ^omega))
b is set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,c,e) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,x,(b + 1)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,A,(E,A)) is functional Element of K7((E ^omega))
x is set
x is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,A,(E,A)) is functional Element of K7((E ^omega))
x is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
x is set
x is set
x is set
b is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,x)) is functional Element of K7((E ^omega))
(E,(E,A,x),(E,A)) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E,(E,A,0),(E,A)) is functional Element of K7((E ^omega))
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E,(E)),(E,A)) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,b)) is functional Element of K7((E ^omega))
(E,(E,A,b),(E,A)) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,(b + 1))) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
(E,(E,A),(E,(E,A,b),A)) is functional Element of K7((E ^omega))
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,(E,A,(b + 1)),(E,A)) is functional Element of K7((E ^omega))
(E,(E,(E,A,b),A),(E,A)) is functional Element of K7((E ^omega))
(E,A,(E,A,b)) is functional Element of K7((E ^omega))
(E,(E,A,(E,A,b)),(E,A)) is functional Element of K7((E ^omega))
(E,A,(E,A)) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,0)) is functional Element of K7((E ^omega))
(E,(E,A),(E,(E))) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,A,(E,A)) is functional Element of K7((E ^omega))
(E,(E)) \/ (E,A,(E,A)) is non empty functional Element of K7((E ^omega))
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,(E)) \/ (E,(E,A),A) is non empty functional Element of K7((E ^omega))
x is set
x is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
x is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
x is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,A,(E,A)) is functional Element of K7((E ^omega))
(E,(E,A),A) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E)) \/ (E,A,(E,A)) is non empty functional Element of K7((E ^omega))
(E,(E)) \/ (E,(E,A),A) is non empty functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
(E,(E,A,x),(E,A)) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,x)) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
(E,(E,A,b),(E,A)) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,b)) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(b + 1)) is functional Element of K7((E ^omega))
(E,(E,A,(b + 1)),(E,A)) is functional Element of K7((E ^omega))
(E,(E,A,b),A) is functional Element of K7((E ^omega))
(E,(E,(E,A,b),A),(E,A)) is functional Element of K7((E ^omega))
(E,A,(E,A)) is functional Element of K7((E ^omega))
(E,(E,A,b),(E,A,(E,A))) is functional Element of K7((E ^omega))
(E,(E,A),A) is functional Element of K7((E ^omega))
(E,(E,A,b),(E,(E,A),A)) is functional Element of K7((E ^omega))
(E,(E,(E,A),(E,A,b)),A) is functional Element of K7((E ^omega))
(E,(E,A),(E,(E,A,b),A)) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,(b + 1))) is functional Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
(E,(E,A,0),(E,A)) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,(E,(E)),(E,A)) is functional Element of K7((E ^omega))
(E,(E,A),(E,(E))) is functional Element of K7((E ^omega))
(E,(E,A),(E,A,0)) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,b) is functional Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
(E,(E,A,c),A) is functional Element of K7((E ^omega))
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,A,(c + 1)) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
(E,A,0) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
b is set
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,c) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E,A)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A),b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
(E,(E,A),(E,A)) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,A,x) is functional Element of K7((E ^omega))
(E,(E,A,x)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A,x),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A,x),b₂) } is set
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,A),x) is functional Element of K7((E ^omega))
(E,(E,A)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E,A),b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E,A),x) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
x \/ A is functional Element of K7((E ^omega))
(E,(x \/ A)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(x \/ A),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(x \/ A),b₂) } is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(x \/ A),b) is functional Element of K7((E ^omega))
b + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,(x \/ A),(b + 1)) is functional Element of K7((E ^omega))
(E,(E,(x \/ A),b),(x \/ A)) is functional Element of K7((E ^omega))
(E,(x \/ A),0) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
b is set
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(x \/ A),c) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,x) is non empty functional V33() V37() Element of K7((E ^omega))
A \/ (E,x) is non empty functional Element of K7((E ^omega))
(E,(A \/ (E,x))) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ (E,x)),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ (E,x)),b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
A \ (E,(E)) is functional Element of K7((E ^omega))
(E,(A \ (E,(E)))) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \ (E,(E))),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \ (E,(E))),b₂) } is set
(A \ (E,(E))) \/ (E,(E)) is non empty functional Element of K7((E ^omega))
(E,((A \ (E,(E))) \/ (E,(E)))) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,((A \ (E,(E))) \/ (E,(E))),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,((A \ (E,(E))) \/ (E,(E))),b₂) } is set
A \/ (E,(E)) is non empty functional Element of K7((E ^omega))
(E,(A \/ (E,(E)))) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ (E,(E))),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ (E,(E))),b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
(E,A) \/ (E,x) is functional Element of K7((E ^omega))
A \/ x is functional Element of K7((E ^omega))
(E,(A \/ x)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ x),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A \/ x),b₂) } is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is functional Element of K7((E ^omega))
A /\ x is functional Element of K7((E ^omega))
(E,(A /\ x)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A /\ x),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(A /\ x),b₂) } is set
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
(E,A) /\ (E,x) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is set
<%A%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
x is functional Element of K7((E ^omega))
(E,x) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,x,b₂) } is set
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
b is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,x,b) is functional Element of K7((E ^omega))
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
c is V1() V5() V6() V7() V11() V12() ext-real non negative set
c + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
(E,x,c) is functional Element of K7((E ^omega))
(E,(E,x,c),x) is functional Element of K7((E ^omega))
e is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
(E,e,b) is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
n2 is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
(E,x,n2) is functional Element of K7((E ^omega))
c₉ is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
(E,x,c₉) is functional Element of K7((E ^omega))
(E,x,1) is functional Element of K7((E ^omega))
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
A is functional Element of K7((E ^omega))
x is set
b is Element of E
<%b%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
{b} is non empty V33() set
rng <%b%> is non empty V33() set
x is set
c is Element of E
b is set
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
A is functional Element of K7((E ^omega))
x is functional Element of K7((E ^omega))
b is set
c is Element of E
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
c is Element of E
<%c%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
E is set
E ^omega is non empty functional M9(E)
(E) is functional Element of K7((E ^omega))
K7((E ^omega)) is non empty set
A is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len A is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(A) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(E,(E),(len A)) is functional Element of K7((E ^omega))
x is V1() V5() V6() V7() V11() V12() ext-real non negative set
(E,(E),x) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
x + 1 is V1() non empty V5() V6() V7() V11() V12() ext-real positive non negative set
c is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len c is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(c) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
e is Element of E
<%e%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set
c ^ <%e%> is V9() V16() V19( NAT ) Function-like V33() V51() set
(E,(E),1) is functional Element of K7((E ^omega))
(E,(E),(x + 1)) is functional Element of K7((E ^omega))
b is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len b is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(b) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(E,(E),0) is functional Element of K7((E ^omega))
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len x is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(x) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(E) is V1() empty V5() V6() V7() V9() V10() V11() V12() ext-real non positive non negative V16() non-empty empty-yielding V19( NAT ) V20(E) Function-like one-to-one constant functional V33() V34() V37() V51() Element of E ^omega
(E,(E)) is non empty functional V33() V37() Element of K7((E ^omega))
E is set
(E) is functional Element of K7((E ^omega))
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E,(E)) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E),b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,(E),b₂) } is set
A is set
x is V9() V16() V19( NAT ) V20(E) Function-like V33() V51() Element of E ^omega
len x is V1() V5() V6() V7() V11() V12() ext-real non negative Element of NAT
K76(x) is V1() V5() V6() V7() V11() V12() ext-real non negative V33() set
(E,(E),(len x)) is functional Element of K7((E ^omega))
A is set
E is set
E ^omega is non empty functional M9(E)
K7((E ^omega)) is non empty set
(E) is functional Element of K7((E ^omega))
A is functional Element of K7((E ^omega))
(E,A) is functional Element of K7((E ^omega))
{ b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
union { b₁ where b₁ is functional Element of K7((E ^omega)) : ex b₂ being V1() V5() V6() V7() V11() V12() ext-real non negative set st b₁ = (E,A,b₂) } is set
x is set
b is Element of E
<%b%> is non empty V9() V16() V19( NAT ) Function-like V33() V40(1) V51() set