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 V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() 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 V33() 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 V15() 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 V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
E is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
E + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B 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
n + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
E + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B - A is V11() ext-real V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
E + B 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
A + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A - E is V11() ext-real V32() set
E - E is V11() ext-real V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
E + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is set
E ^omega is non empty V23() set
A is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
B is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
A ^ B is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
B ^ A is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
len (A ^ B) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75((A ^ B)) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
len A is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75(A) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
len B is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75(B) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
(len A) + (len B) is V4() V5() V6() V10() V11() ext-real non negative V32() set
len (B ^ A) is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75((B ^ A)) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
len B is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75(B) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
len A is V4() V5() V6() V10() V11() ext-real non negative V32() Element of NAT
K75(A) is V4() V5() V6() V10() V11() ext-real non negative V32() V33() set
(len B) + (len A) is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V23() Element of K6((A ^omega))
n is V23() Element of K6((A ^omega))
B ^^ n is V23() Element of K6(K231(A))
E is set
<%E%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
n is V23() Element of K6((A ^omega))
B ^^ n is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
A is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
B ^ A is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(A)
{} ^ <%E%> is V8() V15() V18( NAT ) V20() V33() V51() set
<%E%> ^ {} is V8() V15() V18( NAT ) V20() V33() V51() set
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ n is V23() Element of K6(K231(A))
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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
E is set
<%E%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ n is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B * is V23() Element of K6(K231(A))
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
B |^ B is V23() Element of K6(K231(A))
(B |^ B) ^^ B is V23() Element of K6(K231(A))
A is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
x is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
A ^ x is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(A)
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
E is set
{E} is non empty V33() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ n is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ B is V23() Element of K6(K231(A))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ A is V23() Element of K6(K231(A))
(B |^ B) ^^ (B |^ A) is V23() Element of K6(K231(A))
x is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
kl is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
x ^ kl is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(A)
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ A is V23() Element of K6(K231(A))
(B |^ n) ^^ (B |^ A) is V23() Element of K6(K231(A))
x is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
kl is V8() V15() V18( NAT ) V20() V33() V51() Element of A ^omega
x ^ kl is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(A)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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 |^ B) |^ n is V23() Element of K6(K231(E))
A |^ n is V23() Element of K6(K231(E))
(A |^ n) |^ B is V23() Element of K6(K231(E))
B * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (B * n) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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 V23() Element of K6(K231(E))
(A |^ B) ^^ (A |^ n) is V23() Element of K6(K231(E))
(A |^ n) ^^ (A |^ B) is V23() Element of K6(K231(E))
B + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (B + n) is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ n is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B ^^ (A |^ n) is V23() Element of K6(K231(E))
(A |^ n) ^^ B is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
n is V23() Element of K6((E ^omega))
A ^^ n is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ B is V23() Element of K6(K231(E))
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ A is V23() Element of K6(K231(E))
B + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ (B + A) is V23() Element of K6(K231(E))
(B |^ B) ^^ (B |^ A) is V23() Element of K6(K231(E))
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V23() Element of K6((A ^omega))
B * is V23() Element of K6(K231(A))
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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
(A |^ B) * is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
(A |^ B) * is V23() Element of K6(K231(E))
(A *) |^ B is V23() Element of K6(K231(E))
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
B * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A ^^ (B *) is V23() Element of K6(K231(E))
(B *) ^^ A is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
B 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
A is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
K6(K6((E ^omega))) is non empty set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
B is Element of K6(K6((E ^omega)))
union B is V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is set
B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,B,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
A is set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ x is V23() 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
B |^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
x is V23() Element of K6((E ^omega))
K6(K6((E ^omega))) is non empty set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
kl is Element of K6(K6((E ^omega)))
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ mn is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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
A |^ n is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
A is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() 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
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
n is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
n is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
x is set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ kl is V23() 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
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,B,n) \/ (E,A,n,B) is V23() Element of K6((E ^omega))
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is V23() 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
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,(n + 1),B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,B,n) \/ (E,A,(n + 1),B) is V23() Element of K6((E ^omega))
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B + 0 is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B 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
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,B,(n + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
(E,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
A |^ (n + 1) is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
(E,A,B,n) \/ (A |^ (n + 1)) is V23() Element of K6(K231(E))
(E,A,(n + 1),(n + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n + 1 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
(E,A,B,n) \/ (E,A,(n + 1),(n + 1)) is V23() Element of K6((E ^omega))
{} \/ (A |^ (n + 1)) is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,(B + 1),n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(A |^ B) \/ (E,A,(B + 1),n) is V23() Element of K6((E ^omega))
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,B,B) \/ (E,A,(B + 1),n) is V23() Element of K6((E ^omega))
(A |^ B) \/ {} is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,B,(B + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 1 & b1 = A |^ b2 ) } is set
A |^ B is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
A |^ (B + 1) is V23() Element of K6(K231(E))
(A |^ B) \/ (A |^ (B + 1)) is V23() Element of K6(K231(E))
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,B,B) \/ (A |^ (B + 1)) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,B,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B |^ x is V23() Element of K6(K231(E))
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A,B,n,B) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
B |^ n is V23() Element of K6(K231(A))
A is set
B |^ B is V23() Element of K6(K231(A))
A 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is set
B is set
B is set
{(<%> E)} |^ B is V23() Element of K6(K231(E))
(E,{(<%> E)},B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = {(<%> E)} |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = {(<%> E)} |^ b2 ) } is set
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
{(<%> E)} |^ A is V23() Element of K6(K231(E))
(E,A,0,0) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
A |^ 0 is V23() Element of K6(K231(E))
B is set
(E,A,1,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() Element of K6(K231(E))
(E,A,0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,0,0) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(0 + 1),n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,0,0) \/ (E,A,(0 + 1),n) is V23() Element of K6((E ^omega))
A |^ 0 is V23() Element of K6(K231(E))
(A |^ 0) \/ (E,A,(0 + 1),n) is V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A |^ 0 is V23() Element of K6(K231(E))
(E,A,0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
A |^ B is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
A |^ n is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
A |^ B is V23() Element of K6(K231(E))
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,B,n) ^^ (A |^ B) is V23() Element of K6(K231(E))
(A |^ B) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
A is set
x is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
kl is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
x ^ kl is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ mn is V23() Element of K6(K231(E))
(A |^ mn) ^^ (A |^ B) is V23() Element of K6(K231(E))
(A |^ B) ^^ (A |^ mn) is V23() Element of K6(K231(E))
A is set
x is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
kl is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
x ^ kl is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ mn is V23() Element of K6(K231(E))
(A |^ B) ^^ (A |^ mn) is V23() Element of K6(K231(E))
(A |^ mn) ^^ (A |^ B) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A ^^ (E,A,B,n) is V23() Element of K6(K231(E))
A |^ 1 is V23() Element of K6(K231(E))
(E,A,B,n) ^^ (A |^ 1) is V23() Element of K6(K231(E))
(A |^ 1) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ (E,A,B,A) is V23() 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,A,(B + B),(n + A)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + B <= b2 & b2 <= n + A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + B <= b2 & b2 <= n + A & b1 = A |^ b2 ) } is set
x is set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ kl is V23() Element of K6(K231(E))
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
mn + a is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ mn is V23() Element of K6(K231(E))
A |^ a is V23() Element of K6(K231(E))
(A |^ mn) ^^ (A |^ a) is V23() Element of K6(K231(E))
A |^ (mn + a) is V23() Element of K6(K231(E))
x is set
kl is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
mn is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
kl ^ mn is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
a is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ a is V23() Element of K6(K231(E))
b is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ b is V23() Element of K6(K231(E))
b + a is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (b + a) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() 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
(E,A,(B + 1),(n + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + 1 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + 1 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
(E,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,1,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ (E,A,1,1) is V23() Element of K6(K231(E))
A |^ 1 is V23() Element of K6(K231(E))
(E,A,B,n) ^^ (A |^ 1) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ (E,A,B,A) is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,B,A) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
B + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
n + A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B + B),(n + A)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + B <= b2 & b2 <= n + A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + B <= b2 & b2 <= n + A & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * B),(n * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * B <= b2 & b2 <= n * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * B <= b2 & b2 <= n * B & b1 = A |^ b2 ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ A is V23() Element of K6(K231(E))
(E,A,(B * A),(n * A)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * A <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * A <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,B,n) |^ (A + 1) is V23() Element of K6(K231(E))
(E,A,(B * A),(n * A)) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
(B * A) + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(n * A) + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,((B * A) + B),((n * A) + n)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (B * A) + B <= b2 & b2 <= (n * A) + n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (B * A) + B <= b2 & b2 <= (n * A) + n & b1 = A |^ b2 ) } is set
B * (A + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * (A + 1) is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * (A + 1)),(n * (A + 1))) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * (A + 1) <= b2 & b2 <= n * (A + 1) & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * (A + 1) <= b2 & b2 <= n * (A + 1) & b1 = A |^ b2 ) } is set
(E,A,B,n) |^ 0 is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
A |^ 0 is V23() Element of K6(K231(E))
B * 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
n * 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
(E,A,(B * 0),(n * 0)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * 0 <= b2 & b2 <= n * 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * 0 <= b2 & b2 <= n * 0 & b1 = A |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
A |^ 0 is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ (B + 1) is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ B is V23() Element of K6(K231(E))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A |^ (B + 1)),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ (B + 1)) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ (B + 1)) |^ b2 ) } is set
(E,(A |^ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,(A |^ B),n,B) ^^ (E,A,n,B) is V23() Element of K6(K231(E))
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A |^ (B + 1)) |^ x is V23() Element of K6(K231(E))
A |^ x is V23() Element of K6(K231(E))
(E,(A |^ B),n,B) ^^ (A |^ x) is V23() Element of K6(K231(E))
(B + 1) * x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ ((B + 1) * x) is V23() Element of K6(K231(E))
B * x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(B * x) + x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ ((B * x) + x) is V23() Element of K6(K231(E))
A |^ (B * x) is V23() Element of K6(K231(E))
(A |^ (B * x)) ^^ (A |^ x) is V23() Element of K6(K231(E))
(A |^ B) |^ x is V23() Element of K6(K231(E))
((A |^ B) |^ x) ^^ (A |^ x) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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
B * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A |^ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
B * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * n),(B * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * n <= b2 & b2 <= B * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * n <= b2 & b2 <= B * B & b1 = A |^ b2 ) } is set
A 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
A * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ A is V23() Element of K6(K231(E))
(E,(A |^ A),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ A) |^ b2 ) } is set
(E,A,(A * n),(A * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b2 & b2 <= A * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( A * n <= b2 & b2 <= A * B & b1 = A |^ b2 ) } is set
A |^ 1 is V23() Element of K6(K231(E))
(E,(A |^ 1),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ 1) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ 1) |^ b2 ) } is set
(E,(A |^ A),n,B) ^^ (E,(A |^ 1),n,B) is V23() Element of K6(K231(E))
(E,A,(A * n),(A * B)) ^^ (E,(A |^ 1),n,B) is V23() Element of K6(K231(E))
A + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ (A + 1) is V23() Element of K6(K231(E))
(E,(A |^ (A + 1)),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ (A + 1)) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ (A + 1)) |^ b2 ) } is set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,(A |^ A),n,B) ^^ (E,A,n,B) is V23() Element of K6(K231(E))
(E,A,(A * n),(A * B)) ^^ (E,A,n,B) is V23() Element of K6(K231(E))
(A * n) + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A * B) + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,((A * n) + n),((A * B) + B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A * n) + n <= b2 & b2 <= (A * B) + B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A * n) + n <= b2 & b2 <= (A * B) + B & b1 = A |^ b2 ) } is set
(A + 1) * n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A + 1) * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,((A + 1) * n),((A + 1) * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + 1) * n <= b2 & b2 <= (A + 1) * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( (A + 1) * n <= b2 & b2 <= (A + 1) * B & b1 = A |^ b2 ) } is set
A |^ 0 is V23() Element of K6(K231(E))
(E,(A |^ 0),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ 0) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ 0) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
(E,{(<%> E)},n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = {(<%> E)} |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = {(<%> E)} |^ b2 ) } is set
0 * n is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
0 * B is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
(E,A,(0 * n),(0 * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 * n <= b2 & b2 <= 0 * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 * n <= b2 & b2 <= 0 * B & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A |^ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,n,B) |^ B is V23() Element of K6(K231(E))
n * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(n * B),(B * B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * B <= b2 & b2 <= B * B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n * B <= b2 & b2 <= B * B & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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
B + n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (B + n) is V23() Element of K6(K231(E))
A |^ n is V23() Element of K6(K231(E))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A |^ (B + n)),B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ (B + n)) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ (B + n)) |^ b2 ) } is set
(E,(A |^ B),B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ B) |^ b2 ) } is set
(E,(A |^ n),B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ n) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (A |^ n) |^ b2 ) } is set
(E,(A |^ B),B,A) ^^ (E,(A |^ n),B,A) is V23() Element of K6(K231(E))
x is set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A |^ (B + n)) |^ kl is V23() Element of K6(K231(E))
(B + n) * kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ ((B + n) * kl) is V23() Element of K6(K231(E))
B * kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(B * kl) + (n * kl) is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ ((B * kl) + (n * kl)) is V23() Element of K6(K231(E))
A |^ (B * kl) is V23() Element of K6(K231(E))
A |^ (n * kl) is V23() Element of K6(K231(E))
(A |^ (B * kl)) ^^ (A |^ (n * kl)) is V23() Element of K6(K231(E))
mn is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
a is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
mn ^ a is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
(A |^ n) |^ kl is V23() Element of K6(K231(E))
(A |^ B) |^ kl is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A,0,0) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
A |^ 0 is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
A |^ 0 is V23() Element of K6(K231(E))
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ (0 + 1) is V23() Element of K6(K231(E))
(A |^ 0) \/ (A |^ (0 + 1)) is V23() Element of K6(K231(E))
A |^ 1 is V23() Element of K6(K231(E))
{(<%> E)} \/ (A |^ 1) is non empty V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A,1,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
A |^ 1 is V23() 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
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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A,0,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
A ^^ A is V23() Element of K6(K231(E))
({(<%> E)} \/ A) \/ (A ^^ A) is non empty V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ (1 + 1) is V23() Element of K6(K231(E))
(E,A,0,1) \/ (A |^ (1 + 1)) is V23() Element of K6(K231(E))
({(<%> E)} \/ A) \/ (A |^ (1 + 1)) is non empty V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
(E,A,1,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
A ^^ A is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
A \/ (A ^^ A) is V23() Element of K6(K231(E))
A |^ 1 is V23() Element of K6(K231(E))
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ (1 + 1) is V23() Element of K6(K231(E))
(A |^ 1) \/ (A |^ (1 + 1)) is V23() Element of K6(K231(E))
A |^ 2 is V23() Element of K6(K231(E))
A \/ (A |^ 2) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A,2,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 2 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
A ^^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ 2 is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is set
{A} is non empty V33() set
B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,B,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ A is V23() 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
B |^ x is V23() Element of K6(K231(E))
x is set
E is set
{E} is non empty V33() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A,B,n,B) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B |^ n is V23() Element of K6(K231(A))
B |^ n is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B |^ B is V23() Element of K6(K231(A))
E is set
<%E%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A,B,n,B) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ A is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B |^ B is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
B |^ 1 is V23() Element of K6(K231(A))
K6(K231(A)) is non empty set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
A /\ B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A /\ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A /\ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A /\ B) |^ b2 ) } is set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,B,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
(E,A,n,B) /\ (E,B,n,B) is V23() Element of K6((E ^omega))
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A /\ B) |^ x is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ x is V23() Element of K6(K231(E))
B |^ x is V23() Element of K6(K231(E))
(A |^ x) /\ (B |^ x) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
A \/ B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,B,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = B |^ b2 ) } is set
(E,A,n,B) \/ (E,B,n,B) is V23() Element of K6((E ^omega))
(E,(A \/ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A \/ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A \/ B) |^ b2 ) } is set
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B |^ x is V23() Element of K6(K231(E))
(A |^ x) \/ (B |^ x) is V23() Element of K6(K231(E))
(A \/ B) |^ x is V23() Element of K6(K231(E))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ x is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A |^ x is V23() Element of K6(K231(E))
(A |^ x) \/ (B |^ x) is V23() Element of K6(K231(E))
(A \/ B) |^ x is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B * B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(E,A,B,n),B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (E,A,B,n) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (E,A,B,n) |^ b2 ) } is set
n * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * B),(n * A)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * B <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * B <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
x is set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ kl is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B * kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * kl),(n * kl)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * kl <= b2 & b2 <= n * kl & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * kl <= b2 & b2 <= n * kl & b1 = A |^ b2 ) } 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
B ^^ (E,A,n,B) is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
(E,A,n,B) ^^ B is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
n is V23() Element of K6((E ^omega))
A ^^ n is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,B,B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = B |^ b2 ) } is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + x is V4() V5() V6() V10() V11() ext-real non negative V32() set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,B,x,kl) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b2 & b2 <= kl & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( x <= b2 & b2 <= kl & b1 = B |^ b2 ) } is set
A + kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,B,(B + x),(A + kl)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + x <= b2 & b2 <= A + kl & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B + x <= b2 & b2 <= A + kl & b1 = B |^ b2 ) } is set
mn is set
a is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
b is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
a ^ b is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
(E,B,B,A) ^^ (E,B,x,kl) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) * is V23() Element of K6(K231(E))
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ A is V23() Element of K6(K231(E))
B * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
n * A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,(B * A),(n * A)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * A <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B * A <= b2 & b2 <= n * A & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,(A *),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
B is set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A *) |^ A is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,(A *),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
(A *) |^ n is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) * is V23() Element of K6(K231(E))
A |^ n is V23() Element of K6(K231(E))
(A |^ n) * is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) * is V23() Element of K6(K231(E))
(E,(A *),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (A *) |^ b2 ) } is set
A |^ n is V23() Element of K6(K231(E))
(A |^ n) * is V23() Element of K6(K231(E))
(A *) |^ n is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
B * is V23() 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
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ x is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
B * is V23() 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
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
B \/ (E,A,n,B) is V23() Element of K6((E ^omega))
(B \/ (E,A,n,B)) * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) ^^ (A *) is V23() Element of K6(K231(E))
(A *) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
B is set
A is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
x is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
A ^ x is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ kl is V23() Element of K6(K231(E))
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ mn is V23() Element of K6(K231(E))
(A |^ mn) ^^ (A |^ kl) is V23() Element of K6(K231(E))
mn + kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (mn + kl) is V23() Element of K6(K231(E))
B is set
A is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
x is V8() V15() V18( NAT ) V20() V33() V51() Element of E ^omega
A ^ x is V8() V15() V18( NAT ) V20() V33() V51() Element of K231(E)
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ kl is V23() Element of K6(K231(E))
mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ mn is V23() Element of K6(K231(E))
(A |^ kl) ^^ (A |^ mn) is V23() Element of K6(K231(E))
kl + mn is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (kl + mn) is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(A *) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,(B + B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + B & b1 = A |^ b2 ) } is set
(A *) ^^ (E,A,B,(B + B)) is V23() Element of K6(K231(E))
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
B + (B + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,B,(B + (B + 1))) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + (B + 1) & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + (B + 1) & b1 = A |^ b2 ) } is set
(B + B) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
A |^ ((B + B) + 1) is V23() Element of K6(K231(E))
(E,A,B,(B + B)) \/ (A |^ ((B + B) + 1)) is V23() Element of K6(K231(E))
(A *) ^^ (E,A,B,(B + (B + 1))) is V23() Element of K6(K231(E))
(A *) ^^ (A |^ ((B + B) + 1)) is V23() Element of K6(K231(E))
(A *) \/ ((A *) ^^ (A |^ ((B + B) + 1))) is V23() Element of K6(K231(E))
(A *) \/ (A *) is V23() Element of K6(K231(E))
A |^ B is V23() Element of K6(K231(E))
(A *) ^^ (A |^ B) is V23() Element of K6(K231(E))
B + 0 is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,(B + 0)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 0 & b1 = A |^ b2 ) } is set
(A *) ^^ (E,A,B,(B + 0)) is V23() Element of K6(K231(E))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(A |^ B),n,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( n <= b2 & b2 <= B & b1 = (A |^ B) |^ b2 ) } is set
A is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
(A |^ B) |^ x is V23() Element of K6(K231(E))
B * x is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ (B * x) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
B 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
A is V23() Element of K6((E ^omega))
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(A |^ B) * is V23() Element of K6(K231(E))
(E,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A,B,n) * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(E,A,B,n),B,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (E,A,B,n) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= A & b1 = (E,A,B,n) |^ b2 ) } is set
x is set
kl is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) |^ kl is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
A |^ n is V23() 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
A is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
K6(K6((E ^omega))) is non empty set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
B is Element of K6(K6((E ^omega)))
union B is V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is set
B is V23() Element of K6((E ^omega))
(E,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
n is set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ B is V23() 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
B |^ n is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V23() Element of K6((E ^omega))
K6(K6((E ^omega))) is non empty set
{ b1 where b1 is V23() Element of K6((E ^omega)) : S1[b1] } is set
A is Element of K6(K6((E ^omega)))
x is V4() V5() V6() V10() V11() ext-real non negative V32() set
B |^ x is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() 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
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A |^ 0 is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
A |^ 1 is V23() Element of K6(K231(E))
(A |^ 0) \/ (A |^ 1) is V23() Element of K6(K231(E))
B is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ n is V23() Element of K6(K231(E))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ n is V23() Element of K6(K231(E))
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ n is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
A |^ 0 is V23() Element of K6(K231(E))
A |^ 1 is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
(A,B) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
{(<%> A)} \/ B is non empty V23() Element of K6((A ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
K231(E) is non empty V23() M9(E)
A |^ 0 is V23() Element of K6(K231(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 |^ (0 + 1) is V23() Element of K6(K231(E))
(A |^ 0) \/ (A |^ (0 + 1)) is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,(E,A)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,B,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
E is set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
{(<%> A)} is non empty V23() V33() V37() Element of K6(K231(A))
K6(K231(A)) is non empty set
B is V23() Element of K6((A ^omega))
(A,B) is non empty V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(A,B,0,1) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,(A *)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A *) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A *) |^ b2 ) } is set
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A) * is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} \/ (A *) is non empty V23() Element of K6(K231(E))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
({(<%> E)} \/ A) * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
A /\ B is V23() Element of K6((E ^omega))
(E,(A /\ B)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A /\ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A /\ B) |^ b2 ) } is set
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(E,A) /\ (E,B) is V23() Element of K6((E ^omega))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ (A /\ B) is non empty V23() Element of K6((E ^omega))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
{(<%> E)} \/ B is non empty V23() Element of K6((E ^omega))
({(<%> E)} \/ A) /\ ({(<%> E)} \/ B) is V23() Element of K6((E ^omega))
(E,A) /\ ({(<%> E)} \/ B) is V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(E,A) \/ (E,B) is non empty V23() Element of K6((E ^omega))
A \/ B is V23() Element of K6((E ^omega))
(E,(A \/ B)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A \/ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A \/ B) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ (A \/ B) is non empty V23() Element of K6((E ^omega))
A \/ {(<%> E)} is non empty V23() Element of K6(K231(E))
B \/ {(<%> E)} is non empty V23() Element of K6(K231(E))
(A \/ {(<%> E)}) \/ (B \/ {(<%> E)}) is non empty V23() Element of K6(K231(E))
(E,A) \/ (B \/ {(<%> E)}) is non empty V23() Element of K6(K231(E))
E is set
{E} is non empty V33() set
A is set
A ^omega is non empty V23() set
K6((A ^omega)) is non empty set
<%> A is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(A) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(A)
K231(A) is non empty V23() M9(A)
B is V23() Element of K6((A ^omega))
(A,B) is non empty V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(A,B,0,1) is V23() Element of K6((A ^omega))
{ b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((A ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is set
<%A%> is non empty V8() V15() V18( NAT ) V20() V33() V40(1) V51() set
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(E,B,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = B |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A) ^^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
A ^^ (E,A) is V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A) ^^ A is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,1,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(0 + 1),(1 + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= 1 + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= 1 + 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A) ^^ (E,A) is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,0,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = A |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
0 + 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(0 + 0),(1 + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 0 <= b2 & b2 <= 1 + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 0 <= b2 & b2 <= 1 + 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A) |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,(E,A),0,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = (E,A) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A) |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,0,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
n is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A) |^ n is V23() Element of K6(K231(E))
(E,A,0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
n + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A) |^ (n + 1) is V23() Element of K6(K231(E))
(E,A) |^ 1 is V23() Element of K6(K231(E))
((E,A) |^ n) ^^ ((E,A) |^ 1) is V23() Element of K6(K231(E))
(E,A,0,n) ^^ (E,A) is V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,n) ^^ (E,A,0,1) is V23() Element of K6(K231(E))
0 + 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V20() V21() V22() V23() V32() V33() V34() V37() V51() set
(E,A,(0 + 0),(n + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 0 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 0 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
(E,A,0,(n + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n + 1 & b1 = A |^ b2 ) } is set
(E,A) |^ 0 is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
(E,A,0,0) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B 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,(E,A),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
(E,(E,A),0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,(E,A),0,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = (E,A) |^ b2 ) } is set
(E,A,0,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A) |^ B is V23() 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
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B 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,(E,A),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
(E,A,0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,(E,A),0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A,1,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,(E,A,1,B)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A,1,B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A,1,B) |^ b2 ) } is set
(E,A,0,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ (E,A,1,B) is non empty V23() Element of K6((E ^omega))
(E,A,0,0) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 0 & b1 = A |^ b2 ) } is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(0 + 1),B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + 1 <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,0,0) \/ (E,A,(0 + 1),B) is V23() Element of K6((E ^omega))
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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
A ^^ B is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
B ^^ A is V23() Element of K6(K231(E))
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
A ^^ (E,B) is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,B) ^^ A is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
(E,B,0,2) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 2 & b1 = B |^ b2 ) } is set
n is V23() Element of K6((E ^omega))
A ^^ n is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,B) ^^ (E,B) is V23() 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) ^^ (A |^ B) is V23() Element of K6(K231(E))
(A |^ B) ^^ (E,A) is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
({(<%> E)} \/ A) ^^ (A |^ B) is V23() Element of K6(K231(E))
{(<%> E)} ^^ (A |^ B) is V23() Element of K6(K231(E))
A ^^ (A |^ B) is V23() Element of K6(K231(E))
({(<%> E)} ^^ (A |^ B)) \/ (A ^^ (A |^ B)) is V23() Element of K6(K231(E))
(A |^ B) ^^ A is V23() Element of K6(K231(E))
({(<%> E)} ^^ (A |^ B)) \/ ((A |^ B) ^^ A) is V23() Element of K6(K231(E))
(A |^ B) \/ ((A |^ B) ^^ A) is V23() Element of K6(K231(E))
(A |^ B) ^^ {(<%> E)} is V23() Element of K6(K231(E))
((A |^ B) ^^ {(<%> E)}) \/ ((A |^ B) ^^ A) is V23() Element of K6(K231(E))
A \/ {(<%> E)} is non empty V23() Element of K6(K231(E))
(A |^ B) ^^ (A \/ {(<%> E)}) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
B * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
B * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B \/ (E,A) is non empty V23() Element of K6((E ^omega))
(B \/ (E,A)) * is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) ^^ (A *) is V23() Element of K6(K231(E))
(A *) ^^ (E,A) is V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) ^^ (A *) is V23() Element of K6(K231(E))
(A *) ^^ (E,A,0,1) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) ^^ (A *) is V23() Element of K6(K231(E))
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
({(<%> E)} \/ A) ^^ (A *) is V23() Element of K6(K231(E))
{(<%> E)} ^^ (A *) is V23() Element of K6(K231(E))
A ^^ (A *) is V23() Element of K6(K231(E))
({(<%> E)} ^^ (A *)) \/ (A ^^ (A *)) is V23() Element of K6(K231(E))
(A *) \/ (A ^^ (A *)) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
(E,A) |^ B is V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) |^ B is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
(E,(A |^ B)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A |^ B) |^ b2 ) } is set
(E,(A |^ B),0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = (A |^ B) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = (A |^ B) |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,A) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A,B,n) ^^ (E,A) is V23() Element of K6(K231(E))
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) ^^ (E,A,B,n) is V23() Element of K6(K231(E))
(E,A,B,n) ^^ (E,A,0,1) is V23() Element of K6(K231(E))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V4() V5() V6() V10() V11() ext-real non negative V32() set
A |^ B is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
(E,A) ^^ (A |^ B) is V23() Element of K6(K231(E))
B + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,B,(B + 1)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B + 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = A |^ b2 ) } is set
(E,A,0,1) ^^ (A |^ B) is V23() Element of K6(K231(E))
(E,A,B,B) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= B & b1 = A |^ b2 ) } is set
(E,A,0,1) ^^ (E,A,B,B) is V23() Element of K6(K231(E))
0 + B is V4() V5() V6() V10() V11() ext-real non negative V32() set
1 + B is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() set
(E,A,(0 + B),(1 + B)) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + B <= b2 & b2 <= 1 + B & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 + B <= b2 & b2 <= 1 + B & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,(E,A),B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = (E,A) |^ b2 ) } is set
(E,A,0,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
A * is V23() Element of K6(K231(E))
K231(E) is non empty V23() M9(E)
K6(K231(E)) is non empty set
B 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,A,B,n) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( B <= b2 & b2 <= n & b1 = A |^ b2 ) } is set
(E,(E,A,B,n)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A,B,n) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (E,A,B,n) |^ b2 ) } is set
(E,(E,A,B,n),0,1) is V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = (E,A,B,n) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( 0 <= b2 & b2 <= 1 & b1 = (E,A,B,n) |^ b2 ) } 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() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
A \ {(<%> E)} is V23() Element of K6((E ^omega))
(E,(A \ {(<%> E)})) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A \ {(<%> E)}) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (A \ {(<%> E)}) |^ b2 ) } is set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
{(<%> E)} \/ (A \ {(<%> E)}) is non empty V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
(E,A) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = A |^ b2 ) } is set
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ A is non empty V23() Element of K6((E ^omega))
E is set
E ^omega is non empty V23() set
K6((E ^omega)) is non empty set
A is V23() Element of K6((E ^omega))
B is V23() Element of K6((E ^omega))
(E,B) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = B |^ b2 ) } is set
B \/ A is V23() Element of K6((E ^omega))
(E,(B \/ A)) is non empty V23() Element of K6((E ^omega))
{ b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (B \/ A) |^ b2 ) } is set
union { b1 where b1 is V23() Element of K6((E ^omega)) : ex b2 being V4() V5() V6() V10() V11() ext-real non negative V32() set st
( b2 <= 1 & b1 = (B \/ A) |^ b2 ) } is set
<%> E is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative V15() V16() V17() V18( NAT ) V19(E) V20() V21() V22() V23() V32() V33() V34() V37() V51() Element of K231(E)
K231(E) is non empty V23() M9(E)
{(<%> E)} is non empty V23() V33() V37() Element of K6(K231(E))
K6(K231(E)) is non empty set
{(<%> E)} \/ (B \/ A) is non empty V23() Element of K6((E ^omega))
{(<%> E)} \/ B is non empty V23() Element of K6((E ^omega))
({(<%> E)} \/ B) \/ A is non empty V23() Element of K6((E ^omega))
(E,B) \/ A is non empty V23() Element of K6((E ^omega))