:: BCIALG_6 semantic presentation

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

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

RAT is set
INT 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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
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

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

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
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

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,(),G) is Element of the carrier of X
(X) . (G,()) is set
[G,()] is set
{G,()} is non empty set
{{G,()},{G}} is non empty set
(X) . [G,()] is set
(X,(),((G `) `)) is Element of the carrier of X
(X) . (((G `) `),()) is set
[((G `) `),()] is set
{((G `) `),()} is non empty set
{{((G `) `),()},{((G `) `)}} is non empty set
(X) . [((G `) `),()] is set

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
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
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

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
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
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

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
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
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