:: 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
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
bool is non trivial V46() set
is non trivial V46() set
is non trivial V46() set
bool 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

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
c6 is ext-real V39() V40() Element of REAL
y is ext-real V39() V40() Element of REAL
c6 + y is ext-real V39() V40() Element of REAL
b is ext-real V39() V40() Element of REAL
b + c6 is ext-real V39() V40() Element of REAL
(b + c6) + y is ext-real V39() V40() Element of REAL
b + (c6 + 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
c6 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
c6 is Element of the carrier of G
(n * b) * c6 is Element of the carrier of G
the multF of G . ((n * b),c6) is Element of the carrier of G
[(n * b),c6] is set
the multF of G . [(n * b),c6] is set
b * c6 is Element of the carrier of G
the multF of G . (b,c6) is Element of the carrier of G
[b,c6] is set
the multF of G . [b,c6] is set
n * (b * c6) is Element of the carrier of G
the multF of G . (n,(b * c6)) is Element of the carrier of G
[n,(b * c6)] is set
the multF of G . [n,(b * c6)] 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
c6 is Element of the carrier of G
the Element of the carrier of G * c6 is Element of the carrier of G
the multF of G . ( the Element of the carrier of G,c6) is Element of the carrier of G
[ the Element of the carrier of G,c6] is set
the multF of G . [ the Element of the carrier of G,c6] is set
b * ( the Element of the carrier of G * c6) is Element of the carrier of G
the multF of G . (b,( the Element of the carrier of G * c6)) is Element of the carrier of G
[b,( the Element of the carrier of G * c6)] is set
the multF of G . [b,( the Element of the carrier of G * c6)] 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
c10 is Element of the carrier of G
c10 * n is Element of the carrier of G
the multF of G . (c10,n) is Element of the carrier of G
[c10,n] is set
the multF of G . [c10,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
c6 is ext-real V39() V40() Element of REAL
y is ext-real V39() V40() Element of REAL
c6 + y is ext-real V39() V40() Element of REAL
b is ext-real V39() V40() Element of REAL
b + c6 is ext-real V39() V40() Element of REAL
(b + c6) + y is ext-real V39() V40() Element of REAL
b + (c6 + 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
c6 is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal set
c6 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
n . (c6 + 1) is Element of the carrier of G
n . c6 is Element of the carrier of G
(n . c6) * 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 . c6),IT) is Element of the carrier of G
[(n . c6),IT] is set
the multF of G . [(n . c6),IT] is 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
c6 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
c6 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:]
c6 . 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
c6 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:]
c6 . 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
c6 is ext-real non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
[n,c6] is set
H . [n,c6] is set
IT . [n,c6] is set
IT . (n,c6) is Element of the carrier of G
c6 + 1 is V11() ext-real positive non negative V32() V33() V34() V38() V39() V40() integer V46() cardinal Element of NAT
[n,(c6 + 1)] is set
H . [n,(c6 + 1)] is set
H . (n,(c6 + 1)) is Element of the carrier of G
H . (n,c6) is Element of the carrier of G
(H . (n,c6)) * 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,c6)),n) is Element of the carrier of G
[(H . (n,c6)),n] is set
the multF of G . [(H . (n,c6)),n] is set
IT . (n,(c6 + 1)) is Element of the carrier of G
IT . [n,(c6 + 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