:: BCIALG_2 semantic presentation

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

<