REAL is set
NAT is non empty V21() V22() V23() Element of bool REAL
bool REAL is non empty set
NAT is non empty V21() V22() V23() set
bool NAT is non empty set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
bool NAT is non empty set
K273() is set
1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
{} is set
the empty V21() V22() V23() V25() V26() V27() V74() ext-real non negative V78() set is empty V21() V22() V23() V25() V26() V27() V74() ext-real non negative V78() set
0 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
I is Element of the carrier of X
RI is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . w1 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(y1 . w1) \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((y1 . w1),x1) is Element of the carrier of X
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . x1 is set
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
z1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
z1 is Element of the carrier of X
z1 is Element of the carrier of X
j is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . (w1 + 1) is Element of the carrier of X
y1 is Element of the carrier of X
z1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
z1 . (w1 + 1) is Element of the carrier of X
z1 . 0 is Element of the carrier of X
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
j + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . (j + 1) is Element of the carrier of X
y1 . j is Element of the carrier of X
(y1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((y1 . j),x1) is Element of the carrier of X
x1 . j is Element of the carrier of X
(x1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((x1 . j),x1) is Element of the carrier of X
z1 . (j + 1) is Element of the carrier of X
z1 . j is Element of the carrier of X
(z1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((z1 . j),x1) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is Element of the carrier of X
NAT --> w1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) V25() Element of bool [:NAT, the carrier of X:]
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . x1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . x1 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . (x1 + 1) is Element of the carrier of X
y1 . x1 is Element of the carrier of X
(y1 . x1) \ x1 is Element of the carrier of X
the InternalDiff of X . ((y1 . x1),x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is Element of the carrier of X
x1 is Element of the carrier of X
w1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . IT is Element of the carrier of X
x1 . 0 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . IT is Element of the carrier of X
y1 . 0 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
(x1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((x1 . x1),RI) is Element of the carrier of X
y1 . (x1 + 1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
y1 . (x1 + 1) is Element of the carrier of X
x1 . 0 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 0 is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,1) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 1 is Element of the carrier of X
IT . 0 is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (0 + 1) is Element of the carrier of X
2 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,2) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
(I \ RI) \ RI is Element of the carrier of X
the InternalDiff of X . ((I \ RI),RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 2 is Element of the carrier of X
IT . 0 is Element of the carrier of X
1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (1 + 1) is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (0 + 1) is Element of the carrier of X
(IT . (0 + 1)) \ RI is Element of the carrier of X
the InternalDiff of X . ((IT . (0 + 1)),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(IT + 1)) is Element of the carrier of X
(X,I,RI,IT) is Element of the carrier of X
(X,I,RI,IT) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,RI,IT),RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
w1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
w1 . IT is Element of the carrier of X
w1 . 0 is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . (IT + 1) is Element of the carrier of X
x1 . 0 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
x1 . x1 is Element of the carrier of X
(x1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((x1 . x1),RI) is Element of the carrier of X
w1 . (x1 + 1) is Element of the carrier of X
w1 . x1 is Element of the carrier of X
(w1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((w1 . x1),RI) is Element of the carrier of X
x1 . y1 is Element of the carrier of X
w1 . y1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . y1 is Element of the carrier of X
w1 . y1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
w1 . x1 is Element of the carrier of X
x1 . IT is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(RI + 1)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(w1 + 1)) is Element of the carrier of X
(X,I,(0. X),(IT + 1)) is Element of the carrier of X
(X,I,(0. X),(IT + 1)) \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,(0. X),(IT + 1)),(0. X)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(w1 + 1)) is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(0 + 1)) is Element of the carrier of X
I \ (0. X) is Element of the carrier of X
the InternalDiff of X . (I,(0. X)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(IT + 1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
I is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),I) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),IT) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
I \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),IT) is Element of the carrier of X
(X,(I \ IT),RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
((X,I,RI,x1) \ RI) \ IT is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ RI),IT) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
((X,I,RI,x1) \ IT) \ RI is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ IT),RI) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
(X,(I \ IT),RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(I \ IT),RI,x1),RI) is Element of the carrier of X
(X,(I \ IT),RI,(x1 + 1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
(X,I,RI,0) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,0),IT) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
I \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (I,(I \ RI)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),IT) is Element of the carrier of X
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),(w1 + 1)) is Element of the carrier of X
(X,I,(I \ (I \ RI)),w1) is Element of the carrier of X
(X,I,(I \ (I \ RI)),w1) \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . ((X,I,(I \ (I \ RI)),w1),(I \ (I \ RI))) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),(I \ (I \ RI))) is Element of the carrier of X
I \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . (I,(I \ (I \ RI))) is Element of the carrier of X
(X,(I \ (I \ (I \ RI))),RI,w1) is Element of the carrier of X
(X,(I \ RI),RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),RI) is Element of the carrier of X
(X,I,RI,(w1 + 1)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),x1) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,I,(I \ (I \ RI)),0) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),w1) is Element of the carrier of X
(X,I,RI,w1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
(X,(0. X),(I `),RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(IT + 1)) is Element of the carrier of X
(X,(0. X),I,(IT + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(IT + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(IT + 1))) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),I) is Element of the carrier of X
((X,(0. X),I,IT) \ I) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) \ I)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,IT) `),(I `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I `),IT) is Element of the carrier of X
(X,(0. X),(I `),IT) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),(I `),IT),(I `)) is Element of the carrier of X
(X,(0. X),(I `),(IT + 1)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,w1)) is Element of the carrier of X
(X,(0. X),(I `),w1) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,0)) is Element of the carrier of X
(0. X) ` is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),(I `),IT) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,I,RI,IT),RI,w1) is Element of the carrier of X
IT + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(IT + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,(X,I,RI,x1),RI,w1),RI) is Element of the carrier of X
(x1 + w1) + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,((x1 + w1) + 1)) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
(X,((X,I,RI,x1) \ RI),RI,w1) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,I,RI,w1),IT,x1) is Element of the carrier of X
(X,I,IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,(X,I,RI,x1),IT,x1),RI) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(X,I,IT,x1),RI,x1),RI) is Element of the carrier of X
(X,(X,I,IT,x1),RI,(x1 + 1)) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
(X,((X,I,RI,x1) \ RI),IT,x1) is Element of the carrier of X
(X,I,RI,(x1 + 1)) is Element of the carrier of X
(X,(X,I,RI,(x1 + 1)),IT,x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,y1) is Element of the carrier of X
(X,(X,I,RI,y1),IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,y1) is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
(X,(X,I,RI,0),IT,x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),I,RI) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,RI) `)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(IT + 1)) is Element of the carrier of X
(X,(0. X),I,(IT + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(IT + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(IT + 1))) is Element of the carrier of X
((X,(0. X),I,(IT + 1)) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,(IT + 1)) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,(IT + 1)) `)) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),I) is Element of the carrier of X
((X,(0. X),I,IT) \ I) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) \ I)) is Element of the carrier of X
(((X,(0. X),I,IT) \ I) `) ` is Element of the carrier of X
(0. X) \ (((X,(0. X),I,IT) \ I) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((X,(0. X),I,IT) \ I) `)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
((X,(0. X),I,IT) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,IT) `),(I `)) is Element of the carrier of X
(((X,(0. X),I,IT) `) \ (I `)) ` is Element of the carrier of X
(0. X) \ (((X,(0. X),I,IT) `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((X,(0. X),I,IT) `) \ (I `))) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
(((X,(0. X),I,IT) `) `) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((((X,(0. X),I,IT) `) `),((I `) `)) is Element of the carrier of X
(X,(0. X),I,IT) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),((I `) `)) is Element of the carrier of X
((I `) `) ` is Element of the carrier of X
(0. X) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) `)) is Element of the carrier of X
(X,(((I `) `) `),I,IT) is Element of the carrier of X
(X,(I `),I,IT) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,w1)) is Element of the carrier of X
((X,(0. X),I,w1) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,w1) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,w1) `)) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,0)) is Element of the carrier of X
((X,(0. X),I,0) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,0) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,0) `)) is Element of the carrier of X
(0. X) ` is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X
((0. X) `) ` is Element of the carrier of X
(0. X) \ ((0. X) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((0. X) `)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI + IT)) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,RI) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,RI),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(w1 + IT) + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((w1 + IT) + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + IT)) is Element of the carrier of X
(X,(0. X),I,(w1 + IT)) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + IT)),I) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,w1) \ ((X,(0. X),I,IT) `)) \ I is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ ((X,(0. X),I,IT) `)),I) is Element of the carrier of X
(X,(0. X),I,w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),I) is Element of the carrier of X
((X,(0. X),I,w1) \ I) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ I),((X,(0. X),I,IT) `)) is Element of the carrier of X
(w1 + 1) + IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((w1 + 1) + IT)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(x1 + IT)) is Element of the carrier of X
(X,(0. X),I,x1) is Element of the carrier of X
(X,(0. X),I,x1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,x1),((X,(0. X),I,IT) `)) is Element of the carrier of X
0 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(0 + IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(w1 + IT)) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),((X,(0. X),I,IT) `)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI + IT)) is Element of the carrier of X
(X,(0. X),I,(RI + IT)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(RI + IT)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(RI + IT))) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
((X,(0. X),I,RI) `) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,RI) `),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,RI) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,RI),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `)) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `))) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,RI) `) \ (((X,(0. X),I,IT) `) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,RI) `),(((X,(0. X),I,IT) `) `)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),IT) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),IT) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),IT)) is Element of the carrier of X
RI * IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),(w1 + 1)) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),(w1 + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),(w1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),(w1 + 1))) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),(X,(0. X),I,RI),w1),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI)) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI))) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),w1)) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),(X,(0. X),I,RI),w1) `) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),(X,(0. X),I,RI),w1) `),((X,(0. X),I,RI) `)) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
(X,(0. X),I,(RI * w1)) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(RI * w1)),((X,(0. X),I,RI) `)) is Element of the carrier of X
(RI * w1) + RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((RI * w1) + RI)) is Element of the carrier of X
RI * (w1 + 1) is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * (w1 + 1))) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),x1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),x1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),x1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),x1)) is Element of the carrier of X
RI * x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * x1)) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),0) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),0)) is Element of the carrier of X
(0. X) ` is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),w1)) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * (w1 + 1) is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * (w1 + 1))) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(RI * w1) + RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((RI * w1) + RI)) is Element of the carrier of X
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
(X,(X,(0. X),I,(RI * w1)),I,RI) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * x1)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(w1 + 1)) is Element of the carrier of X
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),RI) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),IT) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),RI,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ (X,(0. X),RI,IT) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),(X,(0. X),RI,IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),x1) is Element of the carrier of X
(X,(0. X),I,x1) is Element of the carrier of X
(X,(0. X),RI,x1) is Element of the carrier of X
(X,(0. X),I,x1) \ (X,(0. X),RI,x1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,x1),(X,(0. X),RI,x1)) is Element of the carrier of X
(X,(0. X),(I \ RI),w1) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),RI,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(0. X),(I \ RI),(w1 + 1)) is Element of the carrier of X
((X,(0. X),I,w1) \ (X,(0. X),RI,w1)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ (X,(0. X),RI,w1)),(I \ RI)) is Element of the carrier of X
(X,(0. X),I,w1) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(I \ RI)) is Element of the carrier of X
((X,(0. X),I,w1) \ (I \ RI)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ (I \ RI)),(X,(0. X),RI,w1)) is Element of the carrier of X
(I \ RI) ` is Element of the carrier of X
(0. X) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ RI)) is Element of the carrier of X
(X,((I \ RI) `),I,w1) is Element of the carrier of X
(X,((I \ RI) `),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((I \ RI) `),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(I `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((I `),(RI `)) is Element of the carrier of X
(X,((I `) \ (RI `)),I,w1) is Element of the carrier of X
(X,((I `) \ (RI `)),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((I `) \ (RI `)),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(I `),I,w1) is Element of the carrier of X
(X,(I `),I,w1) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((X,(I `),I,w1),(RI `)) is Element of the carrier of X
((X,(I `),I,w1) \ (RI `)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(I `),I,w1) \ (RI `)),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(I `),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(I `),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(I `),I,w1) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(I `),I,w1) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),I) is Element of the carrier of X
((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ I),(X,(0. X),RI,w1)) is Element of the carrier of X
(((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),(RI `)) is Element of the carrier of X
((X,(0. X),I,(w1 + 1)) \ (RI `)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,(w1 + 1)) \ (RI `)),(X,(0. X),RI,w1)) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
(X,((RI `) `),I,(w1 + 1)) is Element of the carrier of X
(X,((RI `) `),I,(w1 + 1)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((RI `) `),I,(w1 + 1)),(X,(0. X),RI,w1)) is Element of the carrier of X
((RI `) `) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(((RI `) `) \ (X,(0. X),RI,w1)),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(0. X),RI,w1) `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),RI,w1) `),(RI `)) is Element of the carrier of X
(X,(((X,(0. X),RI,w1) `) \ (RI `)),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),RI,w1),RI) is Element of the carrier of X
((X,(0. X),RI,w1) \ RI) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),RI,w1) \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),RI,w1) \ RI)) is Element of the carrier of X
(X,(((X,(0. X),RI,w1) \ RI) `),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,(w1 + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),RI,(w1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),RI,(w1 + 1))) is Element of the carrier of X
(X,((X,(0. X),RI,(w1 + 1)) `),I,(w1 + 1)) is Element of the carrier of X
(0. X) ` is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X
(X,(0. X),(I \ RI),0) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,0),(0. X)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),w1) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),RI,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,IT,w1) is Element of the carrier of X
(X,RI,IT,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,IT,x1) is Element of the carrier of X
(X,RI,IT,x1) is Element of the carrier of X
(X,I,IT,x1) is Element of the carrier of X
(X,RI,IT,x1) is Element of the carrier of X
(X,I,IT,x1) \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,IT,x1),IT) is Element of the carrier of X
(X,RI,IT,x1) \ IT is Element of the carrier of X
<