:: BCIALG_5 semantic presentation

REAL is non empty V33() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (n + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
n is Element of the carrier of i
j \ m is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
m \ n is Element of the carrier of i
j \ n is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
m \ j is Element of the carrier of i
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of j is non empty set
m is Element of the carrier of j
n is Element of the carrier of j
m \ n is Element of the carrier of j
(m,n) to_power (i + 1) is Element of the carrier of j
(m,n) to_power i is Element of the carrier of j
((m,n) to_power i) \ n is Element of the carrier of j
(((m,n) to_power i) \ n) \ ((m,n) to_power i) is Element of the carrier of j
((m,n) to_power i) \ ((m,n) to_power i) is Element of the carrier of j
(((m,n) to_power i) \ ((m,n) to_power i)) \ n is Element of the carrier of j
n ` is Element of the carrier of j
0. j is V49(j) minimal positive V92(j) Element of the carrier of j
(0. j) \ n is Element of the carrier of j
(m \ n) \ m is Element of the carrier of j
m \ m is Element of the carrier of j
(m \ m) \ n is Element of the carrier of j
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of j is non empty set
0. j is V49(j) minimal positive V92(j) Element of the carrier of j
m is Element of the carrier of j
((0. j),m) to_power i is Element of the carrier of j
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
((0. j),m) to_power n is Element of the carrier of j
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
((0. j),m) to_power (n + 1) is Element of the carrier of j
m ` is Element of the carrier of j
(0. j) \ m is Element of the carrier of j
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
((0. j),m) to_power n is Element of the carrier of j
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
((0. j),m) to_power (n + 1) is Element of the carrier of j
((0. j),m) to_power 0 is Element of the carrier of j
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of m is non empty set
n is Element of the carrier of m
X is Element of the carrier of m
(n,X) to_power i is Element of the carrier of m
(n,X) to_power j is Element of the carrier of m
i - j is V11() V12() ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n,X) to_power X is Element of the carrier of m
((n,X) to_power X) \ n is Element of the carrier of m
n \ n is Element of the carrier of m
((n \ n),X) to_power X is Element of the carrier of m
0. m is V49(m) minimal positive V92(m) Element of the carrier of m
((0. m),X) to_power X is Element of the carrier of m
(((n,X) to_power X),X) to_power j is Element of the carrier of m
X + j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n,X) to_power (X + j) is Element of the carrier of m
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of m is non empty set
n is Element of the carrier of m
X is Element of the carrier of m
(n,X) to_power j is Element of the carrier of m
(n,X) to_power i is Element of the carrier of m
i - j is V11() V12() ext-real Element of REAL
j - j is V11() V12() ext-real Element of REAL
1 + j is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i - j) + j is V11() V12() ext-real Element of REAL
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n,X) to_power (j + 1) is Element of the carrier of m
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n,X) to_power X is Element of the carrier of m
X - j is V11() V12() ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(((n,X) to_power j),X) to_power x is Element of the carrier of m
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(((n,X) to_power j),X) to_power y is Element of the carrier of m
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(((n,X) to_power j),X) to_power (y + 1) is Element of the carrier of m
((((n,X) to_power j),X) to_power y) \ X is Element of the carrier of m
((n,X) to_power j) \ X is Element of the carrier of m
((((n,X) to_power j) \ X),X) to_power y is Element of the carrier of m
(((n,X) to_power (j + 1)),X) to_power y is Element of the carrier of m
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(((n,X) to_power j),X) to_power y is Element of the carrier of m
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(((n,X) to_power j),X) to_power (y + 1) is Element of the carrier of m
(((n,X) to_power j),X) to_power 0 is Element of the carrier of m
j + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n,X) to_power (j + x) is Element of the carrier of m
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n,X) to_power X is Element of the carrier of m
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,0) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,0) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
((i,j,m,0,0),(j \ m)) to_power n is Element of the carrier of i
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n,X) is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (n + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i
((((i,j,m,0,0),(j \ m)) to_power n),(m \ j)) to_power X is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
((j \ (j \ m)),(j \ m)) to_power n is Element of the carrier of i
(j,(j \ m)) to_power n is Element of the carrier of i
((j,(j \ m)) to_power n) \ (j \ m) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,(n + 1),X) is Element of the carrier of i
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power ((n + 1) + 1)),(m \ j)) to_power X is Element of the carrier of i
(i,j,m,n,X) is Element of the carrier of i
(j,(j \ m)) to_power (n + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i
(i,j,m,n,X) \ (j \ m) is Element of the carrier of i
(j,(m \ j)) to_power X is Element of the carrier of i
(((j,(m \ j)) to_power X),(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i
(((j,(m \ j)) to_power X),(j \ m)) to_power (n + 1) is Element of the carrier of i
((((j,(m \ j)) to_power X),(j \ m)) to_power (n + 1)) \ (j \ m) is Element of the carrier of i
((((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X) \ (j \ m) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
m \ j is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,j,m,n,(X + 1)) is Element of the carrier of i
j \ m is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (n + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power (X + 1) is Element of the carrier of i
(i,j,m,n,X) is Element of the carrier of i
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i
(i,j,m,n,X) \ (m \ j) is Element of the carrier of i
K7(NAT, the carrier of i) is set
K6(K7(NAT, the carrier of i)) is set
X is V21() V30( NAT , the carrier of i) Element of K6(K7(NAT, the carrier of i))
X . (X + 1) is Element of the carrier of i
X . 0 is Element of the carrier of i
x is V21() V30( NAT , the carrier of i) Element of K6(K7(NAT, the carrier of i))
x . X is Element of the carrier of i
x . 0 is Element of the carrier of i
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X . y is Element of the carrier of i
x . y is Element of the carrier of i
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X . (y + 1) is Element of the carrier of i
(X . y) \ (m \ j) is Element of the carrier of i
x . (y + 1) is Element of the carrier of i
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X . y is Element of the carrier of i
x . y is Element of the carrier of i
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X . (y + 1) is Element of the carrier of i
x . (y + 1) is Element of the carrier of i
X . X is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,j,m,(n + 1),(n + 1)) is Element of the carrier of i
j \ m is Element of the carrier of i
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power ((n + 1) + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i
(i,m,j,n,(n + 1)) is Element of the carrier of i
(m,(m \ j)) to_power (n + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (n + 1)),(j \ m)) to_power (n + 1) is Element of the carrier of i
(j \ m) \ (j \ m) is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ m is Element of the carrier of i
((j \ (j \ m)),(m \ j)) to_power (n + 1) is Element of the carrier of i
((((j \ (j \ m)),(m \ j)) to_power (n + 1)),(j \ m)) to_power (n + 1) is Element of the carrier of i
((j \ (j \ m)),(j \ m)) to_power (n + 1) is Element of the carrier of i
((((j \ (j \ m)),(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(j \ m)) to_power (n + 1) is Element of the carrier of i
(((((j,(j \ m)) to_power 1),(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,j,m,n,(n + 1)) is Element of the carrier of i
j \ m is Element of the carrier of i
(j,(j \ m)) to_power (n + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i
(i,m,j,n,n) is Element of the carrier of i
(m,(m \ j)) to_power (n + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (n + 1)),(j \ m)) to_power n is Element of the carrier of i
(j \ m) \ (j \ m) is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ m is Element of the carrier of i
((j \ (j \ m)),(j \ m)) to_power n is Element of the carrier of i
(m,(j \ m)) to_power n is Element of the carrier of i
((((j \ (j \ m)),(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i
(((m,(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(j \ m)) to_power n is Element of the carrier of i
(((((j,(j \ m)) to_power 1),(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i
BCI-EXAMPLE is non empty V47() V48() 1 -element strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple alternative commutative BCI-commutative BCI-weakly-commutative V99() Iseki_extension BCK-positive-implicative BCK-implicative BCIStr_0
the carrier of BCI-EXAMPLE is non empty V2() V33() set
i is Element of the carrier of BCI-EXAMPLE
j is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,i,j,0,0) is Element of the carrier of BCI-EXAMPLE
i \ j is Element of the carrier of BCI-EXAMPLE
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,(i \ j)) to_power (0 + 1) is Element of the carrier of BCI-EXAMPLE
j \ i is Element of the carrier of BCI-EXAMPLE
(((i,(i \ j)) to_power (0 + 1)),(j \ i)) to_power 0 is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,j,i,0,0) is Element of the carrier of BCI-EXAMPLE
(j,(j \ i)) to_power (0 + 1) is Element of the carrier of BCI-EXAMPLE
(((j,(j \ i)) to_power (0 + 1)),(i \ j)) to_power 0 is Element of the carrier of BCI-EXAMPLE
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of BCI-EXAMPLE is non empty V2() V33() set
X is Element of the carrier of BCI-EXAMPLE
X is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,X,X,i,j) is Element of the carrier of BCI-EXAMPLE
X \ X is Element of the carrier of BCI-EXAMPLE
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (i + 1) is Element of the carrier of BCI-EXAMPLE
X \ X is Element of the carrier of BCI-EXAMPLE
(((X,(X \ X)) to_power (i + 1)),(X \ X)) to_power j is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,X,X,m,n) is Element of the carrier of BCI-EXAMPLE
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (m + 1) is Element of the carrier of BCI-EXAMPLE
(((X,(X \ X)) to_power (m + 1)),(X \ X)) to_power n is Element of the carrier of BCI-EXAMPLE
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of i is non empty set
X is Element of the carrier of i
x is Element of the carrier of i
(i,X,x,n,X) is Element of the carrier of i
X \ x is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (n + 1) is Element of the carrier of i
x \ X is Element of the carrier of i
(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power X is Element of the carrier of i
(i,x,X,j,m) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (j + 1) is Element of the carrier of i
(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power m is Element of the carrier of i
the carrier of i is non empty set
x is Element of the carrier of i
X is Element of the carrier of i
(i,x,X,n,X) is Element of the carrier of i
x \ X is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (n + 1) is Element of the carrier of i
X \ x is Element of the carrier of i
(((x,(x \ X)) to_power (n + 1)),(X \ x)) to_power X is Element of the carrier of i
(i,X,x,j,m) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (j + 1) is Element of the carrier of i
(((X,(X \ x)) to_power (j + 1)),(x \ X)) to_power m is Element of the carrier of i
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,(i + X),j) is Element of the carrier of X
x \ y is Element of the carrier of X
(i + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power ((i + X) + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power ((i + X) + 1)),(y \ x)) to_power j is Element of the carrier of X
(X,y,x,m,(n + X)) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + X) is Element of the carrier of X
(X,y,x,m,n) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X
((X,y,x,m,n),(x \ y)) to_power X is Element of the carrier of X
(X,x,y,i,j) is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X
((X,x,y,i,j),(x \ y)) to_power X is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X is Element of the carrier of X
(((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X),(y \ x)) to_power j is Element of the carrier of X
(i + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power ((i + 1) + X) is Element of the carrier of X
(((x,(x \ y)) to_power ((i + 1) + X)),(y \ x)) to_power j is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,i,(j + X)) is Element of the carrier of X
x \ y is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + X) is Element of the carrier of X
(X,y,x,(m + X),n) is Element of the carrier of X
(m + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power ((m + X) + 1) is Element of the carrier of X
(((y,(y \ x)) to_power ((m + X) + 1)),(x \ y)) to_power n is Element of the carrier of X
(X,y,x,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X
((X,y,x,m,n),(y \ x)) to_power X is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X is Element of the carrier of X
(((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X),(x \ y)) to_power n is Element of the carrier of X
(m + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power ((m + 1) + X) is Element of the carrier of X
(((y,(y \ x)) to_power ((m + 1) + X)),(x \ y)) to_power n is Element of the carrier of X
(X,x,y,i,j) is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X
((X,x,y,i,j),(y \ x)) to_power X is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of BCI-EXAMPLE is non empty V2() V33() set
X is Element of the carrier of BCI-EXAMPLE
X is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,X,X,i,j) is Element of the carrier of BCI-EXAMPLE
X \ X is Element of the carrier of BCI-EXAMPLE
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (i + 1) is Element of the carrier of BCI-EXAMPLE
X \ X is Element of the carrier of BCI-EXAMPLE
(((X,(X \ X)) to_power (i + 1)),(X \ X)) to_power j is Element of the carrier of BCI-EXAMPLE
(BCI-EXAMPLE,X,X,m,n) is Element of the carrier of BCI-EXAMPLE
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (m + 1) is Element of the carrier of BCI-EXAMPLE
(((X,(X \ X)) to_power (m + 1)),(X \ X)) to_power n is Element of the carrier of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of i is non empty set
X is Element of the carrier of i
x is Element of the carrier of i
(i,X,x,n,X) is Element of the carrier of i
X \ x is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (n + 1) is Element of the carrier of i
x \ X is Element of the carrier of i
(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power X is Element of the carrier of i
(i,x,X,j,m) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (j + 1) is Element of the carrier of i
(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power m is Element of the carrier of i
the carrier of i is non empty set
x is Element of the carrier of i
X is Element of the carrier of i
(i,x,X,n,X) is Element of the carrier of i
x \ X is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (n + 1) is Element of the carrier of i
X \ x is Element of the carrier of i
(((x,(x \ X)) to_power (n + 1)),(X \ x)) to_power X is Element of the carrier of i
(i,X,x,j,m) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (j + 1) is Element of the carrier of i
(((X,(X \ x)) to_power (j + 1)),(x \ X)) to_power m is Element of the carrier of i
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,(i + X),j) is Element of the carrier of X
x \ y is Element of the carrier of X
(i + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power ((i + X) + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power ((i + X) + 1)),(y \ x)) to_power j is Element of the carrier of X
(X,y,x,m,(n + X)) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + X) is Element of the carrier of X
(X,y,x,m,n) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X
((X,y,x,m,n),(x \ y)) to_power X is Element of the carrier of X
(X,x,y,i,j) is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X
((X,x,y,i,j),(x \ y)) to_power X is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X is Element of the carrier of X
(((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X),(y \ x)) to_power j is Element of the carrier of X
(i + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power ((i + 1) + X) is Element of the carrier of X
(((x,(x \ y)) to_power ((i + 1) + X)),(y \ x)) to_power j is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,i,(j + X)) is Element of the carrier of X
x \ y is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + X) is Element of the carrier of X
(X,y,x,(m + X),n) is Element of the carrier of X
(m + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power ((m + X) + 1) is Element of the carrier of X
(((y,(y \ x)) to_power ((m + X) + 1)),(x \ y)) to_power n is Element of the carrier of X
(X,y,x,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X
((X,y,x,m,n),(y \ x)) to_power X is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X is Element of the carrier of X
(((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X),(x \ y)) to_power n is Element of the carrier of X
(m + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power ((m + 1) + X) is Element of the carrier of X
(((y,(y \ x)) to_power ((m + 1) + X)),(x \ y)) to_power n is Element of the carrier of X
(X,x,y,i,j) is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X
((X,x,y,i,j),(y \ x)) to_power X is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,x) to_power (i + 1) is Element of the carrier of X
(X,x) to_power (n + 1) is Element of the carrier of X
X \ x is Element of the carrier of X
(X \ x) \ X is Element of the carrier of X
X \ X is Element of the carrier of X
(X \ X) \ x is Element of the carrier of X
x ` is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(0. X) \ x is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x),X,(m + 1),n) is Element of the carrier of X
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
((X \ x),((X \ x) \ X)) to_power ((m + 1) + 1) is Element of the carrier of X
X \ (X \ x) is Element of the carrier of X
((((X \ x),((X \ x) \ X)) to_power ((m + 1) + 1)),(X \ (X \ x))) to_power n is Element of the carrier of X
((X \ x),(X \ (X \ x))) to_power n is Element of the carrier of X
X \ (X \ (X \ x)) is Element of the carrier of X
((X \ (X \ (X \ x))),(X \ (X \ x))) to_power n is Element of the carrier of X
(X,(X \ (X \ x))) to_power 1 is Element of the carrier of X
(((X,(X \ (X \ x))) to_power 1),(X \ (X \ x))) to_power n is Element of the carrier of X
(X,(X \ (X \ x))) to_power (n + 1) is Element of the carrier of X
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,X,(X \ x),i,(j + 1)) is Element of the carrier of X
(X,(X \ (X \ x))) to_power (i + 1) is Element of the carrier of X
(((X,(X \ (X \ x))) to_power (i + 1)),((X \ x) \ X)) to_power (j + 1) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,x) to_power (j + 1) is Element of the carrier of X
(X,x) to_power (m + 1) is Element of the carrier of X
X \ x is Element of the carrier of X
(X \ x) \ X is Element of the carrier of X
X \ X is Element of the carrier of X
(X \ X) \ x is Element of the carrier of X
x ` is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(0. X) \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x),X,(i + 1),j) is Element of the carrier of X
(i + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
((X \ x),((X \ x) \ X)) to_power ((i + 1) + 1) is Element of the carrier of X
X \ (X \ x) is Element of the carrier of X
((((X \ x),((X \ x) \ X)) to_power ((i + 1) + 1)),(X \ (X \ x))) to_power j is Element of the carrier of X
((X \ x),(X \ (X \ x))) to_power j is Element of the carrier of X
X \ (X \ (X \ x)) is Element of the carrier of X
((X \ (X \ (X \ x))),(X \ (X \ x))) to_power j is Element of the carrier of X
(X,(X \ (X \ x))) to_power 1 is Element of the carrier of X
(((X,(X \ (X \ x))) to_power 1),(X \ (X \ x))) to_power j is Element of the carrier of X
(X,(X \ (X \ x))) to_power (j + 1) is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,X,(X \ x),m,(n + 1)) is Element of the carrier of X
(X,(X \ (X \ x))) to_power (m + 1) is Element of the carrier of X
(((X,(X \ (X \ x))) to_power (m + 1)),((X \ x) \ X)) to_power (n + 1) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
X \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,j,n) is Element of the carrier of X
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (j + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power n is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,n,j) is Element of the carrier of X
X \ x is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (n + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,i) is Element of the carrier of X
X \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X
(X,x,X,i,i) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power i is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power n is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
x is Element of the carrier of X
X is Element of the carrier of X
(X,x,X,i,i) is Element of the carrier of X
x \ X is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
X \ x is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power i is Element of the carrier of X
(X,X,x,i,i) is Element of the carrier of X
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X
(X,X,x,i,i) \ (X,x,X,i,i) is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(X,x,X,i,i) \ (X,X,x,i,i) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
n - i is V11() V12() ext-real Element of REAL
i - i is V11() V12() ext-real Element of REAL
1 + i is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n - i) + i is V11() V12() ext-real Element of REAL
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j - i is V11() V12() ext-real Element of REAL
(j - i) + i is V11() V12() ext-real Element of REAL
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,(i + 1)) is Element of the carrier of X
X \ x is Element of the carrier of X
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (i + 1) is Element of the carrier of X
(X,x,X,i,(i + 1)) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (n + 1) is Element of the carrier of X
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (n + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (n + 1) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,i) is Element of the carrier of X
X \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X
(X,x,X,i,j) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X
(i,i,i,j) is ext-real set
min (i,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
min ((min (i,i)),(min (i,j))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
j - m is V11() V12() ext-real Element of REAL
m - m is V11() V12() ext-real Element of REAL
1 + m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j - m) + m is V11() V12() ext-real Element of REAL
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,(m + 1)) is Element of the carrier of X
X \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (m + 1) is Element of the carrier of X
(X,x,X,m,i) is Element of the carrier of X
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power i is Element of the carrier of X
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,X,x,i,j) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (j + 1) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,i)
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,i,j) is Element of the carrier of X
x \ y is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X
(X,y,x,j,i) is Element of the carrier of X
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (j + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (j + 1)),(x \ y)) to_power i is Element of the carrier of X
(X,y,x,m,i) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power i is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
x is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
X - j is V11() V12() ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X - n is V11() V12() ext-real Element of REAL
t1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + t1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,j,m,n) is ext-real set
max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
X - n is V11() V12() ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X - j is V11() V12() ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
X \ x is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,i,j) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power n is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
x is Element of the carrier of X
X is Element of the carrier of X
(X,x,X,i,j) is Element of the carrier of X
x \ X is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
X \ x is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,X,x,i,j) \ (X,x,X,i,j) is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(X,x,X,i,j) \ (X,X,x,i,j) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
n - i is V11() V12() ext-real Element of REAL
i - i is V11() V12() ext-real Element of REAL
1 + i is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n - i) + i is V11() V12() ext-real Element of REAL
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
X \ x is Element of the carrier of X
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,i,(i + 1)) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,x,X,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power (n + 1) is Element of the carrier of X
(x,(x \ X)) to_power (n + 1) is Element of the carrier of X
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of i is non empty set
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
X is Element of the carrier of i
(0. i) \ X is Element of the carrier of i
(m + n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,X) to_power ((m + n) + 1) is Element of the carrier of i
(((X,X) to_power ((m + n) + 1)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
(X,X) to_power (m + n) is Element of the carrier of i
((X,X) to_power (m + n)) \ X is Element of the carrier of i
((((X,X) to_power (m + n)) \ X),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
X \ X is Element of the carrier of i
((X \ X),X) to_power (m + n) is Element of the carrier of i
((((X \ X),X) to_power (m + n)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
((0. i),X) to_power (m + n) is Element of the carrier of i
((((0. i),X) to_power (m + n)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
((0. i),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
((((0. i),((0. i) \ X)) to_power (j + n)),X) to_power (m + n) is Element of the carrier of i
((0. i),(0. i)) to_power (j + n) is Element of the carrier of i
((0. i),X) to_power (j + n) is Element of the carrier of i
(((0. i),(0. i)) to_power (j + n)) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i
(((((0. i),(0. i)) to_power (j + n)) \ (((0. i),X) to_power (j + n))),X) to_power (m + n) is Element of the carrier of i
(0. i) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i
(((0. i) \ (((0. i),X) to_power (j + n))),X) to_power (m + n) is Element of the carrier of i
(((0. i),X) to_power (m + n)) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i
((0. i),X) to_power m is Element of the carrier of i
((((0. i),X) to_power m),X) to_power n is Element of the carrier of i
(((((0. i),X) to_power m),X) to_power n) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i
((0. i),X) to_power j is Element of the carrier of i
((((0. i),X) to_power j),X) to_power n is Element of the carrier of i
(((((0. i),X) to_power m),X) to_power n) \ (((((0. i),X) to_power j),X) to_power n) is Element of the carrier of i
(((0. i),X) to_power m) \ (((0. i),X) to_power j) is Element of the carrier of i
(i,(0. i),X,j,m) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
((0. i),((0. i) \ X)) to_power (j + 1) is Element of the carrier of i
X \ (0. i) is Element of the carrier of i
((((0. i),((0. i) \ X)) to_power (j + 1)),(X \ (0. i))) to_power m is Element of the carrier of i
(i,X,(0. i),(m + n),(j + n)) is Element of the carrier of i
(X,(X \ (0. i))) to_power ((m + n) + 1) is Element of the carrier of i
(((X,(X \ (0. i))) to_power ((m + n) + 1)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i
((((0. i),((0. i) \ X)) to_power (j + 1)),X) to_power m is Element of the carrier of i
((((0. i),X) to_power m),((0. i) \ X)) to_power (j + 1) is Element of the carrier of i
((0. i),(0. i)) to_power (j + 1) is Element of the carrier of i
((0. i),X) to_power (j + 1) is Element of the carrier of i
(((0. i),(0. i)) to_power (j + 1)) \ (((0. i),X) to_power (j + 1)) is Element of the carrier of i
(((((0. i),(0. i)) to_power (j + 1)) \ (((0. i),X) to_power (j + 1))),X) to_power m is Element of the carrier of i
(0. i) \ (((0. i),X) to_power (j + 1)) is Element of the carrier of i
(((0. i) \ (((0. i),X) to_power (j + 1))),X) to_power m is Element of the carrier of i
(((0. i),X) to_power m) \ (((0. i),X) to_power (j + 1)) is Element of the carrier of i
((((0. i),X) to_power m) \ (((0. i),X) to_power (j + 1))) \ ((((0. i),X) to_power m) \ (((0. i),X) to_power j)) is Element of the carrier of i
(((0. i),X) to_power j) \ (((0. i),X) to_power (j + 1)) is Element of the carrier of i
(0. i) \ ((((0. i),X) to_power j) \ (((0. i),X) to_power (j + 1))) is Element of the carrier of i
(((0. i),X) to_power j) \ X is Element of the carrier of i
(((0. i),X) to_power j) \ ((((0. i),X) to_power j) \ X) is Element of the carrier of i
(((0. i) \ X),X) to_power j is Element of the carrier of i
(((0. i),X) to_power j) \ ((((0. i) \ X),X) to_power j) is Element of the carrier of i
(0. i) \ ((0. i) \ X) is Element of the carrier of i
(0. i) \ ((0. i) \ ((0. i) \ X)) is Element of the carrier of i
X is Element of the carrier of i
X ` is Element of the carrier of i
(0. i) \ X is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of j is non empty set
m is Element of the carrier of j
n is Element of the carrier of j
(j,m,n,0,0) is Element of the carrier of j
m \ n is Element of the carrier of j
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ n)) to_power (0 + 1) is Element of the carrier of j
n \ m is Element of the carrier of j
(((m,(m \ n)) to_power (0 + 1)),(n \ m)) to_power 0 is Element of the carrier of j
(j,n,m,0,0) is Element of the carrier of j
(n,(n \ m)) to_power (0 + 1) is Element of the carrier of j
(((n,(n \ m)) to_power (0 + 1)),(m \ n)) to_power 0 is Element of the carrier of j
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,0) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 0 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
m \ j is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(i,j,m,0,0) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
K6( the carrier of i) is set
j is non empty Element of K6( the carrier of i)
m is non empty Element of K6( the carrier of i)
j /\ m is Element of K6( the carrier of i)
n is non empty being_B being_C being_I being_BCI-4 BCIStr_0
BCK-part n is non empty Element of K6( the carrier of n)
the carrier of n is non empty set
K6( the carrier of n) is set
0. n is V49(n) minimal positive V92(n) Element of the carrier of n
{ b₁ where b₁ is Element of the carrier of n : 0. n <= b₁ } is set
AtomSet n is non empty Element of K6( the carrier of n)
{ b₁ where b₁ is Element of the carrier of n : b₁ is minimal } is set
{(0. n)} is set
X is set
X is Element of the carrier of n
(0. n) \ X is Element of the carrier of n
x is Element of the carrier of n
x is Element of the carrier of n
X is set
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
K6( the carrier of i) is set
j is non empty Element of K6( the carrier of i)
m is non empty being_B being_C being_I being_BCI-4 BCIStr_0
AtomSet m is non empty Element of K6( the carrier of m)
the carrier of m is non empty set
K6( the carrier of m) is set
{ b₁ where b₁ is Element of the carrier of m : b₁ is minimal } is set
0. m is V49(m) minimal positive V92(m) Element of the carrier of m
{(0. m)} is set
n is set
X is Element of the carrier of m
(0. m) \ X is Element of the carrier of m
X ` is Element of the carrier of m
X is Element of the carrier of m
n is set
n is Element of the carrier of m
(0. m) \ n is Element of the carrier of m
n is Element of the carrier of m
n ` is Element of the carrier of m
(0. m) \ n is Element of the carrier of m
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
K6( the carrier of i) is set
j is non empty Element of K6( the carrier of i)
m is non empty being_B being_C being_I being_BCI-4 BCIStr_0
BCK-part m is non empty Element of K6( the carrier of m)
the carrier of m is non empty set
K6( the carrier of m) is set
0. m is V49(m) minimal positive V92(m) Element of the carrier of m
{ b₁ where b₁ is Element of the carrier of m : 0. m <= b₁ } is set
{(0. m)} is set
n is set
X is Element of the carrier of m
X ` is Element of the carrier of m
(0. m) \ X is Element of the carrier of m
(X `) ` is Element of the carrier of m
(0. m) \ (X `) is Element of the carrier of m
(0. m) ` is Element of the carrier of m
(0. m) \ (0. m) is Element of the carrier of m
X is Element of the carrier of m
n is set
X is Element of the carrier of m
X ` is Element of the carrier of m
(0. m) \ X is Element of the carrier of m
n is Element of the carrier of m
n ` is Element of the carrier of m
(0. m) \ n is Element of the carrier of m
(n `) ` is Element of the carrier of m
(0. m) \ (n `) is Element of the carrier of m
(0. m) \ ((0. m) \ n) is Element of the carrier of m
n \ ((0. m) \ ((0. m) \ n)) is Element of the carrier of m
(0. m) \ (n \ ((0. m) \ ((0. m) \ n))) is Element of the carrier of m
((0. m),(n \ ((0. m) \ ((0. m) \ n)))) to_power 1 is Element of the carrier of m
((0. m),n) to_power 1 is Element of the carrier of m
((0. m),((0. m) \ ((0. m) \ n))) to_power 1 is Element of the carrier of m
(((0. m),n) to_power 1) \ (((0. m),((0. m) \ ((0. m) \ n))) to_power 1) is Element of the carrier of m
(((0. m),n) to_power 1) \ (((0. m),n) to_power 1) is Element of the carrier of m
((0. m) \ ((0. m) \ n)) \ n is Element of the carrier of m
((0. m) \ n) \ ((0. m) \ n) is Element of the carrier of m
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
((j \ (j \ m)),(m \ j)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n + m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
the carrier of i is non empty set
X is Element of the carrier of i
X is Element of the carrier of i
(i,X,X,j,j) is Element of the carrier of i
X \ X is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (j + 1) is Element of the carrier of i
X \ X is Element of the carrier of i
(((X,(X \ X)) to_power (j + 1)),(X \ X)) to_power j is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,X,X,x,x) is Element of the carrier of i
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (x + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power x is Element of the carrier of i
(i,X,X,(x + 1),(x + 1)) is Element of the carrier of i
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((x + 1) + 1)),(X \ X)) to_power (x + 1) is Element of the carrier of i
(i,X,X,x,(x + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power (x + 1) is Element of the carrier of i
(i,X,X,x,(x + 1)) \ (X \ X) is Element of the carrier of i
(i,X,X,x,x) \ (X \ X) is Element of the carrier of i
((i,X,X,x,x) \ (X \ X)) \ (X \ X) is Element of the carrier of i
X \ (X \ X) is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,X,X,x,x) is Element of the carrier of i
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (x + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power x is Element of the carrier of i
(i,X,X,(x + 1),(x + 1)) is Element of the carrier of i
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((x + 1) + 1)),(X \ X)) to_power (x + 1) is Element of the carrier of i
(i,X,X,0,0) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (0 + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (0 + 1)),(X \ X)) to_power 0 is Element of the carrier of i
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X is Element of the carrier of i
X is Element of the carrier of i
(i,X,X,n,(n + 1)) is Element of the carrier of i
X \ X is Element of the carrier of i
(X,(X \ X)) to_power (n + 1) is Element of the carrier of i
X \ X is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power (n + 1) is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,x,(x + 1)) is Element of the carrier of i
(X,(X \ X)) to_power (x + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power (x + 1) is Element of the carrier of i
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,(x + 1),((x + 1) + 1)) is Element of the carrier of i
(X,(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((x + 1) + 1)),(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(i,X,X,x,((x + 1) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(i,X,X,x,((x + 1) + 1)) \ (X \ X) is Element of the carrier of i
(i,X,X,x,(x + 1)) \ (X \ X) is Element of the carrier of i
((i,X,X,x,(x + 1)) \ (X \ X)) \ (X \ X) is Element of the carrier of i
X \ (X \ X) is Element of the carrier of i
(X \ (X \ X)) \ (X \ X) is Element of the carrier of i
X \ (X \ X) is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,x,(x + 1)) is Element of the carrier of i
(X,(X \ X)) to_power (x + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (x + 1)),(X \ X)) to_power (x + 1) is Element of the carrier of i
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,(x + 1),((x + 1) + 1)) is Element of the carrier of i
(X,(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((x + 1) + 1)),(X \ X)) to_power ((x + 1) + 1) is Element of the carrier of i
(i,X,X,0,1) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power (0 + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (0 + 1)),(X \ X)) to_power 1 is Element of the carrier of i
(i,X,X,0,0) is Element of the carrier of i
(((X,(X \ X)) to_power (0 + 1)),(X \ X)) to_power 0 is Element of the carrier of i
(i,X,X,0,0) \ (X \ X) is Element of the carrier of i
(i,X,X,0,(0 + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (0 + 1)),(X \ X)) to_power (0 + 1) is Element of the carrier of i
X is Element of the carrier of i
X is Element of the carrier of i
(i,X,X,(j + m),j) is Element of the carrier of i
X \ X is Element of the carrier of i
(j + m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + m) + 1) is Element of the carrier of i
X \ X is Element of the carrier of i
(((X,(X \ X)) to_power ((j + m) + 1)),(X \ X)) to_power j is Element of the carrier of i
(i,X,X,n,((n + m) + 1)) is Element of the carrier of i
(X,(X \ X)) to_power (n + 1) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + m) + 1) is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,X,X,(j + x),j) is Element of the carrier of i
(j + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + x) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((j + x) + 1)),(X \ X)) to_power j is Element of the carrier of i
n + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,((n + x) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + x) + 1) is Element of the carrier of i
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,(j + (x + 1)),j) is Element of the carrier of i
(j + (x + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + (x + 1)) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((j + (x + 1)) + 1)),(X \ X)) to_power j is Element of the carrier of i
(i,X,X,n,((n + x) + 1)) \ (X \ X) is Element of the carrier of i
((n + x) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,(((n + x) + 1) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power (((n + x) + 1) + 1) is Element of the carrier of i
n + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n + (x + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,((n + (x + 1)) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + (x + 1)) + 1) is Element of the carrier of i
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,X,X,(j + x),j) is Element of the carrier of i
(j + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + x) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((j + x) + 1)),(X \ X)) to_power j is Element of the carrier of i
n + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,((n + x) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + x) + 1) is Element of the carrier of i
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,(j + (x + 1)),j) is Element of the carrier of i
(j + (x + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + (x + 1)) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((j + (x + 1)) + 1)),(X \ X)) to_power j is Element of the carrier of i
n + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n + (x + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,((n + (x + 1)) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + (x + 1)) + 1) is Element of the carrier of i
j + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(i,X,X,(j + 0),j) is Element of the carrier of i
(j + 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ X)) to_power ((j + 0) + 1) is Element of the carrier of i
(((X,(X \ X)) to_power ((j + 0) + 1)),(X \ X)) to_power j is Element of the carrier of i
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
(n + 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i,X,X,n,((n + 0) + 1)) is Element of the carrier of i
(((X,(X \ X)) to_power (n + 1)),(X \ X)) to_power ((n + 0) + 1) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
j ` is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
(0. i) \ j is Element of the carrier of i
(j `) ` is Element of the carrier of i
(0. i) \ (j `) is Element of the carrier of i
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,1,0) is Element of the carrier of i
j \ m is Element of the carrier of i
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (1 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (1 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (j \ m) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(j,(j \ m)) to_power 2 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,1,1) is Element of the carrier of i
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ j)) to_power (1 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (1 + 1)),(j \ m)) to_power 1 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(m \ (m \ j)) \ (m \ j) is Element of the carrier of i
((m \ (m \ j)) \ (m \ j)) \ (j \ m) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
((j,(j \ m)) to_power 1) \ (m \ j) is Element of the carrier of i
(((m \ (m \ j)) \ (m \ j)),(j \ m)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 2 is Element of the carrier of i
(((m,(m \ j)) to_power 2),(j \ m)) to_power 1 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,1,1) is Element of the carrier of i
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ j)) to_power (1 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (1 + 1)),(j \ m)) to_power 1 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(m \ (m \ j)) \ (m \ j) is Element of the carrier of i
((m \ (m \ j)) \ (m \ j)) \ (j \ m) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
((j,(j \ m)) to_power 1) \ (m \ j) is Element of the carrier of i
(((m \ (m \ j)) \ (m \ j)),(j \ m)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 2 is Element of the carrier of i
(((m,(m \ j)) to_power 2),(j \ m)) to_power 1 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
((j \ (j \ m)),(m \ j)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
((j \ (j \ m)),(m \ j)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
j \ m is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,0,1) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 1 is Element of the carrier of i
(j \ m) \ (j \ m) is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ m is Element of the carrier of i
(j \ (j \ m)) \ (j \ m) is Element of the carrier of i
m \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
(m \ (j \ m)) \ (m \ j) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(m \ (m \ j)) \ (j \ m) is Element of the carrier of i
(m \ j) \ (m \ j) is Element of the carrier of i
(m \ (m \ j)) \ j is Element of the carrier of i
(m \ (m \ j)) \ (m \ j) is Element of the carrier of i
j \ (m \ j) is Element of the carrier of i
(j \ (m \ j)) \ (j \ m) is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
(((j,(j \ m)) to_power 1),(m \ j)) to_power 1 is Element of the carrier of i
((j,(j \ m)) to_power 1) \ (m \ j) is Element of the carrier of i
((m \ (m \ j)),(j \ m)) to_power 1 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 1 is Element of the carrier of i
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
(j \ m) \ m is Element of the carrier of i
(i,j,(j \ m),0,1) is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ (j \ m))) to_power (0 + 1) is Element of the carrier of i
(j \ m) \ j is Element of the carrier of i
(((j,(j \ (j \ m))) to_power (0 + 1)),((j \ m) \ j)) to_power 1 is Element of the carrier of i
(i,(j \ m),j,0,1) is Element of the carrier of i
((j \ m),((j \ m) \ j)) to_power (0 + 1) is Element of the carrier of i
((((j \ m),((j \ m) \ j)) to_power (0 + 1)),(j \ (j \ m))) to_power 1 is Element of the carrier of i
j \ j is Element of the carrier of i
(j \ j) \ m is Element of the carrier of i
m ` is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
(0. i) \ m is Element of the carrier of i
(j \ m) \ ((j \ m) \ j) is Element of the carrier of i
((j \ m) \ ((j \ m) \ j)) \ (j \ (j \ m)) is Element of the carrier of i
(j \ m) \ (j \ (j \ m)) is Element of the carrier of i
j \ (j \ (j \ m)) is Element of the carrier of i
(j \ (j \ (j \ m))) \ m is Element of the carrier of i
(j \ (j \ (j \ m))) \ ((j \ m) \ j) is Element of the carrier of i
(j,(j \ (j \ m))) to_power 1 is Element of the carrier of i
((j,(j \ (j \ m))) to_power 1) \ ((j \ m) \ j) is Element of the carrier of i
((j \ m),((j \ m) \ j)) to_power 1 is Element of the carrier of i
((((j \ m),((j \ m) \ j)) to_power 1),(j \ (j \ m))) to_power 1 is Element of the carrier of i
(((j \ m) \ ((j \ m) \ j)),(j \ (j \ m))) to_power 1 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
(i,j,m,1,0) is Element of the carrier of i
j \ m is Element of the carrier of i
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (1 + 1) is Element of the carrier of i
m \ j is Element of the carrier of i
(((j,(j \ m)) to_power (1 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (j \ m) is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(j,(j \ m)) to_power 2 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(j \ (j \ m)) \ (j \ m) is Element of the carrier of i
m \ j is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
(i,j,m,1,0) is Element of the carrier of i
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (1 + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (1 + 1)),(m \ j)) to_power 0 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
(j,(j \ m)) to_power 2 is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
i is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
i is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the carrier of i is non empty set
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
(j \ m) \ m is Element of the carrier of i
(j \ m) \ j is Element of the carrier of i
j \ j is Element of the carrier of i
(j \ j) \ m is Element of the carrier of i
m ` is Element of the carrier of i
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
(0. i) \ m is Element of the carrier of i
(j \ m) \ ((j \ m) \ j) is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
((j \ m) \ ((j \ m) \ j)) \ (j \ (j \ m)) is Element of the carrier of i
(j \ m) \ (j \ (j \ m)) is Element of the carrier of i
j \ (j \ (j \ m)) is Element of the carrier of i
(j \ (j \ (j \ m))) \ m is Element of the carrier of i
(j \ (j \ (j \ m))) \ ((j \ m) \ j) is Element of the carrier of i
(i,j,(j \ m),0,1) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ (j \ m))) to_power (0 + 1) is Element of the carrier of i
(((j,(j \ (j \ m))) to_power (0 + 1)),((j \ m) \ j)) to_power 1 is Element of the carrier of i
(i,(j \ m),j,0,1) is Element of the carrier of i
((j \ m),((j \ m) \ j)) to_power (0 + 1) is Element of the carrier of i
((((j \ m),((j \ m) \ j)) to_power (0 + 1)),(j \ (j \ m))) to_power 1 is Element of the carrier of i
(j,(j \ (j \ m))) to_power 1 is Element of the carrier of i
((j,(j \ (j \ m))) to_power 1) \ ((j \ m) \ j) is Element of the carrier of i
((j \ m),((j \ m) \ j)) to_power 1 is Element of the carrier of i
((((j \ m),((j \ m) \ j)) to_power 1),(j \ (j \ m))) to_power 1 is Element of the carrier of i
(((j \ m) \ ((j \ m) \ j)),(j \ (j \ m))) to_power 1 is Element of the carrier of i
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
(j \ m) \ m is Element of the carrier of i
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
i + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the carrier of j is non empty set
m is Element of the carrier of j
n is Element of the carrier of j
(m,n) to_power (i + 1) is Element of the carrier of j
(m,n) to_power (i + 2) is Element of the carrier of j
m \ n is Element of the carrier of j
(m \ n) \ m is Element of the carrier of j
m \ m is Element of the carrier of j
(m \ m) \ n is Element of the carrier of j
n ` is Element of the carrier of j
0. j is V49(j) minimal positive V92(j) Element of the carrier of j
(0. j) \ n is Element of the carrier of j
m \ (m \ n) is Element of the carrier of j
(m,(m \ (m \ n))) to_power (i + 1) is Element of the carrier of j
(((m,(m \ (m \ n))) to_power (i + 1)),((m \ n) \ m)) to_power (i + 1) is Element of the carrier of j
(((m,n) to_power (i + 1)),(0. j)) to_power (i + 1) is Element of the carrier of j
((m \ n),((m \ n) \ m)) to_power (i + 1) is Element of the carrier of j
((((m \ n),((m \ n) \ m)) to_power (i + 1)),(m \ (m \ n))) to_power (i + 1) is Element of the carrier of j
((m \ n),(m \ (m \ n))) to_power (i + 1) is Element of the carrier of j
((m,(m \ (m \ n))) to_power (i + 1)) \ n is Element of the carrier of j
((m,n) to_power (i + 1)) \ n is Element of the carrier of j
(i + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,n) to_power ((i + 1) + 1) is Element of the carrier of j
(j,m,(m \ n),i,(i + 1)) is Element of the carrier of j
(j,(m \ n),m,i,(i + 1)) is Element of the carrier of j
m is Element of the carrier of j
n is Element of the carrier of j
(m,n) to_power (i + 1) is Element of the carrier of j
(m,n) to_power (i + 2) is Element of the carrier of j
m is Element of the carrier of j
n is Element of the carrier of j
(j,m,n,i,(i + 1)) is Element of the carrier of j
m \ n is Element of the carrier of j
(m,(m \ n)) to_power (i + 1) is Element of the carrier of j
n \ m is Element of the carrier of j
(((m,(m \ n)) to_power (i + 1)),(n \ m)) to_power (i + 1) is Element of the carrier of j
(j,n,m,i,(i + 1)) is Element of the carrier of j
(n,(n \ m)) to_power (i + 1) is Element of the carrier of j
(((n,(n \ m)) to_power (i + 1)),(m \ n)) to_power (i + 1) is Element of the carrier of j
(m \ n) \ (m \ n) is Element of the carrier of j
0. j is V49(j) minimal positive V92(j) Element of the carrier of j
m \ (m \ n) is Element of the carrier of j
(m \ (m \ n)) \ n is Element of the carrier of j
((m \ (m \ n)),(m \ n)) to_power (i + 1) is Element of the carrier of j
(n,(m \ n)) to_power (i + 1) is Element of the carrier of j
(m,(m \ n)) to_power 1 is Element of the carrier of j
(((m,(m \ n)) to_power 1),(m \ n)) to_power (i + 1) is Element of the carrier of j
1 + (i + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m,(m \ n)) to_power (1 + (i + 1)) is Element of the carrier of j
(n \ m) \ (n \ m) is Element of the carrier of j
n \ (n \ m) is Element of the carrier of j
(n \ (n \ m)) \ m is Element of the carrier of j
((n \ (n \ m)),(n \ m)) to_power (i + 1) is Element of the carrier of j
(m,(n \ m)) to_power (i + 1) is Element of the carrier of j
(n,(n \ m)) to_power 1 is Element of the carrier of j
(((n,(n \ m)) to_power 1),(n \ m)) to_power (i + 1) is Element of the carrier of j
(n,(n \ m)) to_power (1 + (i + 1)) is Element of the carrier of j
(n,(n \ m)) to_power (i + 2) is Element of the carrier of j
(((m,(n \ m)) to_power (i + 1)),(m \ n)) to_power (i + 1) is Element of the carrier of j
(m,(m \ n)) to_power (i + 2) is Element of the carrier of j
(((n,(m \ n)) to_power (i + 1)),(n \ m)) to_power (i + 1) is Element of the carrier of j
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of i is non empty set
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
m is Element of the carrier of i
j is Element of the carrier of i
m \ j is Element of the carrier of i
j \ m is Element of the carrier of i
j \ (j \ m) is Element of the carrier of i
(i,j,m,0,1) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i
(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 1 is Element of the carrier of i
(i,m,j,0,0) is Element of the carrier of i
(m,(m \ j)) to_power (0 + 1) is Element of the carrier of i
(((m,(m \ j)) to_power (0 + 1)),(j \ m)) to_power 0 is Element of the carrier of i
(j,(j \ m)) to_power 1 is Element of the carrier of i
((j,(j \ m)) to_power 1) \ (m \ j) is Element of the carrier of i
(m,(m \ j)) to_power 1 is Element of the carrier of i
(((m,(m \ j)) to_power 1),(j \ m)) to_power 0 is Element of the carrier of i
(j \ (j \ m)) \ (m \ j) is Element of the carrier of i
(j \ (j \ m)) \ (0. i) is Element of the carrier of i
m \ (0. i) is Element of the carrier of i
j is Element of the carrier of i
m is Element of the carrier of i
j \ m is Element of the carrier of i
m \ j is Element of the carrier of i
m \ (m \ j) is Element of the carrier of i
i is non empty being_B being_C being_I being_BCI-4 BCIStr_0
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
the carrier of i is non empty set
0. i is V49(i) minimal positive V92(i) Element of the carrier of i
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
n is Element of the carrier of i
X is Element of the carrier of i
n \ X is Element of the carrier of i
X \ n is Element of the carrier of i
(X,(X \ n)) to_power (m + 1) is Element of the carrier of i
(X,(X \ n)) to_power 1 is Element of the carrier of i
((0. i),(X \ n)) to_power 1 is Element of the carrier of i
((0. i),X) to_power 1 is Element of the carrier of i
((0. i),n) to_power 1 is Element of the carrier of i
(((0. i),X) to_power 1) \ (((0. i),n) to_power 1) is Element of the carrier of i
(0. i) \ (X \ n) is Element of the carrier of i
(0. i) \ X is Element of the carrier of i
((0. i) \ X) \ (((0. i),n) to_power 1) is Element of the carrier of i
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ n)) to_power (X + 1) is Element of the carrier of i
(0. i) \ n is Element of the carrier of i
((0. i) \ X) \ ((0. i) \ n) is Element of the carrier of i
(((0. i) \ X) \ ((0. i) \ n)) \ (n \ X) is Element of the carrier of i
X \ X is Element of the carrier of i
(X \ X) \ (X \ n) is Element of the carrier of i
X \ (X \ n) is Element of the carrier of i
(X \ (X \ n)) \ X is Element of the carrier of i
((X \ (X \ n)),(X \ n)) to_power (X + 1) is Element of the carrier of i
(((X,(X \ n)) to_power 1),(X \ n)) to_power (X + 1) is Element of the carrier of i
(X + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ n)) to_power ((X + 1) + 1) is Element of the carrier of i
X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ n)) to_power (X + 1) is Element of the carrier of i
(X + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ n)) to_power ((X + 1) + 1) is Element of the carrier of i
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ n)) to_power (0 + 1) is Element of the carrier of i
((X,(X \ n)) to_power (0 + 1)) \ ((X,(X \ n)) to_power 1) is Element of the carrier of i
n is Element of the carrier of i
X is Element of the carrier of i
n \ X is Element of the carrier of i
X \ n is Element of the carrier of i
X \ (X \ n) is Element of the carrier of i
(i,n,X,j,0) is Element of the carrier of i
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(n,(n \ X)) to_power (j + 1) is Element of the carrier of i
(((n,(n \ X)) to_power (j + 1)),(X \ n)) to_power 0 is Element of the carrier of i
(i,X,n,m,m) is Element of the carrier of i
(X,(X \ n)) to_power (m + 1) is Element of the carrier of i
(((X,(X \ n)) to_power (m + 1)),(n \ X)) to_power m is Element of the carrier of i
(n,(X \ n)) to_power 0 is Element of the carrier of i
(((X,(X \ n)) to_power (m + 1)),(0. i)) to_power m is Element of the carrier of i
((((X,(X \ n)) to_power (m + 1)),(0. i)) to_power m) \ (0. i) is Element of the carrier of i
(((X,(X \ n)) to_power (m + 1)),(0. i)) to_power (m + 1) is Element of the carrier of i
(X,(X \ n)) to_power 1 is Element of the carrier of i
(X \ (X \ n)) \ n is Element of the carrier of i
(X \ n) \ (X \ n) is Element of the carrier of i
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,0,0) is Element of the carrier of X
X \ x is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (0 + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (0 + 1)),(x \ X)) to_power 0 is Element of the carrier of X
(X,x,X,0,n) is Element of the carrier of X
(x,(x \ X)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (0 + 1)),(X \ x)) to_power n is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (j + 1) is Element of the carrier of X
(X,(X \ x)) to_power (m + 1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 ( 0 , 0 , 0 ,n)
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,0,0) is Element of the carrier of X
x \ y is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 0 is Element of the carrier of X
(X,y,x,0,0) is Element of the carrier of X
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 0 is Element of the carrier of X
(X,y,x,0,n) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
(X,y,x,0,0) is Element of the carrier of X
y \ x is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
x \ y is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 0 is Element of the carrier of X
(X,x,y,0,0) is Element of the carrier of X
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 0 is Element of the carrier of X
(X,x,y,0,0) \ (X,y,x,0,0) is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(X,y,x,0,0) \ (X,x,y,0,0) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i + 1,j,m,n + 1)
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,0,1) is Element of the carrier of X
x \ y is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 1 is Element of the carrier of X
(X,y,x,0,1) is Element of the carrier of X
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 1 is Element of the carrier of X
(i + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(m + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (j + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (0 + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) is Element of the carrier of X
(X,x,y,(i + 1),j) is Element of the carrier of X
(x,(x \ y)) to_power ((i + 1) + 1) is Element of the carrier of X
(((x,(x \ y)) to_power ((i + 1) + 1)),(y \ x)) to_power j is Element of the carrier of X
(X,y,x,m,(n + 1)) is Element of the carrier of X
(y,(y \ x)) to_power (m + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + 1) is Element of the carrier of X
(x,(x \ y)) to_power (j + 1) is Element of the carrier of X
(x,(x \ y)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power j is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
the carrier of X is non empty set
X is Element of the carrier of X
x is Element of the carrier of X
(X,X,x,0,j) is Element of the carrier of X
X \ x is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (0 + 1) is Element of the carrier of X
x \ X is Element of the carrier of X
(((X,(X \ x)) to_power (0 + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,0,0) is Element of the carrier of X
(x,(x \ X)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (0 + 1)),(X \ x)) to_power 0 is Element of the carrier of X
(X,X,x,i,j) is Element of the carrier of X
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(X,(X \ x)) to_power (i + 1) is Element of the carrier of X
(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X
(X,x,X,m,n) is Element of the carrier of X
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (m + 1) is Element of the carrier of X
(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ X)) to_power (n + 1) is Element of the carrier of X
(x,(x \ X)) to_power (i + 1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 ( 0 ,j, 0 , 0 )
the carrier of X is non empty set
y is Element of the carrier of X
x is Element of the carrier of X
(X,y,x,0,0) is Element of the carrier of X
y \ x is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
x \ y is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 0 is Element of the carrier of X
(X,x,y,0,0) is Element of the carrier of X
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 0 is Element of the carrier of X
(X,x,y,0,j) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power j is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
(X,y,x,0,0) is Element of the carrier of X
y \ x is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
x \ y is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 0 is Element of the carrier of X
(X,x,y,0,0) is Element of the carrier of X
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 0 is Element of the carrier of X
(X,x,y,0,0) \ (X,y,x,0,0) is Element of the carrier of X
0. X is V49(X) minimal positive V92(X) Element of the carrier of X
(X,y,x,0,0) \ (X,x,y,0,0) is Element of the carrier of X
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j + 1,m + 1,n)
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
(X,x,y,0,1) is Element of the carrier of X
x \ y is Element of the carrier of X
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(x,(x \ y)) to_power (0 + 1) is Element of the carrier of X
y \ x is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power 1 is Element of the carrier of X
(X,y,x,0,1) is Element of the carrier of X
(y,(y \ x)) to_power (0 + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power 1 is Element of the carrier of X
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(i + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (i + 1) is Element of the carrier of X
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power (n + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (n + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (0 + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (0 + 1)),(y \ x)) to_power (j + 1) is Element of the carrier of X
(X,x,y,i,(j + 1)) is Element of the carrier of X
(x,(x \ y)) to_power (i + 1) is Element of the carrier of X
(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + 1) is Element of the carrier of X
(X,y,x,(m + 1),n) is Element of the carrier of X
(y,(y \ x)) to_power ((m + 1) + 1) is Element of the carrier of X
(((y,(y \ x)) to_power ((m + 1) + 1)),(x \ y)) to_power n is Element of the carrier of X
(y,(y \ x)) to_power (n + 1) is Element of the carrier of X
(y,(y \ x)) to_power (i + 1) is Element of the carrier of X
(((y,(y \ x)) to_power (0 + 1)),(x \ y)) to_power n is Element of the carrier of X