:: BCIALG_6 semantic presentation

REAL is set

NAT is non empty V24() V25() V26() Element of bool REAL

bool REAL is set

NAT is non empty V24() V25() V26() set

bool NAT is set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:REAL,REAL:] is set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

bool [:[:NAT,NAT:],NAT:] is set

bool NAT is set

{} is empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative set

the empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative set is empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative set

1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

0 is empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative Element of NAT

K186(1) is V92() V93() integer ext-real non positive set

X is set

[:NAT,X:] is set

bool [:NAT,X:] is set

G is Relation-like NAT -defined X -valued Function-like quasi_total Element of bool [:NAT,X:]

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

G . K is set

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

G . RK is Element of X

X is non empty BCIStr_0

the carrier of X is non empty set

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

0. X is V47(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

[:NAT, the carrier of X:] is set

bool [:NAT, the carrier of X:] is set

G is set

K is Element of the carrier of X

RK is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,RK,0) is Element of the carrier of X

K1 is set

RK1 is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

RK1 + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

( the carrier of X,RK,(RK1 + 1)) is Element of the carrier of X

( the carrier of X,RK,RK1) is Element of the carrier of X

( the carrier of X,RK,RK1) ` is Element of the carrier of X

(0. X) \ ( the carrier of X,RK,RK1) 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),( the carrier of X,RK,RK1)) is Element of the carrier of X

[(0. X),( the carrier of X,RK,RK1)] is set

{(0. X),( the carrier of X,RK,RK1)} is non empty set

{(0. X)} is non empty set

{{(0. X),( the carrier of X,RK,RK1)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),( the carrier of X,RK,RK1)] is set

K \ (( the carrier of X,RK,RK1) `) is Element of the carrier of X

the InternalDiff of X . (K,(( the carrier of X,RK,RK1) `)) is Element of the carrier of X

[K,(( the carrier of X,RK,RK1) `)] is set

{K,(( the carrier of X,RK,RK1) `)} is non empty set

{K} is non empty set

{{K,(( the carrier of X,RK,RK1) `)},{K}} is non empty set

the InternalDiff of X . [K,(( the carrier of X,RK,RK1) `)] is set

G is Relation-like Function-like set

dom G is set

K is Element of the carrier of X

G . K is set

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

RK1 is Element of the carrier of X

K1 is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,K1,0) is Element of the carrier of X

( the carrier of X,K1,RK) is Element of the carrier of X

K is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

RK is Element of the carrier of X

K . (RK,0) is Element of the carrier of X

[RK,0] is set

{RK,0} is non empty set

{RK} is non empty set

{{RK,0},{RK}} is non empty set

K . [RK,0] is set

G . RK is set

K1 is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,K1,0) is Element of the carrier of X

I is Element of the carrier of X

RK1 is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,RK1,0) is Element of the carrier of X

K1 is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

K1 + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

K . (RK,(K1 + 1)) is Element of the carrier of X

[RK,(K1 + 1)] is set

{RK,(K1 + 1)} is non empty set

{{RK,(K1 + 1)},{RK}} is non empty set

K . [RK,(K1 + 1)] is set

K . (RK,K1) is Element of the carrier of X

[RK,K1] is set

{RK,K1} is non empty set

{{RK,K1},{RK}} is non empty set

K . [RK,K1] is set

(K . (RK,K1)) ` is Element of the carrier of X

(0. X) \ (K . (RK,K1)) 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),(K . (RK,K1))) is Element of the carrier of X

[(0. X),(K . (RK,K1))] is set

{(0. X),(K . (RK,K1))} is non empty set

{(0. X)} is non empty set

{{(0. X),(K . (RK,K1))},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(K . (RK,K1))] is set

RK \ ((K . (RK,K1)) `) is Element of the carrier of X

the InternalDiff of X . (RK,((K . (RK,K1)) `)) is Element of the carrier of X

[RK,((K . (RK,K1)) `)] is set

{RK,((K . (RK,K1)) `)} is non empty set

{{RK,((K . (RK,K1)) `)},{RK}} is non empty set

the InternalDiff of X . [RK,((K . (RK,K1)) `)] is set

RK1 is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,RK1,K1) is Element of the carrier of X

I is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,I,(K1 + 1)) is Element of the carrier of X

f is Element of the carrier of X

RI is Relation-like NAT -defined the carrier of X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]

( the carrier of X,RI,0) is Element of the carrier of X

G is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

K is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

RK is Element of the carrier of X

RK1 is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

[RK,RK1] is set

{RK,RK1} is non empty set

{RK} is non empty set

{{RK,RK1},{RK}} is non empty set

G . [RK,RK1] is set

K . [RK,RK1] is set

K . (RK,RK1) is Element of the carrier of X

RK1 + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

[RK,(RK1 + 1)] is set

{RK,(RK1 + 1)} is non empty set

{{RK,(RK1 + 1)},{RK}} is non empty set

G . [RK,(RK1 + 1)] is set

G . (RK,(RK1 + 1)) is Element of the carrier of X

G . (RK,RK1) is Element of the carrier of X

(G . (RK,RK1)) ` is Element of the carrier of X

(0. X) \ (G . (RK,RK1)) 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),(G . (RK,RK1))) is Element of the carrier of X

[(0. X),(G . (RK,RK1))] is set

{(0. X),(G . (RK,RK1))} is non empty set

{(0. X)} is non empty set

{{(0. X),(G . (RK,RK1))},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(G . (RK,RK1))] is set

RK \ ((G . (RK,RK1)) `) is Element of the carrier of X

the InternalDiff of X . (RK,((G . (RK,RK1)) `)) is Element of the carrier of X

[RK,((G . (RK,RK1)) `)] is set

{RK,((G . (RK,RK1)) `)} is non empty set

{{RK,((G . (RK,RK1)) `)},{RK}} is non empty set

the InternalDiff of X . [RK,((G . (RK,RK1)) `)] is set

K . (RK,(RK1 + 1)) is Element of the carrier of X

K . [RK,(RK1 + 1)] is set

[RK,0] is set

{RK,0} is non empty set

{{RK,0},{RK}} is non empty set

G . [RK,0] is set

G . (RK,0) is Element of the carrier of X

K . (RK,0) is Element of the carrier of X

K . [RK,0] is set

K1 is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

G . (RK,K1) is Element of the carrier of X

[RK,K1] is set

{RK,K1} is non empty set

{{RK,K1},{RK}} is non empty set

G . [RK,K1] is set

K . (RK,K1) is Element of the carrier of X

K . [RK,K1] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is V92() V93() integer ext-real set

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

K is Element of the carrier of X

abs G is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

(X) . (K,(abs G)) is Element of the carrier of X

[K,(abs G)] is set

{K,(abs G)} is non empty set

{K} is non empty set

{{K,(abs G)},{K}} is non empty set

(X) . [K,(abs G)] is set

K ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ K 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),K) is Element of the carrier of X

[(0. X),K] is set

{(0. X),K} is non empty set

{(0. X)} is non empty set

{{(0. X),K},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),K] is set

(X) . ((K `),(abs G)) is Element of the carrier of X

[(K `),(abs G)] is set

{(K `),(abs G)} is non empty set

{(K `)} is non empty set

{{(K `),(abs G)},{(K `)}} is non empty set

(X) . [(K `),(abs G)] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

K is Element of the carrier of X

(X,G,K) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (K,G) is set

[K,G] is set

{K,G} is non empty set

{K} is non empty set

{{K,G},{K}} is non empty set

(X) . [K,G] is set

RK is Element of the carrier of X

abs G is V24() V25() V26() V30() V92() V93() integer ext-real non negative 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

AtomSet X is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

G is Element of the carrier of X

K is Element of AtomSet X

G \ K 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (G,K) is Element of the carrier of X

[G,K] is set

{G,K} is non empty set

{G} is non empty set

{{G,K},{G}} is non empty set

the InternalDiff of X . [G,K] is set

RK is Element of AtomSet X

G \ RK is Element of the carrier of X

the InternalDiff of X . (G,RK) is Element of the carrier of X

[G,RK] is set

{G,RK} is non empty set

{{G,RK},{G}} is non empty set

the InternalDiff of X . [G,RK] is set

K \ (G \ RK) is Element of the carrier of X

the InternalDiff of X . (K,(G \ RK)) is Element of the carrier of X

[K,(G \ RK)] is set

{K,(G \ RK)} is non empty set

{K} is non empty set

{{K,(G \ RK)},{K}} is non empty set

the InternalDiff of X . [K,(G \ RK)] is set

RK \ (G \ K) is Element of the carrier of X

the InternalDiff of X . (RK,(G \ K)) is Element of the carrier of X

[RK,(G \ K)] is set

{RK,(G \ K)} is non empty set

{RK} is non empty set

{{RK,(G \ K)},{RK}} is non empty set

the InternalDiff of X . [RK,(G \ K)] is set

G \ (G \ RK) is Element of the carrier of X

the InternalDiff of X . (G,(G \ RK)) is Element of the carrier of X

[G,(G \ RK)] is set

{G,(G \ RK)} is non empty set

{{G,(G \ RK)},{G}} is non empty set

the InternalDiff of X . [G,(G \ RK)] is set

(G \ (G \ RK)) \ RK is Element of the carrier of X

the InternalDiff of X . ((G \ (G \ RK)),RK) is Element of the carrier of X

[(G \ (G \ RK)),RK] is set

{(G \ (G \ RK)),RK} is non empty set

{(G \ (G \ RK))} is non empty set

{{(G \ (G \ RK)),RK},{(G \ (G \ RK))}} is non empty set

the InternalDiff of X . [(G \ (G \ RK)),RK] is set

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(RK \ (G \ K)) \ (K \ (G \ RK)) is Element of the carrier of X

the InternalDiff of X . ((RK \ (G \ K)),(K \ (G \ RK))) is Element of the carrier of X

[(RK \ (G \ K)),(K \ (G \ RK))] is set

{(RK \ (G \ K)),(K \ (G \ RK))} is non empty set

{(RK \ (G \ K))} is non empty set

{{(RK \ (G \ K)),(K \ (G \ RK))},{(RK \ (G \ K))}} is non empty set

the InternalDiff of X . [(RK \ (G \ K)),(K \ (G \ RK))] is set

(G \ (G \ RK)) \ (G \ K) is Element of the carrier of X

the InternalDiff of X . ((G \ (G \ RK)),(G \ K)) is Element of the carrier of X

[(G \ (G \ RK)),(G \ K)] is set

{(G \ (G \ RK)),(G \ K)} is non empty set

{{(G \ (G \ RK)),(G \ K)},{(G \ (G \ RK))}} is non empty set

the InternalDiff of X . [(G \ (G \ RK)),(G \ K)] is set

((G \ (G \ RK)) \ (G \ K)) \ (K \ (G \ RK)) is Element of the carrier of X

the InternalDiff of X . (((G \ (G \ RK)) \ (G \ K)),(K \ (G \ RK))) is Element of the carrier of X

[((G \ (G \ RK)) \ (G \ K)),(K \ (G \ RK))] is set

{((G \ (G \ RK)) \ (G \ K)),(K \ (G \ RK))} is non empty set

{((G \ (G \ RK)) \ (G \ K))} is non empty set

{{((G \ (G \ RK)) \ (G \ K)),(K \ (G \ RK))},{((G \ (G \ RK)) \ (G \ K))}} is non empty set

the InternalDiff of X . [((G \ (G \ RK)) \ (G \ K)),(K \ (G \ RK))] is set

K1 is Element of the carrier of X

G \ (G \ K) is Element of the carrier of X

the InternalDiff of X . (G,(G \ K)) is Element of the carrier of X

[G,(G \ K)] is set

{G,(G \ K)} is non empty set

{{G,(G \ K)},{G}} is non empty set

the InternalDiff of X . [G,(G \ K)] is set

(G \ (G \ K)) \ (G \ RK) is Element of the carrier of X

the InternalDiff of X . ((G \ (G \ K)),(G \ RK)) is Element of the carrier of X

[(G \ (G \ K)),(G \ RK)] is set

{(G \ (G \ K)),(G \ RK)} is non empty set

{(G \ (G \ K))} is non empty set

{{(G \ (G \ K)),(G \ RK)},{(G \ (G \ K))}} is non empty set

the InternalDiff of X . [(G \ (G \ K)),(G \ RK)] is set

((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK)) is Element of the carrier of X

the InternalDiff of X . (((G \ (G \ K)) \ (G \ RK)),(K \ (G \ RK))) is Element of the carrier of X

[((G \ (G \ K)) \ (G \ RK)),(K \ (G \ RK))] is set

{((G \ (G \ K)) \ (G \ RK)),(K \ (G \ RK))} is non empty set

{((G \ (G \ K)) \ (G \ RK))} is non empty set

{{((G \ (G \ K)) \ (G \ RK)),(K \ (G \ RK))},{((G \ (G \ K)) \ (G \ RK))}} is non empty set

the InternalDiff of X . [((G \ (G \ K)) \ (G \ RK)),(K \ (G \ RK))] is set

(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))) \ (0. X) is Element of the carrier of X

the InternalDiff of X . ((((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),(0. X)) is Element of the carrier of X

[(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),(0. X)] is set

{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),(0. X)} is non empty set

{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK)))} is non empty set

{{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),(0. X)},{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK)))}} is non empty set

the InternalDiff of X . [(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),(0. X)] is set

(G \ (G \ K)) \ K is Element of the carrier of X

the InternalDiff of X . ((G \ (G \ K)),K) is Element of the carrier of X

[(G \ (G \ K)),K] is set

{(G \ (G \ K)),K} is non empty set

{{(G \ (G \ K)),K},{(G \ (G \ K))}} is non empty set

the InternalDiff of X . [(G \ (G \ K)),K] is set

(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))) \ ((G \ (G \ K)) \ K) is Element of the carrier of X

the InternalDiff of X . ((((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),((G \ (G \ K)) \ K)) is Element of the carrier of X

[(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),((G \ (G \ K)) \ K)] is set

{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),((G \ (G \ K)) \ K)} is non empty set

{{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),((G \ (G \ K)) \ K)},{(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK)))}} is non empty set

the InternalDiff of X . [(((G \ (G \ K)) \ (G \ RK)) \ (K \ (G \ RK))),((G \ (G \ K)) \ K)] is set

(K \ (G \ RK)) \ (RK \ (G \ K)) is Element of the carrier of X

the InternalDiff of X . ((K \ (G \ RK)),(RK \ (G \ K))) is Element of the carrier of X

[(K \ (G \ RK)),(RK \ (G \ K))] is set

{(K \ (G \ RK)),(RK \ (G \ K))} is non empty set

{(K \ (G \ RK))} is non empty set

{{(K \ (G \ RK)),(RK \ (G \ K))},{(K \ (G \ RK))}} is non empty set

the InternalDiff of X . [(K \ (G \ RK)),(RK \ (G \ K))] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is Element of the carrier of X

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

K + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(K + 1),G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (G,(K + 1)) is set

[G,(K + 1)] is set

{G,(K + 1)} is non empty set

{G} is non empty set

{{G,(K + 1)},{G}} is non empty set

(X) . [G,(K + 1)] is set

(X,K,G) is Element of the carrier of X

(X) . (G,K) is set

[G,K] is set

{G,K} is non empty set

{{G,K},{G}} is non empty set

(X) . [G,K] is set

(X,K,G) ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ (X,K,G) 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),(X,K,G)) is Element of the carrier of X

[(0. X),(X,K,G)] is set

{(0. X),(X,K,G)} is non empty set

{(0. X)} is non empty set

{{(0. X),(X,K,G)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(X,K,G)] is set

G \ ((X,K,G) `) is Element of the carrier of X

the InternalDiff of X . (G,((X,K,G) `)) is Element of the carrier of X

[G,((X,K,G) `)] is set

{G,((X,K,G) `)} is non empty set

{{G,((X,K,G) `)},{G}} is non empty set

the InternalDiff of X . [G,((X,K,G) `)] is set

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

RK + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(RK + 1),G) is Element of the carrier of X

(X) . (G,(RK + 1)) is set

[G,(RK + 1)] is set

{G,(RK + 1)} is non empty set

{{G,(RK + 1)},{G}} is non empty set

(X) . [G,(RK + 1)] is set

(X,RK,G) is Element of the carrier of X

(X) . (G,RK) is set

[G,RK] is set

{G,RK} is non empty set

{{G,RK},{G}} is non empty set

(X) . [G,RK] is set

(X,RK,G) ` is Element of the carrier of X

(0. X) \ (X,RK,G) is Element of the carrier of X

the InternalDiff of X . ((0. X),(X,RK,G)) is Element of the carrier of X

[(0. X),(X,RK,G)] is set

{(0. X),(X,RK,G)} is non empty set

{{(0. X),(X,RK,G)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(X,RK,G)] is set

G \ ((X,RK,G) `) is Element of the carrier of X

the InternalDiff of X . (G,((X,RK,G) `)) is Element of the carrier of X

[G,((X,RK,G) `)] is set

{G,((X,RK,G) `)} is non empty set

{{G,((X,RK,G) `)},{G}} is non empty set

the InternalDiff of X . [G,((X,RK,G) `)] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is Element of the carrier of X

(X,0,G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (G,0) is set

[G,0] is set

{G,0} is non empty set

{G} is non empty set

{{G,0},{G}} is non empty set

(X) . [G,0] is set

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X 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

G is Element of the carrier of X

(X,1,G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (G,1) is set

[G,1] is set

{G,1} is non empty set

{G} is non empty set

{{G,1},{G}} is non empty set

(X) . [G,1] is set

0 + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(0 + 1),G) is Element of the carrier of X

(X) . (G,(0 + 1)) is set

[G,(0 + 1)] is set

{G,(0 + 1)} is non empty set

{{G,(0 + 1)},{G}} is non empty set

(X) . [G,(0 + 1)] is set

(X,0,G) is Element of the carrier of X

(X) . (G,0) is set

[G,0] is set

{G,0} is non empty set

{{G,0},{G}} is non empty set

(X) . [G,0] is set

(X,0,G) ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ (X,0,G) 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),(X,0,G)) is Element of the carrier of X

[(0. X),(X,0,G)] is set

{(0. X),(X,0,G)} is non empty set

{(0. X)} is non empty set

{{(0. X),(X,0,G)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(X,0,G)] is set

G \ ((X,0,G) `) is Element of the carrier of X

the InternalDiff of X . (G,((X,0,G) `)) is Element of the carrier of X

[G,((X,0,G) `)] is set

{G,((X,0,G) `)} is non empty set

{{G,((X,0,G) `)},{G}} is non empty set

the InternalDiff of X . [G,((X,0,G) `)] is set

(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),(0. X)] is set

{(0. X),(0. X)} is non empty set

{{(0. X),(0. X)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(0. X)] is set

G \ ((0. X) `) is Element of the carrier of X

the InternalDiff of X . (G,((0. X) `)) is Element of the carrier of X

[G,((0. X) `)] is set

{G,((0. X) `)} is non empty set

{{G,((0. X) `)},{G}} is non empty set

the InternalDiff of X . [G,((0. X) `)] is set

G \ (0. X) is Element of the carrier of X

the InternalDiff of X . (G,(0. X)) is Element of the carrier of X

[G,(0. X)] is set

{G,(0. X)} is non empty set

{{G,(0. X)},{G}} is non empty set

the InternalDiff of X . [G,(0. X)] is set

- 1 is V92() V93() integer ext-real non positive Element of INT

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is Element of the carrier of X

(X,(- 1),G) is Element of the carrier of X

G ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

abs (- 1) is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

(X) . ((G `),(abs (- 1))) is Element of the carrier of X

[(G `),(abs (- 1))] is set

{(G `),(abs (- 1))} is non empty set

{(G `)} is non empty set

{{(G `),(abs (- 1))},{(G `)}} is non empty set

(X) . [(G `),(abs (- 1))] is set

- (- 1) is V92() V93() integer ext-real non negative Element of INT

(X) . ((G `),(- (- 1))) is set

[(G `),(- (- 1))] is set

{(G `),(- (- 1))} is non empty set

{{(G `),(- (- 1))},{(G `)}} is non empty set

(X) . [(G `),(- (- 1))] is set

(X,1,(G `)) is Element of the carrier of X

(X) . ((G `),1) is set

[(G `),1] is set

{(G `),1} is non empty set

{{(G `),1},{(G `)}} is non empty set

(X) . [(G `),1] is set

2 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative 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

G is Element of the carrier of X

(X,2,G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (G,2) is set

[G,2] is set

{G,2} is non empty set

{G} is non empty set

{{G,2},{G}} is non empty set

(X) . [G,2] is set

G ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

G \ (G `) is Element of the carrier of X

the InternalDiff of X . (G,(G `)) is Element of the carrier of X

[G,(G `)] is set

{G,(G `)} is non empty set

{{G,(G `)},{G}} is non empty set

the InternalDiff of X . [G,(G `)] is set

1 + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(1 + 1),G) is Element of the carrier of X

(X) . (G,(1 + 1)) is set

[G,(1 + 1)] is set

{G,(1 + 1)} is non empty set

{{G,(1 + 1)},{G}} is non empty set

(X) . [G,(1 + 1)] is set

(X,1,G) is Element of the carrier of X

(X) . (G,1) is set

[G,1] is set

{G,1} is non empty set

{{G,1},{G}} is non empty set

(X) . [G,1] is set

(X,1,G) ` is Element of the carrier of X

(0. X) \ (X,1,G) is Element of the carrier of X

the InternalDiff of X . ((0. X),(X,1,G)) is Element of the carrier of X

[(0. X),(X,1,G)] is set

{(0. X),(X,1,G)} is non empty set

{{(0. X),(X,1,G)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(X,1,G)] is set

G \ ((X,1,G) `) is Element of the carrier of X

the InternalDiff of X . (G,((X,1,G) `)) is Element of the carrier of X

[G,((X,1,G) `)] is set

{G,((X,1,G) `)} is non empty set

{{G,((X,1,G) `)},{G}} is non empty set

the InternalDiff of X . [G,((X,1,G) `)] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

0. X is V47(X) atom positive nilpotent 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

G is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

(X,G,(0. X)) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . ((0. X),G) is set

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

(X) . [(0. X),G] is set

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

(X,K,(0. X)) is Element of the carrier of X

(X) . ((0. X),K) is set

[(0. X),K] is set

{(0. X),K} is non empty set

{{(0. X),K},{(0. X)}} is non empty set

(X) . [(0. X),K] is set

K + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(K + 1),(0. X)) is Element of the carrier of X

(X) . ((0. X),(K + 1)) is set

[(0. X),(K + 1)] is set

{(0. X),(K + 1)} is non empty set

{{(0. X),(K + 1)},{(0. X)}} is non empty set

(X) . [(0. X),(K + 1)] is set

(0. X) ` is Element of the carrier of X

(0. X) \ (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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X

[(0. X),(0. X)] is set

{(0. X),(0. X)} is non empty set

{{(0. X),(0. X)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(0. X)] is set

((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),((0. X) `)] is set

{(0. X),((0. X) `)} is non empty set

{{(0. X),((0. X) `)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),((0. X) `)] is set

(X,0,(0. X)) is Element of the carrier of X

(X) . ((0. X),0) is set

[(0. X),0] is set

{(0. X),0} is non empty set

{{(0. X),0},{(0. X)}} is non empty set

(X) . [(0. X),0] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

AtomSet X is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

G is Element of AtomSet X

(X,(- 1),G) is Element of the carrier of X

(X,(- 1),(X,(- 1),G)) is Element of the carrier of X

G ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

(X,(- 1),(G `)) is Element of the carrier of X

(G `) ` is Element of the carrier of X

(0. X) \ (G `) is Element of the carrier of X

the InternalDiff of X . ((0. X),(G `)) is Element of the carrier of X

[(0. X),(G `)] is set

{(0. X),(G `)} is non empty set

{{(0. X),(G `)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(G `)] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

G is Element of the carrier of X

G ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

(G `) ` is Element of the carrier of X

(0. X) \ (G `) is Element of the carrier of X

the InternalDiff of X . ((0. X),(G `)) is Element of the carrier of X

[(0. X),(G `)] is set

{(0. X),(G `)} is non empty set

{{(0. X),(G `)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),(G `)] is set

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

- K is V92() V93() integer ext-real non positive Element of INT

(X,(- K),G) is Element of the carrier of X

(X,(- K),((G `) `)) is Element of the carrier of X

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

- RK is V92() V93() integer ext-real non positive Element of INT

(X,(- RK),G) is Element of the carrier of X

(X,(- RK),((G `) `)) is Element of the carrier of X

RK + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

- (RK + 1) is V92() V93() integer ext-real non positive Element of INT

- (- (RK + 1)) is V92() V93() integer ext-real non negative Element of INT

(X,(- (RK + 1)),G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

abs (- (RK + 1)) is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

(X) . ((G `),(abs (- (RK + 1)))) is Element of the carrier of X

[(G `),(abs (- (RK + 1)))] is set

{(G `),(abs (- (RK + 1)))} is non empty set

{(G `)} is non empty set

{{(G `),(abs (- (RK + 1)))},{(G `)}} is non empty set

(X) . [(G `),(abs (- (RK + 1)))] is set

((G `) `) ` is Element of the carrier of X

(0. X) \ ((G `) `) is Element of the carrier of X

the InternalDiff of X . ((0. X),((G `) `)) is Element of the carrier of X

[(0. X),((G `) `)] is set

{(0. X),((G `) `)} is non empty set

{{(0. X),((G `) `)},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),((G `) `)] is set

(X) . ((((G `) `) `),(abs (- (RK + 1)))) is Element of the carrier of X

[(((G `) `) `),(abs (- (RK + 1)))] is set

{(((G `) `) `),(abs (- (RK + 1)))} is non empty set

{(((G `) `) `)} is non empty set

{{(((G `) `) `),(abs (- (RK + 1)))},{(((G `) `) `)}} is non empty set

(X) . [(((G `) `) `),(abs (- (RK + 1)))] is set

(X,(- (RK + 1)),((G `) `)) is Element of the carrier of X

(X,0,G) is Element of the carrier of X

(X) . (G,0) is set

[G,0] is set

{G,0} is non empty set

{G} is non empty set

{{G,0},{G}} is non empty set

(X) . [G,0] is set

(X,0,((G `) `)) is Element of the carrier of X

(X) . (((G `) `),0) is set

[((G `) `),0] is set

{((G `) `),0} is non empty set

{((G `) `)} is non empty set

{{((G `) `),0},{((G `) `)}} is non empty set

(X) . [((G `) `),0] is set

- 0 is empty V24() V25() V26() V28() V29() V30() V92() V93() integer ext-real non positive non negative Element of INT

(X,(- 0),G) is Element of the carrier of X

(X) . (G,(- 0)) is set

[G,(- 0)] is set

{G,(- 0)} is non empty set

{{G,(- 0)},{G}} is non empty set

(X) . [G,(- 0)] is set

(X,(- 0),((G `) `)) is Element of the carrier of X

(X) . (((G `) `),(- 0)) is set

[((G `) `),(- 0)] is set

{((G `) `),(- 0)} is non empty set

{{((G `) `),(- 0)},{((G `) `)}} is non empty set

(X) . [((G `) `),(- 0)] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

AtomSet X is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

G is Element of AtomSet X

G ` is Element of the carrier of X

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

(X,K,(G `)) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . ((G `),K) is set

[(G `),K] is set

{(G `),K} is non empty set

{(G `)} is non empty set

{{(G `),K},{(G `)}} is non empty set

(X) . [(G `),K] is set

- K is V92() V93() integer ext-real non positive Element of INT

(X,(- K),G) is Element of the carrier of X

- (- K) is V92() V93() integer ext-real non negative Element of INT

abs (- K) is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

(X) . ((G `),(abs (- K))) is Element of the carrier of X

[(G `),(abs (- K))] is set

{(G `),(abs (- K))} is non empty set

{{(G `),(abs (- K))},{(G `)}} is non empty set

(X) . [(G `),(abs (- K))] is set

(X) . ((G `),(- (- K))) is set

[(G `),(- (- K))] is set

{(G `),(- (- K))} is non empty set

{{(G `),(- (- K))},{(G `)}} is non empty set

(X) . [(G `),(- (- K))] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of bool the carrier of X

bool the carrier of X is set

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

{ b

G is Element of the carrier of X

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

(X,K,G) is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

(X) . (G,K) is set

[G,K] is set

{G,K} is non empty set

{G} is non empty set

{{G,K},{G}} is non empty set

(X) . [G,K] is set

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

(X,RK,G) is Element of the carrier of X

(X) . (G,RK) is set

[G,RK] is set

{G,RK} is non empty set

{{G,RK},{G}} is non empty set

(X) . [G,RK] is set

RK + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

(X,(RK + 1),G) is Element of the carrier of X

(X) . (G,(RK + 1)) is set

[G,(RK + 1)] is set

{G,(RK + 1)} is non empty set

{{G,(RK + 1)},{G}} is non empty set

(X) . [G,(RK + 1)] is set

G ` is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

G \ (G `) is Element of the carrier of X

the InternalDiff of X . (G,(G `)) is Element of the carrier of X

[G,(G `)] is set

{G,(G `)} is non empty set

{{G,(G `)},{G}} is non empty set

the InternalDiff of X . [G,(G `)] is set

G \ (0. X) is Element of the carrier of X

the InternalDiff of X . (G,(0. X)) is Element of the carrier of X

[G,(0. X)] is set

{G,(0. X)} is non empty set

{{G,(0. X)},{G}} is non empty set

the InternalDiff of X . [G,(0. X)] is set

K1 is Element of the carrier of X

(X,1,G) is Element of the carrier of X

(X) . (G,1) is set

[G,1] is set

{G,1} is non empty set

{{G,1},{G}} is non empty set

(X) . [G,1] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of bool the carrier of X

bool the carrier of X is set

0. X is V47(X) atom positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

{ b

G is Element of the carrier of X

K is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

- K is V92() V93() integer ext-real non positive Element of INT

(X,(- K),G) is Element of the carrier of X

RK is V24() V25() V26() V30() V92() V93() integer ext-real non negative set

- RK is V92() V93() integer ext-real non positive Element of INT

(X,(- RK),G) is Element of the carrier of X

RK + 1 is non empty V24() V25() V26() V30() V92() V93() integer ext-real positive non negative Element of NAT

- (RK + 1) is V92() V93() integer ext-real non positive Element of INT

- (- (RK + 1)) is V92() V93() integer ext-real non negative Element of INT

(X,(- (RK + 1)),G) is Element of the carrier of X

G ` is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

K1 is Element of the carrier of X

(X) is Relation-like [: the carrier of X,NAT:] -defined the carrier of X -valued Function-like V14([: the carrier of X,NAT:]) quasi_total Element of bool [:[: the carrier of X,NAT:], the carrier of X:]

[: the carrier of X,NAT:] is set

[:[: the carrier of X,NAT:], the carrier of X:] is set

bool [:[: the carrier of X,NAT:], the carrier of X:] is set

G ` is Element of the carrier of X

(0. X) \ G 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 V14([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),G) is Element of the carrier of X

[(0. X),G] is set

{(0. X),G} is non empty set

{(0. X)} is non empty set

{{(0. X),G},{(0. X)}} is non empty set

the InternalDiff of X . [(0. X),G] is set

abs (- RK) is V24() V25() V26() V30() V92() V93() integer ext-real non negative Element of NAT

(X) . ((G `),(abs (- RK))) is Element of the carrier of X

[(G `),(abs (- RK))] is set

{(G `),(abs (- RK))} is non empty set

{(G `)} is non empty set

{{(G `),(abs (- RK))},{(G `)}} is non empty set

(X) . [(G `),(abs (- RK))] is set

- (- RK) is V92() V93() integer ext-real non negative Element of INT

(X) . ((G `),(- (- RK))) is set

[(G `),(- (- RK))] is