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 set
(H * (D . H)) * e is Element of the carrier of G
the multF of G . ((H * (D . H)),e) is Element of the carrier of G
[(H * (D . H)),e] is V23() set
{(H * (D . H)),e} is non empty set
{(H * (D . H))} is non empty set
{{(H * (D . H)),e},{(H * (D . H))}} is non empty set
the multF of G . [(H * (D . H)),e] is set
the_unity_wrt H2(G) is Element of the carrier of G
H2(G) . ((the_unity_wrt H2(G)),e) is Element of the carrier of G
[(the_unity_wrt H2(G)),e] is V23() set
{(the_unity_wrt H2(G)),e} is non empty set
{(the_unity_wrt H2(G))} is non empty set
{{(the_unity_wrt H2(G)),e},{(the_unity_wrt H2(G))}} is non empty set
the multF of G . [(the_unity_wrt H2(G)),e] is set
H2(G) . (N,H) is Element of the carrier of G
N * H is Element of the carrier of G
(D . H) * H is Element of the carrier of G
the multF of G . ((D . H),H) is Element of the carrier of G
[(D . H),H] is V23() set
{(D . H),H} is non empty set
{{(D . H),H},{(D . H)}} is non empty set
the multF of G . [(D . H),H] is set
e * ((D . H) * H) is Element of the carrier of G
the multF of G . (e,((D . H) * H)) is Element of the carrier of G
[e,((D . H) * H)] is V23() set
{e,((D . H) * H)} is non empty set
{{e,((D . H) * H)},{e}} is non empty set
the multF of G . [e,((D . H) * H)] is set
H2(G) . (e,(the_unity_wrt H2(G))) is Element of the carrier of G
[e,(the_unity_wrt H2(G))] is V23() set
{e,(the_unity_wrt H2(G))} is non empty set
{{e,(the_unity_wrt H2(G))},{e}} is non empty set
the multF of G . [e,(the_unity_wrt H2(G))] 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
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
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 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
G is non empty multMagma
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 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 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
e is Element of the carrier of G
H2(G) . (H,e) is Element of the carrier of G
[H,e] is V23() set
{H,e} is non empty set
{{H,e},{H}} is non empty set
the multF of G . [H,e] is set
N is Element of the carrier of G
H2(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 * e is Element of the carrier of G
the multF of G . (H,e) is Element of the carrier of G
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} is non empty set
{{e,H},{e}} is non empty set
the multF of G . [e,H] 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 * 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,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
[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
G is non empty multMagma
D is non empty unital Group-like associative multMagma
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
G is non empty multMagma
G is non empty multMagma
G is non empty multMagma
G is non empty multMagma
G is non empty multMagma
G is non empty multMagma
D is non empty unital Group-like associative () () () multMagma
the carrier of D is non empty set
H is Element of the carrier of D
e is Element of the carrier of D
H * e is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] is set
N is Element of the carrier of D
H * N is Element of the carrier of D
the multF of D . (H,N) is Element of the carrier of D
[H,N] is V23() set
{H,N} is non empty set
{{H,N},{H}} is non empty set
the multF of D . [H,N] is set
e * H is Element of the carrier of D
the multF of D . (e,H) is Element of the carrier of D
[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 D . [e,H] is set
N * H is Element of the carrier of D
the multF of D . (N,H) is Element of the carrier of D
[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 D . [N,H] is set
G is non empty multLoopStr
the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G 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
the multF of G . ((1. G),D) is Element of the carrier of G
[(1. G),D] is V23() set
{(1. G),D} is non empty set
{(1. G)} is non empty set
{{(1. G),D},{(1. G)}} is non empty set
the multF of G . [(1. G),D] is set
the multF of G . ((1. G),D) is Element of the carrier of G
(1. G) * D is Element of the carrier of G
D is Element of the carrier of G
the multF of G . (D,(1. G)) is Element of the carrier of G
[D,(1. G)] is V23() set
{D,(1. G)} is non empty set
{D} is non empty set
{{D,(1. G)},{D}} is non empty set
the multF of G . [D,(1. G)] is set
the multF of G . (D,(1. G)) is Element of the carrier of G
D * (1. G) is Element of the carrier of G
D is Element of the carrier of G
D * (1. G) is Element of the carrier of G
the multF of G . (D,(1. G)) is Element of the carrier of G
[D,(1. G)] is V23() set
{D,(1. G)} is non empty set
{D} is non empty set
{{D,(1. G)},{D}} is non empty set
the multF of G . [D,(1. G)] is set
(1. G) * D is Element of the carrier of G
the multF of G . ((1. G),D) is Element of the carrier of G
[(1. G),D] is V23() set
{(1. G),D} is non empty set
{(1. G)} is non empty set
{{(1. G),D},{(1. G)}} is non empty set
the multF of G . [(1. G),D] is set
G is non empty multLoopStr
the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G 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
(1. G) * D is Element of the carrier of G
the multF of G . ((1. G),D) is Element of the carrier of G
[(1. G),D] is V23() set
{(1. G),D} is non empty set
{(1. G)} is non empty set
{{(1. G),D},{(1. G)}} is non empty set
the multF of G . [(1. G),D] is set
H is Element of the carrier of G
H * (1. G) is Element of the carrier of G
the multF of G . (H,(1. G)) is Element of the carrier of G
[H,(1. G)] is V23() set
{H,(1. G)} is non empty set
{H} is non empty set
{{H,(1. G)},{H}} is non empty set
the multF of G . [H,(1. G)] is set
D is Element of the carrier of G
H3(G) * D is Element of the carrier of G
the multF of G . ((1. G),D) is Element of the carrier of G
[(1. G),D] is V23() set
{(1. G),D} is non empty set
{(1. G)} is non empty set
{{(1. G),D},{(1. G)}} is non empty set
the multF of G . [(1. G),D] is set
D * H3(G) is Element of the carrier of G
the multF of G . (D,(1. G)) is Element of the carrier of G
[D,(1. G)] is V23() set
{D,(1. G)} is non empty set
{D} is non empty set
{{D,(1. G)},{D}} is non empty set
the multF of G . [D,(1. G)] is set
H2(G) . (H3(G),D) is Element of the carrier of G
H2(G) . (D,H3(G)) is Element of the carrier of G
G is non empty multLoopStr
1. G is Element of the carrier of G
the carrier of G is non empty set
the OneF of G 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
the_unity_wrt the multF of G is Element of the carrier of G
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 }:]
the Relation-like Function-like Element of { the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set } is Relation-like Function-like Element of { the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set }
multLoopStr(# { 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 }:], the Relation-like Function-like Element of { the Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set } #) is non empty strict multLoopStr
e is non empty strict multLoopStr
the carrier of e is non empty set
[: the carrier of e, the carrier of e:] is Relation-like non empty set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is Relation-like non empty set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
N is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
N is Element of the carrier of e
c7 is Element of the carrier of e
N . (N,c7) is Element of the carrier of e
[N,c7] is V23() set
{N,c7} is non empty set
{N} is non empty set
{{N,c7},{N}} is non empty set
N . [N,c7] is set
N . (c7,N) is Element of the carrier of e
[c7,N] is V23() set
{c7,N} is non empty set
{c7} is non empty set
{{c7,N},{c7}} is non empty set
N . [c7,N] is set
1. e is Element of the carrier of e
the OneF of e is Element of the carrier of e
the multF of e is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
c7 is Element of the carrier of e
b9 is Element of the carrier of e
G is multMagma
the carrier of G is set
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
the Element of the carrier of G is Element of the carrier of G
multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is strict multLoopStr
the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is set
the multF of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):]
[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is Relation-like set
[:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is Relation-like set
bool [:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is non empty set
multMagma(# the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the multF of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) #) is strict multMagma
G is non empty multMagma
D is (G)
the carrier of D is set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is strict 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
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
G is non empty multMagma
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is Relation-like 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:], 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 non empty (G)
the carrier of D is non empty set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is non empty strict multMagma
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
H is Element of the carrier of D
e is Element of the carrier of D
H * e is Element of the carrier of D
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] 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
G is multMagma
the carrier of G is set
the Element of the carrier of G is Element of the carrier of G
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is strict multLoopStr
the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is set
the multF of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):]
[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is Relation-like set
[:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is Relation-like set
bool [:[: the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):], the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #):] is non empty set
multMagma(# the carrier of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #), the multF of multLoopStr(# H1(G),H2(G), the Element of the carrier of G #) #) is strict multMagma
multMagma(# the carrier of G, the multF of G #) is strict multMagma
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is non empty strict 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
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
G is () multMagma
D is (G)
the carrier of D is set
H is Element of the carrier of D
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is strict multMagma
the carrier of G is set
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
G is () () multMagma
D is () (G)
the carrier of D is set
H is Relation-like Function-like Element of the carrier of D
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is strict multMagma
the carrier of G is set
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
G is non empty unital multMagma
D is non empty (G)
G is non empty associative multMagma
D is non empty (G)
G is non empty commutative multMagma
D is non empty (G)
G is non empty () () () multMagma
D is non empty (G)
G is non empty () () () multMagma
D is non empty (G)
G is non empty () multMagma
D is non empty (G)
G is non empty unital multMagma
the carrier of G is non empty set
the multF of G is Relation-like Function-like non empty total quasi_total having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is 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 H2(G) is Element of the carrier of G
multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) is strict multLoopStr
the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) is set
the multF of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):], the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):]
[: the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):] is Relation-like set
[:[: the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):], the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):] is Relation-like set
bool [:[: the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):], the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #):] is non empty set
multMagma(# the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the multF of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) #) is strict multMagma
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
H is non empty unital (G)
the carrier of H is non empty set
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
the multF of H is Relation-like Function-like non empty total quasi_total having_a_unity 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
G is non empty unital multMagma
D is non empty strict unital well-unital (G)
H is non empty strict unital well-unital (G)
1. D is Element of the carrier of D
the carrier of D is non empty set
the OneF of D is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total having_a_unity Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt H2(D) is Element of the carrier of D
1. H is Element of the carrier of H
the carrier of H is non empty set
the OneF of H is Element of the carrier of H
the multF of H is Relation-like Function-like non empty total quasi_total having_a_unity 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
the_unity_wrt H2(H) is Element of the carrier of H
multMagma(# the carrier of D, the multF of D #) is non empty strict multMagma
the carrier of G is non empty set
the multF of G is Relation-like Function-like non empty total quasi_total having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is 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
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
multMagma(# the carrier of H, the multF of H #) is non empty strict multMagma
G is multMagma
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
G is multMagma
the carrier of G is set
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
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
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
G is non empty unital multMagma
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 is Relation-like Function-like non empty total quasi_total having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is 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 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
{D} is non empty Element of bool the carrier of G
bool the carrier of G is non empty set
[:{D},{D}:] is Relation-like non empty set
[:[:{D},{D}:],{D}:] is Relation-like non empty set
bool [:[:{D},{D}:],{D}:] is non empty set
the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] is Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:]
multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #) is non empty strict multMagma
proj1 H2(G) is set
[:H1(G),H1(G):] is Relation-like set
(D,D) .--> D is Relation-like Function-like set
{[D,D]} is Relation-like Function-like non empty set
{[D,D]} --> D is Relation-like Function-like non empty total quasi_total Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like non empty set
bool [:{[D,D]},{D}:] is non empty set
[D,D] is V23() Element of [: the carrier of G, the carrier of G:]
[D,D] .--> D is set
{[D,D]} is Relation-like Function-like non empty set
{[D,D]} --> D is Relation-like Function-like non empty total quasi_total Element of bool [:{[D,D]},{D}:]
[:{[D,D]},{D}:] is Relation-like non empty set
bool [:{[D,D]},{D}:] is non empty set
the multF of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #) is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #), the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):], the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):]
the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #) is non empty set
[: the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #), the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):] is Relation-like non empty set
[:[: the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #), the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):], the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #), the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):], the carrier of multMagma(# {D}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{D},{D}:],{D}:] #):] is non empty set
N is non empty (G)
the carrier of N is non empty set
the multF of N is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like non empty set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is Relation-like non empty set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
G is multMagma
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
the (G) is (G)
H is multLoopStr
e is multLoopStr
the multF of e is Relation-like Function-like quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
the carrier of e is set
[: the carrier of e, the carrier of e:] is Relation-like set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is Relation-like set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
1. e is Element of the carrier of e
the OneF of e is Element of the carrier of e
N is multLoopStr
1. N is Element of the carrier of N
the carrier of N is set
the OneF of N is Element of the carrier of N
1. the (G) is Element of the carrier of the (G)
the carrier of the (G) is set
the OneF of the (G) is Element of the carrier of the (G)
H is multLoopStr
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
the multF of the (G) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):]
[: the carrier of the (G), the carrier of the (G):] is Relation-like set
[:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):] is Relation-like set
bool [:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):] is non empty set
multMagma(# the carrier of the (G), the multF of the (G) #) is strict multMagma
multMagma(# the carrier of G, the multF of G #) is strict multMagma
H is multLoopStr
the multF of H is Relation-like Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
the carrier of H is set
[: the carrier of H, the carrier of H:] is Relation-like set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
e is multLoopStr
G is multMagma
the (G) is (G)
the carrier of the (G) is set
the multF of the (G) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):]
[: the carrier of the (G), the carrier of the (G):] is Relation-like set
[:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):] is Relation-like set
bool [:[: the carrier of the (G), the carrier of the (G):], the carrier of the (G):] is non empty set
the OneF of the (G) is Element of the carrier of the (G)
multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #) is strict multLoopStr
1. multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #) is Element of the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #)
the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #) is set
the OneF of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #) is Element of the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #)
1. the (G) is Element of the carrier of the (G)
H is multLoopStr
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
the multF of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #) is Relation-like Function-like quasi_total Element of bool [:[: the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #), the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):], the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):]
[: the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #), the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):] is Relation-like set
[:[: the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #), the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):], the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):] is Relation-like set
bool [:[: the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #), the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):], the carrier of multLoopStr(# the carrier of the (G), the multF of the (G), the OneF of the (G) #):] is non empty set
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
G is non empty multMagma
D is multLoopStr
the carrier of D is set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the OneF of D is Element of the carrier of D
multLoopStr(# the carrier of D, the multF of D, the OneF of D #) is strict multLoopStr
1. multLoopStr(# the carrier of D, the multF of D, the OneF of D #) is Element of the carrier of multLoopStr(# the carrier of D, the multF of D, the OneF of D #)
the carrier of multLoopStr(# the carrier of D, the multF of D, the OneF of D #) is set
the OneF of multLoopStr(# the carrier of D, the multF of D, the OneF of D #) is Element of the carrier of multLoopStr(# the carrier of D, the multF of D, the OneF of D #)
H is multLoopStr
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
H is (G)
the carrier of H is set
the non empty strict (G) is non empty strict (G)
1. the non empty strict (G) is Element of the carrier of the non empty strict (G)
the carrier of the non empty strict (G) is non empty set
the OneF of the non empty strict (G) is Element of the carrier of the non empty strict (G)
H is multLoopStr
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
the multF of the non empty strict (G) is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of the non empty strict (G), the carrier of the non empty strict (G):], the carrier of the non empty strict (G):]
[: the carrier of the non empty strict (G), the carrier of the non empty strict (G):] is Relation-like non empty set
[:[: the carrier of the non empty strict (G), the carrier of the non empty strict (G):], the carrier of the non empty strict (G):] is Relation-like non empty set
bool [:[: the carrier of the non empty strict (G), the carrier of the non empty strict (G):], the carrier of the non empty strict (G):] is non empty set
multMagma(# the carrier of the non empty strict (G), the multF of the non empty strict (G) #) is non empty strict 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
multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma
H is (G)
G is multLoopStr
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
D is multLoopStr
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the carrier of D is set
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
1. D is Element of the carrier of D
the OneF of D is Element of the carrier of D
H is multLoopStr
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
G is non empty well-unital multLoopStr
1. G is Element of the carrier of G
the carrier of G is non empty set
the OneF of G is Element of the carrier of G
{H3(G)} is non empty Element of bool the carrier of G
bool the carrier of G is non empty set
[:{H3(G)},{H3(G)}:] is Relation-like non empty set
[:[:{H3(G)},{H3(G)}:],{H3(G)}:] is Relation-like non empty set
bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:] is non empty set
the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:] is Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:]
H is Element of {H3(G)}
multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #) is non empty strict multLoopStr
H3(G) * H3(G) 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
the multF of G . ((1. G),(1. G)) is Element of the carrier of G
[(1. G),(1. G)] is V23() set
{(1. G),(1. G)} is non empty set
{(1. G)} is non empty set
{{(1. G),(1. G)},{(1. G)}} is non empty set
the multF of G . [(1. G),(1. G)] is set
proj1 H2(G) is set
[:H1(G),H1(G):] is Relation-like set
[H3(G),H3(G)] is V23() Element of [: the carrier of G, the carrier of G:]
[H3(G),H3(G)] .--> H3(G) is set
{[H3(G),H3(G)]} is Relation-like Function-like non empty set
{[H3(G),H3(G)]} --> (1. G) is Relation-like Function-like non empty total quasi_total Element of bool [:{[H3(G),H3(G)]},{(1. G)}:]
[:{[H3(G),H3(G)]},{(1. G)}:] is Relation-like non empty set
bool [:{[H3(G),H3(G)]},{(1. G)}:] is non empty set
{[H3(G),H3(G)]} is Relation-like Function-like non empty Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
{[H3(G),H3(G)]} --> H3(G) is Relation-like Function-like non empty total quasi_total Element of bool [:{[H3(G),H3(G)]}, the carrier of G:]
[:{[H3(G),H3(G)]}, the carrier of G:] is Relation-like non empty set
bool [:{[H3(G),H3(G)]}, the carrier of G:] is non empty set
[:{[H3(G),H3(G)]},{(1. G)}:] is Relation-like non empty set
(H3(G),H3(G)) .--> H3(G) is Relation-like Function-like set
{[(1. G),(1. G)]} is Relation-like Function-like non empty set
{[(1. G),(1. G)]} --> (1. G) is Relation-like Function-like non empty total quasi_total Element of bool [:{[(1. G),(1. G)]},{(1. G)}:]
[:{[(1. G),(1. G)]},{(1. G)}:] is Relation-like non empty set
bool [:{[(1. G),(1. G)]},{(1. G)}:] is non empty set
1. multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #) is Element of the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #)
the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #) is non empty set
the OneF of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #) is Element of the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #)
the multF of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #) is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #), the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):], the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):]
[: the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #), the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):] is Relation-like non empty set
[:[: the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #), the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):], the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):] is Relation-like non empty set
bool [:[: the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #), the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):], the carrier of multLoopStr(# {H3(G)}, the Relation-like Function-like non empty total quasi_total Element of bool [:[:{H3(G)},{H3(G)}:],{H3(G)}:],H #):] is non empty set
N is non empty (G)
the carrier of N is non empty set
c7 is Element of the carrier of N
the multF of N is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like non empty set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is Relation-like non empty set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
1. N is Element of the carrier of N
the OneF of N is Element of the carrier of N
H2(N) . (H3(N),c7) is Element of the carrier of N
[(1. N),c7] is V23() set
{(1. N),c7} is non empty set
{(1. N)} is non empty set
{{(1. N),c7},{(1. N)}} is non empty set
the multF of N . [(1. N),c7] is set
H2(N) . (c7,H3(N)) is Element of the carrier of N
[c7,(1. N)] is V23() set
{c7,(1. N)} is non empty set
{c7} is non empty set
{{c7,(1. N)},{c7}} is non empty set
the multF of N . [c7,(1. N)] is set
G is multMagma
D is (G)
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the carrier of D is set
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
G is multMagma
D is (G)
H is (D)
the carrier of D is set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is strict multMagma
the carrier of G is set
the multF of G is Relation-like Function-like 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 set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
the multF of H is Relation-like Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
the carrier of H is set
[: the carrier of H, the carrier of H:] is Relation-like set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
G is multMagma
D is (G)
H is (D)
the multF of H is Relation-like Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
the carrier of H is set
[: the carrier of H, the carrier of H:] is Relation-like set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the carrier of D is set
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
G is multMagma
D is (G)
e is (D)
H is (G)
G is multMagma
D is (G)
H is (D)
1. H is Element of the carrier of H
the carrier of H is set
the OneF of H is Element of the carrier of H
1. D is Element of the carrier of D
the carrier of D is set
the OneF of D is Element of the carrier of D
the multF of H is Relation-like Function-like 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 set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of G is Relation-like Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set
e is multLoopStr
1. e is Element of the carrier of e
the carrier of e is set
the OneF of e is Element of the carrier of e
G is non empty multMagma
D is non empty multLoopStr
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 is non empty set
[: 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 multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the carrier of D is non empty set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
1. D is Element of the carrier of D
the OneF of D is Element of the carrier of D
G is non empty multMagma
the carrier of G is non empty set
D is non empty (G)
the carrier of D is non empty set
H is non empty (G)
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
proj1 H2(H) is set
[:H1(H),H1(H):] is Relation-like 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
proj1 H2(G) is set
[:H1(G),H1(G):] is Relation-like set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
proj1 H2(D) is set
[:H1(D),H1(D):] is Relation-like set
e is set
[e,e] is V23() set
{e,e} is non empty set
{e} is non empty set
{{e,e},{e}} is non empty set
e is set
[e,e] is V23() set
{e,e} is non empty set
{e} is non empty set
{{e,e},{e}} is non empty set
G is non empty multMagma
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 is non empty set
[: 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 non empty (G)
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
the carrier of D is non empty set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of G || the carrier of D is Relation-like Function-like set
the multF of G | [: the carrier of D, the carrier of D:] is Relation-like Function-like set
proj1 H2(D) is set
[:H1(D),H1(D):] is Relation-like set
G is non empty multMagma
the carrier of G is non empty set
D is non empty (G)
the carrier of D is non empty set
H is Element of the carrier of D
e is Element of the carrier of D
H * e is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] 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 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 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
proj1 H2(D) is set
[:H1(D),H1(D):] is Relation-like set
[H,e] is V23() Element of [: the carrier of D, the carrier of D:]
H2(D) . [H,e] is Element of the carrier of D
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
H is non empty (G)
the carrier of H is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
multMagma(# the carrier of D, the multF of D #) is non empty strict multMagma
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
multMagma(# the carrier of H, the multF of H #) is non empty strict multMagma
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 is non empty set
[: 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
proj1 H2(D) is set
[:H1(D),H1(D):] is Relation-like set
H2(G) || H1(D) is Relation-like Function-like set
the multF of G | [: the carrier of D, the carrier of D:] is Relation-like Function-like set
proj1 H2(H) is set
G is non empty multLoopStr
D is non empty (G)
the carrier of D is non empty set
H is non empty (G)
the carrier of H is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the OneF of D is Element of the carrier of D
multLoopStr(# the carrier of D, the multF of D, the OneF of D #) is non empty strict multLoopStr
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
the OneF of H is Element of the carrier of H
multLoopStr(# the carrier of H, the multF of H, the OneF of H #) is non empty strict multLoopStr
1. D is Element of the carrier of D
1. G is Element of the carrier of G
the carrier of G is non empty set
the OneF of G is Element of the carrier of G
1. H is Element of the carrier of H
e is (G)
the carrier of e is set
the multF of e is Relation-like Function-like quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
[: the carrier of e, the carrier of e:] is Relation-like set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is Relation-like set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
multMagma(# the carrier of e, the multF of e #) is strict multMagma
N is (G)
the carrier of N is set
the multF of N is Relation-like Function-like quasi_total Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is Relation-like set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
multMagma(# the carrier of N, the multF of N #) is strict multMagma
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
H is non empty (G)
the carrier of H is non empty set
[:H1(D),H1(D):] is Relation-like set
[:H1(H),H1(H):] is Relation-like 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 is non empty set
[: 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
H2(G) || H1(H) is Relation-like Function-like set
[: the carrier of H, the carrier of H:] is Relation-like non empty set
the multF of G | [: the carrier of H, the carrier of H:] is Relation-like Function-like set
(H2(G) || H1(H)) || H1(D) is Relation-like Function-like set
[: the carrier of D, the carrier of D:] is Relation-like non empty set
(H2(G) || H1(H)) | [: the carrier of D, the carrier of D:] is Relation-like Function-like set
H2(G) || H1(D) is Relation-like Function-like set
the multF of G | [: the carrier of D, the carrier of D:] is Relation-like Function-like 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:], 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
proj1 H2(H) is set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
proj1 H2(D) is set
G is non empty multLoopStr
D is non empty (G)
the carrier of D is non empty set
H is non empty (G)
the carrier of H is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] 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
1. D is Element of the carrier of D
the OneF of D is Element of the carrier of D
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
1. G is Element of the carrier of G
the carrier of G is non empty set
the OneF of G 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
D is non empty (G)
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt the multF of D is Element of the carrier of D
the_unity_wrt H2(G) is Element of the carrier of G
N is Element of the carrier of D
e is Element of the carrier of D
e * N is Element of the carrier of D
the multF of D . (e,N) is Element of the carrier of D
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of D . [e,N] is set
N is Element of the carrier of G
(the_unity_wrt H2(G)) * N is Element of the carrier of G
the multF of G . ((the_unity_wrt H2(G)),N) is Element of the carrier of G
[(the_unity_wrt H2(G)),N] is V23() set
{(the_unity_wrt H2(G)),N} is non empty set
{(the_unity_wrt H2(G))} is non empty set
{{(the_unity_wrt H2(G)),N},{(the_unity_wrt H2(G))}} is non empty set
the multF of G . [(the_unity_wrt H2(G)),N] is set
N * e is Element of the carrier of D
the multF of D . (N,e) is Element of the carrier of D
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of D . [N,e] is set
N * (the_unity_wrt H2(G)) is Element of the carrier of G
the multF of G . (N,(the_unity_wrt H2(G))) is Element of the carrier of G
[N,(the_unity_wrt H2(G))] is V23() set
{N,(the_unity_wrt H2(G))} is non empty set
{N} is non empty set
{{N,(the_unity_wrt H2(G))},{N}} is non empty set
the multF of G . [N,(the_unity_wrt H2(G))] is set
N is Element of the carrier of D
e * N is Element of the carrier of D
the multF of D . (e,N) is Element of the carrier of D
[e,N] is V23() set
{e,N} is non empty set
{{e,N},{e}} is non empty set
the multF of D . [e,N] is set
H2(D) . (e,N) is Element of the carrier of D
N * e is Element of the carrier of D
the multF of D . (N,e) is Element of the carrier of D
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of D . [N,e] is set
H2(D) . (N,e) is Element of the carrier of D
G is non empty well-unital multLoopStr
D is non empty (G)
the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G 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
1. D is Element of the carrier of D
the carrier of D is non empty set
the OneF of D is Element of the carrier of D
H is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
H2(D) . (H3(D),H) is Element of the carrier of D
[(1. D),H] is V23() set
{(1. D),H} is non empty set
{(1. D)} is non empty set
{{(1. D),H},{(1. D)}} is non empty set
the multF of D . [(1. D),H] is set
H3(D) * H is Element of the carrier of D
the multF of D . ((1. D),H) is Element of the carrier of D
e is Element of the carrier of G
H3(G) * e is Element of the carrier of G
the multF of G . ((1. G),e) is Element of the carrier of G
[(1. G),e] is V23() set
{(1. G),e} is non empty set
{(1. G)} is non empty set
{{(1. G),e},{(1. G)}} is non empty set
the multF of G . [(1. G),e] is set
H2(D) . (H,H3(D)) is Element of the carrier of D
[H,(1. D)] is V23() set
{H,(1. D)} is non empty set
{H} is non empty set
{{H,(1. D)},{H}} is non empty set
the multF of D . [H,(1. D)] is set
H * H3(D) is Element of the carrier of D
the multF of D . (H,(1. D)) is Element of the carrier of D
e * H3(G) is Element of the carrier of G
the multF of G . (e,(1. G)) is Element of the carrier of G
[e,(1. G)] is V23() set
{e,(1. G)} is non empty set
{e} is non empty set
{{e,(1. G)},{e}} is non empty set
the multF of G . [e,(1. G)] is set
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
the carrier of G is non empty set
H is Element of the carrier of D
e is Element of the carrier of D
H * e is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] 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 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 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
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
e * H is Element of the carrier of D
the multF of D . (e,H) is Element of the carrier of D
[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 D . [e,H] is set
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
the carrier of G is non empty set
H is Element of the carrier of D
e is Element of the carrier of D
N is Element of the carrier of D
H * e is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] is set
e * N is Element of the carrier of D
the multF of D . (e,N) is Element of the carrier of D
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of D . [e,N] is set
(H * e) * N is Element of the carrier of D
the multF of D . ((H * e),N) is Element of the carrier of D
[(H * e),N] is V23() set
{(H * e),N} is non empty set
{(H * e)} is non empty set
{{(H * e),N},{(H * e)}} is non empty set
the multF of D . [(H * e),N] is set
f is Element of the carrier of G
b9 is Element of the carrier of G
f * b9 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
the multF of G . (f,b9) is Element of the carrier of G
[f,b9] is V23() set
{f,b9} is non empty set
{f} is non empty set
{{f,b9},{f}} is non empty set
the multF of G . [f,b9] is set
N is Element of the carrier of G
c7 is Element of the carrier of G
N * c7 is Element of the carrier of G
the multF of G . (N,c7) is Element of the carrier of G
[N,c7] is V23() set
{N,c7} is non empty set
{N} is non empty set
{{N,c7},{N}} is non empty set
the multF of G . [N,c7] is set
(N * c7) * b9 is Element of the carrier of G
the multF of G . ((N * c7),b9) is Element of the carrier of G
[(N * c7),b9] is V23() set
{(N * c7),b9} is non empty set
{(N * c7)} is non empty set
{{(N * c7),b9},{(N * c7)}} is non empty set
the multF of G . [(N * c7),b9] is set
c7 * b9 is Element of the carrier of G
the multF of G . (c7,b9) is Element of the carrier of G
[c7,b9] is V23() set
{c7,b9} is non empty set
{c7} is non empty set
{{c7,b9},{c7}} is non empty set
the multF of G . [c7,b9] is set
N * (c7 * b9) is Element of the carrier of G
the multF of G . (N,(c7 * b9)) is Element of the carrier of G
[N,(c7 * b9)] is V23() set
{N,(c7 * b9)} is non empty set
{{N,(c7 * b9)},{N}} is non empty set
the multF of G . [N,(c7 * b9)] is set
g is Element of the carrier of G
N * g is Element of the carrier of G
the multF of G . (N,g) is Element of the carrier of G
[N,g] is V23() set
{N,g} is non empty set
{{N,g},{N}} is non empty set
the multF of G . [N,g] is set
H * (e * N) is Element of the carrier of D
the multF of D . (H,(e * N)) is Element of the carrier of D
[H,(e * N)] is V23() set
{H,(e * N)} is non empty set
{{H,(e * N)},{H}} is non empty set
the multF of D . [H,(e * N)] is set
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
the carrier of G is non empty set
H is Element of the carrier of D
H * H is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,H) is Element of the carrier of D
[H,H] is V23() set
{H,H} is non empty set
{H} is non empty set
{{H,H},{H}} is non empty set
the multF of D . [H,H] is set
e is Element of the carrier of G
e * 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
the multF of G . (e,e) is Element of the carrier 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
the multF of G . [e,e] is set
G is non empty multMagma
D is non empty (G)
the carrier of D is non empty set
the carrier of G is non empty set
H is Element of the carrier of D
e is Element of the carrier of D
N is Element of the carrier of D
e * H is Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (e,H) is Element of the carrier of D
[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 D . [e,H] is set
c7 is Element of the carrier of G
N is Element of the carrier of G
c7 * N 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
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 * H is Element of the carrier of D
the multF of D . (N,H) is Element of the carrier of D
[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 D . [N,H] is set
b9 is Element of the carrier of G
b9 * N is Element of the carrier of G
the multF of G . (b9,N) is Element of the carrier of G
[b9,N] is V23() set
{b9,N} is non empty set
{b9} is non empty set
{{b9,N},{b9}} is non empty set
the multF of G . [b9,N] is set
H * e is Element of the carrier of D
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] is set
N * c7 is Element of the carrier of G
the multF of G . (N,c7) is Element of the carrier of G
[N,c7] is V23() set
{N,c7} is non empty set
{N} is non empty set
{{N,c7},{N}} is non empty set
the multF of G . [N,c7] is set
H * N is Element of the carrier of D
the multF of D . (H,N) is Element of the carrier of D
[H,N] is V23() set
{H,N} is non empty set
{{H,N},{H}} is non empty set
the multF of D . [H,N] is set
N * b9 is Element of the carrier of G
the multF of G . (N,b9) is Element of the carrier of G
[N,b9] is V23() set
{N,b9} is non empty set
{{N,b9},{N}} is non empty set
the multF of G . [N,b9] 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
the_unity_wrt the multF of G is Element of the carrier of G
D is non empty (G)
the carrier of D is non empty set
the_unity_wrt H2(G) is Element of the carrier of G
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt the multF of D is Element of the carrier of D
H is Element of the carrier of D
e is Element of the carrier of D
the multF of D . (H,e) is Element of the carrier of D
[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 D . [H,e] is set
H2(D) . (H,e) is Element of the carrier of D
H * e is Element of the carrier of D
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
H2(G) . (N,N) is Element of the carrier of G
the_unity_wrt H2(D) is Element of the carrier of D
G is non empty well-unital () multLoopStr
D is non empty (G)
1. G is Element of the carrier of G
the carrier of G is non empty set
the OneF of G is Element of the carrier of G
1. D is Element of the carrier of D
the carrier of D is non empty set
the OneF of D is Element of the carrier of D
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 H2(G) is Element of the carrier of G
G is non empty () multMagma
D is non empty (G)
the carrier of D is non empty set
H is Element of the carrier of D
the carrier of G is non empty set
D is non empty (G)
the carrier of D is non empty set
H is Element of the carrier of D
the carrier of G is non empty set
G is non empty () () multMagma
D is non empty () (G)
the carrier of D is non empty set
H is Relation-like Function-like Element of the carrier of D
the carrier of G is non empty set
D is non empty () (G)
the carrier of D is non empty set
H is Relation-like Function-like Element of the carrier of D
the carrier of G is non empty set
G is non empty well-unital multLoopStr
D is non empty (G)
G is non empty commutative multMagma
D is non empty (G)
D is non empty (G)
G is non empty associative multMagma
D is non empty (G)
D is non empty (G)
G is non empty () multMagma
D is non empty (G)
D is non empty (G)
G is non empty () () () multMagma
D is non empty (G)
D is non empty (G)
G is non empty well-unital () multLoopStr
D is non empty well-unital (G)
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
D is non empty Element of bool 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
proj1 the multF of G is non empty set
the multF of G || D is Relation-like Function-like set
[:D,D:] is Relation-like non empty set
the multF of G | [:D,D:] is Relation-like Function-like set
proj2 ( the multF of G || D) is set
N is set
proj1 ( the multF of G || D) is set
N is set
( the multF of G || D) . N is set
[:D,D:] is Relation-like non empty Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
c7 is Element of [:D,D:]
c7 `1 is Element of D
c7 `2 is Element of D
b9 is Element of D
f is Element of D
[b9,f] is V23() Element of [:D,D:]
{b9,f} is non empty set
{b9} is non empty set
{{b9,f},{b9}} is non empty set
b9 * f is Element of the carrier of G
the multF of G . (b9,f) is Element of the carrier of G
[b9,f] is V23() set
the multF of G . [b9,f] is set
proj1 ( the multF of G || D) is set
[:D,D:] is Relation-like non empty Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is non empty set
[:[:D,D:],D:] is Relation-like non empty set
bool [:[:D,D:],D:] is non empty set
N is Relation-like Function-like non empty total quasi_total Element of bool [:[:D,D:],D:]
multMagma(# D,N #) is non empty strict multMagma
N is non empty strict (G)
the carrier of N is non empty set
F1() is non empty multMagma
the carrier of F1() is non empty set
G is set
H is Element of the carrier of F1()
D is non empty set
H is set
bool the carrier of F1() is non empty set
H is non empty Element of bool the carrier of F1()
e is Element of H
N is Element of H
e * N is Element of the carrier of F1()
the multF of F1() is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of F1(), the carrier of F1():], the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is Relation-like non empty set
[:[: the carrier of F1(), the carrier of F1():], the carrier of F1():] is Relation-like non empty set
bool [:[: the carrier of F1(), the carrier of F1():], the carrier of F1():] is non empty set
the multF of F1() . (e,N) is Element of the carrier of F1()
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of F1() . [e,N] is set
e is non empty strict (F1())
the carrier of e is non empty set
N is Element of the carrier of F1()
N is Element of the carrier of F1()
F1() is non empty multLoopStr
the carrier of F1() is non empty set
1. F1() is Element of the carrier of F1()
the OneF of F1() is Element of the carrier of F1()
G is non empty multMagma
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 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 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 non empty strict (G)
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
H is Element of the carrier of D
multLoopStr(# H1(D),H2(D),H #) is strict multLoopStr
1. multLoopStr(# H1(D),H2(D),H #) is Element of the carrier of multLoopStr(# H1(D),H2(D),H #)
the carrier of multLoopStr(# H1(D),H2(D),H #) is set
the OneF of multLoopStr(# H1(D),H2(D),H #) is Element of the carrier of multLoopStr(# H1(D),H2(D),H #)
the multF of F1() is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of F1(), the carrier of F1():], the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is Relation-like non empty set
[:[: the carrier of F1(), the carrier of F1():], the carrier of F1():] is Relation-like non empty set
bool [:[: the carrier of F1(), the carrier of F1():], the carrier of F1():] is non empty set
N is non empty strict (F1())
the carrier of N is non empty set
N is Element of the carrier of F1()
c7 is Element of the carrier of F1()
G is multMagma
the carrier of G is set
() is non empty multMagma
the carrier of () is non empty set
G is set
D is set
G is non empty associative commutative () () () (())
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 is Relation-like Function-like non empty total quasi_total associative 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 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 ()
N is Element of the carrier of ()
e * N is Element of the carrier of ()
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (e,N) is Element of the carrier of ()
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of () . [e,N] is set
N is V37() V45() V146() Element of REAL
c7 is V37() V45() V146() Element of REAL
N + c7 is V37() V45() V146() Element of REAL
G is non empty unital associative commutative () () () (())
the carrier of G is non empty set
the multF of G is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is 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
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
H2(G) . (D,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
H2(G) . (e,D) is Element of the carrier of G
H is V37() V45() V146() Element of REAL
H + 0 is V37() V45() V146() Element of REAL
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,D},{D}} is non empty set
the multF of G . [D,D] is set
H + H is V37() V45() V146() Element of REAL
G is non empty unital multMagma
D is non empty (G)
proj1 addreal is non empty set
addreal || INT is Relation-like Function-like set
addreal | [:INT,INT:] is Relation-like Function-like set
proj1 (addreal || INT) is set
G is set
G `1 is set
G `2 is set
[(G `1),(G `2)] is V23() set
{(G `1),(G `2)} is non empty set
{(G `1)} is non empty set
{{(G `1),(G `2)},{(G `1)}} is non empty set
addint . G is set
D is V37() V45() integer V47() V146() Element of INT
H is V37() V45() integer V47() V146() Element of INT
addint . (D,H) is V37() V45() integer V47() V146() Element of INT
[D,H] is V23() set
{D,H} is non empty V159() V160() V161() V162() V163() set
{D} is non empty V159() V160() V161() V162() V163() set
{{D,H},{D}} is non empty set
addint . [D,H] is set
addreal . (D,H) is set
addreal . [D,H] is set
(addreal || INT) . G is set
proj1 addint is non empty set
the multF of INT.Group is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:]
[: the carrier of INT.Group, the carrier of INT.Group:] is Relation-like non empty set
[:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:] is Relation-like non empty set
bool [:[: the carrier of INT.Group, the carrier of INT.Group:], the carrier of INT.Group:] is non empty set
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
() is non empty strict unital Group-like associative commutative V170() () () () () () () (())
G is non empty strict associative commutative () () () (())
the carrier of G is non empty set
D is non empty strict associative commutative () () () (())
the carrier of D is non empty set
the carrier of () is non empty V159() V160() V161() V162() V163() set
G is set
D is set
addint || NAT is Relation-like Function-like set
addint | [:NAT,NAT:] is Relation-like Function-like set
proj1 addint is non empty set
proj1 (addint || NAT) is set
[:NAT,NAT:] is Relation-like non empty Element of bool [:REAL,REAL:]
proj2 (addint || NAT) is set
D is set
H is set
(addint || NAT) . H is set
H `1 is set
H `2 is set
e is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
addint . H is set
N is integer set
c7 is integer set
addint . (N,c7) is set
[N,c7] is V23() set
{N,c7} is non empty V159() V160() V161() V162() V163() set
{N} is non empty V159() V160() V161() V162() V163() set
{{N,c7},{N}} is non empty set
addint . [N,c7] is set
e + N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
D is Relation-like Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
multMagma(# NAT,D #) is non empty strict multMagma
H is non empty strict associative commutative () () () ((),())
the carrier of H is non empty set
N is Element of the carrier of H
e is Element of the carrier of H
e * N is Element of the carrier of H
the multF of H is Relation-like Function-like non empty total quasi_total associative 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
the multF of H . (e,N) is Element of the carrier of H
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of H . [e,N] is set
N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
0 + N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N * e is Element of the carrier of H
the multF of H . (N,e) is Element of the carrier of H
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of H . [N,e] is set
N + 0 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N is Element of the carrier of H
H2(H) . (e,N) is Element of the carrier of H
[e,N] is V23() set
{e,N} is non empty set
{{e,N},{e}} is non empty set
the multF of H . [e,N] is set
e * N is Element of the carrier of H
the multF of H . (e,N) is Element of the carrier of H
H2(H) . (N,e) is Element of the carrier of H
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of H . [N,e] is set
N * e is Element of the carrier of H
the multF of H . (N,e) is Element of the carrier of H
the_unity_wrt H2(H) is Element of the carrier of H
N is Element of the carrier of H
N is Element of the carrier of H
N * N is Element of the carrier of H
the multF of H . (N,N) is Element of the carrier of H
[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 H . [N,N] is set
c7 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
b9 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
c7 + b9 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
G is non empty strict unital associative commutative () () () () ((),())
the carrier of G is non empty set
D is non empty strict unital associative commutative () () () () ((),())
the carrier of D is non empty set
() is non empty strict unital associative commutative () () () () ((),())
G is non empty strict unital associative commutative well-unital () () () () (())
D is non empty strict unital associative commutative well-unital () () () () (())
() is non empty strict unital associative commutative well-unital () () () () (())
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
G is Relation-like Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]
D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
H is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
addnat . (D,H) is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
[D,H] is V23() set
{D,H} is non empty V159() V160() V161() V162() V163() V164() set
{D} is non empty V159() V160() V161() V162() V163() V164() set
{{D,H},{D}} is non empty set
addnat . [D,H] is set
D + H is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
addint . (D,H) is set
addint . [D,H] is set
addint || NAT is Relation-like Function-like set
addint | [:NAT,NAT:] is Relation-like Function-like set
[D,H] is V23() Element of [:NAT,NAT:]
(addint || NAT) . [D,H] is set
the multF of () . (D,H) is set
the multF of () . [D,H] is set
multMagma(# NAT,addnat #) is non empty strict multMagma
the carrier of () is non empty set
G is set
[: the carrier of (), the carrier of ():] is Relation-like non empty set
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
G is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
H is Element of the carrier of ()
D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
e is Element of the carrier of ()
H * e is Element of the carrier of ()
the multF of () . (H,e) is Element of the carrier of ()
[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 () . [H,e] is set
G + D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
multLoopStr(# NAT,addnat,0 #) is non empty strict multLoopStr
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
multMagma(# the carrier of (), the multF of () #) is non empty strict associative multMagma
the_unity_wrt H2(()) is Element of the carrier of ()
1. () is Element of the carrier of ()
the OneF of () is Element of the carrier of ()
addreal || NAT is Relation-like Function-like set
addreal | [:NAT,NAT:] is Relation-like Function-like set
addint || NAT is Relation-like Function-like set
addint | [:NAT,NAT:] is Relation-like Function-like set
the_unity_wrt addnat is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
G is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
multMagma(# REAL,multreal #) is non empty strict multMagma
() is non empty strict unital associative commutative multMagma
the carrier of () is non empty set
G is set
D is set
G is non empty associative commutative (())
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 is Relation-like Function-like non empty total quasi_total associative 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 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 ()
N is Element of the carrier of ()
e * N is Element of the carrier of ()
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (e,N) is Element of the carrier of ()
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of () . [e,N] is set
N is V37() V45() V146() Element of REAL
c7 is V37() V45() V146() Element of REAL
N * c7 is V37() V45() V146() Element of REAL
G is non empty unital associative commutative (())
the carrier of G is non empty set
the multF of G is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is 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
(the_unity_wrt H2(G)) * (the_unity_wrt H2(G)) is Element of the carrier of G
the multF of G . ((the_unity_wrt H2(G)),(the_unity_wrt H2(G))) is Element of the carrier of G
[(the_unity_wrt H2(G)),(the_unity_wrt H2(G))] is V23() set
{(the_unity_wrt H2(G)),(the_unity_wrt H2(G))} is non empty set
{(the_unity_wrt H2(G))} is non empty set
{{(the_unity_wrt H2(G)),(the_unity_wrt H2(G))},{(the_unity_wrt H2(G))}} is non empty set
the multF of G . [(the_unity_wrt H2(G)),(the_unity_wrt H2(G))] is set
H is V37() V45() V146() Element of REAL
H * H is V37() V45() V146() Element of REAL
H * 1 is V37() V45() V146() Element of REAL
multreal || NAT is Relation-like Function-like set
multreal | [:NAT,NAT:] is Relation-like Function-like set
proj1 multreal is non empty set
proj1 (multreal || NAT) is set
[:NAT,NAT:] is Relation-like non empty Element of bool [:REAL,REAL:]
proj2 (multreal || NAT) is set
D is set
H is set
(multreal || NAT) . H is set
H `1 is set
H `2 is set
multreal . H is set
e is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
multreal . (e,N) is V37() V45() V146() Element of REAL
[e,N] is V23() set
{e,N} is non empty V159() V160() V161() V162() V163() V164() set
{e} is non empty V159() V160() V161() V162() V163() V164() set
{{e,N},{e}} is non empty set
multreal . [e,N] is set
e * N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
D is Relation-like Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
multMagma(# NAT,D #) is non empty strict multMagma
H is non empty strict associative commutative (())
the carrier of H is non empty set
N is Element of the carrier of H
e is Element of the carrier of H
e * N is Element of the carrier of H
the multF of H is Relation-like Function-like non empty total quasi_total associative 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
the multF of H . (e,N) is Element of the carrier of H
[e,N] is V23() set
{e,N} is non empty set
{e} is non empty set
{{e,N},{e}} is non empty set
the multF of H . [e,N] is set
N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
1 * N is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N * e is Element of the carrier of H
the multF of H . (N,e) is Element of the carrier of H
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of H . [N,e] is set
N * 1 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
N is Element of the carrier of H
H2(H) . (e,N) is Element of the carrier of H
[e,N] is V23() set
{e,N} is non empty set
{{e,N},{e}} is non empty set
the multF of H . [e,N] is set
e * N is Element of the carrier of H
the multF of H . (e,N) is Element of the carrier of H
H2(H) . (N,e) is Element of the carrier of H
[N,e] is V23() set
{N,e} is non empty set
{N} is non empty set
{{N,e},{N}} is non empty set
the multF of H . [N,e] is set
N * e is Element of the carrier of H
the multF of H . (N,e) is Element of the carrier of H
the_unity_wrt H2(H) is Element of the carrier of H
N is Element of the carrier of H
N is Element of the carrier of H
N * N is Element of the carrier of H
the multF of H . (N,N) is Element of the carrier of H
[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 H . [N,N] is set
c7 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
b9 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
c7 * b9 is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
G is non empty strict unital associative commutative () (())
the carrier of G is non empty set
D is non empty strict unital associative commutative () (())
the carrier of D is non empty set
() is non empty strict unital associative commutative () (())
G is non empty strict unital associative commutative well-unital () (())
D is non empty strict unital associative commutative well-unital () (())
() is non empty strict unital associative commutative well-unital () (())
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
G is Relation-like Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]
D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
H is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
multnat . (D,H) is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
[D,H] is V23() set
{D,H} is non empty V159() V160() V161() V162() V163() V164() set
{D} is non empty V159() V160() V161() V162() V163() V164() set
{{D,H},{D}} is non empty set
multnat . [D,H] is set
D * H is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
multreal . (D,H) is V37() V45() V146() Element of REAL
multreal . [D,H] is set
multreal || NAT is Relation-like Function-like set
multreal | [:NAT,NAT:] is Relation-like Function-like set
[D,H] is V23() Element of [:NAT,NAT:]
(multreal || NAT) . [D,H] is set
the multF of () . (D,H) is set
the multF of () . [D,H] is set
multMagma(# NAT,multnat #) is non empty strict multMagma
G is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
H is Element of the carrier of ()
D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
e is Element of the carrier of ()
H * e is Element of the carrier of ()
the multF of () . (H,e) is Element of the carrier of ()
[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 () . [H,e] is set
G * D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
the_unity_wrt the multF of () is Element of the carrier of ()
the carrier of () is non empty set
G is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
G * D is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
H is Element of the carrier of ()
e is Element of the carrier of ()
H * e is Element of the carrier of ()
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (H,e) is Element of the carrier of ()
[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 () . [H,e] is set
multMagma(# the carrier of (), the multF of () #) is non empty strict associative multMagma
N is Element of the carrier of ()
N is Element of the carrier of ()
N * N is Element of the carrier of ()
the multF of () . (N,N) is Element of the carrier of ()
[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 () . [N,N] is set
multLoopStr(# NAT,multnat,1 #) is non empty strict multLoopStr
the multF of () is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
multMagma(# the carrier of (), the multF of () #) is non empty strict associative multMagma
the_unity_wrt H2(()) is Element of the carrier of ()
1. () is Element of the carrier of ()
the OneF of () is Element of the carrier of ()
multreal || NAT is Relation-like Function-like set
multreal | [:NAT,NAT:] is Relation-like Function-like set
G is V37() V38() V39() V40() V44() V45() integer V47() V146() V159() V160() V161() V162() V163() V164() Element of NAT
G is non empty set
G * is functional non empty FinSequence-membered M13(G)
[:(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 *):]
multMagma(# (G *),D #) is non empty strict multMagma
the carrier of multMagma(# (G *),D #) is non empty set
e is Element of the carrier of multMagma(# (G *),D #)
e is non empty strict () () multMagma
the multF of e is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of e, the carrier of e:], the carrier of e:]
the carrier of e is non empty set
[: the carrier of e, the carrier of e:] is Relation-like non empty set
[:[: the carrier of e, the carrier of e:], the carrier of e:] is Relation-like non empty set
bool [:[: the carrier of e, the carrier of e:], the carrier of e:] is non empty set
<*> G is Relation-like non-empty empty-yielding NAT -defined G -valued Function-like one-to-one constant functional empty proper V38() V39() V40() V42() V43() V44() V50() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V163() V164() V165() FinSequence of G
[:NAT,G:] is Relation-like non empty set
c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
c7 * b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (c7,b9) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[c7,b9] is V23() set
{c7,b9} is functional non empty set
{c7} is functional non empty set
{{c7,b9},{c7}} is non empty set
the multF of e . [c7,b9] is set
c7 ^ b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 * c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,c7) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,c7] is V23() set
{b9,c7} is functional non empty set
{b9} is functional non empty set
{{b9,c7},{b9}} is non empty set
the multF of e . [b9,c7] is set
b9 ^ c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 * f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,f) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,f] is V23() set
{b9,f} is functional non empty set
{b9} is functional non empty set
{{b9,f},{b9}} is non empty set
the multF of e . [b9,f] is set
g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
f * g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (f,g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[f,g] is V23() set
{f,g} is functional non empty set
{f} is functional non empty set
{{f,g},{f}} is non empty set
the multF of e . [f,g] is set
(b9 * f) * g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . ((b9 * f),g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[(b9 * f),g] is V23() set
{(b9 * f),g} is functional non empty set
{(b9 * f)} is functional non empty set
{{(b9 * f),g},{(b9 * f)}} is non empty set
the multF of e . [(b9 * f),g] is set
f9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
f9 ^ g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 ^ f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(b9 ^ f) ^ g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
f ^ g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 ^ (f ^ g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
f9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 ^ f9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 * (f * g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,(f * g)) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,(f * g)] is V23() set
{b9,(f * g)} is functional non empty set
{{b9,(f * g)},{b9}} is non empty set
the multF of e . [b9,(f * g)] is set
f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
f * b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (f,b9) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[f,b9] is V23() set
{f,b9} is functional non empty set
{f} is functional non empty set
{{f,b9},{f}} is non empty set
the multF of e . [f,b9] is set
f ^ b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
g * b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (g,b9) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[g,b9] is V23() set
{g,b9} is functional non empty set
{g} is functional non empty set
{{g,b9},{g}} is non empty set
the multF of e . [g,b9] is set
g ^ b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 * f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,f) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,f] is V23() set
{b9,f} is functional non empty set
{b9} is functional non empty set
{{b9,f},{b9}} is non empty set
the multF of e . [b9,f] is set
b9 ^ f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 * g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,g] is V23() set
{b9,g} is functional non empty set
{{b9,g},{b9}} is non empty set
the multF of e . [b9,g] is set
b9 ^ g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
the_unity_wrt the multF of e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (b9,f) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[b9,f] is V23() set
{b9,f} is functional non empty set
{b9} is functional non empty set
{{b9,f},{b9}} is non empty set
the multF of e . [b9,f] is set
g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
c7 * g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (c7,g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[c7,g] is V23() set
{c7,g} is functional non empty set
{{c7,g},{c7}} is non empty set
the multF of e . [c7,g] is set
H2(e) . (c7,g) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
g * c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the multF of e . (g,c7) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
[g,c7] is V23() set
{g,c7} is functional non empty set
{g} is functional non empty set
{{g,c7},{g}} is non empty set
the multF of e . [g,c7] is set
H2(e) . (g,c7) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
H2(e) . (b9,f) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
the_unity_wrt H2(e) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 * f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of e
b9 ^ f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
N is non empty strict unital associative () () () () () () multMagma
the carrier of N is non empty set
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of N
c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of N
N * c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of N
the multF of N is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like non empty set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is Relation-like non empty set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
the multF of N . (N,c7) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of N
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of N . [N,c7] is set
N ^ c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
D is non empty strict unital associative () () () () () () multMagma
the carrier of D is non empty set
H is non empty strict unital associative () () () () () () multMagma
the carrier of H is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of H is Relation-like Function-like non empty total quasi_total associative having_a_unity 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
N is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like Element of G *
c7 is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like Element of G *
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of H
f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of H
b9 * f is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of H
the multF of H . (b9,f) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of H
[b9,f] is V23() set
{b9,f} is functional non empty set
{b9} is functional non empty set
{{b9,f},{b9}} is non empty set
the multF of H . [b9,f] is set
f9 is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like Element of G *
r is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like Element of G *
(G,f9,r) is Relation-like NAT -defined G -valued Function-like V50() FinSequence-like FinSubsequence-like Element of G *
g is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
f9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
g * f9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
the multF of D . (g,f9) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
[g,f9] is V23() set
{g,f9} is functional non empty set
{g} is functional non empty set
{{g,f9},{g}} is non empty set
the multF of D . [g,f9] is set
H2(D) . (N,c7) is set
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of D . [N,c7] is set
H2(H) . (N,c7) is set
the multF of H . [N,c7] is set
G is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
D is non empty strict unital associative well-unital () () () () () () ((G))
H is non empty strict unital associative well-unital () () () () () () ((G))
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
G * is functional non empty FinSequence-membered M13(G)
[:(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) is non empty strict unital associative () () () () () () multMagma
G * is functional non empty FinSequence-membered M13(G)
(G) is Relation-like Function-like non empty total quasi_total Element of bool [:[:(G *),(G *):],(G *):]
[:(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
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
multMagma(# (G *),(G) #) is non empty strict multMagma
G is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
G * is functional non empty FinSequence-membered M13(G)
<*> G is Relation-like non-empty empty-yielding NAT -defined G -valued Function-like one-to-one constant functional empty proper V38() V39() V40() V42() V43() V44() V50() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V163() V164() V165() FinSequence of G
[:NAT,G:] is Relation-like non empty set
e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
H2((G)) . (e,N) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
e * N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) . (e,N) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
{} ^ N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
H2((G)) . (N,e) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[N,e] is V23() set
{N,e} is functional non empty set
{N} is functional non empty set
{{N,e},{N}} is non empty set
the multF of (G) . [N,e] is set
N * e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) . (N,e) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N ^ {} is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
G is non empty set
(G) is non empty strict unital associative well-unital () () () () () () ((G))
(G) is non empty strict unital associative () () () () () () multMagma
the carrier of (G) is non empty set
G * is functional non empty FinSequence-membered M13(G)
[: the carrier of (G), the carrier of (G):] is Relation-like non empty set
[:(G *),(G *):] is Relation-like non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is Relation-like non empty set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is non empty set
(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
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
1. (G) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the OneF of (G) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
multMagma(# the carrier of (G), the multF of (G) #) is non empty strict associative multMagma
the_unity_wrt H2((G)) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
G is non empty set
(G) is non empty strict unital associative well-unital () () () () () () ((G))
(G) is non empty strict unital associative () () () () () () multMagma
the carrier of (G) is non empty set
D is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
H is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
D * H is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (D,H) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[D,H] is V23() set
{D,H} is functional non empty set
{D} is functional non empty set
{{D,H},{D}} is non empty set
the multF of (G) . [D,H] is set
D ^ H is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
multMagma(# the carrier of (G), the multF of (G) #) is non empty strict associative multMagma
the carrier of (G) is non empty set
e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
e * N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (e,N) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
G is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
D is non empty associative () () () () () ((G))
the carrier of D is non empty set
H is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
H * e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total associative Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
[H,e] is V23() set
{H,e} is functional non empty set
{H} is functional non empty set
{{H,e},{H}} is non empty set
the multF of D . [H,e] is set
H ^ e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
the carrier of (G) is non empty set
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N * N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (N,N) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[N,N] is V23() set
{N,N} is functional non empty set
{N} is functional non empty set
{{N,N},{N}} is non empty set
the multF of (G) . [N,N] is set
G is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
D is non empty unital associative () () () () () ((G))
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt the multF of D is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
the_unity_wrt H2(D) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
e ^ {} is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(the_unity_wrt H2(D)) * (the_unity_wrt H2(D)) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
the multF of D . ((the_unity_wrt H2(D)),(the_unity_wrt H2(D))) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
[(the_unity_wrt H2(D)),(the_unity_wrt H2(D))] is V23() set
{(the_unity_wrt H2(D)),(the_unity_wrt H2(D))} is functional non empty set
{(the_unity_wrt H2(D))} is functional non empty set
{{(the_unity_wrt H2(D)),(the_unity_wrt H2(D))},{(the_unity_wrt H2(D))}} is non empty set
the multF of D . [(the_unity_wrt H2(D)),(the_unity_wrt H2(D))] is set
e ^ e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
G is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
D is non empty associative () () () () () ((G))
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total associative Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt the multF of D is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of D
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 H2((G)) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
G is non empty set
D is non empty set
(G) is non empty strict unital associative () () () () () () multMagma
(D) is non empty strict unital associative () () () () () () multMagma
the carrier of (G) is non empty set
G * is functional non empty FinSequence-membered M13(G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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
proj1 H2((G)) is set
[:(G *),(G *):] is Relation-like non empty set
the carrier of (D) is non empty set
D * is functional non empty FinSequence-membered M13(D)
the multF of (D) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is Relation-like non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is Relation-like non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
proj1 H2((D)) is set
[:(D *),(D *):] is Relation-like non empty set
H is set
H `1 is set
H `2 is set
H2((G)) . H is set
e is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
e * N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
the multF of (G) . (e,N) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
e ^ N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (D)
c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (D)
N * c7 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (D)
the multF of (D) . (N,c7) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of (D)
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of (D) . [N,c7] is set
H2((D)) . H is set
G is non empty set
G * is functional non empty FinSequence-membered M13(G)
(G) is Relation-like Function-like non empty total quasi_total Element of bool [:[:(G *),(G *):],(G *):]
[:(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 strict unital associative () () () () () () multMagma
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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 (G) is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of G *
multMagma(# (G *),(G) #) is non empty strict multMagma
G is set
PFuncs (G,G) is functional non empty set
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
e is Relation-like Function-like Element of PFuncs (G,G)
N is Relation-like Function-like Element of PFuncs (G,G)
N is Relation-like Function-like Element of bool [:G,G:]
c7 is Relation-like Function-like Element of bool [:G,G:]
c7 * N is Relation-like Function-like Element of bool [:G,G:]
b9 is Relation-like Function-like Element of PFuncs (G,G)
N * c7 is Relation-like Function-like set
[:(PFuncs (G,G)),(PFuncs (G,G)):] is Relation-like non empty set
[:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is Relation-like non empty set
bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is non empty set
e is Relation-like Function-like non empty total quasi_total Element of bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):]
multMagma(# (PFuncs (G,G)),e #) is non empty strict multMagma
the carrier of multMagma(# (PFuncs (G,G)),e #) is non empty set
N is Element of the carrier of multMagma(# (PFuncs (G,G)),e #)
N is strict () multMagma
the carrier of N is set
c7 is Relation-like Function-like Element of the carrier of N
b9 is Relation-like Function-like Element of the carrier of N
c7 * b9 is Relation-like Function-like Element of the carrier of N
the multF of N is Relation-like Function-like quasi_total Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is Relation-like set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is Relation-like set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty set
the multF of N . (c7,b9) is Relation-like Function-like Element of the carrier of N
[c7,b9] is V23() set
{c7,b9} is functional non empty set
{c7} is functional non empty set
{{c7,b9},{c7}} is non empty set
the multF of N . [c7,b9] is set
c7 * b9 is Relation-like Function-like set
f is Relation-like Function-like Element of PFuncs (G,G)
g is Relation-like Function-like Element of PFuncs (G,G)
e . (f,g) is Relation-like Function-like Element of PFuncs (G,G)
[f,g] is V23() set
{f,g} is functional non empty set
{f} is functional non empty set
{{f,g},{f}} is non empty set
e . [f,g] is set
f9 is Relation-like Function-like Element of bool [:G,G:]
f9 is Relation-like Function-like Element of bool [:G,G:]
f9 * f9 is Relation-like Function-like set
D is strict () multMagma
the carrier of D is set
H is strict () multMagma
the carrier of H is set
the multF of D is Relation-like Function-like quasi_total Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of H is Relation-like Function-like 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 set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
N is Relation-like Function-like Element of the carrier of D
c7 is Relation-like Function-like Element of the carrier of D
N * c7 is Relation-like Function-like Element of the carrier of D
the multF of D . (N,c7) is Relation-like Function-like Element of the carrier of D
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of D . [N,c7] is set
N * c7 is Relation-like Function-like set
b9 is Relation-like Function-like Element of the carrier of H
f is Relation-like Function-like Element of the carrier of H
b9 * f is Relation-like Function-like Element of the carrier of H
the multF of H . (b9,f) is Relation-like Function-like Element of the carrier of H
[b9,f] is V23() set
{b9,f} is functional non empty set
{b9} is functional non empty set
{{b9,f},{b9}} is non empty set
the multF of H . [b9,f] is set
b9 * f is Relation-like Function-like set
H2(D) . (N,c7) is Relation-like Function-like Element of the carrier of D
H2(H) . (N,c7) is set
the multF of H . [N,c7] is set
G is set
(G) is strict () multMagma
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
PFuncs (G,G) is functional non empty set
the carrier of (G) is set
N is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
N * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like 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 set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is Relation-like set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is non empty set
the multF of (G) . (N,N) is Relation-like Function-like Element of the carrier of (G)
[N,N] is V23() set
{N,N} is functional non empty set
{N} is functional non empty set
{{N,N},{N}} is non empty set
the multF of (G) . [N,N] is set
c7 is Relation-like Function-like Element of the carrier of (G)
N * c7 is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,c7) is Relation-like Function-like Element of the carrier of (G)
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of (G) . [N,c7] is set
(N * N) * c7 is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((N * N),c7) is Relation-like Function-like Element of the carrier of (G)
[(N * N),c7] is V23() set
{(N * N),c7} is functional non empty set
{(N * N)} is functional non empty set
{{(N * N),c7},{(N * N)}} is non empty set
the multF of (G) . [(N * N),c7] is set
b9 is Relation-like Function-like Element of the carrier of (G)
b9 * c7 is Relation-like Function-like set
N * N is Relation-like Function-like set
(N * N) * c7 is Relation-like Function-like set
N * c7 is Relation-like Function-like set
N * (N * c7) is Relation-like Function-like set
f is Relation-like Function-like Element of the carrier of (G)
N * f is Relation-like Function-like set
N * (N * c7) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,(N * c7)) is Relation-like Function-like Element of the carrier of (G)
[N,(N * c7)] is V23() set
{N,(N * c7)} is functional non empty set
{{N,(N * c7)},{N}} is non empty set
the multF of (G) . [N,(N * c7)] is set
H is Relation-like Function-like Element of bool [:G,G:]
N is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
N * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,N) is Relation-like Function-like Element of the carrier of (G)
[N,N] is V23() set
{N,N} is functional non empty set
{N} is functional non empty set
{{N,N},{N}} is non empty set
the multF of (G) . [N,N] is set
c7 is Relation-like Function-like Element of bool [:G,G:]
H * c7 is Relation-like Function-like set
N * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,N) is Relation-like Function-like Element of the carrier of (G)
[N,N] is V23() set
{N,N} is functional non empty set
{N} is functional non empty set
{{N,N},{N}} is non empty set
the multF of (G) . [N,N] is set
c7 * H is Relation-like Function-like set
G is set
(G) is non empty strict unital associative () multMagma
D is non empty strict unital associative well-unital () ((G))
H is non empty strict unital associative well-unital () ((G))
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
PFuncs (G,G) is functional non empty set
[:(PFuncs (G,G)),(PFuncs (G,G)):] is Relation-like non empty set
[:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is Relation-like non empty set
bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is non empty set
G is set
D is set
(D) is non empty strict unital associative () multMagma
the carrier of (D) is non empty set
[:D,D:] is Relation-like set
bool [:D,D:] is non empty set
PFuncs (D,D) is functional non empty set
G is set
(G) is non empty strict unital associative () multMagma
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 Relation-like Function-like Element of the carrier of (G)
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
PFuncs (G,G) is functional non empty set
D is Relation-like Function-like Element of bool [:G,G:]
N is Relation-like Function-like Element of the carrier of (G)
e is Relation-like Function-like Element of the carrier of (G)
H2((G)) . (e,N) is Relation-like Function-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
e * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (e,N) is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of bool [:G,G:]
D * N is Relation-like Function-like set
H2((G)) . (N,e) is Relation-like Function-like Element of the carrier of (G)
[N,e] is V23() set
{N,e} is functional non empty set
{N} is functional non empty set
{{N,e},{N}} is non empty set
the multF of (G) . [N,e] is set
N * e is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,e) is Relation-like Function-like Element of the carrier of (G)
N * D is Relation-like Function-like set
G is set
(G) is non empty strict unital associative () multMagma
D is non empty associative () ((G))
the carrier of D is non empty set
H is Relation-like Function-like Element of the carrier of D
e is Relation-like Function-like Element of the carrier of D
H * e is Relation-like Function-like Element of the carrier of D
the multF of D is Relation-like Function-like non empty total quasi_total associative Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the multF of D . (H,e) is Relation-like Function-like Element of the carrier of D
[H,e] is V23() set
{H,e} is functional non empty set
{H} is functional non empty set
{{H,e},{H}} is non empty set
the multF of D . [H,e] is set
H * e is Relation-like Function-like set
the carrier of (G) is non empty set
N is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
N * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (N,N) is Relation-like Function-like Element of the carrier of (G)
[N,N] is V23() set
{N,N} is functional non empty set
{N} is functional non empty set
{{N,N},{N}} is non empty set
the multF of (G) . [N,N] is set
G is set
(G) is non empty strict unital associative () multMagma
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
D is non empty associative () ((G))
the carrier of D is non empty set
the multF of D is Relation-like Function-like non empty total quasi_total associative Element of bool [:[: the carrier of D, the carrier of D:], the carrier of D:]
[: the carrier of D, the carrier of D:] is Relation-like non empty set
[:[: the carrier of D, the carrier of D:], the carrier of D:] is Relation-like non empty set
bool [:[: the carrier of D, the carrier of D:], the carrier of D:] is non empty set
the_unity_wrt the multF of D is Relation-like Function-like Element of the carrier of D
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 H2((G)) is Relation-like Function-like Element of the carrier of (G)
G is set
(G) is non empty strict unital associative () multMagma
D is set
(D) is non empty strict unital associative () multMagma
the carrier of (G) is non empty set
PFuncs (G,G) is functional non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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
proj1 H2((G)) is set
[:(PFuncs (G,G)),(PFuncs (G,G)):] is Relation-like non empty set
the carrier of (D) is non empty set
PFuncs (D,D) is functional non empty set
the multF of (D) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):]
[: the carrier of (D), the carrier of (D):] is Relation-like non empty set
[:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is Relation-like non empty set
bool [:[: the carrier of (D), the carrier of (D):], the carrier of (D):] is non empty set
proj1 H2((D)) is set
[:(PFuncs (D,D)),(PFuncs (D,D)):] is Relation-like non empty set
H is set
H `1 is set
H `2 is set
H2((G)) . H is set
e is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
e * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (e,N) is Relation-like Function-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
e * N is Relation-like Function-like set
N is Relation-like Function-like Element of the carrier of (D)
c7 is Relation-like Function-like Element of the carrier of (D)
N * c7 is Relation-like Function-like Element of the carrier of (D)
the multF of (D) . (N,c7) is Relation-like Function-like Element of the carrier of (D)
[N,c7] is V23() set
{N,c7} is functional non empty set
{N} is functional non empty set
{{N,c7},{N}} is non empty set
the multF of (D) . [N,c7] is set
H2((D)) . H is set
G is set
(G) is non empty strict unital associative () multMagma
Funcs (G,G) is functional non empty set
PFuncs (G,G) is functional non empty set
the carrier of (G) is non empty set
bool the carrier of (G) is non empty set
D is non empty Element of bool the carrier of (G)
H is Element of D
e is Element of D
H * e is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (H,e) is Relation-like Function-like 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
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
N is Relation-like Function-like total quasi_total Element of bool [:G,G:]
N is Relation-like Function-like total quasi_total Element of bool [:G,G:]
N * N is Relation-like Function-like total quasi_total Element of bool [:G,G:]
H is non empty strict associative () ((G))
the carrier of H is non empty set
D is strict ((G))
the carrier of D is set
H is strict ((G))
the carrier of H is set
G is set
(G) is strict ((G))
(G) is non empty strict unital associative () multMagma
the carrier of (G) is set
Funcs (G,G) is functional non empty set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
G is set
(G) is non empty strict unital associative () ((G))
(G) is non empty strict unital associative () multMagma
D is non empty strict unital associative well-unital () ((G))
H is non empty strict unital associative well-unital () ((G))
G is set
D is set
(D) is non empty strict unital associative () ((D))
(D) is non empty strict unital associative () multMagma
the carrier of (D) is non empty set
[:D,D:] is Relation-like set
bool [:D,D:] is non empty set
Funcs (D,D) is functional non empty set
G is set
(G) is non empty strict unital associative () ((G))
(G) is non empty strict unital associative () multMagma
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
(G) is Relation-like Function-like non empty total quasi_total Element of bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):]
PFuncs (G,G) is functional non empty set
[:(PFuncs (G,G)),(PFuncs (G,G)):] is Relation-like non empty set
[:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is Relation-like non empty set
bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
Funcs (G,G) is functional non empty set
(G) || (Funcs (G,G)) is Relation-like Function-like set
[:(Funcs (G,G)),(Funcs (G,G)):] is Relation-like non empty set
(G) | [:(Funcs (G,G)),(Funcs (G,G)):] is Relation-like Function-like set
proj1 H2((G)) is set
[:H1((G)),H1((G)):] is Relation-like set
G is set
(G) is non empty strict unital associative () ((G))
(G) is non empty strict unital associative () multMagma
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 Relation-like Function-like Element of the carrier of (G)
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
Funcs (G,G) is functional non empty set
G is set
(G) is non empty strict unital associative well-unital () ((G))
(G) is non empty strict unital associative () ((G))
(G) is non empty strict unital associative () multMagma
the carrier of (G) is non empty set
Funcs (G,G) is functional non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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
(G) is Relation-like Function-like non empty total quasi_total Element of bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):]
PFuncs (G,G) is functional non empty set
[:(PFuncs (G,G)),(PFuncs (G,G)):] is Relation-like non empty set
[:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is Relation-like non empty set
bool [:[:(PFuncs (G,G)),(PFuncs (G,G)):],(PFuncs (G,G)):] is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
the carrier of (G) is non empty set
[: 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
(G) || (Funcs (G,G)) is Relation-like Function-like set
[:(Funcs (G,G)),(Funcs (G,G)):] is Relation-like non empty set
(G) | [:(Funcs (G,G)),(Funcs (G,G)):] is Relation-like Function-like set
1. (G) is Relation-like Function-like Element of the carrier of (G)
the OneF of (G) is Relation-like Function-like Element of the carrier of (G)
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 H2((G)) is Relation-like Function-like Element of the carrier of (G)
multMagma(# the carrier of (G), the multF of (G) #) is non empty strict associative multMagma
G is set
(G) is non empty strict unital associative () multMagma
(G) is non empty strict unital associative () ((G))
the carrier of (G) is non empty set
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
the Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:] is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
Funcs (G,G) is functional non empty set
H is Relation-like Function-like Element of the carrier of (G)
Funcs (G,G) is functional non empty set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
H is Relation-like Function-like Element of the carrier of (G)
e is Relation-like Function-like Element of the carrier of (G)
H * e is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (H,e) is Relation-like Function-like Element of the carrier of (G)
[H,e] is V23() set
{H,e} is functional non empty set
{H} is functional non empty set
{{H,e},{H}} is non empty set
the multF of (G) . [H,e] is set
N is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
N is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
N * N is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
H is non empty strict associative () ((G),(G))
the carrier of H is non empty set
e is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
D is non empty strict associative () ((G),(G))
the carrier of D is non empty set
H is non empty strict associative () ((G),(G))
the carrier of H is non empty set
e is set
N is Relation-like Function-like Element of the carrier of (G)
e is set
N is Relation-like Function-like Element of the carrier of (G)
G is set
(G) is non empty strict associative () ((G),(G))
(G) is non empty strict unital associative () multMagma
(G) is non empty strict unital associative () ((G))
the carrier of (G) is non empty set
Funcs (G,G) is functional non empty set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
H is Relation-like Function-like Element of the carrier of (G)
the carrier of (G) is non empty set
N is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
c7 is Relation-like Function-like Element of the carrier of (G)
b9 is Relation-like Function-like Element of the carrier of (G)
e is Relation-like Function-like Element of the carrier of (G)
f is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
f " is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
(f ") * f is Relation-like Function-like one-to-one set
f * (f ") is Relation-like Function-like one-to-one set
g is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
e * g is Relation-like Function-like set
g * e is Relation-like Function-like set
f9 is Relation-like Function-like Element of the carrier of (G)
f9 is Relation-like Function-like Element of the carrier of (G)
f9 * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative 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 multF of (G) . (f9,N) is Relation-like Function-like Element of the carrier of (G)
[f9,N] is V23() set
{f9,N} is functional non empty set
{f9} is functional non empty set
{{f9,N},{f9}} is non empty set
the multF of (G) . [f9,N] is set
N * f9 is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,f9) is Relation-like Function-like Element of the carrier of (G)
[N,f9] is V23() set
{N,f9} is functional non empty set
{N} is functional non empty set
{{N,f9},{N}} is non empty set
the multF of (G) . [N,f9] is set
r is Relation-like Function-like Element of the carrier of (G)
l is Relation-like Function-like Element of the carrier of (G)
e * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (e,N) is Relation-like Function-like Element of the carrier of (G)
[e,N] is V23() set
{e,N} is functional non empty set
{e} is functional non empty set
{{e,N},{e}} is non empty set
the multF of (G) . [e,N] is set
(id G) * g is Relation-like G -defined Function-like one-to-one set
N * e is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,e) is Relation-like Function-like Element of the carrier of (G)
[N,e] is V23() set
{N,e} is functional non empty set
{{N,e},{N}} is non empty set
the multF of (G) . [N,e] is set
g * (id G) is Relation-like G -valued Function-like one-to-one set
N * f9 is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,f9) is Relation-like Function-like Element of the carrier of (G)
[N,f9] is V23() set
{N,f9} is functional non empty set
{N} is functional non empty set
{{N,f9},{N}} is non empty set
the multF of (G) . [N,f9] is set
f9 * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (f9,N) is Relation-like Function-like Element of the carrier of (G)
[f9,N] is V23() set
{f9,N} is functional non empty set
{{f9,N},{f9}} is non empty set
the multF of (G) . [f9,N] is set
r is Relation-like Function-like Element of the carrier of (G)
N * r is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (N,r) is Relation-like Function-like Element of the carrier of (G)
[N,r] is V23() set
{N,r} is functional non empty set
{{N,r},{N}} is non empty set
the multF of (G) . [N,r] is set
l is Relation-like Function-like Element of the carrier of (G)
l * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (l,N) is Relation-like Function-like Element of the carrier of (G)
[l,N] is V23() set
{l,N} is functional non empty set
{l} is functional non empty set
{{l,N},{l}} is non empty set
the multF of (G) . [l,N] is set
G is set
D is set
(D) is non empty strict unital Group-like associative () () () () () () () ((D),(D))
(D) is non empty strict unital associative () multMagma
(D) is non empty strict unital associative () ((D))
the carrier of (D) is non empty set
[:D,D:] is Relation-like set
bool [:D,D:] is non empty set
Funcs (D,D) is functional non empty set
the carrier of (D) is non empty set
G is set
(G) is non empty strict unital Group-like associative () () () () () () () ((G),(G))
(G) is non empty strict unital associative () multMagma
(G) is non empty strict unital associative () ((G))
the carrier of (G) is non empty set
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 Relation-like Function-like Element of the carrier of (G)
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
1_ (G) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G)
H is Relation-like Function-like Element of the carrier of (G)
D is Relation-like Function-like Element of the carrier of (G)
H * D is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (H,D) is Relation-like Function-like Element of the carrier of (G)
[H,D] is V23() set
{H,D} is functional non empty set
{H} is functional non empty set
{{H,D},{H}} is non empty set
the multF of (G) . [H,D] is set
H * D is Relation-like Function-like set
H2((G)) . (H,D) is Relation-like Function-like Element of the carrier of (G)
e is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
e * D is Relation-like Function-like set
D * H is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (D,H) is Relation-like Function-like Element of the carrier of (G)
[D,H] is V23() set
{D,H} is functional non empty set
{D} is functional non empty set
{{D,H},{D}} is non empty set
the multF of (G) . [D,H] is set
D * H is Relation-like Function-like set
H2((G)) . (D,H) is Relation-like Function-like Element of the carrier of (G)
the_unity_wrt H2((G)) is Relation-like Function-like Element of the carrier of (G)
G is set
(G) is non empty strict unital Group-like associative () () () () () () () ((G),(G))
(G) is non empty strict unital associative () multMagma
(G) is non empty strict unital associative () ((G))
the carrier of (G) is non empty set
D is Relation-like Function-like Element of the carrier of (G)
D " is Relation-like Function-like Element of the carrier of (G)
D " is Relation-like Function-like set
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
H is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
H " is Relation-like Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
(H ") * H is Relation-like Function-like one-to-one set
id G is Relation-like G -defined G -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:G,G:]
H * (H ") is Relation-like Function-like one-to-one set
e is Relation-like Function-like Element of the carrier of (G)
N is Relation-like Function-like Element of the carrier of (G)
N * D is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like Function-like non empty total quasi_total associative having_a_unity having_an_inverseOp Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is 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 multF of (G) . (N,D) is Relation-like Function-like Element of the carrier of (G)
[N,D] is V23() set
{N,D} is functional non empty set
{N} is functional non empty set
{{N,D},{N}} is non empty set
the multF of (G) . [N,D] is set
1_ (G) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G)
D * N is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (D,N) is Relation-like Function-like Element of the carrier of (G)
[D,N] is V23() set
{D,N} is functional non empty set
{D} is functional non empty set
{{D,N},{D}} is non empty set
the multF of (G) . [D,N] is set
G is 1-sorted
the carrier of G is set
D is Element of the carrier of G
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
D is non empty Element of bool the carrier of G
G is non empty multLoopStr
the carrier of G is non empty set
bool the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
D is non empty Element of bool the carrier of G
H is non empty strict (G)
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
multLoopStr(# the carrier of H, the multF of H,e #) is non empty strict multLoopStr
the multF of multLoopStr(# the carrier of H, the multF of H,e #) is Relation-like Function-like non empty total quasi_total Element of bool [:[: the carrier of multLoopStr(# the carrier of H, the multF of H,e #), the carrier of multLoopStr(# the carrier of H, the multF of H,e #):], the carrier of multLoopStr(# the carrier of H, the multF of H,e #):]
the carrier of multLoopStr(# the carrier of H, the multF of H,e #) is non empty set
[: the carrier of multLoopStr(# the carrier of H, the multF of H,e #), the carrier of multLoopStr(# the carrier of H, the multF of H,e #):] is Relation-like non empty set
[:[: the carrier of multLoopStr(# the carrier of H, the multF of H,e #), the carrier of multLoopStr(# the carrier of H, the multF of H,e #):], the carrier of multLoopStr(# the carrier of H, the multF of H,e #):] is Relation-like non empty set
bool [:[: the carrier of multLoopStr(# the carrier of H, the multF of H,e #), the carrier of multLoopStr(# the carrier of H, the multF of H,e #):], the carrier of multLoopStr(# the carrier of H, the multF of H,e #):] 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
1. multLoopStr(# the carrier of H, the multF of H,e #) is Element of the carrier of multLoopStr(# the carrier of H, the multF of H,e #)
the OneF of multLoopStr(# the carrier of H, the multF of H,e #) is Element of the carrier of multLoopStr(# the carrier of H, the multF of H,e #)
N is multLoopStr
1. N is Element of the carrier of N
the carrier of N is set
the OneF of N is Element of the carrier of N
N is non empty strict (G)
the carrier of N is non empty set