:: MONOID_0 semantic presentation

REAL is non empty V50() V159() V160() V161() V165() set

NAT is non empty V38() V39() V40() V159() V160() V161() V162() V163() V164() V165() Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty V50() V159() V165() set

RAT is non empty V50() V159() V160() V161() V162() V165() set

INT is non empty V50() V159() V160() V161() V162() V163() V165() set

[:COMPLEX,COMPLEX:] is Relation-like non empty set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is Relation-like non empty set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is Relation-like non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is Relation-like non empty set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is Relation-like non empty set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is Relation-like non empty set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is Relation-like non empty set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is Relation-like non empty set

[:[:NAT,NAT:],NAT:] is Relation-like non empty set

bool [:[:NAT,NAT:],NAT:] is non empty set

NAT is non empty V38() V39() V40() V159() V160() V161() V162() V163() V164() V165() set

bool NAT is non empty set

bool NAT is non empty set

INT.Group is non empty strict unital Group-like associative commutative V170() multMagma

the carrier of INT.Group is non empty V159() V160() V161() V162() V163() set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V38() V39() V40() V42() V43() V44() V50() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V163() V164() V165() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V38() V39() V40() V42() V43() V44() V50() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V163() V164() V165() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V38() V39() V40() V42() V43() V44() V50() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V163() V164() V165() set

1 is non empty V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT

2 is non empty V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT

3 is non empty V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V37() V38() V39() V40() V42() V43() V44() V45() integer V47() V50() FinSequence-like FinSubsequence-like FinSequence-membered V146() V159() V160() V161() V162() V163() V164() V165() Element of NAT

addreal is Relation-like Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[:REAL,REAL:],REAL:]

multMagma(# REAL,addreal #) is non empty strict multMagma

addint is Relation-like Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[:INT,INT:],INT:]

multMagma(# INT,addint #) is non empty strict multMagma

multreal is Relation-like Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[:REAL,REAL:],REAL:]

addnat is Relation-like Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[:NAT,NAT:],NAT:]

multnat is Relation-like Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[:NAT,NAT:],NAT:]

the_unity_wrt multreal is V37() V45() V146() Element of REAL

the Relation-like Function-like set is Relation-like Function-like set

{ the Relation-like Function-like set } is functional non empty set

1-sorted(# { the Relation-like Function-like set } #) is strict 1-sorted

D is strict 1-sorted

the carrier of D is set

H is Element of the carrier of D

the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set

{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set } is functional non empty set

1-sorted(# { the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set } #) is strict 1-sorted

D is strict 1-sorted

the carrier of D is set

H is Element of the carrier of D

G is () 1-sorted

the carrier of G is set

D is Element of the carrier of G

H is Element of the carrier of G

G is 1-sorted

the carrier of G is set

D is Element of H

G is () () 1-sorted

the carrier of G is set

D is Relation-like Function-like Element of the carrier of G

G is set

D is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of G

H is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of G

D ^ H is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set

G * is functional non empty FinSequence-membered M13(G)

D ^ H is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like FinSequence of G

G is non empty set

[:G,G:] is Relation-like non empty set

[:[:G,G:],G:] is Relation-like non empty set

bool [:[:G,G:],G:] is non empty set

G is non empty set

[:G,G:] is Relation-like non empty set

[:[:G,G:],G:] is Relation-like non empty set

bool [:[:G,G:],G:] is non empty set

D is Relation-like Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]

H is Element of G

e is Element of G

N is Element of G

D . (H,N) is Element of G

[H,N] is V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

D . [H,N] is set

N is Element of G

D . (N,H) is Element of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

c

D . (c

[c

{c

{c

{{c

D . [c

H is Element of G

e is Element of G

H is Element of G

e is Element of G

N is Element of G

D . (H,N) is Element of G

[H,N] is V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

D . [H,N] is set

N is Element of G

D . (N,H) is Element of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

H is Element of G

e is Element of G

N is Element of G

D . (N,H) is Element of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

N is Element of G

D . (H,N) is Element of G

[H,N] is V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

D . [H,N] is set

G is non empty set

[:G,G:] is Relation-like non empty set

[:[:G,G:],G:] is Relation-like non empty set

bool [:[:G,G:],G:] is non empty set

D is Relation-like Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]

H is Element of G

e is Element of G

D . (H,e) is Element of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

D . [H,e] is set

N is Element of G

D . (H,N) is Element of G

[H,N] is V23() set

{H,N} is non empty set

{{H,N},{H}} is non empty set

D . [H,N] is set

e is Element of G

H is Element of G

D . (e,H) is Element of G

[e,H] is V23() set

{e,H} is non empty set

{e} is non empty set

{{e,H},{e}} is non empty set

D . [e,H] is set

N is Element of G

D . (N,H) is Element of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

H is Element of G

e is Element of G

D . (H,e) is Element of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

D . [H,e] is set

N is Element of G

D . (H,N) is Element of G

[H,N] is V23() set

{H,N} is non empty set

{{H,N},{H}} is non empty set

D . [H,N] is set

D . (e,H) is Element of G

[e,H] is V23() set

{e,H} is non empty set

{e} is non empty set

{{e,H},{e}} is non empty set

D . [e,H] is set

D . (N,H) is Element of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

G is set

{G} is non empty set

[:{G},{G}:] is Relation-like non empty set

[:[:{G},{G}:],{G}:] is Relation-like non empty set

bool [:[:{G},{G}:],{G}:] is non empty set

(G,G) .--> G is Relation-like Function-like set

[G,G] is V23() set

{G,G} is non empty set

{{G,G},{G}} is non empty set

{[G,G]} is Relation-like Function-like non empty set

{[G,G]} --> G is Relation-like Function-like non empty total quasi_total Element of bool [:{[G,G]},{G}:]

[:{[G,G]},{G}:] is Relation-like non empty set

bool [:{[G,G]},{G}:] is non empty set

D is Relation-like Function-like non empty total quasi_total Element of bool [:[:{G},{G}:],{G}:]

e is set

D . e is set

N is Element of [:{G},{G}:]

D . N is Element of {G}

((G,G) .--> G) . e is set

proj1 D is non empty set

proj1 ((G,G) .--> G) is set

e is Element of {G}

N is Element of {G}

H is Element of {G}

e is Element of {G}

D . (H,e) is Element of {G}

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

D . [H,e] is set

N is Element of {G}

D . (N,H) is Element of {G}

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

D . [N,H] is set

e is Element of {G}

N is Element of {G}

D . (e,N) is Element of {G}

[e,N] is V23() set

{e,N} is non empty set

{e} is non empty set

{{e,N},{e}} is non empty set

D . [e,N] is set

D . (N,e) is Element of {G}

[N,e] is V23() set

{N,e} is non empty set

{N} is non empty set

{{N,e},{N}} is non empty set

D . [N,e] is set

e is Element of {G}

N is Element of {G}

N is Element of {G}

D . (N,N) is Element of {G}

[N,N] is V23() set

{N,N} is non empty set

{N} is non empty set

{{N,N},{N}} is non empty set

D . [N,N] is set

D . (e,(D . (N,N))) is Element of {G}

[e,(D . (N,N))] is V23() set

{e,(D . (N,N))} is non empty set

{e} is non empty set

{{e,(D . (N,N))},{e}} is non empty set

D . [e,(D . (N,N))] is set

D . (e,N) is Element of {G}

[e,N] is V23() set

{e,N} is non empty set

{{e,N},{e}} is non empty set

D . [e,N] is set

D . ((D . (e,N)),N) is Element of {G}

[(D . (e,N)),N] is V23() set

{(D . (e,N)),N} is non empty set

{(D . (e,N))} is non empty set

{{(D . (e,N)),N},{(D . (e,N))}} is non empty set

D . [(D . (e,N)),N] is set

e is Element of {G}

D . (e,e) is Element of {G}

[e,e] is V23() set

{e,e} is non empty set

{e} is non empty set

{{e,e},{e}} is non empty set

D . [e,e] is set

e is Element of {G}

N is Element of {G}

D . (e,e) is Element of {G}

[e,e] is V23() set

{e,e} is non empty set

{e} is non empty set

{{e,e},{e}} is non empty set

D . [e,e] is set

e is Element of {G}

N is Element of {G}

D . (e,N) is Element of {G}

[e,N] is V23() set

{e,N} is non empty set

{e} is non empty set

{{e,N},{e}} is non empty set

D . [e,N] is set

N is Element of {G}

D . (e,N) is Element of {G}

[e,N] is V23() set

{e,N} is non empty set

{{e,N},{e}} is non empty set

D . [e,N] is set

D . (N,e) is Element of {G}

[N,e] is V23() set

{N,e} is non empty set

{N} is non empty set

{{N,e},{N}} is non empty set

D . [N,e] is set

D . (N,e) is Element of {G}

[N,e] is V23() set

{N,e} is non empty set

{N} is non empty set

{{N,e},{N}} is non empty set

D . [N,e] is set

the_unity_wrt D is Element of {G}

e is Element of {G}

N is Element of {G}

D . (e,N) is Element of {G}

[e,N] is V23() set

{e,N} is non empty set

{e} is non empty set

{{e,N},{e}} is non empty set

D . [e,N] is set

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

H

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

H

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

e is Element of the carrier of G

(D * H) * e is Element of the carrier of G

the multF of G . ((D * H),e) is Element of the carrier of G

[(D * H),e] is V23() set

{(D * H),e} is non empty set

{(D * H)} is non empty set

{{(D * H),e},{(D * H)}} is non empty set

the multF of G . [(D * H),e] is set

H * e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

the multF of G . [H,e] is set

D * (H * e) is Element of the carrier of G

the multF of G . (D,(H * e)) is Element of the carrier of G

[D,(H * e)] is V23() set

{D,(H * e)} is non empty set

{{D,(H * e)},{D}} is non empty set

the multF of G . [D,(H * e)] is set

the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set

{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set } is functional non empty set

[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:] is Relation-like non empty set

[:[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:],{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:] is Relation-like non empty set

bool [:[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:],{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:] is non empty set

the Relation-like Function-like non empty total quasi_total Element of bool [:[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:],{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:] is Relation-like Function-like non empty total quasi_total Element of bool [:[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:],{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:]

multMagma(# { the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set },{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:],{ the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }:] #) is non empty strict multMagma

H is non empty strict multMagma

the carrier of H is non empty set

the multF of H is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

e is Element of the carrier of H

N is Element of the carrier of H

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the_unity_wrt the multF of G is Element of the carrier of G

D is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the_unity_wrt the multF of G is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

(the_unity_wrt the multF of G) * e is Element of the carrier of G

the multF of G . ((the_unity_wrt the multF of G),e) is Element of the carrier of G

[(the_unity_wrt the multF of G),e] is V23() set

{(the_unity_wrt the multF of G),e} is non empty set

{(the_unity_wrt the multF of G)} is non empty set

{{(the_unity_wrt the multF of G),e},{(the_unity_wrt the multF of G)}} is non empty set

the multF of G . [(the_unity_wrt the multF of G),e] is set

e * (the_unity_wrt the multF of G) is Element of the carrier of G

the multF of G . (e,(the_unity_wrt the multF of G)) is Element of the carrier of G

[e,(the_unity_wrt the multF of G)] is V23() set

{e,(the_unity_wrt the multF of G)} is non empty set

{e} is non empty set

{{e,(the_unity_wrt the multF of G)},{e}} is non empty set

the multF of G . [e,(the_unity_wrt the multF of G)] is set

H is Element of the carrier of G

e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

the multF of G . [H,e] is set

H * e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

e is Element of the carrier of G

the multF of G . (e,H) is Element of the carrier of G

[e,H] is V23() set

{e,H} is non empty set

{e} is non empty set

{{e,H},{e}} is non empty set

the multF of G . [e,H] is set

e * H is Element of the carrier of G

the multF of G . (e,H) is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

D is Element of the carrier of G

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

H

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

H

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

e is Element of the carrier of G

(D * H) * e is Element of the carrier of G

the multF of G . ((D * H),e) is Element of the carrier of G

[(D * H),e] is V23() set

{(D * H),e} is non empty set

{(D * H)} is non empty set

{{(D * H),e},{(D * H)}} is non empty set

the multF of G . [(D * H),e] is set

H * e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

the multF of G . [H,e] is set

D * (H * e) is Element of the carrier of G

the multF of G . (D,(H * e)) is Element of the carrier of G

[D,(H * e)] is V23() set

{D,(H * e)} is non empty set

{{D,(H * e)},{D}} is non empty set

the multF of G . [D,(H * e)] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

[H,e] is V23() set

{H,e} is non empty set

{H} is non empty set

{{H,e},{H}} is non empty set

the multF of G . [H,e] is set

the multF of G . (D,( the multF of G . (H,e))) is Element of the carrier of G

[D,( the multF of G . (H,e))] is V23() set

{D,( the multF of G . (H,e))} is non empty set

{{D,( the multF of G . (H,e))},{D}} is non empty set

the multF of G . [D,( the multF of G . (H,e))] is set

the multF of G . (( the multF of G . (D,H)),e) is Element of the carrier of G

[( the multF of G . (D,H)),e] is V23() set

{( the multF of G . (D,H)),e} is non empty set

{( the multF of G . (D,H))} is non empty set

{{( the multF of G . (D,H)),e},{( the multF of G . (D,H))}} is non empty set

the multF of G . [( the multF of G . (D,H)),e] is set

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

H

[(D * H),e] is V23() set

{(D * H),e} is non empty set

{(D * H)} is non empty set

{{(D * H),e},{(D * H)}} is non empty set

the multF of G . [(D * H),e] is set

(D * H) * e is Element of the carrier of G

the multF of G . ((D * H),e) is Element of the carrier of G

H * e is Element of the carrier of G

the multF of G . (H,e) is Element of the carrier of G

H

[D,(H * e)] is V23() set

{D,(H * e)} is non empty set

{{D,(H * e)},{D}} is non empty set

the multF of G . [D,(H * e)] is set

D * (H * e) is Element of the carrier of G

the multF of G . (D,(H * e)) is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

D * D is Element of the carrier of G

the multF of G . (D,D) is Element of the carrier of G

[D,D] is V23() set

{D,D} is non empty set

{D} is non empty set

{{D,D},{D}} is non empty set

the multF of G . [D,D] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

the multF of G . (D,D) is Element of the carrier of G

[D,D] is V23() set

{D,D} is non empty set

{D} is non empty set

{{D,D},{D}} is non empty set

the multF of G . [D,D] is set

H

D * D is Element of the carrier of G

the multF of G . (D,D) is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

H

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

e * D is Element of the carrier of G

the multF of G . (e,D) is Element of the carrier of G

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

e * D is Element of the carrier of G

the multF of G . (e,D) is Element of the carrier of G

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

H

[D,e] is V23() set

{D,e} is non empty set

{D} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{D} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

H

[D,e] is V23() set

{D,e} is non empty set

{D} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

N is Element of the carrier of G

H

[N,D] is V23() set

{N,D} is non empty set

{N} is non empty set

{{N,D},{N}} is non empty set

the multF of G . [N,D] is set

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

N * D is Element of the carrier of G

the multF of G . (N,D) is Element of the carrier of G

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

e is Element of the carrier of G

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{D} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

N is Element of the carrier of G

N * D is Element of the carrier of G

the multF of G . (N,D) is Element of the carrier of G

[N,D] is V23() set

{N,D} is non empty set

{N} is non empty set

{{N,D},{N}} is non empty set

the multF of G . [N,D] is set

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

e is Element of the carrier of G

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

D * H is Element of the carrier of G

H

D * e is Element of the carrier of G

H

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

e is Element of the carrier of G

e * D is Element of the carrier of G

the multF of G . (e,D) is Element of the carrier of G

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

e is Element of the carrier of G

the multF of G . (e,D) is Element of the carrier of G

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

H * D is Element of the carrier of G

H

e * D is Element of the carrier of G

H

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

H * D is Element of the carrier of G

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

e is Element of the carrier of G

D * e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

e * D is Element of the carrier of G

the multF of G . (e,D) is Element of the carrier of G

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

the multF of G . (H,D) is Element of the carrier of G

[H,D] is V23() set

{H,D} is non empty set

{H} is non empty set

{{H,D},{H}} is non empty set

the multF of G . [H,D] is set

e is Element of the carrier of G

the multF of G . (D,e) is Element of the carrier of G

[D,e] is V23() set

{D,e} is non empty set

{{D,e},{D}} is non empty set

the multF of G . [D,e] is set

the multF of G . (e,D) is Element of the carrier of G

[e,D] is V23() set

{e,D} is non empty set

{e} is non empty set

{{e,D},{e}} is non empty set

the multF of G . [e,D] is set

H * D is Element of the carrier of G

H

e * D is Element of the carrier of G

H

D * H is Element of the carrier of G

H

D * e is Element of the carrier of G

H

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the_unity_wrt the multF of G is Element of the carrier of G

the_unity_wrt H

D is Element of the carrier of G

H is Element of the carrier of G

D * H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

D is Element of the carrier of G

H is Element of the carrier of G

the multF of G . (D,H) is Element of the carrier of G

[D,H] is V23() set

{D,H} is non empty set

{D} is non empty set

{{D,H},{D}} is non empty set

the multF of G . [D,H] is set

D * H is Element of the carrier of G

H

G is non empty multMagma

the carrier of G is non empty set

the multF of G is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the Element of the carrier of G is Element of the carrier of G

H is Element of the carrier of G

the Element of the carrier of G * H is Element of the carrier of G

the multF of G . ( the Element of the carrier of G,H) is Element of the carrier of G

[ the Element of the carrier of G,H] is V23() set

{ the Element of the carrier of G,H} is non empty set

{ the Element of the carrier of G} is non empty set

{{ the Element of the carrier of G,H},{ the Element of the carrier of G}} is non empty set

the multF of G . [ the Element of the carrier of G,H] is set

e is Element of the carrier of G

e * the Element of the carrier of G is Element of the carrier of G

the multF of G . (e, the Element of the carrier of G) is Element of the carrier of G

[e, the Element of the carrier of G] is V23() set

{e, the Element of the carrier of G} is non empty set

{e} is non empty set

{{e, the Element of the carrier of G},{e}} is non empty set

the multF of G . [e, the Element of the carrier of G] is set

N is Element of the carrier of G

e * N is Element of the carrier of G

the multF of G . (e,N) is Element of the carrier of G

[e,N] is V23() set

{e,N} is non empty set

{{e,N},{e}} is non empty set

the multF of G . [e,N] is set

N is Element of the carrier of G

the Element of the carrier of G * N is Element of the carrier of G

the multF of G . ( the Element of the carrier of G,N) is Element of the carrier of G

[ the Element of the carrier of G,N] is V23() set

{ the Element of the carrier of G,N} is non empty set

{{ the Element of the carrier of G,N},{ the Element of the carrier of G}} is non empty set

the multF of G . [ the Element of the carrier of G,N] is set

c

c

the multF of G . (c

[c

{c

{c

{{c

the multF of G . [c

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 V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

the multF of G . [N,H] is set

N is Element of the carrier of G

the Element of the carrier of G * N is Element of the carrier of G

the multF of G . ( the Element of the carrier of G,N) is Element of the carrier of G

[ the Element of the carrier of G,N] is V23() set

{ the Element of the carrier of G,N} is non empty set

{{ the Element of the carrier of G,N},{ the Element of the carrier of G}} is non empty set

the multF of G . [ the Element of the carrier of G,N] is set

c

c

the multF of G . (c

[c

{c

{c

{{c

the multF of G . [c

e * H is Element of the carrier of G

the multF of G . (e,H) is Element of the carrier of G

[e,H] is V23() set

{e,H} is non empty set

{{e,H},{e}} is non empty set

the multF of G . [e,H] is set

N is Element of the carrier of G

N is Element of the carrier of G

N * N is Element of the carrier of G

the multF of G . (N,N) is Element of the carrier of G

[N,N] is V23() set

{N,N} is non empty set

{N} is non empty set

{{N,N},{N}} is non empty set

the multF of G . [N,N] is set

c

c

the multF of G . (c

[c

{c

{c

{{c

the multF of G . [c

N * N is Element of the carrier of G

the multF of G . (N,N) is Element of the carrier of G

[N,N] is V23() set

{N,N} is non empty set

{N} is non empty set

{{N,N},{N}} is non empty set

the multF of G . [N,N] is set

c

the multF of G . (c

[c

{c

{{c

the multF of G . [c

(c

the multF of G . ((c

[(c

{(c

{(c

{{(c

the multF of G . [(c

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 V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

the multF of G . [H,N] is set

bool [: the carrier of G, the carrier of G:] is non empty set

[:H

bool [:H

N is Relation-like Function-like non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]

N is Relation-like Function-like total quasi_total Element of bool [:H

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 V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

the multF of G . [H,N] is set

H

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 V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

the multF of G . [N,H] is set

H

the_unity_wrt H

N is Element of the carrier of G

N . N is Element of the carrier of G

H

[N,(N . N)] is V23() set

{N,(N . N)} is non empty set

{N} is non empty set

{{N,(N . N)},{N}} is non empty set

the multF of G . [N,(N . N)] is set

H

[(N . N),N] is V23() set

{(N . N),N} is non empty set

{(N . N)} is non empty set

{{(N . N),N},{(N . N)}} is non empty set

the multF of G . [(N . N),N] is set

N . N is Element of H

H

[N,(N . N)] is V23() set

{N,(N . N)} is non empty set

{{N,(N . N)},{N}} is non empty set

the multF of G . [N,(N . N)] is set

N * (N . N) is Element of the carrier of G

the multF of G . (N,(N . N)) is Element of the carrier of G

H

[(N . N),N] is V23() set

{(N . N),N} is non empty set

{(N . N)} is non empty set

{{(N . N),N},{(N . N)}} is non empty set

the multF of G . [(N . N),N] is set

(N . N) * N is Element of the carrier of G

the multF of G . ((N . N),N) is Element of the carrier of G

[:H

bool [:H

D is Relation-like Function-like total quasi_total Element of bool [:H

H is Element of the carrier of G

e is Element of the carrier of G

D . H is Element of H

(D . H) * e is Element of the carrier of G

the multF of G . ((D . H),e) is Element of the carrier of G

[(D . H),e] is V23() set

{(D . H),e} is non empty set

{(D . H)} is non empty set

{{(D . H),e},{(D . H)}} is non empty set

the multF of G . [(D . H),e] is set

N is Element of the carrier of G

the multF of G . (H,N) is Element of the carrier of G

[H,N] is V23() set

{H,N} is non empty set

{H} is non empty set

{{H,N},{H}} is non empty set

the multF of G . [H,N] is set

e * (D . H) is Element of the carrier of G

the multF of G . (e,(D . H)) is Element of the carrier of G

[e,(D . H)] is V23() set

{e,(D . H)} is non empty set

{e} is non empty set

{{e,(D . H)},{e}} is non empty set

the multF of G . [e,(D . H)] is set

N is Element of the carrier of G

the multF of G . (N,H) is Element of the carrier of G

[N,H] is V23() set

{N,H} is non empty set

{N} is non empty set

{{N,H},{N}} is non empty set

the multF of G . [N,H] is set

H

H * N is Element of the carrier of G

H * (D . H) is Element of the carrier of G

the multF of G . (H,(D . H)) is Element of the carrier of G

[H,(D . H)] is V23() set

{H,(D . H)} is non empty set

{{H,(D . H)},{H}} is non empty set

the multF of G . [H,(D . H)] is