:: FLANG_3 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() Element of K6(REAL)
K6(REAL) is non empty set
NAT is non empty V4() V5() V6() set
K6(NAT) is non empty set
K6(NAT) is non empty set
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() Element of NAT
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
K157(NAT,0,1) is non empty Element of K6(NAT)
K157(NAT,0,1) ^omega is non empty V23() set
K6((K157(NAT,0,1) ^omega)) is non empty set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is non empty set
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() Element of NAT
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
A * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(A *) ^^ x is Element of K6(K231(E))
x ^^ (A *) is Element of K6(K231(E))
(A *) ^^ (A *) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
K6(K6((E ^omega))) is non empty set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
n is Element of K6(K6((E ^omega)))
union n is Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is set
A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
k is Element of K6((E ^omega))
K6(K6((E ^omega))) is non empty set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
a is Element of K6(K6((E ^omega)))
b is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ b is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
k is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x |^ 0 is Element of K6(K231(E))
K6(K231(E)) is non empty set
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
{(<%> E)} is non empty Element of K6(K231(E))
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (n,x) is Element of K6((E ^omega))
k is set
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ a is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
(E,x,(n + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) \/ (E,x,(n + 1)) is Element of K6((E ^omega))
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ A) \/ (E,x,(A + 1)) is Element of K6((E ^omega))
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
x |^ (A,A) is Element of K6((E ^omega))
(x |^ (A,A)) \/ (E,x,(A + 1)) is Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} is non empty Element of K6(K231(E))
K6(K231(E)) is non empty set
x |^ 0 is Element of K6(K231(E))
x |^ A is Element of K6(K231(E))
x |^ A is Element of K6(K231(E))
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
x |^ A is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (0,A) is Element of K6((E ^omega))
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (0,A)) \/ (E,x,(A + 1)) is Element of K6((E ^omega))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ k is Element of K6(K231(E))
E is set
x is set
x ^omega is non empty V23() set
K6((x ^omega)) is non empty set
<%> x is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(x) V20() V32() V33() V51() Element of K231(x)
K231(x) is non empty V23() M9(x)
{(<%> x)} is non empty Element of K6(K231(x))
K6(K231(x)) is non empty set
A is Element of K6((x ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x,A,n) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
A |^ 1 is Element of K6(K231(x))
A |^ n is Element of K6(K231(x))
x is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty Element of K6(K231(E))
K6(K231(E)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
x is set
n is set
n is set
x |^ A is Element of K6(K231(E))
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
x * is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ k is Element of K6(K231(E))
x |^ 1 is Element of K6(K231(E))
(x |^ k) ^^ (x |^ 1) is Element of K6(K231(E))
a is V8() V33() Element of E ^omega
b is V8() V33() Element of E ^omega
a ^ b is V8() V33() Element of K231(E)
(E,x,A) ^^ (x |^ 1) is Element of K6(K231(E))
n is set
x is V8() V33() Element of E ^omega
k is V8() V33() Element of E ^omega
x ^ k is V8() V33() Element of K231(E)
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ a is Element of K6(K231(E))
a + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (a + 1) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (x *) is Element of K6(K231(E))
n is set
x is V8() V33() Element of E ^omega
k is V8() V33() Element of E ^omega
x ^ k is V8() V33() Element of K231(E)
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ a is Element of K6(K231(E))
b is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ b is Element of K6(K231(E))
b + a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (b + a) is Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,n) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,x) is Element of K6(K231(E))
A + x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + x <= b₂ & b₁ = x |^ b₂ ) } is set
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(x + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,(x + 1)) is Element of K6(K231(E))
(E,x,x) ^^ x is Element of K6(K231(E))
(E,x,A) ^^ ((E,x,x) ^^ x) is Element of K6(K231(E))
(E,x,(A + x)) ^^ x is Element of K6(K231(E))
(A + x) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,((A + x) + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + x) + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + x) + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
A + (x + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,0) is Element of K6(K231(E))
x * is Element of K6(K231(E))
(E,x,A) ^^ (x *) is Element of K6(K231(E))
A + 0 is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + 0)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * A <= b₂ & b₁ = x |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) |^ x is Element of K6(K231(E))
n * x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * x <= b₂ & b₁ = x |^ b₂ ) } is set
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,n) |^ (x + 1) is Element of K6(K231(E))
n * (x + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ (x + 1) is Element of K6(K231(E))
(E,x,(n * x)) ^^ (E,x,n) is Element of K6(K231(E))
(n * x) + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,((n * x) + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (n * x) + n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (n * x) + n <= b₂ & b₁ = x |^ b₂ ) } is set
n * (x + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ (x + 1) is Element of K6(K231(E))
n * (x + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ (x + 1) is Element of K6(K231(E))
n * (x + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(n * (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ 0 is Element of K6(K231(E))
n * 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V32() set
(E,x,(n * 0)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * 0 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,A) ? is Element of K6((E ^omega))
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) |^ x is Element of K6(K231(E))
(E,x,A) |^ 0 is Element of K6(K231(E))
(E,x,A) |^ 1 is Element of K6(K231(E))
((E,x,A) |^ 0) \/ ((E,x,A) |^ 1) is Element of K6(K231(E))
A * x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A * x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * x <= b₂ & b₁ = x |^ b₂ ) } is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,A) |^ 1 is Element of K6(K231(E))
(E,x,A) |^ 0 is Element of K6(K231(E))
((E,x,A) |^ 0) \/ ((E,x,A) |^ 1) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
n is Element of K6((E ^omega))
x ^^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = A |^ b₂ ) } is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,k) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = A |^ b₂ ) } is set
x + k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(x + k)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + k <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + k <= b₂ & b₁ = A |^ b₂ ) } is set
a is set
b is V8() V33() Element of E ^omega
b is V8() V33() Element of E ^omega
b ^ b is V8() V33() Element of K231(E)
(E,A,x) ^^ (E,A,k) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
x |^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,A) ^^ (x |^ n) is Element of K6(K231(E))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + x <= b₂ & b₁ = x |^ b₂ ) } is set
x |^ x is Element of K6(K231(E))
(E,x,A) ^^ (x |^ x) is Element of K6(K231(E))
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A + (x + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + (x + 1))) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + (x + 1) <= b₂ & b₁ = x |^ b₂ ) } is set
(A + x) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,((A + x) + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + x) + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + x) + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
((E,x,A) ^^ (x |^ x)) ^^ x is Element of K6(K231(E))
(x |^ x) ^^ x is Element of K6(K231(E))
(E,x,A) ^^ ((x |^ x) ^^ x) is Element of K6(K231(E))
x |^ (x + 1) is Element of K6(K231(E))
(E,x,A) ^^ (x |^ (x + 1)) is Element of K6(K231(E))
A + 0 is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + 0)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
(E,x,A) ^^ {(<%> E)} is Element of K6(K231(E))
x |^ 0 is Element of K6(K231(E))
(E,x,A) ^^ (x |^ 0) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
x ^^ (E,x,A) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,A) ^^ x is Element of K6(K231(E))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
x ^^ (E,x,n) is Element of K6(K231(E))
(E,x,n) ^^ x is Element of K6(K231(E))
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(n + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
x ^^ (E,x,(n + 1)) is Element of K6(K231(E))
x ^^ ((E,x,n) ^^ x) is Element of K6(K231(E))
((E,x,n) ^^ x) ^^ x is Element of K6(K231(E))
(E,x,(n + 1)) ^^ x is Element of K6(K231(E))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
x ^^ (E,x,0) is Element of K6(K231(E))
x * is Element of K6(K231(E))
x ^^ (x *) is Element of K6(K231(E))
(x *) ^^ x is Element of K6(K231(E))
(E,x,0) ^^ x is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ A) ^^ (E,x,n) is Element of K6(K231(E))
(E,x,n) ^^ (x |^ A) is Element of K6(K231(E))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
(x |^ x) ^^ (E,x,n) is Element of K6(K231(E))
(E,x,n) ^^ (x |^ x) is Element of K6(K231(E))
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (x + 1) is Element of K6(K231(E))
(x |^ (x + 1)) ^^ (E,x,n) is Element of K6(K231(E))
(x |^ x) ^^ x is Element of K6(K231(E))
((x |^ x) ^^ x) ^^ (E,x,n) is Element of K6(K231(E))
x ^^ (x |^ x) is Element of K6(K231(E))
(x ^^ (x |^ x)) ^^ (E,x,n) is Element of K6(K231(E))
x ^^ ((E,x,n) ^^ (x |^ x)) is Element of K6(K231(E))
x ^^ (E,x,n) is Element of K6(K231(E))
(x ^^ (E,x,n)) ^^ (x |^ x) is Element of K6(K231(E))
(E,x,n) ^^ x is Element of K6(K231(E))
((E,x,n) ^^ x) ^^ (x |^ x) is Element of K6(K231(E))
(E,x,n) ^^ (x ^^ (x |^ x)) is Element of K6(K231(E))
(E,x,n) ^^ ((x |^ x) ^^ x) is Element of K6(K231(E))
(E,x,n) ^^ (x |^ (x + 1)) is Element of K6(K231(E))
x |^ 0 is Element of K6(K231(E))
(x |^ 0) ^^ (E,x,n) is Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
{(<%> E)} ^^ (E,x,n) is Element of K6(K231(E))
(E,x,n) ^^ {(<%> E)} is Element of K6(K231(E))
(E,x,n) ^^ (x |^ 0) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) ^^ (E,x,x) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,x) ^^ (x |^ (A,n)) is Element of K6(K231(E))
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,k) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) ^^ (E,x,k) is Element of K6(K231(E))
(E,x,k) ^^ (x |^ (A,n)) is Element of K6(K231(E))
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(k + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) ^^ (E,x,(k + 1)) is Element of K6(K231(E))
(E,x,k) ^^ x is Element of K6(K231(E))
(x |^ (A,n)) ^^ ((E,x,k) ^^ x) is Element of K6(K231(E))
((E,x,k) ^^ (x |^ (A,n))) ^^ x is Element of K6(K231(E))
(x |^ (A,n)) ^^ x is Element of K6(K231(E))
(E,x,k) ^^ ((x |^ (A,n)) ^^ x) is Element of K6(K231(E))
x ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,k) ^^ (x ^^ (x |^ (A,n))) is Element of K6(K231(E))
((E,x,k) ^^ x) ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,(k + 1)) ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) ^^ (E,x,0) is Element of K6(K231(E))
x * is Element of K6(K231(E))
(x |^ (A,n)) ^^ (x *) is Element of K6(K231(E))
(x *) ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,0) ^^ (x |^ (A,n)) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
A ^^ (E,x,n) is Element of K6(K231(E))
K6(K231(E)) is non empty set
(E,x,n) ^^ A is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,n) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,n) ^^ (E,x,A) is Element of K6(K231(E))
A + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + n <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (k + 1) is Element of K6(K231(E))
(x |^ k) ^^ x is Element of K6(K231(E))
(E,A,n) ^^ (E,A,n) is Element of K6(K231(E))
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (k + 1) is Element of K6(K231(E))
n + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(n + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
x |^ 0 is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
k is set
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ a is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(x *) ^^ x is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
A is set
n is V8() V33() Element of E ^omega
x is V8() V33() Element of E ^omega
n ^ x is V8() V33() Element of K231(E)
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ 1 is Element of K6(K231(E))
x |^ (k + 1) is Element of K6(K231(E))
A is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (x + 1) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
(x *) ^^ (x |^ A) is Element of K6(K231(E))
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
(x *) ^^ (x |^ n) is Element of K6(K231(E))
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
x |^ (n + 1) is Element of K6(K231(E))
(x *) ^^ (x |^ (n + 1)) is Element of K6(K231(E))
(x |^ n) ^^ x is Element of K6(K231(E))
(x *) ^^ ((x |^ n) ^^ x) is Element of K6(K231(E))
(E,x,n) ^^ x is Element of K6(K231(E))
(E,x,(n + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
x |^ 0 is Element of K6(K231(E))
(x *) ^^ (x |^ 0) is Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
(x *) ^^ {(<%> E)} is Element of K6(K231(E))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (x *) is Element of K6(K231(E))
(x *) ^^ (E,x,A) is Element of K6(K231(E))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,0) is Element of K6(K231(E))
(E,x,0) ^^ (E,x,A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,x) ^^ (x |^ (A,n)) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(x + A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + A <= b₂ & b₁ = x |^ b₂ ) } is set
k is set
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ a is Element of K6(K231(E))
b is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x + A) + b is V4() V5() V6() V10() V11() ext-real non negative V32() set
x + b is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x + b) + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (x + b) is Element of K6(K231(E))
x |^ A is Element of K6(K231(E))
(x |^ (x + b)) ^^ (x |^ A) is Element of K6(K231(E))
b is V8() V33() Element of E ^omega
c₁₀ is V8() V33() Element of E ^omega
b ^ c₁₀ is V8() V33() Element of K231(E)
k is set
a is V8() V33() Element of E ^omega
b is V8() V33() Element of E ^omega
a ^ b is V8() V33() Element of K231(E)
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,x) ^^ (E,x,A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
(x *) ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,0) ^^ (x |^ (A,n)) is Element of K6(K231(E))
0 + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(0 + A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + A <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(x |^ A),n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x |^ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x |^ A) |^ b₂ ) } is set
A * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A * n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b₂ & b₁ = x |^ b₂ ) } is set
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x |^ A) |^ k is Element of K6(K231(E))
A * k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A * k) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(x |^ A),n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x |^ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x |^ A) |^ b₂ ) } is set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,n) |^ A is Element of K6(K231(E))
A * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A * n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b₂ & b₁ = x |^ b₂ ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
(E,{(<%> E)},n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = {(<%> E)} |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = {(<%> E)} |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is V8() V33() Element of E ^omega
n is V8() V33() Element of E ^omega
A ^ n is V8() V33() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b₂ & b₁ = x |^ b₂ ) } is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,k) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
x + k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(x + k)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + k <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x + k <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,x) ^^ (E,x,k) is Element of K6(K231(E))
K6(K231(E)) is non empty set
E is set
{E} is non empty set
x is set
x ^omega is non empty V23() set
K6((x ^omega)) is non empty set
<%> x is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(x) V20() V32() V33() V51() Element of K231(x)
K231(x) is non empty V23() M9(x)
A is Element of K6((x ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x,A,n) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is V8() V33() Element of x ^omega
x ^ x is V8() V33() Element of K231(x)
n + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x,A,(n + n)) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
A * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
x ? is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x ? is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (x ?) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x |^ (0,1) is Element of K6((E ^omega))
(E,x,A) ^^ (x |^ (0,1)) is Element of K6(K231(E))
A + 0 is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(A + 0)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 0 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x ? is Element of K6((E ^omega))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (x ?) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(x ?) ^^ (E,x,A) is Element of K6(K231(E))
x |^ (0,1) is Element of K6((E ^omega))
(E,x,A) ^^ (x |^ (0,1)) is Element of K6(K231(E))
(x |^ (0,1)) ^^ (E,x,A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
A * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
(E,A,n) ^^ x is Element of K6(K231(E))
x ^^ (E,A,n) is Element of K6(K231(E))
(A *) ^^ (E,A,n) is Element of K6(K231(E))
(E,A,n) ^^ (A *) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
x /\ A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(x /\ A),n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x /\ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x /\ A) |^ b₂ ) } is set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
(E,x,n) /\ (E,A,n) is Element of K6((E ^omega))
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x /\ A) |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ k is Element of K6(K231(E))
x |^ k is Element of K6(K231(E))
(x |^ k) /\ (A |^ k) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
x \/ A is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
(E,x,n) \/ (E,A,n) is Element of K6((E ^omega))
(E,(x \/ A),n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x \/ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (x \/ A) |^ b₂ ) } is set
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ k is Element of K6(K231(E))
(x |^ k) \/ (A |^ k) is Element of K6(K231(E))
(x \/ A) |^ k is Element of K6(K231(E))
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x |^ k is Element of K6(K231(E))
(x |^ k) \/ (A |^ k) is Element of K6(K231(E))
(x \/ A) |^ k is Element of K6(K231(E))
E is set
<%E%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
x is set
x ^omega is non empty V23() set
K6((x ^omega)) is non empty set
<%> x is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(x) V20() V32() V33() V51() Element of K231(x)
K231(x) is non empty V23() M9(x)
A is Element of K6((x ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x,A,n) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is Element of K6(K231(x))
K6(K231(x)) is non empty set
A |^ n is Element of K6(K231(x))
K6(K231(x)) is non empty set
A * is Element of K6(K231(x))
K6(K231(x)) is non empty set
A |^ n is Element of K6(K231(x))
K6(K231(x)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
A \/ x is Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = A |^ b₂ ) } is set
(E,(A \/ x),n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (A \/ x) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = (A \/ x) |^ b₂ ) } is set
A |^ 1 is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A \/ x) |^ x is Element of K6(K231(E))
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(A \/ x) |^ n is Element of K6(K231(E))
(E,A,1) |^ n is Element of K6(K231(E))
1 * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(1 * n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 * n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 * n <= b₂ & b₁ = A |^ b₂ ) } is set
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
n + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(n + n)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + n <= b₂ & b₁ = A |^ b₂ ) } is set
((A \/ x) |^ x) ^^ x is Element of K6(K231(E))
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(n + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b₂ & b₁ = A |^ b₂ ) } is set
((A \/ x) |^ x) ^^ A is Element of K6(K231(E))
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
((A \/ x) |^ x) ^^ (A \/ x) is Element of K6(K231(E))
(((A \/ x) |^ x) ^^ A) \/ (((A \/ x) |^ x) ^^ x) is Element of K6(K231(E))
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
(A \/ x) |^ (x + 1) is Element of K6(K231(E))
(A \/ x) |^ 0 is Element of K6(K231(E))
A * is Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A \/ x) |^ k is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
K6(K6((E ^omega))) is non empty set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
A is Element of K6(K6((E ^omega)))
union A is Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is set
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
n is set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is Element of K6((E ^omega))
K6(K6((E ^omega))) is non empty set
{ b₁ where b₁ is Element of K6((E ^omega)) : S₁[b₁] } is set
k is Element of K6(K6((E ^omega)))
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ a is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
A is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(x *) ^^ x is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty Element of K6(K231(E))
K6(K231(E)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
{(<%> E)} \/ (E,x) is non empty Element of K6((E ^omega))
(x *) ^^ x is Element of K6(K231(E))
{(<%> E)} \/ ((x *) ^^ x) is non empty Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (1,A) is Element of K6((E ^omega))
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (1,A)) \/ (E,x,(A + 1)) is Element of K6((E ^omega))
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
K6(K231(E)) is non empty set
(x *) ^^ x is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x |^ 1 is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,(x *)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x *) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x *) |^ b₂ ) } is set
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x) * is Element of K6(K231(E))
A is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(x *) |^ n is Element of K6(K231(E))
A is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x) |^ n is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
A * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,(A *)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (A *) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (A *) |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,(E,x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (E,x) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (E,x) |^ b₂ ) } is set
A is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x * is Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} is non empty Element of K6(K231(E))
(E,x) \/ {(<%> E)} is non empty Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
E is set
x is set
x ^omega is non empty V23() set
K6((x ^omega)) is non empty set
<%> x is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(x) V20() V32() V33() V51() Element of K231(x)
K231(x) is non empty V23() M9(x)
{(<%> x)} is non empty Element of K6(K231(x))
K6(K231(x)) is non empty set
A is Element of K6((x ^omega))
(x,A) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(x,A,1) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty Element of K6(K231(E))
K6(K231(E)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x) ? is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x ? is Element of K6((E ^omega))
(E,(x ?)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x ?) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x ?) |^ b₂ ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
{(<%> E)} \/ (E,x) is non empty Element of K6((E ^omega))
(x ?) * is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V8() V33() Element of E ^omega
n is V8() V33() Element of E ^omega
A ^ n is V8() V33() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
K6(K231(E)) is non empty set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
k + x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (k + x) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
n is Element of K6((E ^omega))
x ^^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is set
k is V8() V33() Element of E ^omega
a is V8() V33() Element of E ^omega
k ^ a is V8() V33() Element of K231(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x ^^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x |^ 2 is Element of K6(K231(E))
E is set
{E} is non empty set
x is set
x ^omega is non empty V23() set
K6((x ^omega)) is non empty set
<%> x is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(x) V20() V32() V33() V51() Element of K231(x)
K231(x) is non empty V23() M9(x)
A is Element of K6((x ^omega))
(x,A) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(x,A,1) is Element of K6((x ^omega))
{ b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((x ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x ^^ (E,x) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) ^^ x is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
x ^^ (E,x,1) is Element of K6(K231(E))
(E,x,1) ^^ x is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(x |^ A) ^^ (E,x) is Element of K6(K231(E))
(E,x) ^^ (x |^ A) is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ A) ^^ (E,x,1) is Element of K6(K231(E))
(E,x,1) ^^ (x |^ A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
(x |^ (A,n)) ^^ (E,x) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) ^^ (x |^ (A,n)) is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x |^ (A,n)) ^^ (E,x,1) is Element of K6(K231(E))
(E,x,1) ^^ (x |^ (A,n)) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
A ^^ (E,x) is Element of K6(K231(E))
K6(K231(E)) is non empty set
(E,x) ^^ A is Element of K6(K231(E))
x * is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x) ^^ (E,x) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,2) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (E,x) is Element of K6(K231(E))
(E,x,1) ^^ (E,x,1) is Element of K6(K231(E))
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(1 + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) ^^ (x |^ A) is Element of K6(K231(E))
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (x |^ A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x) ^^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,2) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b₂ & b₁ = x |^ b₂ ) } is set
x |^ 1 is Element of K6(K231(E))
(E,x) ^^ (x |^ 1) is Element of K6(K231(E))
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(1 + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
(E,x) ^^ (x |^ (A,n)) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (x |^ (A,n)) is Element of K6(K231(E))
1 + A is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(1 + A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 + A <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ n is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x ? is Element of K6((E ^omega))
(E,x) ^^ (x ?) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(x ?) ^^ (E,x) is Element of K6(K231(E))
x |^ (0,1) is Element of K6((E ^omega))
(E,x) ^^ (x |^ (0,1)) is Element of K6(K231(E))
(x |^ (0,1)) ^^ (E,x) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x ? is Element of K6((E ^omega))
(E,x) ^^ (x ?) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (x ?) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
x is Element of K6((E ^omega))
x ? is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
A \/ x is Element of K6((E ^omega))
(E,(A \/ x)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (A \/ x) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (A \/ x) |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
(E,(A \/ x),1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (A \/ x) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (A \/ x) |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ x is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ (A,n) is Element of K6((E ^omega))
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
x |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
(x *) ^^ (E,x) is Element of K6(K231(E))
(E,x) ^^ (x *) is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(x *) ^^ (E,x,1) is Element of K6(K231(E))
(E,x,1) ^^ (x *) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x) |^ A is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) |^ A is Element of K6(K231(E))
1 * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,(1 * A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 * A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 * A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,0) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b₂ & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V18( NAT ) V19(E) V20() V32() V33() V51() Element of K231(E)
{(<%> E)} is non empty Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x) |^ (A,n) is Element of K6((E ^omega))
x is set
k is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x) |^ k is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,k) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( k <= b₂ & b₁ = x |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,n) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x) ^^ (E,x,A) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (E,x,A) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,x,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x) ^^ (E,x,A) is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x,A) ^^ (E,x) is Element of K6(K231(E))
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,x,(A + 1)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A + 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,A) ^^ (E,x,1) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
x * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,x) ^^ (x *) is Element of K6(K231(E))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,x,1) ^^ (x *) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
A is Element of K6((E ^omega))
A * is Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,A) ^^ x is Element of K6(K231(E))
x ^^ (E,A) is Element of K6(K231(E))
(A *) ^^ (E,A) is Element of K6(K231(E))
(E,A) ^^ (A *) is Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
x /\ A is Element of K6((E ^omega))
(E,(x /\ A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x /\ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x /\ A) |^ b₂ ) } is set
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,x) /\ (E,A) is Element of K6((E ^omega))
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
(E,(x /\ A),1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (x /\ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (x /\ A) |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is Element of K6((E ^omega))
(E,x) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = x |^ b₂ ) } is set
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,x) \/ (E,A) is Element of K6((E ^omega))
x \/ A is Element of K6((E ^omega))
(E,(x \/ A)) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x \/ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = (x \/ A) |^ b₂ ) } is set
(E,x,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = x |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
(E,(x \/ A),1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (x \/ A) |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = (x \/ A) |^ b₂ ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
x is set
<%x%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
A is Element of K6((E ^omega))
(E,A) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( not b₂ <= 0 & b₁ = A |^ b₂ ) } is set
(E,A,1) is Element of K6((E ^omega))
{ b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set
union { b₁ where b₁ is Element of K6((E ^omega)) : ex b₂ being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b₂ & b₁ = A |^ b₂ ) } is set