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