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

( A <= b

union { b

( A <= b

K6(K6((E ^omega))) is non empty set

{ b

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

( n <= b

union { b

( n <= b

x is set

{ b

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

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

( A <= b

union { b

( A <= b

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

( A <= b

union { b

( A <= b

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

( 0 <= b

union { b

( 0 <= b

{(<%> 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

( A <= b

union { b

( A <= b

n is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,x,n) is Element of K6((E ^omega))

{ b

( n <= b

union { b

( n <= b

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

( A <= b

union { b

( A <= b

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

( A <= b

union { b

( A <= b

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

( n + 1 <= b

union { b

( n + 1 <= b

(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

( A + 1 <= b

union { b

( A + 1 <= b

(x |^ A) \/ (E,x,(A + 1)) is Element of K6((E ^omega))

(E,x,A) is Element of K6((E ^omega))

{ b

( A <= b

union { b

( A <= b

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

( A <= b

union { b

( A <= b

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

( A <= b

union { b

( A <= b

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

( A <= b

union { b

( A <= b

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

( A + 1 <= b

union { b

( A + 1 <= b

(x |^ (0,A)) \/ (E,x,(A + 1)) is Element of K6((E ^omega))

(E,x,0) is Element of K6((E ^omega))

{ b

( 0 <= b

union { b

( 0 <= b

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

( n <= b

union { b

( n <= b

(E,A,n) is Element of K6((E ^omega))

{ b

( n <= b

union { b

( n <= b

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

( n <= b

union { b

( n <= b

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

( A <= b

union { b

( A <= b

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

( A + 1 <= b

union { b

( A + 1 <= b

(E,x,A) is Element of K6((E ^omega))

{ b

( A <= b

union { b

( A <= b

(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

( A <= b

union { b

( A <= b

(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

( A <= b

union { b

( A <= b

n is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,x,n) is Element of K6((E ^omega))

{ b

( n <= b

union { b

( n <= b

(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

( A + n <= b

union { b

( A + n <= b

x is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,x,x) is Element of K6((E ^omega))

{ b

( x <= b

union { b

( x <= b

(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

( A + x <= b

union { b

( A + x <= b

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

( x + 1 <= b

union { b

( x + 1 <= b

(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

( (A + x) + 1 <= b

union { b

( (A + x) + 1 <= b

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

( A + (x + 1) <= b

union { b

( A + (x + 1) <= b

(E,x,0) is Element of K6((E ^omega))

{ b

( 0 <= b

union { b

( 0 <= b

(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

( A + 0 <= b

union { b

( A + 0 <= b

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

( n <= b

union { b

( n <= b

(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

( n * A <= b

union { b

( n * A <= b

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

( n * x <= b

union { b

( n * x <= b

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

( n * (x + 1) <= b

union { b

( n * (x + 1) <= b

(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

( (n * x) + n <= b

union { b

( (n * x) + n <= b

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

( n * (x + 1) <= b

union { b

( n * (x + 1) <= b

(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

( n * (x + 1) <= b

union { b

( n * (x + 1) <= b

(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

( n * (x + 1) <= b

union { b

( n * (x + 1) <= b

(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

( n * 0 <= b

union { b

( n * 0 <= b

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

( A <= b

union { b

( A <= b

(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

( A * x <= b

union { b

( A * x <= b

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

( x <= b

union { b

( x <= b

k is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,A,k) is Element of K6((E ^omega))

{ b

( k <= b

union { b

( k <= b

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

( x + k <= b

union { b

( x + k <= b

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

( A <= b

union { b

( A <= b

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

( A + n <= b

union { b

( A + n <= b

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

( A + x <= b

union { b

( A + x <= b

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

( A + (x + 1) <= b

union { b

( A + (x + 1) <= b

(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

( (A + x) + 1 <= b

union { b

( (A + x) + 1 <= b

((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

( A + 0 <= b

union { b

( A + 0 <= b

<%> 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

( A <= b

union { b

( A <= b

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

( n <= b

union { b

( n <= b

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

( n + 1 <= b

union { b

( n + 1 <= b

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

( 0 <= b

union { b

( 0 <= b

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

( n <= b

union { b

( n <= b

(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

( x <= b

union { b

( x <= b

(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

( k <= b

union { b

( k <= b

(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

( k + 1 <= b

union { b

( k + 1 <= b

(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

( 0 <= b

union { b

( 0 <= b

(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

( n <= b

union { b

( n <= b

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

( A <= b

union { b

( A <= b

n is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,x,n) is Element of K6((E ^omega))

{ b

( n <= b

union { b

( n <= b

(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

( A + n <= b

union { b

( A + n <= b

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

( n <= b

union { b

( n <= b

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

( n + n <= b

union { b

( n + n <= b

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

( n <= b

union { b

( n <= b

x is V4() V5() V6() V10() V11() ext-real non negative V32() set

(E,x,x) is Element of K6((E ^omega))

{ b

( x <= b

union { b

( x <= b

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

( 1 <= b

union { b

( 1 <= b

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

( A <= b

union { b

( A <= b

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

( n <= b

union { b

( n <= b

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

( n + 1 <= b

union { b

( n + 1 <= b

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

( 0 <= b

union { b

( 0 <= b

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

( A <= b

union { b

( A <= b

(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

( 0 <= b

union { b

( 0 <= b

(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

( x <= b

union { b

( x <= b

(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

( x + A <= b

union { b

( x + A <= b

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

b ^ c

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

( A <= b

union { b

( A <= b

(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

( A <= b

union { b

( A <= b

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

( 0 <= b

union { b

( 0 <= b

(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

( 0 + A <= b

union { b

( 0 + A <= b

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