:: 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