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

y is ext-real V39() V40() Element of REAL

c

b is ext-real V39() V40() Element of REAL

b + c

(b + c

b + (c

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

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

(n * b) * c

the multF of G . ((n * b),c

[(n * b),c

the multF of G . [(n * b),c

b * c

the multF of G . (b,c

[b,c

the multF of G . [b,c

n * (b * c

the multF of G . (n,(b * c

[n,(b * c

the multF of G . [n,(b * c

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

the Element of the carrier of G * c

the multF of G . ( the Element of the carrier of G,c

[ the Element of the carrier of G,c

the multF of G . [ the Element of the carrier of G,c

b * ( the Element of the carrier of G * c

the multF of G . (b,( the Element of the carrier of G * c

[b,( the Element of the carrier of G * c

the multF of G . [b,( the Element of the carrier of G * c

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

c

the multF of G . (c

[c

the multF of G . [c

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

y is ext-real V39() V40() Element of REAL

c

b is ext-real V39() V40() Element of REAL

b + c

(b + c

b + (c

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

c

n . (c

n . c

(n . c

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

[(n . c

the multF of G . [(n . c

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

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

c

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

c

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

[n,c

H . [n,c

IT . [n,c

IT . (n,c

c

[n,(c

H . [n,(c

H . (n,(c

H . (n,c

(H . (n,c

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

[(H . (n,c

the multF of G . [(H . (n,c

IT . (n,(c

IT . [n,(c

[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