:: GROUP_1 semantic presentation

REAL is V11() non trivial V46() set
NAT is V11() non trivial V32() V33() V34() V46() cardinal limit_cardinal Element of bool REAL
bool REAL is non trivial V46() set
0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element set
COMPLEX is V11() non trivial V46() set
RAT is V11() non trivial V46() set
INT is V11() non trivial V46() set
[:COMPLEX,COMPLEX:] is non trivial V46() set
bool [:COMPLEX,COMPLEX:] is non trivial V46() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V46() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V46() set
[:REAL,REAL:] is non trivial V46() set
bool [:REAL,REAL:] is non trivial V46() set
[:[:REAL,REAL:],REAL:] is non trivial V46() set
bool [:[:REAL,REAL:],REAL:] is non trivial V46() set
[:RAT,RAT:] is non trivial V46() set
bool [:RAT,RAT:] is non trivial V46() set
[:[:RAT,RAT:],RAT:] is non trivial V46() set
bool [:[:RAT,RAT:],RAT:] is non trivial V46() set
[:INT,INT:] is non trivial V46() set
bool [:INT,INT:] is non trivial V46() set
[:[:INT,INT:],INT:] is non trivial V46() set
bool [:[:INT,INT:],INT:] is non trivial V46() set
[:NAT,NAT:] is non trivial V46() set
[:[:NAT,NAT:],NAT:] is non trivial V46() set
bool [:[:NAT,NAT:],NAT:] is non trivial V46() set
NAT is V11() non trivial V32() V33() V34() V46() cardinal limit_cardinal set
bool NAT is non trivial V46() set
bool NAT is non trivial V46() set
1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of NAT
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V18([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
multMagma(# REAL,addreal #) is non empty non trivial strict multMagma
the carrier of multMagma(# REAL,addreal #) is V11() non trivial set
H is Element of the carrier of multMagma(# REAL,addreal #)
IT is Element of the carrier of multMagma(# REAL,addreal #)
H * IT is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) is Relation-like [: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):] -defined the carrier of multMagma(# REAL,addreal #) -valued Function-like V18([: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #)) Element of bool [:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):]
[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):] is set
[:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):] is set
bool [:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):] is set
the multF of multMagma(# REAL,addreal #) . (H,IT) is Element of the carrier of multMagma(# REAL,addreal #)
[H,IT] is set
the multF of multMagma(# REAL,addreal #) . [H,IT] is set
n is Element of the carrier of multMagma(# REAL,addreal #)
(H * IT) * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . ((H * IT),n) is Element of the carrier of multMagma(# REAL,addreal #)
[(H * IT),n] is set
the multF of multMagma(# REAL,addreal #) . [(H * IT),n] is set
IT * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (IT,n) is Element of the carrier of multMagma(# REAL,addreal #)
[IT,n] is set
the multF of multMagma(# REAL,addreal #) . [IT,n] is set
H * (IT * n) is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (H,(IT * n)) is Element of the carrier of multMagma(# REAL,addreal #)
[H,(IT * n)] is set
the multF of multMagma(# REAL,addreal #) . [H,(IT * n)] is set
c₆ is ext-real V39() V40() Element of REAL
y is ext-real V39() V40() Element of REAL
c₆ + y is ext-real V39() V40() Element of REAL
b is ext-real V39() V40() Element of REAL
b + c₆ is ext-real V39() V40() Element of REAL
(b + c₆) + y is ext-real V39() V40() Element of REAL
b + (c₆ + y) is ext-real V39() V40() Element of REAL
H is Element of the carrier of multMagma(# REAL,addreal #)
n is Element of the carrier of multMagma(# REAL,addreal #)
IT is Element of the carrier of multMagma(# REAL,addreal #)
n * IT is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) is Relation-like [: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):] -defined the carrier of multMagma(# REAL,addreal #) -valued Function-like V18([: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #)) Element of bool [:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):]
[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):] is set
[:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):] is set
bool [:[: the carrier of multMagma(# REAL,addreal #), the carrier of multMagma(# REAL,addreal #):], the carrier of multMagma(# REAL,addreal #):] is set
the multF of multMagma(# REAL,addreal #) . (n,IT) is Element of the carrier of multMagma(# REAL,addreal #)
[n,IT] is set
the multF of multMagma(# REAL,addreal #) . [n,IT] is set
b is ext-real V39() V40() Element of REAL
b + 0 is ext-real V39() V40() Element of REAL
IT * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (IT,n) is Element of the carrier of multMagma(# REAL,addreal #)
[IT,n] is set
the multF of multMagma(# REAL,addreal #) . [IT,n] is set
0 + b is ext-real V39() V40() Element of REAL
- b is ext-real V39() V40() Element of REAL
c₆ is Element of the carrier of multMagma(# REAL,addreal #)
y is Element of the carrier of multMagma(# REAL,addreal #)
n * y is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (n,y) is Element of the carrier of multMagma(# REAL,addreal #)
[n,y] is set
the multF of multMagma(# REAL,addreal #) . [n,y] is set
b + (- b) is ext-real V39() V40() Element of REAL
y * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (y,n) is Element of the carrier of multMagma(# REAL,addreal #)
[y,n] is set
the multF of multMagma(# REAL,addreal #) . [y,n] is set
(- b) + b is ext-real V39() V40() Element of REAL
G is multMagma
the carrier of G is set
H is Element of the carrier of G
G is Element of the carrier of multMagma(# REAL,addreal #)
G is non empty multMagma
the carrier of G is V11() set
H is Element of the carrier of G
G is non empty multMagma
the carrier of G is V11() set
the Element of the carrier of G is Element of the carrier of G
IT is Element of the carrier of G
the Element of the carrier of G * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ( the Element of the carrier of G,IT) is Element of the carrier of G
[ the Element of the carrier of G,IT] is set
the multF of G . [ the Element of the carrier of G,IT] is set
n is Element of the carrier of G
b is Element of the carrier of G
n * b is Element of the carrier of G
the multF of G . (n,b) is Element of the carrier of G
[n,b] is set
the multF of G . [n,b] is set
c₆ is Element of the carrier of G
(n * b) * c₆ is Element of the carrier of G
the multF of G . ((n * b),c₆) is Element of the carrier of G
[(n * b),c₆] is set
the multF of G . [(n * b),c₆] is set
b * c₆ is Element of the carrier of G
the multF of G . (b,c₆) is Element of the carrier of G
[b,c₆] is set
the multF of G . [b,c₆] is set
n * (b * c₆) is Element of the carrier of G
the multF of G . (n,(b * c₆)) is Element of the carrier of G
[n,(b * c₆)] is set
the multF of G . [n,(b * c₆)] is set
n is Element of the carrier of G
n * IT is Element of the carrier of G
the multF of G . (n,IT) is Element of the carrier of G
[n,IT] is set
the multF of G . [n,IT] is set
IT * n is Element of the carrier of G
the multF of G . (IT,n) is Element of the carrier of G
[IT,n] is set
the multF of G . [IT,n] is set
b is Element of the carrier of G
b * the Element of the carrier of G is Element of the carrier of G
the multF of G . (b, the Element of the carrier of G) is Element of the carrier of G
[b, the Element of the carrier of G] is set
the multF of G . [b, the Element of the carrier of G] is set
b is Element of the carrier of G
b * the Element of the carrier of G is Element of the carrier of G
the multF of G . (b, the Element of the carrier of G) is Element of the carrier of G
[b, the Element of the carrier of G] is set
the multF of G . [b, the Element of the carrier of G] is set
c₆ is Element of the carrier of G
the Element of the carrier of G * c₆ is Element of the carrier of G
the multF of G . ( the Element of the carrier of G,c₆) is Element of the carrier of G
[ the Element of the carrier of G,c₆] is set
the multF of G . [ the Element of the carrier of G,c₆] is set
b * ( the Element of the carrier of G * c₆) is Element of the carrier of G
the multF of G . (b,( the Element of the carrier of G * c₆)) is Element of the carrier of G
[b,( the Element of the carrier of G * c₆)] is set
the multF of G . [b,( the Element of the carrier of G * c₆)] is set
y is Element of the carrier of G
y * the Element of the carrier of G is Element of the carrier of G
the multF of G . (y, the Element of the carrier of G) is Element of the carrier of G
[y, the Element of the carrier of G] is set
the multF of G . [y, the Element of the carrier of G] is set
y is Element of the carrier of G
the Element of the carrier of G * y is Element of the carrier of G
the multF of G . ( the Element of the carrier of G,y) is Element of the carrier of G
[ the Element of the carrier of G,y] is set
the multF of G . [ the Element of the carrier of G,y] is set
y is Element of the carrier of G
n * y is Element of the carrier of G
the multF of G . (n,y) is Element of the carrier of G
[n,y] is set
the multF of G . [n,y] is set
z is Element of the carrier of G
z * n is Element of the carrier of G
the multF of G . (z,n) is Element of the carrier of G
[z,n] is set
the multF of G . [z,n] is set
y * n is Element of the carrier of G
the multF of G . (y,n) is Element of the carrier of G
[y,n] is set
the multF of G . [y,n] is set
r1 is Element of the carrier of G
n * r1 is Element of the carrier of G
the multF of G . (n,r1) is Element of the carrier of G
[n,r1] is set
the multF of G . [n,r1] is set
IT * (n * r1) is Element of the carrier of G
the multF of G . (IT,(n * r1)) is Element of the carrier of G
[IT,(n * r1)] is set
the multF of G . [IT,(n * r1)] is set
z * (n * y) is Element of the carrier of G
the multF of G . (z,(n * y)) is Element of the carrier of G
[z,(n * y)] is set
the multF of G . [z,(n * y)] is set
c₁₀ is Element of the carrier of G
c₁₀ * n is Element of the carrier of G
the multF of G . (c₁₀,n) is Element of the carrier of G
[c₁₀,n] is set
the multF of G . [c₁₀,n] is set
H is Element of the carrier of multMagma(# REAL,addreal #)
IT is Element of the carrier of multMagma(# REAL,addreal #)
H * IT is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (H,IT) is Element of the carrier of multMagma(# REAL,addreal #)
[H,IT] is set
the multF of multMagma(# REAL,addreal #) . [H,IT] is set
n is Element of the carrier of multMagma(# REAL,addreal #)
(H * IT) * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . ((H * IT),n) is Element of the carrier of multMagma(# REAL,addreal #)
[(H * IT),n] is set
the multF of multMagma(# REAL,addreal #) . [(H * IT),n] is set
IT * n is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (IT,n) is Element of the carrier of multMagma(# REAL,addreal #)
[IT,n] is set
the multF of multMagma(# REAL,addreal #) . [IT,n] is set
H * (IT * n) is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (H,(IT * n)) is Element of the carrier of multMagma(# REAL,addreal #)
[H,(IT * n)] is set
the multF of multMagma(# REAL,addreal #) . [H,(IT * n)] is set
c₆ is ext-real V39() V40() Element of REAL
y is ext-real V39() V40() Element of REAL
c₆ + y is ext-real V39() V40() Element of REAL
b is ext-real V39() V40() Element of REAL
b + c₆ is ext-real V39() V40() Element of REAL
(b + c₆) + y is ext-real V39() V40() Element of REAL
b + (c₆ + y) is ext-real V39() V40() Element of REAL
H is Element of the carrier of multMagma(# REAL,addreal #)
IT is Element of the carrier of multMagma(# REAL,addreal #)
IT * H is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (IT,H) is Element of the carrier of multMagma(# REAL,addreal #)
[IT,H] is set
the multF of multMagma(# REAL,addreal #) . [IT,H] is set
H * IT is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (H,IT) is Element of the carrier of multMagma(# REAL,addreal #)
[H,IT] is set
the multF of multMagma(# REAL,addreal #) . [H,IT] is set
n is ext-real V39() V40() Element of REAL
n + 0 is ext-real V39() V40() Element of REAL
0 + n is ext-real V39() V40() Element of REAL
- n is ext-real V39() V40() Element of REAL
b is Element of the carrier of multMagma(# REAL,addreal #)
IT * b is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (IT,b) is Element of the carrier of multMagma(# REAL,addreal #)
[IT,b] is set
the multF of multMagma(# REAL,addreal #) . [IT,b] is set
b * IT is Element of the carrier of multMagma(# REAL,addreal #)
the multF of multMagma(# REAL,addreal #) . (b,IT) is Element of the carrier of multMagma(# REAL,addreal #)
[b,IT] is set
the multF of multMagma(# REAL,addreal #) . [b,IT] is set
n + (- n) is ext-real V39() V40() Element of REAL
(- n) + n is ext-real V39() V40() Element of REAL
G is multMagma
the carrier of G is set
H is Element of the carrier of G
IT is Element of the carrier of G
IT * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
G is non empty () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G) is Element of the carrier of G
IT is Element of the carrier of G
n is Element of the carrier of G
H * n is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,n) is Element of the carrier of G
[H,n] is set
the multF of G . [H,n] is set
n * H is Element of the carrier of G
the multF of G . (n,H) is Element of the carrier of G
[n,H] is set
the multF of G . [n,H] is set
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
n is Element of the carrier of G
H * n is Element of the carrier of G
the multF of G . (H,n) is Element of the carrier of G
[H,n] is set
the multF of G . [H,n] is set
n * H is Element of the carrier of G
the multF of G . (n,H) is Element of the carrier of G
[n,H] is set
the multF of G . [n,H] is set
(G) * IT is Element of the carrier of G
the multF of G . ((G),IT) is Element of the carrier of G
[(G),IT] is set
the multF of G . [(G),IT] is set
n * (H * IT) is Element of the carrier of G
the multF of G . (n,(H * IT)) is Element of the carrier of G
[n,(H * IT)] is set
the multF of G . [n,(H * IT)] is set
n is Element of the carrier of G
IT is Element of the carrier of G
n * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (n,IT) is Element of the carrier of G
[n,IT] is set
the multF of G . [n,IT] is set
IT * n is Element of the carrier of G
the multF of G . (IT,n) is Element of the carrier of G
[IT,n] is set
the multF of G . [IT,n] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
(G) is Element of the carrier of G
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
(G,H) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
n is Element of the carrier of G
H * n is Element of the carrier of G
the multF of G . (H,n) is Element of the carrier of G
[H,n] is set
the multF of G . [H,n] is set
n * H is Element of the carrier of G
the multF of G . (n,H) is Element of the carrier of G
[n,H] is set
the multF of G . [n,H] is set
(G,H) is Element of the carrier of G
(G,H) * (H * IT) is Element of the carrier of G
the multF of G . ((G,H),(H * IT)) is Element of the carrier of G
[(G,H),(H * IT)] is set
the multF of G . [(G,H),(H * IT)] is set
(G,H) * H is Element of the carrier of G
the multF of G . ((G,H),H) is Element of the carrier of G
[(G,H),H] is set
the multF of G . [(G,H),H] is set
((G,H) * H) * n is Element of the carrier of G
the multF of G . (((G,H) * H),n) is Element of the carrier of G
[((G,H) * H),n] is set
the multF of G . [((G,H) * H),n] is set
(IT * H) * (G,H) is Element of the carrier of G
the multF of G . ((IT * H),(G,H)) is Element of the carrier of G
[(IT * H),(G,H)] is set
the multF of G . [(IT * H),(G,H)] is set
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
n * (H * (G,H)) is Element of the carrier of G
the multF of G . (n,(H * (G,H))) is Element of the carrier of G
[n,(H * (G,H))] is set
the multF of G . [n,(H * (G,H))] is set
(G) is Element of the carrier of G
(G) * n is Element of the carrier of G
the multF of G . ((G),n) is Element of the carrier of G
[(G),n] is set
the multF of G . [(G),n] is set
IT * (H * (G,H)) is Element of the carrier of G
the multF of G . (IT,(H * (G,H))) is Element of the carrier of G
[IT,(H * (G,H))] is set
the multF of G . [IT,(H * (G,H))] is set
IT * (G) is Element of the carrier of G
the multF of G . (IT,(G)) is Element of the carrier of G
[IT,(G)] is set
the multF of G . [IT,(G)] is set
((G,H) * H) * IT is Element of the carrier of G
the multF of G . (((G,H) * H),IT) is Element of the carrier of G
[((G,H) * H),IT] is set
the multF of G . [((G,H) * H),IT] is set
n * (G) is Element of the carrier of G
the multF of G . (n,(G)) is Element of the carrier of G
[n,(G)] is set
the multF of G . [n,(G)] is set
(G) * IT is Element of the carrier of G
the multF of G . ((G),IT) is Element of the carrier of G
[(G),IT] is set
the multF of G . [(G),IT] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Element of the carrier of G
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
H * (G) is Element of the carrier of G
the multF of G . (H,(G)) is Element of the carrier of G
[H,(G)] is set
the multF of G . [H,(G)] is set
(G) * H is Element of the carrier of G
the multF of G . ((G),H) is Element of the carrier of G
[(G),H] is set
the multF of G . [(G),H] is set
G is non empty () () () multMagma
(G) is Element of the carrier of G
the carrier of G is V11() set
(G,(G)) is Element of the carrier of G
(G,(G)) * (G) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((G,(G)),(G)) is Element of the carrier of G
[(G,(G)),(G)] is set
the multF of G . [(G,(G)),(G)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
(G,IT) is Element of the carrier of G
H * (G,IT) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(G,IT)) is Element of the carrier of G
[H,(G,IT)] is set
the multF of G . [H,(G,IT)] is set
(G) is Element of the carrier of G
IT * (G,IT) is Element of the carrier of G
the multF of G . (IT,(G,IT)) is Element of the carrier of G
[IT,(G,IT)] is set
the multF of G . [IT,(G,IT)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Element of the carrier of G
H is Element of the carrier of G
(G,H) is Element of the carrier of G
(G,(G)) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Element of the carrier of G
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
(G,IT) is Element of the carrier of G
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
(G,IT) * IT is Element of the carrier of G
the multF of G . ((G,IT),IT) is Element of the carrier of G
[(G,IT),IT] is set
the multF of G . [(G,IT),IT] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
n is Element of the carrier of G
(G,H) * n is Element of the carrier of G
the multF of G . ((G,H),n) is Element of the carrier of G
[(G,H),n] is set
the multF of G . [(G,H),n] is set
H * ((G,H) * n) is Element of the carrier of G
the multF of G . (H,((G,H) * n)) is Element of the carrier of G
[H,((G,H) * n)] is set
the multF of G . [H,((G,H) * n)] is set
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
(H * (G,H)) * n is Element of the carrier of G
the multF of G . ((H * (G,H)),n) is Element of the carrier of G
[(H * (G,H)),n] is set
the multF of G . [(H * (G,H)),n] is set
(G) is Element of the carrier of G
(G) * n is Element of the carrier of G
the multF of G . ((G),n) is Element of the carrier of G
[(G),n] is set
the multF of G . [(G),n] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
(G,IT) is Element of the carrier of G
n is Element of the carrier of G
n * (G,IT) is Element of the carrier of G
the multF of G . (n,(G,IT)) is Element of the carrier of G
[n,(G,IT)] is set
the multF of G . [n,(G,IT)] is set
(n * (G,IT)) * IT is Element of the carrier of G
the multF of G . ((n * (G,IT)),IT) is Element of the carrier of G
[(n * (G,IT)),IT] is set
the multF of G . [(n * (G,IT)),IT] is set
(G,IT) * IT is Element of the carrier of G
the multF of G . ((G,IT),IT) is Element of the carrier of G
[(G,IT),IT] is set
the multF of G . [(G,IT),IT] is set
n * ((G,IT) * IT) is Element of the carrier of G
the multF of G . (n,((G,IT) * IT)) is Element of the carrier of G
[n,((G,IT) * IT)] is set
the multF of G . [n,((G,IT) * IT)] is set
(G) is Element of the carrier of G
n * (G) is Element of the carrier of G
the multF of G . (n,(G)) is Element of the carrier of G
[n,(G)] is set
the multF of G . [n,(G)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
(G,H) is Element of the carrier of G
(G,H) * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((G,H),IT) is Element of the carrier of G
[(G,H),IT] is set
the multF of G . [(G,H),IT] is set
H * ((G,H) * IT) is Element of the carrier of G
the multF of G . (H,((G,H) * IT)) is Element of the carrier of G
[H,((G,H) * IT)] is set
the multF of G . [H,((G,H) * IT)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
(G,H) is Element of the carrier of G
IT * (G,H) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (IT,(G,H)) is Element of the carrier of G
[IT,(G,H)] is set
the multF of G . [IT,(G,H)] is set
(IT * (G,H)) * H is Element of the carrier of G
the multF of G . ((IT * (G,H)),H) is Element of the carrier of G
[(IT * (G,H)),H] is set
the multF of G . [(IT * (G,H)),H] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
(G,(H * IT)) is Element of the carrier of G
(G,IT) is Element of the carrier of G
(G,IT) * (G,H) is Element of the carrier of G
the multF of G . ((G,IT),(G,H)) is Element of the carrier of G
[(G,IT),(G,H)] is set
the multF of G . [(G,IT),(G,H)] is set
((G,IT) * (G,H)) * (H * IT) is Element of the carrier of G
the multF of G . (((G,IT) * (G,H)),(H * IT)) is Element of the carrier of G
[((G,IT) * (G,H)),(H * IT)] is set
the multF of G . [((G,IT) * (G,H)),(H * IT)] is set
((G,IT) * (G,H)) * H is Element of the carrier of G
the multF of G . (((G,IT) * (G,H)),H) is Element of the carrier of G
[((G,IT) * (G,H)),H] is set
the multF of G . [((G,IT) * (G,H)),H] is set
(((G,IT) * (G,H)) * H) * IT is Element of the carrier of G
the multF of G . ((((G,IT) * (G,H)) * H),IT) is Element of the carrier of G
[(((G,IT) * (G,H)) * H),IT] is set
the multF of G . [(((G,IT) * (G,H)) * H),IT] is set
(G,H) * H is Element of the carrier of G
the multF of G . ((G,H),H) is Element of the carrier of G
[(G,H),H] is set
the multF of G . [(G,H),H] is set
(G,IT) * ((G,H) * H) is Element of the carrier of G
the multF of G . ((G,IT),((G,H) * H)) is Element of the carrier of G
[(G,IT),((G,H) * H)] is set
the multF of G . [(G,IT),((G,H) * H)] is set
((G,IT) * ((G,H) * H)) * IT is Element of the carrier of G
the multF of G . (((G,IT) * ((G,H) * H)),IT) is Element of the carrier of G
[((G,IT) * ((G,H) * H)),IT] is set
the multF of G . [((G,IT) * ((G,H) * H)),IT] is set
(G) is Element of the carrier of G
(G,IT) * (G) is Element of the carrier of G
the multF of G . ((G,IT),(G)) is Element of the carrier of G
[(G,IT),(G)] is set
the multF of G . [(G,IT),(G)] is set
((G,IT) * (G)) * IT is Element of the carrier of G
the multF of G . (((G,IT) * (G)),IT) is Element of the carrier of G
[((G,IT) * (G)),IT] is set
the multF of G . [((G,IT) * (G)),IT] is set
(G,IT) * IT is Element of the carrier of G
the multF of G . ((G,IT),IT) is Element of the carrier of G
[(G,IT),IT] is set
the multF of G . [(G,IT),IT] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
(G,(H * IT)) is Element of the carrier of G
(G,IT) is Element of the carrier of G
(G,H) * (G,IT) is Element of the carrier of G
the multF of G . ((G,H),(G,IT)) is Element of the carrier of G
[(G,H),(G,IT)] is set
the multF of G . [(G,H),(G,IT)] is set
(IT * H) * (G,(H * IT)) is Element of the carrier of G
the multF of G . ((IT * H),(G,(H * IT))) is Element of the carrier of G
[(IT * H),(G,(H * IT))] is set
the multF of G . [(IT * H),(G,(H * IT))] is set
(IT * H) * (G,H) is Element of the carrier of G
the multF of G . ((IT * H),(G,H)) is Element of the carrier of G
[(IT * H),(G,H)] is set
the multF of G . [(IT * H),(G,H)] is set
((IT * H) * (G,H)) * (G,IT) is Element of the carrier of G
the multF of G . (((IT * H) * (G,H)),(G,IT)) is Element of the carrier of G
[((IT * H) * (G,H)),(G,IT)] is set
the multF of G . [((IT * H) * (G,H)),(G,IT)] is set
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
IT * (H * (G,H)) is Element of the carrier of G
the multF of G . (IT,(H * (G,H))) is Element of the carrier of G
[IT,(H * (G,H))] is set
the multF of G . [IT,(H * (G,H))] is set
(IT * (H * (G,H))) * (G,IT) is Element of the carrier of G
the multF of G . ((IT * (H * (G,H))),(G,IT)) is Element of the carrier of G
[(IT * (H * (G,H))),(G,IT)] is set
the multF of G . [(IT * (H * (G,H))),(G,IT)] is set
(G) is Element of the carrier of G
IT * (G) is Element of the carrier of G
the multF of G . (IT,(G)) is Element of the carrier of G
[IT,(G)] is set
the multF of G . [IT,(G)] is set
(IT * (G)) * (G,IT) is Element of the carrier of G
the multF of G . ((IT * (G)),(G,IT)) is Element of the carrier of G
[(IT * (G)),(G,IT)] is set
the multF of G . [(IT * (G)),(G,IT)] is set
IT * (G,IT) is Element of the carrier of G
the multF of G . (IT,(G,IT)) is Element of the carrier of G
[IT,(G,IT)] is set
the multF of G . [IT,(G,IT)] is set
(H * IT) * (G,(H * IT)) is Element of the carrier of G
the multF of G . ((H * IT),(G,(H * IT))) is Element of the carrier of G
[(H * IT),(G,(H * IT))] is set
the multF of G . [(H * IT),(G,(H * IT))] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,H) is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
(G,IT) is Element of the carrier of G
(G,H) * (G,IT) is Element of the carrier of G
the multF of G . ((G,H),(G,IT)) is Element of the carrier of G
[(G,H),(G,IT)] is set
the multF of G . [(G,H),(G,IT)] is set
(G,IT) * (G,H) is Element of the carrier of G
the multF of G . ((G,IT),(G,H)) is Element of the carrier of G
[(G,IT),(G,H)] is set
the multF of G . [(G,IT),(G,H)] is set
(G,(H * IT)) is Element of the carrier of G
(G,(H * IT)) is Element of the carrier of G
(G,(G,(H * IT))) is Element of the carrier of G
(G,((G,IT) * (G,H))) is Element of the carrier of G
(G,(G,IT)) is Element of the carrier of G
(G,(G,H)) is Element of the carrier of G
(G,(G,IT)) * (G,(G,H)) is Element of the carrier of G
the multF of G . ((G,(G,IT)),(G,(G,H))) is Element of the carrier of G
[(G,(G,IT)),(G,(G,H))] is set
the multF of G . [(G,(G,IT)),(G,(G,H))] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
(G,IT) is Element of the carrier of G
H * (G,IT) is Element of the carrier of G
the multF of G . (H,(G,IT)) is Element of the carrier of G
[H,(G,IT)] is set
the multF of G . [H,(G,IT)] is set
(G,IT) * H is Element of the carrier of G
the multF of G . ((G,IT),H) is Element of the carrier of G
[(G,IT),H] is set
the multF of G . [(G,IT),H] is set
(G,H) is Element of the carrier of G
(G,H) * IT is Element of the carrier of G
the multF of G . ((G,H),IT) is Element of the carrier of G
[(G,H),IT] is set
the multF of G . [(G,H),IT] is set
(H * (G,IT)) * ((G,H) * IT) is Element of the carrier of G
the multF of G . ((H * (G,IT)),((G,H) * IT)) is Element of the carrier of G
[(H * (G,IT)),((G,H) * IT)] is set
the multF of G . [(H * (G,IT)),((G,H) * IT)] is set
(H * (G,IT)) * (G,H) is Element of the carrier of G
the multF of G . ((H * (G,IT)),(G,H)) is Element of the carrier of G
[(H * (G,IT)),(G,H)] is set
the multF of G . [(H * (G,IT)),(G,H)] is set
((H * (G,IT)) * (G,H)) * IT is Element of the carrier of G
the multF of G . (((H * (G,IT)) * (G,H)),IT) is Element of the carrier of G
[((H * (G,IT)) * (G,H)),IT] is set
the multF of G . [((H * (G,IT)) * (G,H)),IT] is set
(G,IT) * (G,H) is Element of the carrier of G
the multF of G . ((G,IT),(G,H)) is Element of the carrier of G
[(G,IT),(G,H)] is set
the multF of G . [(G,IT),(G,H)] is set
H * ((G,IT) * (G,H)) is Element of the carrier of G
the multF of G . (H,((G,IT) * (G,H))) is Element of the carrier of G
[H,((G,IT) * (G,H))] is set
the multF of G . [H,((G,IT) * (G,H))] is set
(H * ((G,IT) * (G,H))) * IT is Element of the carrier of G
the multF of G . ((H * ((G,IT) * (G,H))),IT) is Element of the carrier of G
[(H * ((G,IT) * (G,H))),IT] is set
the multF of G . [(H * ((G,IT) * (G,H))),IT] is set
(G,H) * (G,IT) is Element of the carrier of G
the multF of G . ((G,H),(G,IT)) is Element of the carrier of G
[(G,H),(G,IT)] is set
the multF of G . [(G,H),(G,IT)] is set
H * ((G,H) * (G,IT)) is Element of the carrier of G
the multF of G . (H,((G,H) * (G,IT))) is Element of the carrier of G
[H,((G,H) * (G,IT))] is set
the multF of G . [H,((G,H) * (G,IT))] is set
(H * ((G,H) * (G,IT))) * IT is Element of the carrier of G
the multF of G . ((H * ((G,H) * (G,IT))),IT) is Element of the carrier of G
[(H * ((G,H) * (G,IT))),IT] is set
the multF of G . [(H * ((G,H) * (G,IT))),IT] is set
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
(H * (G,H)) * (G,IT) is Element of the carrier of G
the multF of G . ((H * (G,H)),(G,IT)) is Element of the carrier of G
[(H * (G,H)),(G,IT)] is set
the multF of G . [(H * (G,H)),(G,IT)] is set
((H * (G,H)) * (G,IT)) * IT is Element of the carrier of G
the multF of G . (((H * (G,H)) * (G,IT)),IT) is Element of the carrier of G
[((H * (G,H)) * (G,IT)),IT] is set
the multF of G . [((H * (G,H)) * (G,IT)),IT] is set
(G) is Element of the carrier of G
(G) * (G,IT) is Element of the carrier of G
the multF of G . ((G),(G,IT)) is Element of the carrier of G
[(G),(G,IT)] is set
the multF of G . [(G),(G,IT)] is set
((G) * (G,IT)) * IT is Element of the carrier of G
the multF of G . (((G) * (G,IT)),IT) is Element of the carrier of G
[((G) * (G,IT)),IT] is set
the multF of G . [((G) * (G,IT)),IT] is set
(G,IT) * IT is Element of the carrier of G
the multF of G . ((G,IT),IT) is Element of the carrier of G
[(G,IT),IT] is set
the multF of G . [(G,IT),IT] is set
(G,((G,H) * IT)) is Element of the carrier of G
(G,(G,H)) is Element of the carrier of G
(G,IT) * (G,(G,H)) is Element of the carrier of G
the multF of G . ((G,IT),(G,(G,H))) is Element of the carrier of G
[(G,IT),(G,(G,H))] is set
the multF of G . [(G,IT),(G,(G,H))] is set
(G,IT) * IT is Element of the carrier of G
the multF of G . ((G,IT),IT) is Element of the carrier of G
[(G,IT),IT] is set
the multF of G . [(G,IT),IT] is set
H * ((G,IT) * IT) is Element of the carrier of G
the multF of G . (H,((G,IT) * IT)) is Element of the carrier of G
[H,((G,IT) * IT)] is set
the multF of G . [H,((G,IT) * IT)] is set
((G,IT) * H) * IT is Element of the carrier of G
the multF of G . (((G,IT) * H),IT) is Element of the carrier of G
[((G,IT) * H),IT] is set
the multF of G . [((G,IT) * H),IT] is set
(G) is Element of the carrier of G
H * (G) is Element of the carrier of G
the multF of G . (H,(G)) is Element of the carrier of G
[H,(G)] is set
the multF of G . [H,(G)] is set
(G,IT) * (H * IT) is Element of the carrier of G
the multF of G . ((G,IT),(H * IT)) is Element of the carrier of G
[(G,IT),(H * IT)] is set
the multF of G . [(G,IT),(H * IT)] is set
IT * (G,IT) is Element of the carrier of G
the multF of G . (IT,(G,IT)) is Element of the carrier of G
[IT,(G,IT)] is set
the multF of G . [IT,(G,IT)] is set
(IT * (G,IT)) * (H * IT) is Element of the carrier of G
the multF of G . ((IT * (G,IT)),(H * IT)) is Element of the carrier of G
[(IT * (G,IT)),(H * IT)] is set
the multF of G . [(IT * (G,IT)),(H * IT)] is set
(G) * (H * IT) is Element of the carrier of G
the multF of G . ((G),(H * IT)) is Element of the carrier of G
[(G),(H * IT)] is set
the multF of G . [(G),(H * IT)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
H is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
IT is Element of the carrier of G
H . IT is Element of the carrier of G
(G,IT) is Element of the carrier of G
H is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
IT is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
n is Element of the carrier of G
H . n is set
IT . n is set
H . n is Element of the carrier of G
(G,n) is Element of the carrier of G
IT . n is Element of the carrier of G
G is non empty () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
H is Element of the carrier of G
IT is Element of the carrier of G
n is Element of the carrier of G
the multF of G . (IT,n) is Element of the carrier of G
[IT,n] is set
the multF of G . [IT,n] is set
the multF of G . (H,( the multF of G . (IT,n))) is Element of the carrier of G
[H,( the multF of G . (IT,n))] is set
the multF of G . [H,( the multF of G . (IT,n))] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
the multF of G . (( the multF of G . (H,IT)),n) is Element of the carrier of G
[( the multF of G . (H,IT)),n] is set
the multF of G . [( the multF of G . (H,IT)),n] is set
the multF of G . (IT,n) is Element of the carrier of G
the multF of G . (H,( the multF of G . (IT,n))) is Element of the carrier of G
[H,( the multF of G . (IT,n))] is set
the multF of G . [H,( the multF of G . (IT,n))] is set
IT * n is Element of the carrier of G
H * (IT * n) is Element of the carrier of G
the multF of G . (H,(IT * n)) is Element of the carrier of G
[H,(IT * n)] is set
the multF of G . [H,(IT * n)] is set
H * IT is Element of the carrier of G
the multF of G . (H,IT) is Element of the carrier of G
(H * IT) * n is Element of the carrier of G
the multF of G . ((H * IT),n) is Element of the carrier of G
[(H * IT),n] is set
the multF of G . [(H * IT),n] is set
the multF of G . (( the multF of G . (H,IT)),n) is Element of the carrier of G
[( the multF of G . (H,IT)),n] is set
the multF of G . [( the multF of G . (H,IT)),n] is set
G is non empty () multMagma
the carrier of G is V11() set
(G) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
IT is Element of the carrier of G
the multF of G . ((G),IT) is Element of the carrier of G
[(G),IT] is set
the multF of G . [(G),IT] is set
(G) * IT is Element of the carrier of G
the multF of G . (IT,(G)) is Element of the carrier of G
[IT,(G)] is set
the multF of G . [IT,(G)] is set
IT * (G) is Element of the carrier of G
G is non empty () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the_unity_wrt the multF of G is Element of the carrier of G
(G) is Element of the carrier of G
G is non empty () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
(G) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
H is Element of the carrier of G
(G) . H is Element of the carrier of G
the multF of G . (H,((G) . H)) is Element of the carrier of G
[H,((G) . H)] is set
the multF of G . [H,((G) . H)] is set
the_unity_wrt the multF of G is Element of the carrier of G
the multF of G . (((G) . H),H) is Element of the carrier of G
[((G) . H),H] is set
the multF of G . [((G) . H),H] is set
(G,H) is Element of the carrier of G
H * (G,H) is Element of the carrier of G
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
(G) is Element of the carrier of G
(G,H) * H is Element of the carrier of G
the multF of G . ((G,H),H) is Element of the carrier of G
[(G,H),H] is set
the multF of G . [(G,H),H] is set
G is non empty () () () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
(G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
G is non empty () () () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the_inverseOp_wrt the multF of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
(G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty multMagma
the carrier of G is V11() set
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) is Element of the carrier of G
[:NAT, the carrier of G:] is non trivial V46() set
bool [:NAT, the carrier of G:] is non trivial V46() set
H is set
IT is Element of the carrier of G
n is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
n . 0 is Element of the carrier of G
b is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
c₆ + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n . (c₆ + 1) is Element of the carrier of G
n . c₆ is Element of the carrier of G
(n . c₆) * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((n . c₆),IT) is Element of the carrier of G
[(n . c₆),IT] is set
the multF of G . [(n . c₆),IT] is set
H is Relation-like Function-like set
dom H is set
IT is Element of the carrier of G
H . IT is set
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
c₆ is Element of the carrier of G
b is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
b . 0 is Element of the carrier of G
b . n is Element of the carrier of G
IT is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
n is Element of the carrier of G
IT . (n,0) is Element of the carrier of G
[n,0] is set
IT . [n,0] is set
H . n is set
b is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
b . 0 is Element of the carrier of G
y is Element of the carrier of G
c₆ is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
c₆ . 0 is Element of the carrier of G
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
b + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
IT . (n,(b + 1)) is Element of the carrier of G
[n,(b + 1)] is set
IT . [n,(b + 1)] is set
IT . (n,b) is Element of the carrier of G
[n,b] is set
IT . [n,b] is set
(IT . (n,b)) * n is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((IT . (n,b)),n) is Element of the carrier of G
[(IT . (n,b)),n] is set
the multF of G . [(IT . (n,b)),n] is set
c₆ is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
c₆ . b is Element of the carrier of G
y is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
y . (b + 1) is Element of the carrier of G
r1 is Element of the carrier of G
z is Relation-like NAT -defined the carrier of G -valued Function-like V18( NAT , the carrier of G) Element of bool [:NAT, the carrier of G:]
z . 0 is Element of the carrier of G
H is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
IT is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
n is Element of the carrier of G
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
[n,c₆] is set
H . [n,c₆] is set
IT . [n,c₆] is set
IT . (n,c₆) is Element of the carrier of G
c₆ + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
[n,(c₆ + 1)] is set
H . [n,(c₆ + 1)] is set
H . (n,(c₆ + 1)) is Element of the carrier of G
H . (n,c₆) is Element of the carrier of G
(H . (n,c₆)) * n is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((H . (n,c₆)),n) is Element of the carrier of G
[(H . (n,c₆)),n] is set
the multF of G . [(H . (n,c₆)),n] is set
IT . (n,(c₆ + 1)) is Element of the carrier of G
IT . [n,(c₆ + 1)] is set
[n,0] is set
H . [n,0] is set
H . (n,0) is Element of the carrier of G
IT . (n,0) is Element of the carrier of G
IT . [n,0] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
H . (n,b) is Element of the carrier of G
[n,b] is set
H . [n,b] is set
IT . (n,b) is Element of the carrier of G
IT . [n,b] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is ext-real V39() V40() integer set
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
IT is Element of the carrier of G
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G) . (IT,(abs H)) is Element of the carrier of G
[IT,(abs H)] is set
(G) . [IT,(abs H)] is set
(G,((G) . (IT,(abs H)))) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
IT is Element of the carrier of G
(G,H,IT) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (IT,H) is set
[IT,H] is set
(G) . [IT,H] is set
n is Element of the carrier of G
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
G + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(G + 1),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(G + 1)) is set
[IT,(G + 1)] is set
(H) . [IT,(G + 1)] is set
(H,G,IT) is Element of the carrier of H
(H) . (IT,G) is set
[IT,G] is set
(H) . [IT,G] is set
(H,G,IT) * IT is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,G,IT),IT) is Element of the carrier of H
[(H,G,IT),IT] is set
the multF of H . [(H,G,IT),IT] is set
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(n + 1),IT) is Element of the carrier of H
(H) . (IT,(n + 1)) is set
[IT,(n + 1)] is set
(H) . [IT,(n + 1)] is set
(H,n,IT) is Element of the carrier of H
(H) . (IT,n) is set
[IT,n] is set
(H) . [IT,n] is set
(H,n,IT) * IT is Element of the carrier of H
the multF of H . ((H,n,IT),IT) is Element of the carrier of H
[(H,n,IT),IT] is set
the multF of H . [(H,n,IT),IT] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,0,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,0) is set
[H,0] is set
(G) . [H,0] is set
(G) is Element of the carrier of G
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is non empty () () () multMagma
(H) is Element of the carrier of H
the carrier of H is V11() set
(H,G,(H)) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . ((H),G) is set
[(H),G] is set
(H) . [(H),G] is set
IT is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,IT,(H)) is Element of the carrier of H
(H) . ((H),IT) is set
[(H),IT] is set
(H) . [(H),IT] is set
IT + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(IT + 1),(H)) is Element of the carrier of H
(H) . ((H),(IT + 1)) is set
[(H),(IT + 1)] is set
(H) . [(H),(IT + 1)] is set
(H) * (H) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H),(H)) is Element of the carrier of H
[(H),(H)] is set
the multF of H . [(H),(H)] is set
(H,0,(H)) is Element of the carrier of H
(H) . ((H),0) is set
[(H),0] is set
(H) . [(H),0] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,0,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,0) is set
[H,0] is set
(G) . [H,0] is set
(G) is Element of the carrier of G
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,1,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,1) is set
[H,1] is set
(G) . [H,1] is set
0 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,(0 + 1),H) is Element of the carrier of G
(G) . (H,(0 + 1)) is set
[H,(0 + 1)] is set
(G) . [H,(0 + 1)] is set
(G,0,H) is Element of the carrier of G
(G) . (H,0) is set
[H,0] is set
(G) . [H,0] is set
(G,0,H) * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((G,0,H),H) is Element of the carrier of G
[(G,0,H),H] is set
the multF of G . [(G,0,H),H] is set
(G) is Element of the carrier of G
(G) * H is Element of the carrier of G
the multF of G . ((G),H) is Element of the carrier of G
[(G),H] is set
the multF of G . [(G),H] is set
2 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,2,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,2) is set
[H,2] is set
(G) . [H,2] is set
H * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,H) is Element of the carrier of G
[H,H] is set
the multF of G . [H,H] is set
1 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,(1 + 1),H) is Element of the carrier of G
(G) . (H,(1 + 1)) is set
[H,(1 + 1)] is set
(G) . [H,(1 + 1)] is set
(G,1,H) is Element of the carrier of G
(G) . (H,1) is set
[H,1] is set
(G) . [H,1] is set
(G,1,H) * H is Element of the carrier of G
the multF of G . ((G,1,H),H) is Element of the carrier of G
[(G,1,H),H] is set
the multF of G . [(G,1,H),H] is set
3 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,3,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,3) is set
[H,3] is set
(G) . [H,3] is set
H * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,H) is Element of the carrier of G
[H,H] is set
the multF of G . [H,H] is set
(H * H) * H is Element of the carrier of G
the multF of G . ((H * H),H) is Element of the carrier of G
[(H * H),H] is set
the multF of G . [(H * H),H] is set
2 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,(2 + 1),H) is Element of the carrier of G
(G) . (H,(2 + 1)) is set
[H,(2 + 1)] is set
(G) . [H,(2 + 1)] is set
(G,2,H) is Element of the carrier of G
(G) . (H,2) is set
[H,2] is set
(G) . [H,2] is set
(G,2,H) * H is Element of the carrier of G
the multF of G . ((G,2,H),H) is Element of the carrier of G
[(G,2,H),H] is set
the multF of G . [(G,2,H),H] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Element of the carrier of G
H is Element of the carrier of G
(G,2,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,2) is set
[H,2] is set
(G) . [H,2] is set
(G,H) is Element of the carrier of G
H * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,H) is Element of the carrier of G
[H,H] is set
the multF of G . [H,H] is set
H * (G,H) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(G,H)) is Element of the carrier of G
[H,(G,H)] is set
the multF of G . [H,(G,H)] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
G + H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,(G + H),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(G + H)) is set
[n,(G + H)] is set
(IT) . [n,(G + H)] is set
(IT,G,n) is Element of the carrier of IT
(IT) . (n,G) is set
[n,G] is set
(IT) . [n,G] is set
(IT,H,n) is Element of the carrier of IT
(IT) . (n,H) is set
[n,H] is set
(IT) . [n,H] is set
(IT,G,n) * (IT,H,n) is Element of the carrier of IT
the multF of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
the multF of IT . ((IT,G,n),(IT,H,n)) is Element of the carrier of IT
[(IT,G,n),(IT,H,n)] is set
the multF of IT . [(IT,G,n),(IT,H,n)] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(IT,b,n) is Element of the carrier of IT
(IT) . (n,b) is set
[n,b] is set
(IT) . [n,b] is set
b + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(b + 1),n) is Element of the carrier of IT
(IT) . (n,(b + 1)) is set
[n,(b + 1)] is set
(IT) . [n,(b + 1)] is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
c₆ + (b + 1) is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(c₆ + (b + 1)),n) is Element of the carrier of IT
(IT) . (n,(c₆ + (b + 1))) is set
[n,(c₆ + (b + 1))] is set
(IT) . [n,(c₆ + (b + 1))] is set
(IT,c₆,n) is Element of the carrier of IT
(IT) . (n,c₆) is set
[n,c₆] is set
(IT) . [n,c₆] is set
(IT,c₆,n) * (IT,(b + 1),n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,(b + 1),n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,(b + 1),n)] is set
the multF of IT . [(IT,c₆,n),(IT,(b + 1),n)] is set
c₆ + (b + 1) is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(c₆ + (b + 1)),n) is Element of the carrier of IT
(IT) . (n,(c₆ + (b + 1))) is set
[n,(c₆ + (b + 1))] is set
(IT) . [n,(c₆ + (b + 1))] is set
c₆ + b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(c₆ + b) + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,((c₆ + b) + 1),n) is Element of the carrier of IT
(IT) . (n,((c₆ + b) + 1)) is set
[n,((c₆ + b) + 1)] is set
(IT) . [n,((c₆ + b) + 1)] is set
(IT,(c₆ + b),n) is Element of the carrier of IT
(IT) . (n,(c₆ + b)) is set
[n,(c₆ + b)] is set
(IT) . [n,(c₆ + b)] is set
(IT,(c₆ + b),n) * n is Element of the carrier of IT
the multF of IT . ((IT,(c₆ + b),n),n) is Element of the carrier of IT
[(IT,(c₆ + b),n),n] is set
the multF of IT . [(IT,(c₆ + b),n),n] is set
(IT,c₆,n) * (IT,b,n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,b,n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,b,n)] is set
the multF of IT . [(IT,c₆,n),(IT,b,n)] is set
((IT,c₆,n) * (IT,b,n)) * n is Element of the carrier of IT
the multF of IT . (((IT,c₆,n) * (IT,b,n)),n) is Element of the carrier of IT
[((IT,c₆,n) * (IT,b,n)),n] is set
the multF of IT . [((IT,c₆,n) * (IT,b,n)),n] is set
(IT,b,n) * n is Element of the carrier of IT
the multF of IT . ((IT,b,n),n) is Element of the carrier of IT
[(IT,b,n),n] is set
the multF of IT . [(IT,b,n),n] is set
(IT,c₆,n) * ((IT,b,n) * n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),((IT,b,n) * n)) is Element of the carrier of IT
[(IT,c₆,n),((IT,b,n) * n)] is set
the multF of IT . [(IT,c₆,n),((IT,b,n) * n)] is set
(IT,0,n) is Element of the carrier of IT
(IT) . (n,0) is set
[n,0] is set
(IT) . [n,0] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
b + 0 is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(b + 0),n) is Element of the carrier of IT
(IT) . (n,(b + 0)) is set
[n,(b + 0)] is set
(IT) . [n,(b + 0)] is set
(IT,b,n) is Element of the carrier of IT
(IT) . (n,b) is set
[n,b] is set
(IT) . [n,b] is set
(IT,b,n) * (IT,0,n) is Element of the carrier of IT
the multF of IT . ((IT,b,n),(IT,0,n)) is Element of the carrier of IT
[(IT,b,n),(IT,0,n)] is set
the multF of IT . [(IT,b,n),(IT,0,n)] is set
b + 0 is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(b + 0),n) is Element of the carrier of IT
(IT) . (n,(b + 0)) is set
[n,(b + 0)] is set
(IT) . [n,(b + 0)] is set
(IT) is Element of the carrier of IT
(IT,b,n) * (IT) is Element of the carrier of IT
the multF of IT . ((IT,b,n),(IT)) is Element of the carrier of IT
[(IT,b,n),(IT)] is set
the multF of IT . [(IT,b,n),(IT)] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
G + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(G + 1),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(G + 1)) is set
[IT,(G + 1)] is set
(H) . [IT,(G + 1)] is set
(H,G,IT) is Element of the carrier of H
(H) . (IT,G) is set
[IT,G] is set
(H) . [IT,G] is set
(H,G,IT) * IT is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,G,IT),IT) is Element of the carrier of H
[(H,G,IT),IT] is set
the multF of H . [(H,G,IT),IT] is set
IT * (H,G,IT) is Element of the carrier of H
the multF of H . (IT,(H,G,IT)) is Element of the carrier of H
[IT,(H,G,IT)] is set
the multF of H . [IT,(H,G,IT)] is set
(H,1,IT) is Element of the carrier of H
(H) . (IT,1) is set
[IT,1] is set
(H) . [IT,1] is set
(H,1,IT) * (H,G,IT) is Element of the carrier of H
the multF of H . ((H,1,IT),(H,G,IT)) is Element of the carrier of H
[(H,1,IT),(H,G,IT)] is set
the multF of H . [(H,1,IT),(H,G,IT)] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
G * H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,(G * H),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(G * H)) is set
[n,(G * H)] is set
(IT) . [n,(G * H)] is set
(IT,G,n) is Element of the carrier of IT
(IT) . (n,G) is set
[n,G] is set
(IT) . [n,G] is set
(IT,H,(IT,G,n)) is Element of the carrier of IT
(IT) . ((IT,G,n),H) is set
[(IT,G,n),H] is set
(IT) . [(IT,G,n),H] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
b + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
c₆ * (b + 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(c₆ * (b + 1)),n) is Element of the carrier of IT
(IT) . (n,(c₆ * (b + 1))) is set
[n,(c₆ * (b + 1))] is set
(IT) . [n,(c₆ * (b + 1))] is set
(IT,c₆,n) is Element of the carrier of IT
(IT) . (n,c₆) is set
[n,c₆] is set
(IT) . [n,c₆] is set
(IT,(b + 1),(IT,c₆,n)) is Element of the carrier of IT
(IT) . ((IT,c₆,n),(b + 1)) is set
[(IT,c₆,n),(b + 1)] is set
(IT) . [(IT,c₆,n),(b + 1)] is set
c₆ * (b + 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(c₆ * (b + 1)),n) is Element of the carrier of IT
(IT) . (n,(c₆ * (b + 1))) is set
[n,(c₆ * (b + 1))] is set
(IT) . [n,(c₆ * (b + 1))] is set
c₆ * b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
c₆ * 1 is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(c₆ * b) + (c₆ * 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,((c₆ * b) + (c₆ * 1)),n) is Element of the carrier of IT
(IT) . (n,((c₆ * b) + (c₆ * 1))) is set
[n,((c₆ * b) + (c₆ * 1))] is set
(IT) . [n,((c₆ * b) + (c₆ * 1))] is set
(IT,(c₆ * b),n) is Element of the carrier of IT
(IT) . (n,(c₆ * b)) is set
[n,(c₆ * b)] is set
(IT) . [n,(c₆ * b)] is set
(IT,(c₆ * b),n) * (IT,c₆,n) is Element of the carrier of IT
the multF of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
the multF of IT . ((IT,(c₆ * b),n),(IT,c₆,n)) is Element of the carrier of IT
[(IT,(c₆ * b),n),(IT,c₆,n)] is set
the multF of IT . [(IT,(c₆ * b),n),(IT,c₆,n)] is set
(IT,b,(IT,c₆,n)) is Element of the carrier of IT
(IT) . ((IT,c₆,n),b) is set
[(IT,c₆,n),b] is set
(IT) . [(IT,c₆,n),b] is set
(IT,b,(IT,c₆,n)) * (IT,c₆,n) is Element of the carrier of IT
the multF of IT . ((IT,b,(IT,c₆,n)),(IT,c₆,n)) is Element of the carrier of IT
[(IT,b,(IT,c₆,n)),(IT,c₆,n)] is set
the multF of IT . [(IT,b,(IT,c₆,n)),(IT,c₆,n)] is set
(IT,1,(IT,c₆,n)) is Element of the carrier of IT
(IT) . ((IT,c₆,n),1) is set
[(IT,c₆,n),1] is set
(IT) . [(IT,c₆,n),1] is set
(IT,b,(IT,c₆,n)) * (IT,1,(IT,c₆,n)) is Element of the carrier of IT
the multF of IT . ((IT,b,(IT,c₆,n)),(IT,1,(IT,c₆,n))) is Element of the carrier of IT
[(IT,b,(IT,c₆,n)),(IT,1,(IT,c₆,n))] is set
the multF of IT . [(IT,b,(IT,c₆,n)),(IT,1,(IT,c₆,n))] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
b * 0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of NAT
(IT,(b * 0),n) is Element of the carrier of IT
(IT) . (n,(b * 0)) is set
[n,(b * 0)] is set
(IT) . [n,(b * 0)] is set
(IT,b,n) is Element of the carrier of IT
(IT) . (n,b) is set
[n,b] is set
(IT) . [n,b] is set
(IT,0,(IT,b,n)) is Element of the carrier of IT
(IT) . ((IT,b,n),0) is set
[(IT,b,n),0] is set
(IT) . [(IT,b,n),0] is set
b * 0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of NAT
(IT,(b * 0),n) is Element of the carrier of IT
(IT) . (n,(b * 0)) is set
[n,(b * 0)] is set
(IT) . [n,(b * 0)] is set
(IT) is Element of the carrier of IT
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,IT) is Element of the carrier of H
(H,G,(H,IT)) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . ((H,IT),G) is set
[(H,IT),G] is set
(H) . [(H,IT),G] is set
(H,G,IT) is Element of the carrier of H
(H) . (IT,G) is set
[IT,G] is set
(H) . [IT,G] is set
(H,(H,G,IT)) is Element of the carrier of H
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,n,(H,IT)) is Element of the carrier of H
(H) . ((H,IT),n) is set
[(H,IT),n] is set
(H) . [(H,IT),n] is set
(H,n,IT) is Element of the carrier of H
(H) . (IT,n) is set
[IT,n] is set
(H) . [IT,n] is set
(H,(H,n,IT)) is Element of the carrier of H
n + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(n + 1),(H,IT)) is Element of the carrier of H
(H) . ((H,IT),(n + 1)) is set
[(H,IT),(n + 1)] is set
(H) . [(H,IT),(n + 1)] is set
(H,(H,n,IT)) * (H,IT) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,(H,n,IT)),(H,IT)) is Element of the carrier of H
[(H,(H,n,IT)),(H,IT)] is set
the multF of H . [(H,(H,n,IT)),(H,IT)] is set
IT * (H,n,IT) is Element of the carrier of H
the multF of H . (IT,(H,n,IT)) is Element of the carrier of H
[IT,(H,n,IT)] is set
the multF of H . [IT,(H,n,IT)] is set
(H,(IT * (H,n,IT))) is Element of the carrier of H
(H,(n + 1),IT) is Element of the carrier of H
(H) . (IT,(n + 1)) is set
[IT,(n + 1)] is set
(H) . [IT,(n + 1)] is set
(H,(H,(n + 1),IT)) is Element of the carrier of H
(H,0,(H,IT)) is Element of the carrier of H
(H) . ((H,IT),0) is set
[(H,IT),0] is set
(H) . [(H,IT),0] is set
(H) is Element of the carrier of H
(H,(H)) is Element of the carrier of H
(H,0,IT) is Element of the carrier of H
(H) . (IT,0) is set
[IT,0] is set
(H) . [IT,0] is set
(H,(H,0,IT)) is Element of the carrier of H
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
n is Element of the carrier of H
IT * n is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . (IT,n) is Element of the carrier of H
[IT,n] is set
the multF of H . [IT,n] is set
n * IT is Element of the carrier of H
the multF of H . (n,IT) is Element of the carrier of H
[n,IT] is set
the multF of H . [n,IT] is set
(H,G,n) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (n,G) is set
[n,G] is set
(H) . [n,G] is set
IT * (H,G,n) is Element of the carrier of H
the multF of H . (IT,(H,G,n)) is Element of the carrier of H
[IT,(H,G,n)] is set
the multF of H . [IT,(H,G,n)] is set
(H,G,n) * IT is Element of the carrier of H
the multF of H . ((H,G,n),IT) is Element of the carrier of H
[(H,G,n),IT] is set
the multF of H . [(H,G,n),IT] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,b,n) is Element of the carrier of H
(H) . (n,b) is set
[n,b] is set
(H) . [n,b] is set
IT * (H,b,n) is Element of the carrier of H
the multF of H . (IT,(H,b,n)) is Element of the carrier of H
[IT,(H,b,n)] is set
the multF of H . [IT,(H,b,n)] is set
(H,b,n) * IT is Element of the carrier of H
the multF of H . ((H,b,n),IT) is Element of the carrier of H
[(H,b,n),IT] is set
the multF of H . [(H,b,n),IT] is set
b + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(b + 1),n) is Element of the carrier of H
(H) . (n,(b + 1)) is set
[n,(b + 1)] is set
(H) . [n,(b + 1)] is set
IT * (H,(b + 1),n) is Element of the carrier of H
the multF of H . (IT,(H,(b + 1),n)) is Element of the carrier of H
[IT,(H,(b + 1),n)] is set
the multF of H . [IT,(H,(b + 1),n)] is set
(H,(b + 1),n) * IT is Element of the carrier of H
the multF of H . ((H,(b + 1),n),IT) is Element of the carrier of H
[(H,(b + 1),n),IT] is set
the multF of H . [(H,(b + 1),n),IT] is set
n * (H,b,n) is Element of the carrier of H
the multF of H . (n,(H,b,n)) is Element of the carrier of H
[n,(H,b,n)] is set
the multF of H . [n,(H,b,n)] is set
IT * (n * (H,b,n)) is Element of the carrier of H
the multF of H . (IT,(n * (H,b,n))) is Element of the carrier of H
[IT,(n * (H,b,n))] is set
the multF of H . [IT,(n * (H,b,n))] is set
(IT * n) * (H,b,n) is Element of the carrier of H
the multF of H . ((IT * n),(H,b,n)) is Element of the carrier of H
[(IT * n),(H,b,n)] is set
the multF of H . [(IT * n),(H,b,n)] is set
n * ((H,b,n) * IT) is Element of the carrier of H
the multF of H . (n,((H,b,n) * IT)) is Element of the carrier of H
[n,((H,b,n) * IT)] is set
the multF of H . [n,((H,b,n) * IT)] is set
(n * (H,b,n)) * IT is Element of the carrier of H
the multF of H . ((n * (H,b,n)),IT) is Element of the carrier of H
[(n * (H,b,n)),IT] is set
the multF of H . [(n * (H,b,n)),IT] is set
(H,0,n) is Element of the carrier of H
(H) . (n,0) is set
[n,0] is set
(H) . [n,0] is set
IT * (H,0,n) is Element of the carrier of H
the multF of H . (IT,(H,0,n)) is Element of the carrier of H
[IT,(H,0,n)] is set
the multF of H . [IT,(H,0,n)] is set
(H,0,n) * IT is Element of the carrier of H
the multF of H . ((H,0,n),IT) is Element of the carrier of H
[(H,0,n),IT] is set
the multF of H . [(H,0,n),IT] is set
(H) is Element of the carrier of H
IT * (H) is Element of the carrier of H
the multF of H . (IT,(H)) is Element of the carrier of H
[IT,(H)] is set
the multF of H . [IT,(H)] is set
(H) * IT is Element of the carrier of H
the multF of H . ((H),IT) is Element of the carrier of H
[(H),IT] is set
the multF of H . [(H),IT] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,G,n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,G) is set
[n,G] is set
(IT) . [n,G] is set
b is Element of the carrier of IT
n * b is Element of the carrier of IT
the multF of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
the multF of IT . (n,b) is Element of the carrier of IT
[n,b] is set
the multF of IT . [n,b] is set
b * n is Element of the carrier of IT
the multF of IT . (b,n) is Element of the carrier of IT
[b,n] is set
the multF of IT . [b,n] is set
(IT,H,b) is Element of the carrier of IT
(IT) . (b,H) is set
[b,H] is set
(IT) . [b,H] is set
(IT,G,n) * (IT,H,b) is Element of the carrier of IT
the multF of IT . ((IT,G,n),(IT,H,b)) is Element of the carrier of IT
[(IT,G,n),(IT,H,b)] is set
the multF of IT . [(IT,G,n),(IT,H,b)] is set
(IT,H,b) * (IT,G,n) is Element of the carrier of IT
the multF of IT . ((IT,H,b),(IT,G,n)) is Element of the carrier of IT
[(IT,H,b),(IT,G,n)] is set
the multF of IT . [(IT,H,b),(IT,G,n)] is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(IT,c₆,n) is Element of the carrier of IT
(IT) . (n,c₆) is set
[n,c₆] is set
(IT) . [n,c₆] is set
c₆ + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(c₆ + 1),n) is Element of the carrier of IT
(IT) . (n,(c₆ + 1)) is set
[n,(c₆ + 1)] is set
(IT) . [n,(c₆ + 1)] is set
y is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(IT,y,b) is Element of the carrier of IT
(IT) . (b,y) is set
[b,y] is set
(IT) . [b,y] is set
(IT,(c₆ + 1),n) * (IT,y,b) is Element of the carrier of IT
the multF of IT . ((IT,(c₆ + 1),n),(IT,y,b)) is Element of the carrier of IT
[(IT,(c₆ + 1),n),(IT,y,b)] is set
the multF of IT . [(IT,(c₆ + 1),n),(IT,y,b)] is set
(IT,y,b) * (IT,(c₆ + 1),n) is Element of the carrier of IT
the multF of IT . ((IT,y,b),(IT,(c₆ + 1),n)) is Element of the carrier of IT
[(IT,y,b),(IT,(c₆ + 1),n)] is set
the multF of IT . [(IT,y,b),(IT,(c₆ + 1),n)] is set
n * (IT,c₆,n) is Element of the carrier of IT
the multF of IT . (n,(IT,c₆,n)) is Element of the carrier of IT
[n,(IT,c₆,n)] is set
the multF of IT . [n,(IT,c₆,n)] is set
(n * (IT,c₆,n)) * (IT,y,b) is Element of the carrier of IT
the multF of IT . ((n * (IT,c₆,n)),(IT,y,b)) is Element of the carrier of IT
[(n * (IT,c₆,n)),(IT,y,b)] is set
the multF of IT . [(n * (IT,c₆,n)),(IT,y,b)] is set
(IT,c₆,n) * (IT,y,b) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,y,b)) is Element of the carrier of IT
[(IT,c₆,n),(IT,y,b)] is set
the multF of IT . [(IT,c₆,n),(IT,y,b)] is set
n * ((IT,c₆,n) * (IT,y,b)) is Element of the carrier of IT
the multF of IT . (n,((IT,c₆,n) * (IT,y,b))) is Element of the carrier of IT
[n,((IT,c₆,n) * (IT,y,b))] is set
the multF of IT . [n,((IT,c₆,n) * (IT,y,b))] is set
(IT,y,b) * (IT,c₆,n) is Element of the carrier of IT
the multF of IT . ((IT,y,b),(IT,c₆,n)) is Element of the carrier of IT
[(IT,y,b),(IT,c₆,n)] is set
the multF of IT . [(IT,y,b),(IT,c₆,n)] is set
n * ((IT,y,b) * (IT,c₆,n)) is Element of the carrier of IT
the multF of IT . (n,((IT,y,b) * (IT,c₆,n))) is Element of the carrier of IT
[n,((IT,y,b) * (IT,c₆,n))] is set
the multF of IT . [n,((IT,y,b) * (IT,c₆,n))] is set
n * (IT,y,b) is Element of the carrier of IT
the multF of IT . (n,(IT,y,b)) is Element of the carrier of IT
[n,(IT,y,b)] is set
the multF of IT . [n,(IT,y,b)] is set
(n * (IT,y,b)) * (IT,c₆,n) is Element of the carrier of IT
the multF of IT . ((n * (IT,y,b)),(IT,c₆,n)) is Element of the carrier of IT
[(n * (IT,y,b)),(IT,c₆,n)] is set
the multF of IT . [(n * (IT,y,b)),(IT,c₆,n)] is set
(IT,y,b) * n is Element of the carrier of IT
the multF of IT . ((IT,y,b),n) is Element of the carrier of IT
[(IT,y,b),n] is set
the multF of IT . [(IT,y,b),n] is set
((IT,y,b) * n) * (IT,c₆,n) is Element of the carrier of IT
the multF of IT . (((IT,y,b) * n),(IT,c₆,n)) is Element of the carrier of IT
[((IT,y,b) * n),(IT,c₆,n)] is set
the multF of IT . [((IT,y,b) * n),(IT,c₆,n)] is set
(IT,y,b) * (n * (IT,c₆,n)) is Element of the carrier of IT
the multF of IT . ((IT,y,b),(n * (IT,c₆,n))) is Element of the carrier of IT
[(IT,y,b),(n * (IT,c₆,n))] is set
the multF of IT . [(IT,y,b),(n * (IT,c₆,n))] is set
(IT,0,n) is Element of the carrier of IT
(IT) . (n,0) is set
[n,0] is set
(IT) . [n,0] is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(IT,c₆,b) is Element of the carrier of IT
(IT) . (b,c₆) is set
[b,c₆] is set
(IT) . [b,c₆] is set
(IT,0,n) * (IT,c₆,b) is Element of the carrier of IT
the multF of IT . ((IT,0,n),(IT,c₆,b)) is Element of the carrier of IT
[(IT,0,n),(IT,c₆,b)] is set
the multF of IT . [(IT,0,n),(IT,c₆,b)] is set
(IT,c₆,b) * (IT,0,n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,b),(IT,0,n)) is Element of the carrier of IT
[(IT,c₆,b),(IT,0,n)] is set
the multF of IT . [(IT,c₆,b),(IT,0,n)] is set
(IT) is Element of the carrier of IT
(IT) * (IT,c₆,b) is Element of the carrier of IT
the multF of IT . ((IT),(IT,c₆,b)) is Element of the carrier of IT
[(IT),(IT,c₆,b)] is set
the multF of IT . [(IT),(IT,c₆,b)] is set
(IT,c₆,b) * (IT) is Element of the carrier of IT
the multF of IT . ((IT,c₆,b),(IT)) is Element of the carrier of IT
[(IT,c₆,b),(IT)] is set
the multF of IT . [(IT,c₆,b),(IT)] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,G) is set
[IT,G] is set
(H) . [IT,G] is set
n is Element of the carrier of H
IT * n is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . (IT,n) is Element of the carrier of H
[IT,n] is set
the multF of H . [IT,n] is set
n * IT is Element of the carrier of H
the multF of H . (n,IT) is Element of the carrier of H
[n,IT] is set
the multF of H . [n,IT] is set
(H,G,(IT * n)) is Element of the carrier of H
(H) . ((IT * n),G) is set
[(IT * n),G] is set
(H) . [(IT * n),G] is set
(H,G,n) is Element of the carrier of H
(H) . (n,G) is set
[n,G] is set
(H) . [n,G] is set
(H,G,IT) * (H,G,n) is Element of the carrier of H
the multF of H . ((H,G,IT),(H,G,n)) is Element of the carrier of H
[(H,G,IT),(H,G,n)] is set
the multF of H . [(H,G,IT),(H,G,n)] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,b,(IT * n)) is Element of the carrier of H
(H) . ((IT * n),b) is set
[(IT * n),b] is set
(H) . [(IT * n),b] is set
(H,b,IT) is Element of the carrier of H
(H) . (IT,b) is set
[IT,b] is set
(H) . [IT,b] is set
(H,b,n) is Element of the carrier of H
(H) . (n,b) is set
[n,b] is set
(H) . [n,b] is set
(H,b,IT) * (H,b,n) is Element of the carrier of H
the multF of H . ((H,b,IT),(H,b,n)) is Element of the carrier of H
[(H,b,IT),(H,b,n)] is set
the multF of H . [(H,b,IT),(H,b,n)] is set
b + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(b + 1),(IT * n)) is Element of the carrier of H
(H) . ((IT * n),(b + 1)) is set
[(IT * n),(b + 1)] is set
(H) . [(IT * n),(b + 1)] is set
(H,(b + 1),IT) is Element of the carrier of H
(H) . (IT,(b + 1)) is set
[IT,(b + 1)] is set
(H) . [IT,(b + 1)] is set
(H,(b + 1),n) is Element of the carrier of H
(H) . (n,(b + 1)) is set
[n,(b + 1)] is set
(H) . [n,(b + 1)] is set
(H,(b + 1),IT) * (H,(b + 1),n) is Element of the carrier of H
the multF of H . ((H,(b + 1),IT),(H,(b + 1),n)) is Element of the carrier of H
[(H,(b + 1),IT),(H,(b + 1),n)] is set
the multF of H . [(H,(b + 1),IT),(H,(b + 1),n)] is set
((H,b,IT) * (H,b,n)) * (n * IT) is Element of the carrier of H
the multF of H . (((H,b,IT) * (H,b,n)),(n * IT)) is Element of the carrier of H
[((H,b,IT) * (H,b,n)),(n * IT)] is set
the multF of H . [((H,b,IT) * (H,b,n)),(n * IT)] is set
((H,b,IT) * (H,b,n)) * n is Element of the carrier of H
the multF of H . (((H,b,IT) * (H,b,n)),n) is Element of the carrier of H
[((H,b,IT) * (H,b,n)),n] is set
the multF of H . [((H,b,IT) * (H,b,n)),n] is set
(((H,b,IT) * (H,b,n)) * n) * IT is Element of the carrier of H
the multF of H . ((((H,b,IT) * (H,b,n)) * n),IT) is Element of the carrier of H
[(((H,b,IT) * (H,b,n)) * n),IT] is set
the multF of H . [(((H,b,IT) * (H,b,n)) * n),IT] is set
(H,b,n) * n is Element of the carrier of H
the multF of H . ((H,b,n),n) is Element of the carrier of H
[(H,b,n),n] is set
the multF of H . [(H,b,n),n] is set
(H,b,IT) * ((H,b,n) * n) is Element of the carrier of H
the multF of H . ((H,b,IT),((H,b,n) * n)) is Element of the carrier of H
[(H,b,IT),((H,b,n) * n)] is set
the multF of H . [(H,b,IT),((H,b,n) * n)] is set
((H,b,IT) * ((H,b,n) * n)) * IT is Element of the carrier of H
the multF of H . (((H,b,IT) * ((H,b,n) * n)),IT) is Element of the carrier of H
[((H,b,IT) * ((H,b,n) * n)),IT] is set
the multF of H . [((H,b,IT) * ((H,b,n) * n)),IT] is set
(H,b,IT) * (H,(b + 1),n) is Element of the carrier of H
the multF of H . ((H,b,IT),(H,(b + 1),n)) is Element of the carrier of H
[(H,b,IT),(H,(b + 1),n)] is set
the multF of H . [(H,b,IT),(H,(b + 1),n)] is set
((H,b,IT) * (H,(b + 1),n)) * IT is Element of the carrier of H
the multF of H . (((H,b,IT) * (H,(b + 1),n)),IT) is Element of the carrier of H
[((H,b,IT) * (H,(b + 1),n)),IT] is set
the multF of H . [((H,b,IT) * (H,(b + 1),n)),IT] is set
(H,(b + 1),n) * (H,b,IT) is Element of the carrier of H
the multF of H . ((H,(b + 1),n),(H,b,IT)) is Element of the carrier of H
[(H,(b + 1),n),(H,b,IT)] is set
the multF of H . [(H,(b + 1),n),(H,b,IT)] is set
((H,(b + 1),n) * (H,b,IT)) * IT is Element of the carrier of H
the multF of H . (((H,(b + 1),n) * (H,b,IT)),IT) is Element of the carrier of H
[((H,(b + 1),n) * (H,b,IT)),IT] is set
the multF of H . [((H,(b + 1),n) * (H,b,IT)),IT] is set
(H,b,IT) * IT is Element of the carrier of H
the multF of H . ((H,b,IT),IT) is Element of the carrier of H
[(H,b,IT),IT] is set
the multF of H . [(H,b,IT),IT] is set
(H,(b + 1),n) * ((H,b,IT) * IT) is Element of the carrier of H
the multF of H . ((H,(b + 1),n),((H,b,IT) * IT)) is Element of the carrier of H
[(H,(b + 1),n),((H,b,IT) * IT)] is set
the multF of H . [(H,(b + 1),n),((H,b,IT) * IT)] is set
(H,(b + 1),n) * (H,(b + 1),IT) is Element of the carrier of H
the multF of H . ((H,(b + 1),n),(H,(b + 1),IT)) is Element of the carrier of H
[(H,(b + 1),n),(H,(b + 1),IT)] is set
the multF of H . [(H,(b + 1),n),(H,(b + 1),IT)] is set
(H,0,(IT * n)) is Element of the carrier of H
(H) . ((IT * n),0) is set
[(IT * n),0] is set
(H) . [(IT * n),0] is set
(H,0,IT) is Element of the carrier of H
(H) . (IT,0) is set
[IT,0] is set
(H) . [IT,0] is set
(H,0,n) is Element of the carrier of H
(H) . (n,0) is set
[n,0] is set
(H) . [n,0] is set
(H,0,IT) * (H,0,n) is Element of the carrier of H
the multF of H . ((H,0,IT),(H,0,n)) is Element of the carrier of H
[(H,0,IT),(H,0,n)] is set
the multF of H . [(H,0,IT),(H,0,n)] is set
(H) is Element of the carrier of H
(H) * (H) is Element of the carrier of H
the multF of H . ((H),(H)) is Element of the carrier of H
[(H),(H)] is set
the multF of H . [(H),(H)] is set
(H,0,IT) * (H) is Element of the carrier of H
the multF of H . ((H,0,IT),(H)) is Element of the carrier of H
[(H,0,IT),(H)] is set
the multF of H . [(H,0,IT),(H)] is set
G is ext-real V39() V40() integer set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(abs G),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
(H,(H,(abs G),IT)) is Element of the carrier of H
(H) is Element of the carrier of H
(H,(H)) is Element of the carrier of H
(H,0,IT) is Element of the carrier of H
(H) . (IT,0) is set
[IT,0] is set
(H) . [IT,0] is set
(H,(H,0,IT)) is Element of the carrier of H
G is ext-real V39() V40() integer set
H is non empty () () () multMagma
(H) is Element of the carrier of H
the carrier of H is V11() set
(H,G,(H)) is Element of the carrier of H
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),(H)) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . ((H),(abs G)) is set
[(H),(abs G)] is set
(H) . [(H),(abs G)] is set
(H,(H,(abs G),(H))) is Element of the carrier of H
(H,(H)) is Element of the carrier of H
- 1 is ext-real non positive V39() V40() integer Element of INT
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G,(- 1),H) is Element of the carrier of G
(G,H) is Element of the carrier of G
abs (- 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
- (- 1) is ext-real non negative V39() V40() integer Element of INT
(G,1,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,1) is set
[H,1] is set
(G) . [H,1] is set
(G,(G,1,H)) is Element of the carrier of G
G is ext-real V39() V40() integer set
- G is ext-real V39() V40() integer Element of INT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(- G),IT) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(H,G,IT)) is Element of the carrier of H
- 0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of INT
abs (- G) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs (- G)),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(abs (- G))) is set
[IT,(abs (- G))] is set
(H) . [IT,(abs (- G))] is set
(H,(H,(abs (- G)),IT)) is Element of the carrier of H
- (- G) is ext-real V39() V40() integer Element of INT
(H,(- (- G)),IT) is Element of the carrier of H
(H,(H,(- (- G)),IT)) is Element of the carrier of H
(H) is Element of the carrier of H
(H,(H)) is Element of the carrier of H
- 0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of INT
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
(H,(H,(abs G),IT)) is Element of the carrier of H
G is ext-real V39() V40() integer set
G is ext-real V39() V40() integer set
G - 1 is ext-real V39() V40() integer Element of INT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(G - 1),IT) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(- 1),IT) is Element of the carrier of H
(H,G,IT) * (H,(- 1),IT) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,G,IT),(H,(- 1),IT)) is Element of the carrier of H
[(H,G,IT),(H,(- 1),IT)] is set
the multF of H . [(H,G,IT),(H,(- 1),IT)] is set
1 + 0 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
abs (G - 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(abs (G - 1)) + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G - 1) + 1 is ext-real V39() V40() integer Element of INT
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
- G is ext-real V39() V40() integer Element of INT
abs (- G) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(- G),IT) is Element of the carrier of H
IT * (H,(- G),IT) is Element of the carrier of H
the multF of H . (IT,(H,(- G),IT)) is Element of the carrier of H
[IT,(H,(- G),IT)] is set
the multF of H . [IT,(H,(- G),IT)] is set
(H,(G - 1),IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
(H,(G - 1),IT) * IT is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),IT) is Element of the carrier of H
[(H,(G - 1),IT),IT] is set
the multF of H . [(H,(G - 1),IT),IT] is set
((H,(G - 1),IT) * IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . (((H,(G - 1),IT) * IT),(H,(- G),IT)) is Element of the carrier of H
[((H,(G - 1),IT) * IT),(H,(- G),IT)] is set
the multF of H . [((H,(G - 1),IT) * IT),(H,(- G),IT)] is set
(H,(abs (G - 1)),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(abs (G - 1))) is set
[IT,(abs (G - 1))] is set
(H) . [IT,(abs (G - 1))] is set
(H,(abs (G - 1)),IT) * IT is Element of the carrier of H
the multF of H . ((H,(abs (G - 1)),IT),IT) is Element of the carrier of H
[(H,(abs (G - 1)),IT),IT] is set
the multF of H . [(H,(abs (G - 1)),IT),IT] is set
((H,(abs (G - 1)),IT) * IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . (((H,(abs (G - 1)),IT) * IT),(H,(- G),IT)) is Element of the carrier of H
[((H,(abs (G - 1)),IT) * IT),(H,(- G),IT)] is set
the multF of H . [((H,(abs (G - 1)),IT) * IT),(H,(- G),IT)] is set
(H,(abs (- G)),IT) is Element of the carrier of H
(H) . (IT,(abs (- G))) is set
[IT,(abs (- G))] is set
(H) . [IT,(abs (- G))] is set
(H,(H,(abs (- G)),IT)) is Element of the carrier of H
((H,(abs (G - 1)),IT) * IT) * (H,(H,(abs (- G)),IT)) is Element of the carrier of H
the multF of H . (((H,(abs (G - 1)),IT) * IT),(H,(H,(abs (- G)),IT))) is Element of the carrier of H
[((H,(abs (G - 1)),IT) * IT),(H,(H,(abs (- G)),IT))] is set
the multF of H . [((H,(abs (G - 1)),IT) * IT),(H,(H,(abs (- G)),IT))] is set
(H,((abs (G - 1)) + 1),IT) is Element of the carrier of H
(H) . (IT,((abs (G - 1)) + 1)) is set
[IT,((abs (G - 1)) + 1)] is set
(H) . [IT,((abs (G - 1)) + 1)] is set
(H,((abs (G - 1)) + 1),IT) * (H,(H,(abs (- G)),IT)) is Element of the carrier of H
the multF of H . ((H,((abs (G - 1)) + 1),IT),(H,(H,(abs (- G)),IT))) is Element of the carrier of H
[(H,((abs (G - 1)) + 1),IT),(H,(H,(abs (- G)),IT))] is set
the multF of H . [(H,((abs (G - 1)) + 1),IT),(H,(H,(abs (- G)),IT))] is set
(H) is Element of the carrier of H
1 - G is ext-real V39() V40() integer Element of INT
- (G - 1) is ext-real V39() V40() integer Element of INT
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
IT * (H,(- G),IT) is Element of the carrier of H
the multF of H . (IT,(H,(- G),IT)) is Element of the carrier of H
[IT,(H,(- G),IT)] is set
the multF of H . [IT,(H,(- G),IT)] is set
(H,(G - 1),IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
abs (G - 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs (G - 1)),IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,(abs (G - 1))) is set
[IT,(abs (G - 1))] is set
(H) . [IT,(abs (G - 1))] is set
(H,(H,(abs (G - 1)),IT)) is Element of the carrier of H
(H,(H,(abs (G - 1)),IT)) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G - 1)),IT)),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(H,(abs (G - 1)),IT)),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(H,(abs (G - 1)),IT)),(IT * (H,(- G),IT))] is set
abs (- G) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs (- G)),IT) is Element of the carrier of H
(H) . (IT,(abs (- G))) is set
[IT,(abs (- G))] is set
(H) . [IT,(abs (- G))] is set
IT * (H,(abs (- G)),IT) is Element of the carrier of H
the multF of H . (IT,(H,(abs (- G)),IT)) is Element of the carrier of H
[IT,(H,(abs (- G)),IT)] is set
the multF of H . [IT,(H,(abs (- G)),IT)] is set
(H,(H,(abs (G - 1)),IT)) * (IT * (H,(abs (- G)),IT)) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G - 1)),IT)),(IT * (H,(abs (- G)),IT))) is Element of the carrier of H
[(H,(H,(abs (G - 1)),IT)),(IT * (H,(abs (- G)),IT))] is set
the multF of H . [(H,(H,(abs (G - 1)),IT)),(IT * (H,(abs (- G)),IT))] is set
1 + (abs (- G)) is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(1 + (abs (- G))),IT) is Element of the carrier of H
(H) . (IT,(1 + (abs (- G)))) is set
[IT,(1 + (abs (- G)))] is set
(H) . [IT,(1 + (abs (- G)))] is set
(H,(H,(abs (G - 1)),IT)) * (H,(1 + (abs (- G))),IT) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G - 1)),IT)),(H,(1 + (abs (- G))),IT)) is Element of the carrier of H
[(H,(H,(abs (G - 1)),IT)),(H,(1 + (abs (- G))),IT)] is set
the multF of H . [(H,(H,(abs (G - 1)),IT)),(H,(1 + (abs (- G))),IT)] is set
1 + (- G) is ext-real V39() V40() integer Element of INT
(H,(1 + (- G)),IT) is Element of the carrier of H
(H,(H,(abs (G - 1)),IT)) * (H,(1 + (- G)),IT) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G - 1)),IT)),(H,(1 + (- G)),IT)) is Element of the carrier of H
[(H,(H,(abs (G - 1)),IT)),(H,(1 + (- G)),IT)] is set
the multF of H . [(H,(H,(abs (G - 1)),IT)),(H,(1 + (- G)),IT)] is set
(H,(H,(abs (G - 1)),IT)) * (H,(abs (G - 1)),IT) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G - 1)),IT)),(H,(abs (G - 1)),IT)) is Element of the carrier of H
[(H,(H,(abs (G - 1)),IT)),(H,(abs (G - 1)),IT)] is set
the multF of H . [(H,(H,(abs (G - 1)),IT)),(H,(abs (G - 1)),IT)] is set
(H) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
IT * (H,(- G),IT) is Element of the carrier of H
the multF of H . (IT,(H,(- G),IT)) is Element of the carrier of H
[IT,(H,(- G),IT)] is set
the multF of H . [IT,(H,(- G),IT)] is set
(H,(G - 1),IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
(H,IT) is Element of the carrier of H
(H,IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,IT),(IT * (H,(- G),IT))] is set
(H,IT) * IT is Element of the carrier of H
the multF of H . ((H,IT),IT) is Element of the carrier of H
[(H,IT),IT] is set
the multF of H . [(H,IT),IT] is set
((H,IT) * IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . (((H,IT) * IT),(H,(- G),IT)) is Element of the carrier of H
[((H,IT) * IT),(H,(- G),IT)] is set
the multF of H . [((H,IT) * IT),(H,(- G),IT)] is set
(H) is Element of the carrier of H
(H) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H),(H,(- G),IT)) is Element of the carrier of H
[(H),(H,(- G),IT)] is set
the multF of H . [(H),(H,(- G),IT)] is set
(H,0,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,0) is set
[IT,0] is set
(H) . [IT,0] is set
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
IT * (H,(- G),IT) is Element of the carrier of H
the multF of H . (IT,(H,(- G),IT)) is Element of the carrier of H
[IT,(H,(- G),IT)] is set
the multF of H . [IT,(H,(- G),IT)] is set
(H,(G - 1),IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
(H) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
IT * (H,(- G),IT) is Element of the carrier of H
the multF of H . (IT,(H,(- G),IT)) is Element of the carrier of H
[IT,(H,(- G),IT)] is set
the multF of H . [IT,(H,(- G),IT)] is set
(H,(G - 1),IT) * (IT * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(IT * (H,(- G),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
the multF of H . [(H,(G - 1),IT),(IT * (H,(- G),IT))] is set
(H) is Element of the carrier of H
1 - G is ext-real V39() V40() integer Element of INT
(H,(1 - G),IT) is Element of the carrier of H
(H,(G - 1),IT) * (H,(1 - G),IT) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(H,(1 - G),IT)) is Element of the carrier of H
[(H,(G - 1),IT),(H,(1 - G),IT)] is set
the multF of H . [(H,(G - 1),IT),(H,(1 - G),IT)] is set
- (G - 1) is ext-real V39() V40() integer Element of INT
(H,(- (G - 1)),IT) is Element of the carrier of H
(H,(G - 1),IT) * (H,(- (G - 1)),IT) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(H,(- (G - 1)),IT)) is Element of the carrier of H
[(H,(G - 1),IT),(H,(- (G - 1)),IT)] is set
the multF of H . [(H,(G - 1),IT),(H,(- (G - 1)),IT)] is set
(H,(H,(G - 1),IT)) is Element of the carrier of H
(H,(G - 1),IT) * (H,(H,(G - 1),IT)) is Element of the carrier of H
the multF of H . ((H,(G - 1),IT),(H,(H,(G - 1),IT))) is Element of the carrier of H
[(H,(G - 1),IT),(H,(H,(G - 1),IT))] is set
the multF of H . [(H,(G - 1),IT),(H,(H,(G - 1),IT))] is set
(H,(H,(1 - G),IT)) is Element of the carrier of H
(H,(H,(- G),IT)) is Element of the carrier of H
(H,IT) is Element of the carrier of H
(H,(H,(- G),IT)) * (H,IT) is Element of the carrier of H
the multF of H . ((H,(H,(- G),IT)),(H,IT)) is Element of the carrier of H
[(H,(H,(- G),IT)),(H,IT)] is set
the multF of H . [(H,(H,(- G),IT)),(H,IT)] is set
- (- G) is ext-real V39() V40() integer Element of INT
(H,(- (- G)),IT) is Element of the carrier of H
(H,(- (- G)),IT) * (H,IT) is Element of the carrier of H
the multF of H . ((H,(- (- G)),IT),(H,IT)) is Element of the carrier of H
[(H,(- (- G)),IT),(H,IT)] is set
the multF of H . [(H,(- (- G)),IT),(H,IT)] is set
- (1 - G) is ext-real V39() V40() integer Element of INT
(H,(- (1 - G)),IT) is Element of the carrier of H
G is ext-real V39() V40() integer set
- G is ext-real V39() V40() integer Element of INT
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
- 0 is V11() ext-real non positive non negative V32() V33() V34() V36() V37() V38() V39() V40() integer V46() V50() cardinal 0 -element Element of INT
- (- G) is ext-real V39() V40() integer Element of INT
G is ext-real V39() V40() integer set
G + 1 is ext-real V39() V40() integer Element of INT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(G + 1),IT) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,1,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,1) is set
[IT,1] is set
(H) . [IT,1] is set
(H,G,IT) * (H,1,IT) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,G,IT),(H,1,IT)) is Element of the carrier of H
[(H,G,IT),(H,1,IT)] is set
the multF of H . [(H,G,IT),(H,1,IT)] is set
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
abs (G + 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(- 1),IT) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
(H,(- 1),IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(- 1),IT),(H,(- G),IT)) is Element of the carrier of H
[(H,(- 1),IT),(H,(- G),IT)] is set
the multF of H . [(H,(- 1),IT),(H,(- G),IT)] is set
(H,(G + 1),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
(H,(abs (G + 1)),IT) is Element of the carrier of H
(H) . (IT,(abs (G + 1))) is set
[IT,(abs (G + 1))] is set
(H) . [IT,(abs (G + 1))] is set
(H,(abs (G + 1)),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(abs (G + 1)),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
(H,IT) is Element of the carrier of H
(H,IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,IT),(H,(- G),IT)) is Element of the carrier of H
[(H,IT),(H,(- G),IT)] is set
the multF of H . [(H,IT),(H,(- G),IT)] is set
(H,(abs (G + 1)),IT) * ((H,IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),((H,IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),((H,IT) * (H,(- G),IT))] is set
the multF of H . [(H,(abs (G + 1)),IT),((H,IT) * (H,(- G),IT))] is set
(H,(H,G,IT)) is Element of the carrier of H
(H,IT) * (H,(H,G,IT)) is Element of the carrier of H
the multF of H . ((H,IT),(H,(H,G,IT))) is Element of the carrier of H
[(H,IT),(H,(H,G,IT))] is set
the multF of H . [(H,IT),(H,(H,G,IT))] is set
(H,(abs (G + 1)),IT) * ((H,IT) * (H,(H,G,IT))) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),((H,IT) * (H,(H,G,IT)))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),((H,IT) * (H,(H,G,IT)))] is set
the multF of H . [(H,(abs (G + 1)),IT),((H,IT) * (H,(H,G,IT)))] is set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),IT) is Element of the carrier of H
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
(H,(H,(abs G),IT)) is Element of the carrier of H
(H,IT) * (H,(H,(abs G),IT)) is Element of the carrier of H
the multF of H . ((H,IT),(H,(H,(abs G),IT))) is Element of the carrier of H
[(H,IT),(H,(H,(abs G),IT))] is set
the multF of H . [(H,IT),(H,(H,(abs G),IT))] is set
(H,(abs (G + 1)),IT) * ((H,IT) * (H,(H,(abs G),IT))) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),((H,IT) * (H,(H,(abs G),IT)))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),((H,IT) * (H,(H,(abs G),IT)))] is set
the multF of H . [(H,(abs (G + 1)),IT),((H,IT) * (H,(H,(abs G),IT)))] is set
(H,(abs G),IT) * IT is Element of the carrier of H
the multF of H . ((H,(abs G),IT),IT) is Element of the carrier of H
[(H,(abs G),IT),IT] is set
the multF of H . [(H,(abs G),IT),IT] is set
(H,((H,(abs G),IT) * IT)) is Element of the carrier of H
(H,(abs (G + 1)),IT) * (H,((H,(abs G),IT) * IT)) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),(H,((H,(abs G),IT) * IT))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),(H,((H,(abs G),IT) * IT))] is set
the multF of H . [(H,(abs (G + 1)),IT),(H,((H,(abs G),IT) * IT))] is set
(abs G) + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,((abs G) + 1),IT) is Element of the carrier of H
(H) . (IT,((abs G) + 1)) is set
[IT,((abs G) + 1)] is set
(H) . [IT,((abs G) + 1)] is set
(H,(H,((abs G) + 1),IT)) is Element of the carrier of H
(H,(abs (G + 1)),IT) * (H,(H,((abs G) + 1),IT)) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),(H,(H,((abs G) + 1),IT))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),(H,(H,((abs G) + 1),IT))] is set
the multF of H . [(H,(abs (G + 1)),IT),(H,(H,((abs G) + 1),IT))] is set
(H,(H,(abs (G + 1)),IT)) is Element of the carrier of H
(H,(abs (G + 1)),IT) * (H,(H,(abs (G + 1)),IT)) is Element of the carrier of H
the multF of H . ((H,(abs (G + 1)),IT),(H,(H,(abs (G + 1)),IT))) is Element of the carrier of H
[(H,(abs (G + 1)),IT),(H,(H,(abs (G + 1)),IT))] is set
the multF of H . [(H,(abs (G + 1)),IT),(H,(H,(abs (G + 1)),IT))] is set
(H) is Element of the carrier of H
(- 1) + 1 is ext-real V39() V40() integer Element of INT
(H,(- 1),IT) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
(H,(- 1),IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(- 1),IT),(H,(- G),IT)) is Element of the carrier of H
[(H,(- 1),IT),(H,(- G),IT)] is set
the multF of H . [(H,(- 1),IT),(H,(- G),IT)] is set
(H,(G + 1),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
abs (G + 1) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs (G + 1)),IT) is Element of the carrier of H
(H) . (IT,(abs (G + 1))) is set
[IT,(abs (G + 1))] is set
(H) . [IT,(abs (G + 1))] is set
(H,(H,(abs (G + 1)),IT)) is Element of the carrier of H
(H,(H,(abs (G + 1)),IT)) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G + 1)),IT)),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(H,(abs (G + 1)),IT)),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(H,(abs (G + 1)),IT)),((H,(- 1),IT) * (H,(- G),IT))] is set
(H,IT) is Element of the carrier of H
(H,IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,IT),(H,(- G),IT)) is Element of the carrier of H
[(H,IT),(H,(- G),IT)] is set
the multF of H . [(H,IT),(H,(- G),IT)] is set
(H,(H,(abs (G + 1)),IT)) * ((H,IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G + 1)),IT)),((H,IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(H,(abs (G + 1)),IT)),((H,IT) * (H,(- G),IT))] is set
the multF of H . [(H,(H,(abs (G + 1)),IT)),((H,IT) * (H,(- G),IT))] is set
(H,(H,(abs (G + 1)),IT)) * (H,IT) is Element of the carrier of H
the multF of H . ((H,(H,(abs (G + 1)),IT)),(H,IT)) is Element of the carrier of H
[(H,(H,(abs (G + 1)),IT)),(H,IT)] is set
the multF of H . [(H,(H,(abs (G + 1)),IT)),(H,IT)] is set
((H,(H,(abs (G + 1)),IT)) * (H,IT)) * (H,(- G),IT) is Element of the carrier of H
the multF of H . (((H,(H,(abs (G + 1)),IT)) * (H,IT)),(H,(- G),IT)) is Element of the carrier of H
[((H,(H,(abs (G + 1)),IT)) * (H,IT)),(H,(- G),IT)] is set
the multF of H . [((H,(H,(abs (G + 1)),IT)) * (H,IT)),(H,(- G),IT)] is set
IT * (H,(abs (G + 1)),IT) is Element of the carrier of H
the multF of H . (IT,(H,(abs (G + 1)),IT)) is Element of the carrier of H
[IT,(H,(abs (G + 1)),IT)] is set
the multF of H . [IT,(H,(abs (G + 1)),IT)] is set
(H,(IT * (H,(abs (G + 1)),IT))) is Element of the carrier of H
(H,(IT * (H,(abs (G + 1)),IT))) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(IT * (H,(abs (G + 1)),IT))),(H,(- G),IT)) is Element of the carrier of H
[(H,(IT * (H,(abs (G + 1)),IT))),(H,(- G),IT)] is set
the multF of H . [(H,(IT * (H,(abs (G + 1)),IT))),(H,(- G),IT)] is set
(abs (G + 1)) + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,((abs (G + 1)) + 1),IT) is Element of the carrier of H
(H) . (IT,((abs (G + 1)) + 1)) is set
[IT,((abs (G + 1)) + 1)] is set
(H) . [IT,((abs (G + 1)) + 1)] is set
(H,(H,((abs (G + 1)) + 1),IT)) is Element of the carrier of H
(H,(H,((abs (G + 1)) + 1),IT)) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(H,((abs (G + 1)) + 1),IT)),(H,(- G),IT)) is Element of the carrier of H
[(H,(H,((abs (G + 1)) + 1),IT)),(H,(- G),IT)] is set
the multF of H . [(H,(H,((abs (G + 1)) + 1),IT)),(H,(- G),IT)] is set
- (G + 1) is ext-real V39() V40() integer Element of INT
(- (G + 1)) + 1 is ext-real V39() V40() integer Element of INT
(H,((- (G + 1)) + 1),IT) is Element of the carrier of H
(H,(H,((- (G + 1)) + 1),IT)) is Element of the carrier of H
(H,(H,((- (G + 1)) + 1),IT)) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(H,((- (G + 1)) + 1),IT)),(H,(- G),IT)) is Element of the carrier of H
[(H,(H,((- (G + 1)) + 1),IT)),(H,(- G),IT)] is set
the multF of H . [(H,(H,((- (G + 1)) + 1),IT)),(H,(- G),IT)] is set
(H) is Element of the carrier of H
(H,(- 1),IT) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
(H,(- 1),IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(- 1),IT),(H,(- G),IT)) is Element of the carrier of H
[(H,(- 1),IT),(H,(- G),IT)] is set
the multF of H . [(H,(- 1),IT),(H,(- G),IT)] is set
(H,(G + 1),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
(H) is Element of the carrier of H
(H) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H),((H,(- 1),IT) * (H,(- G),IT))] is set
(H,IT) is Element of the carrier of H
(H,IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,IT),(H,(- G),IT)) is Element of the carrier of H
[(H,IT),(H,(- G),IT)] is set
the multF of H . [(H,IT),(H,(- G),IT)] is set
(H,(H,G,IT)) is Element of the carrier of H
(H,IT) * (H,(H,G,IT)) is Element of the carrier of H
the multF of H . ((H,IT),(H,(H,G,IT))) is Element of the carrier of H
[(H,IT),(H,(H,G,IT))] is set
the multF of H . [(H,IT),(H,(H,G,IT))] is set
(H,(H,IT)) is Element of the carrier of H
(H,IT) * (H,(H,IT)) is Element of the carrier of H
the multF of H . ((H,IT),(H,(H,IT))) is Element of the carrier of H
[(H,IT),(H,(H,IT))] is set
the multF of H . [(H,IT),(H,(H,IT))] is set
(H,(- 1),IT) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
(H,(- 1),IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(- 1),IT),(H,(- G),IT)) is Element of the carrier of H
[(H,(- 1),IT),(H,(- G),IT)] is set
the multF of H . [(H,(- 1),IT),(H,(- G),IT)] is set
(H,(G + 1),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
(H) is Element of the carrier of H
(H,(- 1),IT) is Element of the carrier of H
- G is ext-real V39() V40() integer Element of INT
(H,(- G),IT) is Element of the carrier of H
(H,(- 1),IT) * (H,(- G),IT) is Element of the carrier of H
the multF of H . ((H,(- 1),IT),(H,(- G),IT)) is Element of the carrier of H
[(H,(- 1),IT),(H,(- G),IT)] is set
the multF of H . [(H,(- 1),IT),(H,(- G),IT)] is set
(H,(G + 1),IT) * ((H,(- 1),IT) * (H,(- G),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
[(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
the multF of H . [(H,(G + 1),IT),((H,(- 1),IT) * (H,(- G),IT))] is set
(H) is Element of the carrier of H
- (G + 1) is ext-real V39() V40() integer Element of INT
(H,(- (G + 1)),IT) is Element of the carrier of H
(H,(G + 1),IT) * (H,(- (G + 1)),IT) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),(H,(- (G + 1)),IT)) is Element of the carrier of H
[(H,(G + 1),IT),(H,(- (G + 1)),IT)] is set
the multF of H . [(H,(G + 1),IT),(H,(- (G + 1)),IT)] is set
(H,(H,(G + 1),IT)) is Element of the carrier of H
(H,(G + 1),IT) * (H,(H,(G + 1),IT)) is Element of the carrier of H
the multF of H . ((H,(G + 1),IT),(H,(H,(G + 1),IT))) is Element of the carrier of H
[(H,(G + 1),IT),(H,(H,(G + 1),IT))] is set
the multF of H . [(H,(G + 1),IT),(H,(H,(G + 1),IT))] is set
- (- (G + 1)) is ext-real V39() V40() integer Element of INT
(H,(- (- (G + 1))),IT) is Element of the carrier of H
(H,((H,(- 1),IT) * (H,(- G),IT))) is Element of the carrier of H
(H,(H,(- G),IT)) is Element of the carrier of H
(H,(H,(- 1),IT)) is Element of the carrier of H
(H,(H,(- G),IT)) * (H,(H,(- 1),IT)) is Element of the carrier of H
the multF of H . ((H,(H,(- G),IT)),(H,(H,(- 1),IT))) is Element of the carrier of H
[(H,(H,(- G),IT)),(H,(H,(- 1),IT))] is set
the multF of H . [(H,(H,(- G),IT)),(H,(H,(- 1),IT))] is set
- (- G) is ext-real V39() V40() integer Element of INT
(H,(- (- G)),IT) is Element of the carrier of H
(H,(- (- G)),IT) * (H,(H,(- 1),IT)) is Element of the carrier of H
the multF of H . ((H,(- (- G)),IT),(H,(H,(- 1),IT))) is Element of the carrier of H
[(H,(- (- G)),IT),(H,(H,(- 1),IT))] is set
the multF of H . [(H,(- (- G)),IT),(H,(H,(- 1),IT))] is set
- (- 1) is ext-real non negative V39() V40() integer Element of INT
(H,(- (- 1)),IT) is Element of the carrier of H
(H,G,IT) * (H,(- (- 1)),IT) is Element of the carrier of H
the multF of H . ((H,G,IT),(H,(- (- 1)),IT)) is Element of the carrier of H
[(H,G,IT),(H,(- (- 1)),IT)] is set
the multF of H . [(H,G,IT),(H,(- (- 1)),IT)] is set
G is ext-real V39() V40() integer set
H is ext-real V39() V40() integer set
G + H is ext-real V39() V40() integer Element of INT
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,(G + H),n) is Element of the carrier of IT
(IT,G,n) is Element of the carrier of IT
(IT,H,n) is Element of the carrier of IT
(IT,G,n) * (IT,H,n) is Element of the carrier of IT
the multF of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
the multF of IT . ((IT,G,n),(IT,H,n)) is Element of the carrier of IT
[(IT,G,n),(IT,H,n)] is set
the multF of IT . [(IT,G,n),(IT,H,n)] is set
b is ext-real V39() V40() integer set
(IT,b,n) is Element of the carrier of IT
b - 1 is ext-real V39() V40() integer Element of INT
(IT,(b - 1),n) is Element of the carrier of IT
b + 1 is ext-real V39() V40() integer Element of INT
(IT,(b + 1),n) is Element of the carrier of IT
c₆ is ext-real V39() V40() integer set
c₆ + (b - 1) is ext-real V39() V40() integer Element of INT
(IT,(c₆ + (b - 1)),n) is Element of the carrier of IT
(IT,c₆,n) is Element of the carrier of IT
(IT,c₆,n) * (IT,(b - 1),n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,(b - 1),n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,(b - 1),n)] is set
the multF of IT . [(IT,c₆,n),(IT,(b - 1),n)] is set
c₆ - 1 is ext-real V39() V40() integer Element of INT
(c₆ - 1) + b is ext-real V39() V40() integer Element of INT
(IT,((c₆ - 1) + b),n) is Element of the carrier of IT
(IT,(c₆ - 1),n) is Element of the carrier of IT
(IT,(c₆ - 1),n) * (IT,b,n) is Element of the carrier of IT
the multF of IT . ((IT,(c₆ - 1),n),(IT,b,n)) is Element of the carrier of IT
[(IT,(c₆ - 1),n),(IT,b,n)] is set
the multF of IT . [(IT,(c₆ - 1),n),(IT,b,n)] is set
(IT,(- 1),n) is Element of the carrier of IT
(IT,c₆,n) * (IT,(- 1),n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,(- 1),n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,(- 1),n)] is set
the multF of IT . [(IT,c₆,n),(IT,(- 1),n)] is set
((IT,c₆,n) * (IT,(- 1),n)) * (IT,b,n) is Element of the carrier of IT
the multF of IT . (((IT,c₆,n) * (IT,(- 1),n)),(IT,b,n)) is Element of the carrier of IT
[((IT,c₆,n) * (IT,(- 1),n)),(IT,b,n)] is set
the multF of IT . [((IT,c₆,n) * (IT,(- 1),n)),(IT,b,n)] is set
(IT,(- 1),n) * (IT,b,n) is Element of the carrier of IT
the multF of IT . ((IT,(- 1),n),(IT,b,n)) is Element of the carrier of IT
[(IT,(- 1),n),(IT,b,n)] is set
the multF of IT . [(IT,(- 1),n),(IT,b,n)] is set
(IT,c₆,n) * ((IT,(- 1),n) * (IT,b,n)) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),((IT,(- 1),n) * (IT,b,n))) is Element of the carrier of IT
[(IT,c₆,n),((IT,(- 1),n) * (IT,b,n))] is set
the multF of IT . [(IT,c₆,n),((IT,(- 1),n) * (IT,b,n))] is set
b + (- 1) is ext-real V39() V40() integer Element of INT
(IT,(b + (- 1)),n) is Element of the carrier of IT
(IT,c₆,n) * (IT,(b + (- 1)),n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,(b + (- 1)),n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,(b + (- 1)),n)] is set
the multF of IT . [(IT,c₆,n),(IT,(b + (- 1)),n)] is set
c₆ is ext-real V39() V40() integer set
c₆ + (b + 1) is ext-real V39() V40() integer Element of INT
(IT,(c₆ + (b + 1)),n) is Element of the carrier of IT
(IT,c₆,n) is Element of the carrier of IT
(IT,c₆,n) * (IT,(b + 1),n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,(b + 1),n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,(b + 1),n)] is set
the multF of IT . [(IT,c₆,n),(IT,(b + 1),n)] is set
c₆ + 1 is ext-real V39() V40() integer Element of INT
(c₆ + 1) + b is ext-real V39() V40() integer Element of INT
(IT,((c₆ + 1) + b),n) is Element of the carrier of IT
(IT,(c₆ + 1),n) is Element of the carrier of IT
(IT,(c₆ + 1),n) * (IT,b,n) is Element of the carrier of IT
the multF of IT . ((IT,(c₆ + 1),n),(IT,b,n)) is Element of the carrier of IT
[(IT,(c₆ + 1),n),(IT,b,n)] is set
the multF of IT . [(IT,(c₆ + 1),n),(IT,b,n)] is set
(IT,1,n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,1) is set
[n,1] is set
(IT) . [n,1] is set
(IT,c₆,n) * (IT,1,n) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),(IT,1,n)) is Element of the carrier of IT
[(IT,c₆,n),(IT,1,n)] is set
the multF of IT . [(IT,c₆,n),(IT,1,n)] is set
((IT,c₆,n) * (IT,1,n)) * (IT,b,n) is Element of the carrier of IT
the multF of IT . (((IT,c₆,n) * (IT,1,n)),(IT,b,n)) is Element of the carrier of IT
[((IT,c₆,n) * (IT,1,n)),(IT,b,n)] is set
the multF of IT . [((IT,c₆,n) * (IT,1,n)),(IT,b,n)] is set
(IT,1,n) * (IT,b,n) is Element of the carrier of IT
the multF of IT . ((IT,1,n),(IT,b,n)) is Element of the carrier of IT
[(IT,1,n),(IT,b,n)] is set
the multF of IT . [(IT,1,n),(IT,b,n)] is set
(IT,c₆,n) * ((IT,1,n) * (IT,b,n)) is Element of the carrier of IT
the multF of IT . ((IT,c₆,n),((IT,1,n) * (IT,b,n))) is Element of the carrier of IT
[(IT,c₆,n),((IT,1,n) * (IT,b,n))] is set
the multF of IT . [(IT,c₆,n),((IT,1,n) * (IT,b,n))] is set
(IT,0,n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,0) is set
[n,0] is set
(IT) . [n,0] is set
b is ext-real V39() V40() integer set
b + 0 is ext-real V39() V40() integer Element of INT
(IT,(b + 0),n) is Element of the carrier of IT
(IT,b,n) is Element of the carrier of IT
(IT,b,n) * (IT,0,n) is Element of the carrier of IT
the multF of IT . ((IT,b,n),(IT,0,n)) is Element of the carrier of IT
[(IT,b,n),(IT,0,n)] is set
the multF of IT . [(IT,b,n),(IT,0,n)] is set
(IT) is Element of the carrier of IT
(IT,b,n) * (IT) is Element of the carrier of IT
the multF of IT . ((IT,b,n),(IT)) is Element of the carrier of IT
[(IT,b,n),(IT)] is set
the multF of IT . [(IT,b,n),(IT)] is set
G is ext-real V39() V40() integer set
G + 1 is ext-real V39() V40() integer Element of INT
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,(G + 1),IT) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,G,IT) * IT is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,G,IT),IT) is Element of the carrier of H
[(H,G,IT),IT] is set
the multF of H . [(H,G,IT),IT] is set
IT * (H,G,IT) is Element of the carrier of H
the multF of H . (IT,(H,G,IT)) is Element of the carrier of H
[IT,(H,G,IT)] is set
the multF of H . [IT,(H,G,IT)] is set
(H,1,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,1) is set
[IT,1] is set
(H) . [IT,1] is set
G is ext-real V39() V40() integer set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,IT) is Element of the carrier of H
(H,G,(H,IT)) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(H,G,IT)) is Element of the carrier of H
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,n,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,n) is set
[IT,n] is set
(H) . [IT,n] is set
(H,(H,n,IT)) is Element of the carrier of H
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),(H,IT)) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . ((H,IT),(abs G)) is set
[(H,IT),(abs G)] is set
(H) . [(H,IT),(abs G)] is set
(H,(H,(abs G),(H,IT))) is Element of the carrier of H
(H,(abs G),IT) is Element of the carrier of H
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
(H,(H,(abs G),IT)) is Element of the carrier of H
(H,(H,(H,(abs G),IT))) is Element of the carrier of H
G is ext-real V39() V40() integer set
H is ext-real V39() V40() integer set
G * H is ext-real V39() V40() integer Element of INT
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,(G * H),n) is Element of the carrier of IT
(IT,G,n) is Element of the carrier of IT
(IT,H,(IT,G,n)) is Element of the carrier of IT
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,b,n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,b) is set
[n,b] is set
(IT) . [n,b] is set
(IT,c₆,(IT,b,n)) is Element of the carrier of IT
(IT) . ((IT,b,n),c₆) is set
[(IT,b,n),c₆] is set
(IT) . [(IT,b,n),c₆] is set
- H is ext-real V39() V40() integer Element of INT
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G * c₆ is ext-real V39() V40() integer Element of INT
- (G * c₆) is ext-real V39() V40() integer Element of INT
(IT,(G * c₆),n) is Element of the carrier of IT
(IT,(IT,(G * c₆),n)) is Element of the carrier of IT
(IT,n) is Element of the carrier of IT
(IT,(G * c₆),(IT,n)) is Element of the carrier of IT
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,b,(IT,n)) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . ((IT,n),b) is set
[(IT,n),b] is set
(IT) . [(IT,n),b] is set
(IT,c₆,(IT,b,(IT,n))) is Element of the carrier of IT
(IT) . ((IT,b,(IT,n)),c₆) is set
[(IT,b,(IT,n)),c₆] is set
(IT) . [(IT,b,(IT,n)),c₆] is set
(IT,(IT,G,n)) is Element of the carrier of IT
(IT,c₆,(IT,(IT,G,n))) is Element of the carrier of IT
(IT) . ((IT,(IT,G,n)),c₆) is set
[(IT,(IT,G,n)),c₆] is set
(IT) . [(IT,(IT,G,n)),c₆] is set
(IT,H,(IT,(IT,G,n))) is Element of the carrier of IT
(IT,(IT,H,(IT,(IT,G,n)))) is Element of the carrier of IT
(IT,(IT,H,(IT,G,n))) is Element of the carrier of IT
(IT,(IT,(IT,H,(IT,G,n)))) is Element of the carrier of IT
- G is ext-real V39() V40() integer Element of INT
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
b * H is ext-real V39() V40() integer Element of INT
- (b * H) is ext-real V39() V40() integer Element of INT
(IT,(b * H),n) is Element of the carrier of IT
(IT,(IT,(b * H),n)) is Element of the carrier of IT
(IT,n) is Element of the carrier of IT
(IT,(b * H),(IT,n)) is Element of the carrier of IT
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,b,(IT,n)) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . ((IT,n),b) is set
[(IT,n),b] is set
(IT) . [(IT,n),b] is set
(IT,c₆,(IT,b,(IT,n))) is Element of the carrier of IT
(IT) . ((IT,b,(IT,n)),c₆) is set
[(IT,b,(IT,n)),c₆] is set
(IT) . [(IT,b,(IT,n)),c₆] is set
(IT,G,(IT,n)) is Element of the carrier of IT
(IT,(IT,G,(IT,n))) is Element of the carrier of IT
(IT,c₆,(IT,(IT,G,(IT,n)))) is Element of the carrier of IT
(IT) . ((IT,(IT,G,(IT,n))),c₆) is set
[(IT,(IT,G,(IT,n))),c₆] is set
(IT) . [(IT,(IT,G,(IT,n))),c₆] is set
(IT,(IT,G,n)) is Element of the carrier of IT
(IT,(IT,(IT,G,n))) is Element of the carrier of IT
(IT,H,(IT,(IT,(IT,G,n)))) is Element of the carrier of IT
- G is ext-real V39() V40() integer Element of INT
- H is ext-real V39() V40() integer Element of INT
(- 1) * (- 1) is ext-real non negative V39() V40() integer Element of INT
(G * H) * ((- 1) * (- 1)) is ext-real V39() V40() integer Element of INT
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
b * c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,b,n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,b) is set
[n,b] is set
(IT) . [n,b] is set
(IT,c₆,(IT,b,n)) is Element of the carrier of IT
(IT) . ((IT,b,n),c₆) is set
[(IT,b,n),c₆] is set
(IT) . [(IT,b,n),c₆] is set
(IT,(- G),n) is Element of the carrier of IT
(IT,H,(IT,(- G),n)) is Element of the carrier of IT
(IT,(IT,H,(IT,(- G),n))) is Element of the carrier of IT
(IT,(IT,G,n)) is Element of the carrier of IT
(IT,H,(IT,(IT,G,n))) is Element of the carrier of IT
(IT,(IT,H,(IT,(IT,G,n)))) is Element of the carrier of IT
(IT,n) is Element of the carrier of IT
(IT,G,(IT,n)) is Element of the carrier of IT
(IT,H,(IT,G,(IT,n))) is Element of the carrier of IT
(IT,(IT,H,(IT,G,(IT,n)))) is Element of the carrier of IT
(IT,(IT,G,(IT,n))) is Element of the carrier of IT
(IT,H,(IT,(IT,G,(IT,n)))) is Element of the carrier of IT
(IT,(IT,n)) is Element of the carrier of IT
(IT,G,(IT,(IT,n))) is Element of the carrier of IT
(IT,H,(IT,G,(IT,(IT,n)))) is Element of the carrier of IT
H is non empty () () () multMagma
the carrier of H is V11() set
G is ext-real V39() V40() integer set
- G is ext-real V39() V40() integer Element of INT
IT is Element of the carrier of H
(H,(- G),IT) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(H,G,IT)) is Element of the carrier of H
H is non empty () () () multMagma
the carrier of H is V11() set
G is ext-real V39() V40() integer set
IT is Element of the carrier of H
(H,IT) is Element of the carrier of H
(H,G,(H,IT)) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,(H,G,IT)) is Element of the carrier of H
G is ext-real V39() V40() integer set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
n is Element of the carrier of H
IT * n is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . (IT,n) is Element of the carrier of H
[IT,n] is set
the multF of H . [IT,n] is set
n * IT is Element of the carrier of H
the multF of H . (n,IT) is Element of the carrier of H
[n,IT] is set
the multF of H . [n,IT] is set
(H,G,(IT * n)) is Element of the carrier of H
(H,G,n) is Element of the carrier of H
(H,G,IT) * (H,G,n) is Element of the carrier of H
the multF of H . ((H,G,IT),(H,G,n)) is Element of the carrier of H
[(H,G,IT),(H,G,n)] is set
the multF of H . [(H,G,IT),(H,G,n)] is set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),n) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (n,(abs G)) is set
[n,(abs G)] is set
(H) . [n,(abs G)] is set
(H,(abs G),(IT * n)) is Element of the carrier of H
(H) . ((IT * n),(abs G)) is set
[(IT * n),(abs G)] is set
(H) . [(IT * n),(abs G)] is set
(H,(abs G),IT) is Element of the carrier of H
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(abs G),(n * IT)) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . ((n * IT),(abs G)) is set
[(n * IT),(abs G)] is set
(H) . [(n * IT),(abs G)] is set
(H,(H,(abs G),(n * IT))) is Element of the carrier of H
(H,(abs G),n) is Element of the carrier of H
(H) . (n,(abs G)) is set
[n,(abs G)] is set
(H) . [n,(abs G)] is set
(H,(abs G),IT) is Element of the carrier of H
(H) . (IT,(abs G)) is set
[IT,(abs G)] is set
(H) . [IT,(abs G)] is set
(H,(abs G),n) * (H,(abs G),IT) is Element of the carrier of H
the multF of H . ((H,(abs G),n),(H,(abs G),IT)) is Element of the carrier of H
[(H,(abs G),n),(H,(abs G),IT)] is set
the multF of H . [(H,(abs G),n),(H,(abs G),IT)] is set
(H,((H,(abs G),n) * (H,(abs G),IT))) is Element of the carrier of H
(H,(H,(abs G),IT)) is Element of the carrier of H
(H,(H,(abs G),n)) is Element of the carrier of H
(H,(H,(abs G),IT)) * (H,(H,(abs G),n)) is Element of the carrier of H
the multF of H . ((H,(H,(abs G),IT)),(H,(H,(abs G),n))) is Element of the carrier of H
[(H,(H,(abs G),IT)),(H,(H,(abs G),n))] is set
the multF of H . [(H,(H,(abs G),IT)),(H,(H,(abs G),n))] is set
(H,G,IT) * (H,(H,(abs G),n)) is Element of the carrier of H
the multF of H . ((H,G,IT),(H,(H,(abs G),n))) is Element of the carrier of H
[(H,G,IT),(H,(H,(abs G),n))] is set
the multF of H . [(H,G,IT),(H,(H,(abs G),n))] is set
G is ext-real V39() V40() integer set
H is ext-real V39() V40() integer set
IT is non empty () () () multMagma
the carrier of IT is V11() set
n is Element of the carrier of IT
(IT,G,n) is Element of the carrier of IT
b is Element of the carrier of IT
n * b is Element of the carrier of IT
the multF of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is set
the multF of IT . (n,b) is Element of the carrier of IT
[n,b] is set
the multF of IT . [n,b] is set
b * n is Element of the carrier of IT
the multF of IT . (b,n) is Element of the carrier of IT
[b,n] is set
the multF of IT . [b,n] is set
(IT,H,b) is Element of the carrier of IT
(IT,G,n) * (IT,H,b) is Element of the carrier of IT
the multF of IT . ((IT,G,n),(IT,H,b)) is Element of the carrier of IT
[(IT,G,n),(IT,H,b)] is set
the multF of IT . [(IT,G,n),(IT,H,b)] is set
(IT,H,b) * (IT,G,n) is Element of the carrier of IT
the multF of IT . ((IT,H,b),(IT,G,n)) is Element of the carrier of IT
[(IT,H,b),(IT,G,n)] is set
the multF of IT . [(IT,H,b),(IT,G,n)] is set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs G),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(abs G)) is set
[n,(abs G)] is set
(IT) . [n,(abs G)] is set
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs H),b) is Element of the carrier of IT
(IT) . (b,(abs H)) is set
[b,(abs H)] is set
(IT) . [b,(abs H)] is set
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs G),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(abs G)) is set
[n,(abs G)] is set
(IT) . [n,(abs G)] is set
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs H),b) is Element of the carrier of IT
(IT) . (b,(abs H)) is set
[b,(abs H)] is set
(IT) . [b,(abs H)] is set
(IT,(abs G),n) * (IT,(abs H),b) is Element of the carrier of IT
the multF of IT . ((IT,(abs G),n),(IT,(abs H),b)) is Element of the carrier of IT
[(IT,(abs G),n),(IT,(abs H),b)] is set
the multF of IT . [(IT,(abs G),n),(IT,(abs H),b)] is set
(IT,(abs H),b) * (IT,(abs G),n) is Element of the carrier of IT
the multF of IT . ((IT,(abs H),b),(IT,(abs G),n)) is Element of the carrier of IT
[(IT,(abs H),b),(IT,(abs G),n)] is set
the multF of IT . [(IT,(abs H),b),(IT,(abs G),n)] is set
(IT,(IT,(abs H),b)) is Element of the carrier of IT
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs G),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(abs G)) is set
[n,(abs G)] is set
(IT) . [n,(abs G)] is set
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs H),b) is Element of the carrier of IT
(IT) . (b,(abs H)) is set
[b,(abs H)] is set
(IT) . [b,(abs H)] is set
(IT,(abs G),n) * (IT,(abs H),b) is Element of the carrier of IT
the multF of IT . ((IT,(abs G),n),(IT,(abs H),b)) is Element of the carrier of IT
[(IT,(abs G),n),(IT,(abs H),b)] is set
the multF of IT . [(IT,(abs G),n),(IT,(abs H),b)] is set
(IT,(abs H),b) * (IT,(abs G),n) is Element of the carrier of IT
the multF of IT . ((IT,(abs H),b),(IT,(abs G),n)) is Element of the carrier of IT
[(IT,(abs H),b),(IT,(abs G),n)] is set
the multF of IT . [(IT,(abs H),b),(IT,(abs G),n)] is set
(IT,(IT,(abs G),n)) is Element of the carrier of IT
abs G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs G),n) is Element of the carrier of IT
(IT) is Relation-like [: the carrier of IT,NAT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT,NAT:], the carrier of IT) Element of bool [:[: the carrier of IT,NAT:], the carrier of IT:]
[: the carrier of IT,NAT:] is non trivial V46() set
[:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
bool [:[: the carrier of IT,NAT:], the carrier of IT:] is non trivial V46() set
(IT) . (n,(abs G)) is set
[n,(abs G)] is set
(IT) . [n,(abs G)] is set
(IT,(IT,(abs G),n)) is Element of the carrier of IT
abs H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(IT,(abs H),b) is Element of the carrier of IT
(IT) . (b,(abs H)) is set
[b,(abs H)] is set
(IT) . [b,(abs H)] is set
(IT,(IT,(abs H),b)) is Element of the carrier of IT
(IT,(abs H),b) * (IT,(abs G),n) is Element of the carrier of IT
the multF of IT . ((IT,(abs H),b),(IT,(abs G),n)) is Element of the carrier of IT
[(IT,(abs H),b),(IT,(abs G),n)] is set
the multF of IT . [(IT,(abs H),b),(IT,(abs G),n)] is set
(IT,((IT,(abs H),b) * (IT,(abs G),n))) is Element of the carrier of IT
(IT,(abs G),n) * (IT,(abs H),b) is Element of the carrier of IT
the multF of IT . ((IT,(abs G),n),(IT,(abs H),b)) is Element of the carrier of IT
[(IT,(abs G),n),(IT,(abs H),b)] is set
the multF of IT . [(IT,(abs G),n),(IT,(abs H),b)] is set
(IT,((IT,(abs G),n) * (IT,(abs H),b))) is Element of the carrier of IT
G is ext-real V39() V40() integer set
H is non empty () () () multMagma
the carrier of H is V11() set
IT is Element of the carrier of H
n is Element of the carrier of H
IT * n is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . (IT,n) is Element of the carrier of H
[IT,n] is set
the multF of H . [IT,n] is set
n * IT is Element of the carrier of H
the multF of H . (n,IT) is Element of the carrier of H
[n,IT] is set
the multF of H . [n,IT] is set
(H,G,n) is Element of the carrier of H
IT * (H,G,n) is Element of the carrier of H
the multF of H . (IT,(H,G,n)) is Element of the carrier of H
[IT,(H,G,n)] is set
the multF of H . [IT,(H,G,n)] is set
(H,G,n) * IT is Element of the carrier of H
the multF of H . ((H,G,n),IT) is Element of the carrier of H
[(H,G,n),IT] is set
the multF of H . [(H,G,n),IT] is set
(H,1,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,1) is set
[IT,1] is set
(H) . [IT,1] is set
(H,1,IT) * (H,G,n) is Element of the carrier of H
the multF of H . ((H,1,IT),(H,G,n)) is Element of the carrier of H
[(H,1,IT),(H,G,n)] is set
the multF of H . [(H,1,IT),(H,G,n)] is set
(H,G,n) * (H,1,IT) is Element of the carrier of H
the multF of H . ((H,G,n),(H,1,IT)) is Element of the carrier of H
[(H,G,n),(H,1,IT)] is set
the multF of H . [(H,G,n),(H,1,IT)] is set
G is non empty () () () multMagma
the carrier of G is V11() set
G is non empty () () () multMagma
(G) is Element of the carrier of G
the carrier of G is V11() set
8 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,8,(G)) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . ((G),8) is set
[(G),8] is set
(G) . [(G),8] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
(G) is (G) Element of the carrier of G
IT is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(G,IT,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,IT) is set
[H,IT] is set
(G) . [H,IT] is set
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,b,H) is Element of the carrier of G
(G) . (H,b) is set
[H,b] is set
(G) . [H,b] is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(G,c₆,H) is Element of the carrier of G
(G) . (H,c₆) is set
[H,c₆] is set
(G) . [H,c₆] is set
IT is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,IT,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,IT) is set
[H,IT] is set
(G) . [H,IT] is set
(G,n,H) is Element of the carrier of G
(G) . (H,n) is set
[H,n] is set
(G) . [H,n] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is (G) Element of the carrier of G
H is Element of the carrier of G
(G,H) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,(G,H),H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,(G,H)) is set
[H,(G,H)] is set
(G) . [H,(G,H)] is set
G is non empty () () () multMagma
(G) is (G) Element of the carrier of G
the carrier of G is V11() set
(G,(G)) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
H is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(G,H,(G)) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . ((G),H) is set
[(G),H] is set
(G) . [(G),H] is set
(G,1,(G)) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . ((G),1) is set
[(G),1] is set
(G) . [(G),1] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is (G) Element of the carrier of G
H is Element of the carrier of G
(G,H) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G,1,H) is Element of the carrier of G
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
(G) . (H,1) is set
[H,1] is set
(G) . [H,1] is set
G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
H is non empty () () () multMagma
the carrier of H is V11() set
(H) is (H) Element of the carrier of H
IT is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H) is Relation-like [: the carrier of H,NAT:] -defined the carrier of H -valued Function-like V18([: the carrier of H,NAT:], the carrier of H) Element of bool [:[: the carrier of H,NAT:], the carrier of H:]
[: the carrier of H,NAT:] is non trivial V46() set
[:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
bool [:[: the carrier of H,NAT:], the carrier of H:] is non trivial V46() set
(H) . (IT,G) is set
[IT,G] is set
(H) . [IT,G] is set
(H,IT) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,n,IT) is Element of the carrier of H
(H) . (IT,n) is set
[IT,n] is set
(H) . [IT,n] is set
b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,IT) + b is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,(H,IT),IT) is Element of the carrier of H
(H) . (IT,(H,IT)) is set
[IT,(H,IT)] is set
(H) . [IT,(H,IT)] is set
(H,b,IT) is Element of the carrier of H
(H) . (IT,b) is set
[IT,b] is set
(H) . [IT,b] is set
(H,(H,IT),IT) * (H,b,IT) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . ((H,(H,IT),IT),(H,b,IT)) is Element of the carrier of H
[(H,(H,IT),IT),(H,b,IT)] is set
the multF of H . [(H,(H,IT),IT),(H,b,IT)] is set
(H) * (H,b,IT) is Element of the carrier of H
the multF of H . ((H),(H,b,IT)) is Element of the carrier of H
[(H),(H,b,IT)] is set
the multF of H . [(H),(H,b,IT)] is set
c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
(H,IT) * c₆ is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
1 + c₆ is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(H,IT) * (1 + c₆) is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is finite 1-sorted
card G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
the carrier of G is V46() set
card the carrier of G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
card the carrier of G is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is non empty finite 1-sorted
(G) is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
the carrier of G is V11() V46() set
card the carrier of G is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
the Element of the carrier of G is Element of the carrier of G
{ the Element of the carrier of G} is V11() trivial V46() 1 -element set
card { the Element of the carrier of G} is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
b is ext-real V39() V40() Element of REAL
n is ext-real V39() V40() Element of REAL
b + n is ext-real V39() V40() Element of REAL
G is non empty () multMagma
the carrier of G is V11() set
n is Element of the carrier of G
b is Element of the carrier of G
n * b is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (n,b) is Element of the carrier of G
[n,b] is set
the multF of G . [n,b] is set
b * n is Element of the carrier of G
the multF of G . (b,n) is Element of the carrier of G
[b,n] is set
the multF of G . [b,n] is set
G is non empty () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
H * IT is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
IT * H is Element of the carrier of G
the multF of G . (IT,H) is Element of the carrier of G
[IT,H] is set
the multF of G . [IT,H] is set
b is ext-real V39() V40() Element of REAL
n is ext-real V39() V40() Element of REAL
b + n is ext-real V39() V40() Element of REAL
G is non empty () () () () multMagma
the carrier of G is V11() set
H is Element of the carrier of G
IT is Element of the carrier of G
(G,H,IT) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
(G,(G,H,IT)) is Element of the carrier of G
(G,H) is Element of the carrier of G
(G,IT) is Element of the carrier of G
(G,(G,H),(G,IT)) is Element of the carrier of G
the multF of G . ((G,H),(G,IT)) is Element of the carrier of G
[(G,H),(G,IT)] is set
the multF of G . [(G,H),(G,IT)] is set
H is non empty () () () () multMagma
the carrier of H is V11() set
G is ext-real V39() V40() integer set
IT is Element of the carrier of H
n is Element of the carrier of H
(H,IT,n) is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the multF of H . (IT,n) is Element of the carrier of H
[IT,n] is set
the multF of H . [IT,n] is set
(H,G,(H,IT,n)) is Element of the carrier of H
(H,G,IT) is Element of the carrier of H
(H,G,n) is Element of the carrier of H
(H,(H,G,IT),(H,G,n)) is Element of the carrier of H
the multF of H . ((H,G,IT),(H,G,n)) is Element of the carrier of H
[(H,G,IT),(H,G,n)] is set
the multF of H . [(H,G,IT),(H,G,n)] is set
G is non empty () () () () multMagma
the carrier of G is V11() set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
(G) is (G) Element of the carrier of G
addLoopStr(# the carrier of G, the multF of G,(G) #) is non empty strict addLoopStr
the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #) is V11() set
IT is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
n is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
IT + n is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) is Relation-like [: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] -defined the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):]
[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
[:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
bool [:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (IT,n) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[IT,n] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [IT,n] is set
n + IT is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (n,IT) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[n,IT] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [n,IT] is set
y is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
r1 is Element of the carrier of G
z is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
c₁₀ is Element of the carrier of G
y + z is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (y,z) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[y,z] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [y,z] is set
(G,r1,c₁₀) is Element of the carrier of G
the multF of G . (r1,c₁₀) is Element of the carrier of G
[r1,c₁₀] is set
the multF of G . [r1,c₁₀] is set
b is Element of the carrier of G
c₆ is Element of the carrier of G
(G,b,c₆) is Element of the carrier of G
the multF of G . (b,c₆) is Element of the carrier of G
[b,c₆] is set
the multF of G . [b,c₆] is set
the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #) is V11() set
IT is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
n is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
b is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
IT + n is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) is Relation-like [: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] -defined the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):]
[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
[:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
bool [:[: the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #), the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):], the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #):] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (IT,n) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[IT,n] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [IT,n] is set
(IT + n) + b is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . ((IT + n),b) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[(IT + n),b] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [(IT + n),b] is set
c₆ is Element of the carrier of G
y is Element of the carrier of G
(G,c₆,y) is Element of the carrier of G
the multF of G . (c₆,y) is Element of the carrier of G
[c₆,y] is set
the multF of G . [c₆,y] is set
z is Element of the carrier of G
(G,(G,c₆,y),z) is Element of the carrier of G
the multF of G . ((G,c₆,y),z) is Element of the carrier of G
[(G,c₆,y),z] is set
the multF of G . [(G,c₆,y),z] is set
(G,y,z) is Element of the carrier of G
the multF of G . (y,z) is Element of the carrier of G
[y,z] is set
the multF of G . [y,z] is set
(G,c₆,(G,y,z)) is Element of the carrier of G
the multF of G . (c₆,(G,y,z)) is Element of the carrier of G
[c₆,(G,y,z)] is set
the multF of G . [c₆,(G,y,z)] is set
n + b is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (n,b) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[n,b] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [n,b] is set
IT + (n + b) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (IT,(n + b)) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[IT,(n + b)] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [IT,(n + b)] is set
IT is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
0. addLoopStr(# the carrier of G, the multF of G,(G) #) is V66( addLoopStr(# the carrier of G, the multF of G,(G) #)) Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the ZeroF of addLoopStr(# the carrier of G, the multF of G,(G) #) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
IT + (0. addLoopStr(# the carrier of G, the multF of G,(G) #)) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (IT,(0. addLoopStr(# the carrier of G, the multF of G,(G) #))) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[IT,(0. addLoopStr(# the carrier of G, the multF of G,(G) #))] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [IT,(0. addLoopStr(# the carrier of G, the multF of G,(G) #))] is set
n is Element of the carrier of G
(G,n,(G)) is Element of the carrier of G
the multF of G . (n,(G)) is Element of the carrier of G
[n,(G)] is set
the multF of G . [n,(G)] is set
IT is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
(G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
n is Element of the carrier of G
(G) . n is Element of the carrier of G
b is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
IT + b is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . (IT,b) is Element of the carrier of addLoopStr(# the carrier of G, the multF of G,(G) #)
[IT,b] is set
the addF of addLoopStr(# the carrier of G, the multF of G,(G) #) . [IT,b] is set
(G,n) is Element of the carrier of G
(G,n,(G,n)) is Element of the carrier of G
the multF of G . (n,(G,n)) is Element of the carrier of G
[n,(G,n)] is set
the multF of G . [n,(G,n)] is set
G is non empty () multMagma
the carrier of G is V11() set
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
H is Element of the carrier of G
(G) . (H,1) is Element of the carrier of G
[H,1] is set
(G) . [H,1] is set
0 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G) . (H,0) is Element of the carrier of G
[H,0] is set
(G) . [H,0] is set
((G) . (H,0)) * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (((G) . (H,0)),H) is Element of the carrier of G
[((G) . (H,0)),H] is set
the multF of G . [((G) . (H,0)),H] is set
(G) is Element of the carrier of G
(G) * H is Element of the carrier of G
the multF of G . ((G),H) is Element of the carrier of G
[(G),H] is set
the multF of G . [(G),H] is set
G is non empty () multMagma
the carrier of G is V11() set
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
H is Element of the carrier of G
(G) . (H,2) is Element of the carrier of G
[H,2] is set
(G) . [H,2] is set
H * H is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,H) is Element of the carrier of G
[H,H] is set
the multF of G . [H,H] is set
1 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G) . (H,1) is Element of the carrier of G
[H,1] is set
(G) . [H,1] is set
((G) . (H,1)) * H is Element of the carrier of G
the multF of G . (((G) . (H,1)),H) is Element of the carrier of G
[((G) . (H,1)),H] is set
the multF of G . [((G) . (H,1)),H] is set
G is non empty () () () multMagma
the carrier of G is V11() set
(G) is Relation-like [: the carrier of G,NAT:] -defined the carrier of G -valued Function-like V18([: the carrier of G,NAT:], the carrier of G) Element of bool [:[: the carrier of G,NAT:], the carrier of G:]
[: the carrier of G,NAT:] is non trivial V46() set
[:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
bool [:[: the carrier of G,NAT:], the carrier of G:] is non trivial V46() set
H is Element of the carrier of G
IT is Element of the carrier of G
(G,H,IT) is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,IT) is Element of the carrier of G
[H,IT] is set
the multF of G . [H,IT] is set
n is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G) . ((G,H,IT),n) is Element of the carrier of G
[(G,H,IT),n] is set
(G) . [(G,H,IT),n] is set
(G) . (H,n) is Element of the carrier of G
[H,n] is set
(G) . [H,n] is set
(G) . (IT,n) is Element of the carrier of G
[IT,n] is set
(G) . [IT,n] is set
(G,((G) . (H,n)),((G) . (IT,n))) is Element of the carrier of G
the multF of G . (((G) . (H,n)),((G) . (IT,n))) is Element of the carrier of G
[((G) . (H,n)),((G) . (IT,n))] is set
the multF of G . [((G) . (H,n)),((G) . (IT,n))] is set
n + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
(G) . ((G,H,IT),(n + 1)) is Element of the carrier of G
[(G,H,IT),(n + 1)] is set
(G) . [(G,H,IT),(n + 1)] is set
(G,(G,((G) . (H,n)),((G) . (IT,n))),(G,H,IT)) is Element of the carrier of G
the multF of G . ((G,((G) . (H,n)),((G) . (IT,n))),(G,H,IT)) is Element of the carrier of G
[(G,((G) . (H,n)),((G) . (IT,n))),(G,H,IT)] is set
the multF of G . [(G,((G) . (H,n)),((G) . (IT,n))),(G,H,IT)] is set
(G,((G) . (IT,n)),(G,H,IT)) is Element of the carrier of G
the multF of G . (((G) . (IT,n)),(G,H,IT)) is Element of the carrier of G
[((G) . (IT,n)),(G,H,IT)] is set
the multF of G . [((G) . (IT,n)),(G,H,IT)] is set
(G,((G) . (H,n)),(G,((G) . (IT,n)),(G,H,IT))) is Element of the carrier of G
the multF of G . (((G) . (H,n)),(G,((G) . (IT,n)),(G,H,IT))) is Element of the carrier of G
[((G) . (H,n)),(G,((G) . (IT,n)),(G,H,IT))] is set
the multF of G . [((G) . (H,n)),(G,((G) . (IT,n)),(G,H,IT))] is set
(G,((G) . (IT,n)),IT) is Element of the carrier of G
the multF of G . (((G) . (IT,n)),IT) is Element of the carrier of G
[((G) . (IT,n)),IT] is set
the multF of G . [((G) . (IT,n)),IT] is set
(G,H,(G,((G) . (IT,n)),IT)) is Element of the carrier of G
the multF of G . (H,(G,((G) . (IT,n)),IT)) is Element of the carrier of G
[H,(G,((G) . (IT,n)),IT)] is set
the multF of G . [H,(G,((G) . (IT,n)),IT)] is set
(G,((G) . (H,n)),(G,H,(G,((G) . (IT,n)),IT))) is Element of the carrier of G
the multF of G . (((G) . (H,n)),(G,H,(G,((G) . (IT,n)),IT))) is Element of the carrier of G
[((G) . (H,n)),(G,H,(G,((G) . (IT,n)),IT))] is set
the multF of G . [((G) . (H,n)),(G,H,(G,((G) . (IT,n)),IT))] is set
(G) . (IT,(n + 1)) is Element of the carrier of G
[IT,(n + 1)] is set
(G) . [IT,(n + 1)] is set
(G,H,((G) . (IT,(n + 1)))) is Element of the carrier of G
the multF of G . (H,((G) . (IT,(n + 1)))) is Element of the carrier of G
[H,((G) . (IT,(n + 1)))] is set
the multF of G . [H,((G) . (IT,(n + 1)))] is set
(G,((G) . (H,n)),(G,H,((G) . (IT,(n + 1))))) is Element of the carrier of G
the multF of G . (((G) . (H,n)),(G,H,((G) . (IT,(n + 1))))) is Element of the carrier of G
[((G) . (H,n)),(G,H,((G) . (IT,(n + 1))))] is set
the multF of G . [((G) . (H,n)),(G,H,((G) . (IT,(n + 1))))] is set
(G,((G) . (H,n)),H) is Element of the carrier of G
the multF of G . (((G) . (H,n)),H) is Element of the carrier of G
[((G) . (H,n)),H] is set
the multF of G . [((G) . (H,n)),H] is set
(G,(G,((G) . (H,n)),H),((G) . (IT,(n + 1)))) is Element of the carrier of G
the multF of G . ((G,((G) . (H,n)),H),((G) . (IT,(n + 1)))) is Element of the carrier of G
[(G,((G) . (H,n)),H),((G) . (IT,(n + 1)))] is set
the multF of G . [(G,((G) . (H,n)),H),((G) . (IT,(n + 1)))] is set
(G) . (H,(n + 1)) is Element of the carrier of G
[H,(n + 1)] is set
(G) . [H,(n + 1)] is set
(G,((G) . (H,(n + 1))),((G) . (IT,(n + 1)))) is Element of the carrier of G
the multF of G . (((G) . (H,(n + 1))),((G) . (IT,(n + 1)))) is Element of the carrier of G
[((G) . (H,(n + 1))),((G) . (IT,(n + 1)))] is set
the multF of G . [((G) . (H,(n + 1))),((G) . (IT,(n + 1)))] is set
(G) . ((G,H,IT),0) is Element of the carrier of G
[(G,H,IT),0] is set
(G) . [(G,H,IT),0] is set
(G) is Element of the carrier of G
(G,(G),(G)) is Element of the carrier of G
the multF of G . ((G),(G)) is Element of the carrier of G
[(G),(G)] is set
the multF of G . [(G),(G)] is set
(G) . (H,0) is Element of the carrier of G
[H,0] is set
(G) . [H,0] is set
(G,((G) . (H,0)),(G)) is Element of the carrier of G
the multF of G . (((G) . (H,0)),(G)) is Element of the carrier of G
[((G) . (H,0)),(G)] is set
the multF of G . [((G) . (H,0)),(G)] is set
(G) . (IT,0) is Element of the carrier of G
[IT,0] is set
(G) . [IT,0] is set
(G,((G) . (H,0)),((G) . (IT,0))) is Element of the carrier of G
the multF of G . (((G) . (H,0)),((G) . (IT,0))) is Element of the carrier of G
[((G) . (H,0)),((G) . (IT,0))] is set
the multF of G . [((G) . (H,0)),((G) . (IT,0))] is set
G is multMagma
the carrier of G is set
H is multMagma
the carrier of H is set
[: the carrier of G, the carrier of H:] is set
bool [: the carrier of G, the carrier of H:] is set