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 H1(G)
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
c7 is Element of G
D . (c7,H) is Element of G
[c7,H] is V23() set
{c7,H} is non empty set
{c7} is non empty set
{{c7,H},{c7}} is non empty set
D . [c7,H] is set
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
H2(G) . (D,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
H2(G) . (H,D) 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
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
H2(G) . (D,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
H2(G) . (H,D) 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
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
H2(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
(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
H2(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
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
H2(G) . (D,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
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
H2(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
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
H2(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
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
H2(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
H2(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
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
H2(G) . (D,H) is Element of the carrier of G
D * e is Element of the carrier of G
H2(G) . (D,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
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
H2(G) . (H,D) is Element of the carrier of G
e * D is Element of the carrier of G
H2(G) . (e,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
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
H2(G) . (H,D) is Element of the carrier of G
e * D is Element of the carrier of G
H2(G) . (e,D) is Element of the carrier of G
D * H is Element of the carrier of G
H2(G) . (D,H) is Element of the carrier of G
D * e is Element of the carrier of G
H2(G) . (D,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
the_unity_wrt the multF of G is Element of the carrier of G
the_unity_wrt H2(G) 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
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
H2(G) . (D,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
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
c7 is Element of the carrier of G
c7 * the Element of the carrier of G is Element of the carrier of G
the multF of G . (c7, the Element of the carrier of G) is Element of the carrier of G
[c7, the Element of the carrier of G] is V23() set
{c7, the Element of the carrier of G} is non empty set
{c7} is non empty set
{{c7, the Element of the carrier of G},{c7}} is non empty set
the multF of G . [c7, the Element of the carrier of G] 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 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
c7 is Element of the carrier of G
c7 * the Element of the carrier of G is Element of the carrier of G
the multF of G . (c7, the Element of the carrier of G) is Element of the carrier of G
[c7, the Element of the carrier of G] is V23() set
{c7, the Element of the carrier of G} is non empty set
{c7} is non empty set
{{c7, the Element of the carrier of G},{c7}} is non empty set
the multF of G . [c7, the Element of the carrier of G] is set
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
c7 is Element of the carrier of G
c7 * N is Element of the carrier of G
the multF of G . (c7,N) is Element of the carrier of G
[c7,N] is V23() set
{c7,N} is non empty set
{c7} is non empty set
{{c7,N},{c7}} is non empty set
the multF of G . [c7,N] is set
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
c7 * (N * N) is Element of the carrier of G
the multF of G . (c7,(N * N)) is Element of the carrier of G
[c7,(N * N)] is V23() set
{c7,(N * N)} is non empty set
{{c7,(N * N)},{c7}} is non empty set
the multF of G . [c7,(N * N)] is set
(c7 * N) * N is Element of the carrier of G
the multF of G . ((c7 * N),N) is Element of the carrier of G
[(c7 * N),N] is V23() set
{(c7 * N),N} is non empty set
{(c7 * N)} is non empty set
{{(c7 * N),N},{(c7 * N)}} is non empty set
the multF of G . [(c7 * N),N] is set
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
[:H1(G),H1(G):] is Relation-like set
bool [:H1(G),H1(G):] is non empty set
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 [:H1(G),H1(G):]
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
H2(G) . (H,N) is Element of the carrier of G
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
H2(G) . (N,H) is Element of the carrier of G
the_unity_wrt H2(G) is Element of the carrier of G
N is Element of the carrier of G
N . N is Element of the carrier of G
H2(G) . (N,(N . N)) is Element of the carrier of G
[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
H2(G) . ((N . N),N) is Element of the carrier of G
[(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 H1(G)
H2(G) . (N,(N . N)) is Element of H1(G)
[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
H2(G) . ((N . N),N) is Element of the carrier of G
[(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
[:H1(G),H1(G):] is Relation-like set
bool [:H1(G),H1(G):] is non empty set
D is Relation-like Function-like total quasi_total Element of bool [:H1(G),H1(G):]
H is Element of the carrier of G
e is Element of the carrier of G
D . H is Element of H1(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
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
H2(G) . (H,N) is Element of the carrier of G
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