:: MONOID_1 semantic presentation

REAL is set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set
1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{{},1} is non empty finite V46() set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
[:1,1:] is Relation-like non empty finite set
bool [:1,1:] is non empty finite V46() set
[:[:1,1:],1:] is Relation-like non empty finite set
bool [:[:1,1:],1:] is non empty finite V46() set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K452() is non empty strict multMagma
the carrier of K452() is non empty set
<REAL,+> is non empty strict unital V127() associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable cancelable multMagma
K215() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total Element of bool [:[:REAL,REAL:],REAL:]
multMagma(# REAL,K215() #) is strict multMagma
K458() is non empty strict associative commutative left-cancelable right-cancelable cancelable SubStr of <REAL,+>
<NAT,+> is non empty strict unital associative commutative left-cancelable right-cancelable cancelable uniquely-decomposable SubStr of K458()
<REAL,*> is non empty strict unital associative commutative multMagma
K217() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total Element of bool [:[:REAL,REAL:],REAL:]
multMagma(# REAL,K217() #) is strict multMagma
<NAT,*> is non empty strict unital associative commutative uniquely-decomposable SubStr of <REAL,*>
2 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
3 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() Element of NAT
<NAT,+,0> is non empty strict unital associative commutative well-unital left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalExtension of <NAT,+>
the carrier of <NAT,+,0> is non empty set
addnat is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]
the multF of <NAT,+> is Relation-like [: the carrier of <NAT,+>, the carrier of <NAT,+>:] -defined the carrier of <NAT,+> -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:]
the carrier of <NAT,+> is non empty set
[: the carrier of <NAT,+>, the carrier of <NAT,+>:] is Relation-like non empty set
[:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:] is Relation-like non empty set
bool [:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:] is non empty set
multLoopStr(# NAT,addnat,0 #) is strict multLoopStr
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set
rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set
G is Relation-like Function-like set
M is set
A is set
[M,A] is set
{M,A} is non empty finite set
{M} is non empty trivial finite 1 -element set
{{M,A},{M}} is non empty finite V46() set
B is set
G .. ([M,A],B) is set
K232(G) is Relation-like Function-like set
K232(G) . ([M,A],B) is set
[[M,A],B] is set
{[M,A],B} is non empty finite set
{[M,A]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{{[M,A],B},{[M,A]}} is non empty finite V46() set
K232(G) . [[M,A],B] is set
M is non empty set
A is non empty set
[:M,A:] is Relation-like non empty set
G is non empty set
B is non empty set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B
[:[:M,A:],(Funcs (G,B)):] is Relation-like non empty set
bool [:[:M,A:],(Funcs (G,B)):] is non empty set
a is Relation-like [:M,A:] -defined Funcs (G,B) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:M,A:],(Funcs (G,B)):]
a1 is Element of M
a2 is Element of A
a1 is Element of G
(a,a1,a2,a1) is set
[a1,a2] is set
{a1,a2} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
a .. ([a1,a2],a1) is set
K232(a) is Relation-like Function-like set
K232(a) . ([a1,a2],a1) is set
[[a1,a2],a1] is set
{[a1,a2],a1} is non empty finite set
{[a1,a2]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{{[a1,a2],a1},{[a1,a2]}} is non empty finite V46() set
K232(a) . [[a1,a2],a1] is set
a . (a1,a2) is Relation-like Function-like Element of Funcs (G,B)
a . [a1,a2] is Relation-like Function-like set
[a1,a2] is Element of [:M,A:]
dom a is Relation-like M -defined A -valued non empty Element of bool [:M,A:]
bool [:M,A:] is non empty set
a2 is Relation-like G -defined B -valued Function-like total quasi_total Element of Funcs (G,B)
dom a2 is Element of bool G
bool G is non empty set
a2 . a1 is Element of B
M is non empty set
A is non empty set
[:M,A:] is Relation-like non empty set
B is non empty set
[:[:M,A:],B:] is Relation-like non empty set
bool [:[:M,A:],B:] is non empty set
G is set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
[:G,A:] is Relation-like set
bool [:G,A:] is non empty set
a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
a2 is Relation-like G -defined A -valued Function-like total quasi_total Element of bool [:G,A:]
a .: (a1,a2) is Relation-like Function-like set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B
<:a1,a2:> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]
[:G,[:M,A:]:] is Relation-like set
bool [:G,[:M,A:]:] is non empty set
a * <:a1,a2:> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]
[:G,B:] is Relation-like set
bool [:G,B:] is non empty set
dom (a .: (a1,a2)) is set
rng (a .: (a1,a2)) is set
G is non empty set
G is non empty set
M is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
A is Element of G
M |-> A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is non empty set
M is set
A is Element of G
M --> A is Relation-like M -defined G -valued Function-like constant total set
Funcs (M,G) is functional non empty FUNCTION_DOMAIN of M,G
M --> A is Relation-like M -defined G -valued Function-like constant total quasi_total Element of bool [:M,G:]
[:M,G:] is Relation-like set
bool [:M,G:] is non empty set
dom (M --> A) is Element of bool M
bool M is non empty set
rng (M --> A) is trivial finite Element of bool G
bool G is non empty set
{A} is non empty trivial finite 1 -element Element of bool G
M is non empty set
A is non empty set
[:M,A:] is Relation-like non empty set
B is non empty set
[:[:M,A:],B:] is Relation-like non empty set
bool [:[:M,A:],B:] is non empty set
G is set
[:G,A:] is Relation-like set
bool [:G,A:] is non empty set
a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]
a1 is Element of M
a2 is Relation-like G -defined A -valued Function-like total quasi_total Element of bool [:G,A:]
a [;] (a1,a2) is Relation-like Function-like set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B
dom a2 is Element of bool G
bool G is non empty set
(M,G,a1) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
<:(M,G,a1),a2:> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]
[:G,[:M,A:]:] is Relation-like set
bool [:G,[:M,A:]:] is non empty set
a * <:(M,G,a1),a2:> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]
[:G,B:] is Relation-like set
bool [:G,B:] is non empty set
dom (a [;] (a1,a2)) is set
rng (a [;] (a1,a2)) is set
M is non empty set
A is non empty set
[:M,A:] is Relation-like non empty set
B is non empty set
[:[:M,A:],B:] is Relation-like non empty set
bool [:[:M,A:],B:] is non empty set
G is set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
a2 is Element of A
a [:] (a1,a2) is Relation-like Function-like set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B
dom a1 is Element of bool G
bool G is non empty set
(A,G,a2) is Relation-like G -defined A -valued Function-like constant total quasi_total Element of Funcs (G,A)
Funcs (G,A) is functional non empty FUNCTION_DOMAIN of G,A
<:a1,(A,G,a2):> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]
[:G,[:M,A:]:] is Relation-like set
bool [:G,[:M,A:]:] is non empty set
a * <:a1,(A,G,a2):> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]
[:G,B:] is Relation-like set
bool [:G,B:] is non empty set
dom (a [:] (a1,a2)) is set
rng (a [:] (a1,a2)) is set
M is Relation-like Function-like set
G is Relation-like Function-like set
A is set
G | A is Relation-like Function-like set
M * (G | A) is Relation-like Function-like set
A |` M is Relation-like Function-like set
(A |` M) * G is Relation-like Function-like set
dom (G | A) is set
dom G is set
(dom G) /\ A is set
dom (M * (G | A)) is set
dom ((A |` M) * G) is set
B is set
dom M is set
M . B is set
dom (A |` M) is set
(A |` M) . B is set
B is set
dom (A |` M) is set
dom M is set
(A |` M) . B is set
M . B is set
B is set
(M * (G | A)) . B is set
M . B is set
(G | A) . (M . B) is set
G . (M . B) is set
((A |` M) * G) . B is set
(A |` M) . B is set
G . ((A |` M) . B) is set
dom (A |` M) is set
F<sub>1</sub>() is set
F<sub>2</sub>() is non empty set
[:F<sub>1</sub>(),F<sub>2</sub>():] is Relation-like set
bool [:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
G is set
M is Element of F<sub>2</sub>()
G is Relation-like Function-like set
dom G is set
rng G is set
M is Relation-like F<sub>1</sub>() -defined F<sub>2</sub>() -valued Function-like total quasi_total Element of bool [:F<sub>1</sub>(),F<sub>2</sub>():]
A is set
M . A is set
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
a is set
Funcs (a,G) is functional non empty FUNCTION_DOMAIN of a,G
Funcs (a,M) is functional non empty FUNCTION_DOMAIN of a,M
[:(Funcs (a,G)),(Funcs (a,M)):] is Relation-like non empty set
Funcs (a,A) is functional non empty FUNCTION_DOMAIN of a,A
[:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):] is Relation-like non empty set
bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):] is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
a1 is Relation-like [:(Funcs (a,G)),(Funcs (a,M)):] -defined Funcs (a,A) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):]
a2 is Relation-like a -defined G -valued Function-like total quasi_total Element of Funcs (a,G)
a1 is Relation-like a -defined M -valued Function-like total quasi_total Element of Funcs (a,M)
a1 . (a2,a1) is Relation-like Function-like Element of Funcs (a,A)
[a2,a1] is set
{a2,a1} is functional non empty finite set
{a2} is functional non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
a1 . [a2,a1] is Relation-like Function-like set
(a,G,M,A,B,a2,a1) is Relation-like a -defined A -valued Function-like total quasi_total Element of Funcs (a,A)
a1 is Relation-like [:(Funcs (a,G)),(Funcs (a,M)):] -defined Funcs (a,A) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):]
a2 is Relation-like [:(Funcs (a,G)),(Funcs (a,M)):] -defined Funcs (a,A) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):]
a1 is Relation-like a -defined G -valued Function-like total quasi_total Element of Funcs (a,G)
a2 is Relation-like a -defined M -valued Function-like total quasi_total Element of Funcs (a,M)
a1 . (a1,a2) is Relation-like Function-like Element of Funcs (a,A)
[a1,a2] is set
{a1,a2} is functional non empty finite set
{a1} is functional non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
a1 . [a1,a2] is Relation-like Function-like set
(a,G,M,A,B,a1,a2) is Relation-like a -defined A -valued Function-like total quasi_total Element of Funcs (a,A)
a2 . (a1,a2) is Relation-like Function-like Element of Funcs (a,A)
a2 . [a1,a2] is Relation-like Function-like set
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
a is set
[:a,G:] is Relation-like set
bool [:a,G:] is non empty set
[:a,M:] is Relation-like set
bool [:a,M:] is non empty set
(G,M,A,B,a) is Relation-like [:(Funcs (a,G)),(Funcs (a,M)):] -defined Funcs (a,A) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):]
Funcs (a,G) is functional non empty FUNCTION_DOMAIN of a,G
Funcs (a,M) is functional non empty FUNCTION_DOMAIN of a,M
[:(Funcs (a,G)),(Funcs (a,M)):] is Relation-like non empty set
Funcs (a,A) is functional non empty FUNCTION_DOMAIN of a,A
[:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):] is Relation-like non empty set
bool [:[:(Funcs (a,G)),(Funcs (a,M)):],(Funcs (a,A)):] is non empty set
a1 is Relation-like a -defined G -valued Function-like total quasi_total Element of bool [:a,G:]
a2 is Relation-like a -defined M -valued Function-like total quasi_total Element of bool [:a,M:]
dom a2 is Element of bool a
bool a is non empty set
rng a2 is Element of bool M
bool M is non empty set
dom a1 is Element of bool a
rng a1 is Element of bool G
bool G is non empty set
a2 is Relation-like a -defined G -valued Function-like total quasi_total Element of Funcs (a,G)
a1 is Relation-like a -defined M -valued Function-like total quasi_total Element of Funcs (a,M)
(a,G,M,A,B,a2,a1) is Relation-like a -defined A -valued Function-like total quasi_total Element of Funcs (a,A)
dom (a,G,M,A,B,a2,a1) is Element of bool a
(G,M,A,B,a) . (a2,a1) is Relation-like Function-like Element of Funcs (a,A)
[a2,a1] is set
{a2,a1} is functional non empty finite set
{a2} is functional non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
(G,M,A,B,a) . [a2,a1] is Relation-like Function-like set
[a2,a1] is Element of [:(Funcs (a,G)),(Funcs (a,M)):]
x is set
((G,M,A,B,a),a1,a2,x) is set
[a1,a2] is set
{a1,a2} is functional non empty finite set
{a1} is functional non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
(G,M,A,B,a) .. ([a1,a2],x) is set
K232((G,M,A,B,a)) is Relation-like Function-like set
K232((G,M,A,B,a)) . ([a1,a2],x) is set
[[a1,a2],x] is set
{[a1,a2],x} is non empty finite set
{[a1,a2]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{{[a1,a2],x},{[a1,a2]}} is non empty finite V46() set
K232((G,M,A,B,a)) . [[a1,a2],x] is set
a1 . x is set
a2 . x is set
B . ((a1 . x),(a2 . x)) is set
[(a1 . x),(a2 . x)] is set
{(a1 . x),(a2 . x)} is non empty finite set
{(a1 . x)} is non empty trivial finite 1 -element set
{{(a1 . x),(a2 . x)},{(a1 . x)}} is non empty finite V46() set
B . [(a1 . x),(a2 . x)] is set
dom (G,M,A,B,a) is Relation-like Funcs (a,G) -defined Funcs (a,M) -valued non empty Element of bool [:(Funcs (a,G)),(Funcs (a,M)):]
bool [:(Funcs (a,G)),(Funcs (a,M)):] is non empty set
(a,G,M,A,B,a2,a1) . x is set
a2 . x is set
a1 . x is set
B . ((a2 . x),(a1 . x)) is set
[(a2 . x),(a1 . x)] is set
{(a2 . x),(a1 . x)} is non empty finite set
{(a2 . x)} is non empty trivial finite 1 -element set
{{(a2 . x),(a1 . x)},{(a2 . x)}} is non empty finite V46() set
B . [(a2 . x),(a1 . x)] is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
B is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
a is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
(G,M,M,M,A,B,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
(G,M,M,M,A,a,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,B,a) is Element of bool G
bool G is non empty set
dom B is Element of bool G
dom a is Element of bool G
dom (G,M,M,M,A,a,B) is Element of bool G
a1 is set
B . a1 is set
rng B is Element of bool M
bool M is non empty set
a . a1 is set
rng a is Element of bool M
(G,M,M,M,A,B,a) . a1 is set
a2 is Element of M
a1 is Element of M
A . (a2,a1) is Element of M
[a2,a1] is set
{a2,a1} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
A . [a2,a1] is set
A . (a1,a2) is Element of M
[a1,a2] is set
{a1,a2} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
A . [a1,a2] is set
(G,M,M,M,A,a,B) . a1 is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
B is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
a is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
(G,M,M,M,A,B,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
(G,M,M,M,A,(G,M,M,M,A,B,a),a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,a,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,B,(G,M,M,M,A,a,a1)) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,B,a) is Element of bool G
bool G is non empty set
dom (G,M,M,M,A,a,a1) is Element of bool G
dom B is Element of bool G
dom a is Element of bool G
dom (G,M,M,M,A,(G,M,M,M,A,B,a),a1) is Element of bool G
dom a1 is Element of bool G
dom (G,M,M,M,A,B,(G,M,M,M,A,a,a1)) is Element of bool G
a2 is set
a1 . a2 is set
rng a1 is Element of bool M
bool M is non empty set
B . a2 is set
rng B is Element of bool M
a . a2 is set
rng a is Element of bool M
(G,M,M,M,A,(G,M,M,M,A,B,a),a1) . a2 is set
(G,M,M,M,A,B,a) . a2 is set
x is Element of M
A . (((G,M,M,M,A,B,a) . a2),x) is set
[((G,M,M,M,A,B,a) . a2),x] is set
{((G,M,M,M,A,B,a) . a2),x} is non empty finite set
{((G,M,M,M,A,B,a) . a2)} is non empty trivial finite 1 -element set
{{((G,M,M,M,A,B,a) . a2),x},{((G,M,M,M,A,B,a) . a2)}} is non empty finite V46() set
A . [((G,M,M,M,A,B,a) . a2),x] is set
a1 is Element of M
a2 is Element of M
A . (a1,a2) is Element of M
[a1,a2] is set
{a1,a2} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
A . [a1,a2] is set
A . ((A . (a1,a2)),x) is Element of M
[(A . (a1,a2)),x] is set
{(A . (a1,a2)),x} is non empty finite set
{(A . (a1,a2))} is non empty trivial finite 1 -element set
{{(A . (a1,a2)),x},{(A . (a1,a2))}} is non empty finite V46() set
A . [(A . (a1,a2)),x] is set
A . (a2,x) is Element of M
[a2,x] is set
{a2,x} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,x},{a2}} is non empty finite V46() set
A . [a2,x] is set
A . (a1,(A . (a2,x))) is Element of M
[a1,(A . (a2,x))] is set
{a1,(A . (a2,x))} is non empty finite set
{{a1,(A . (a2,x))},{a1}} is non empty finite V46() set
A . [a1,(A . (a2,x))] is set
(G,M,M,M,A,a,a1) . a2 is set
A . (a1,((G,M,M,M,A,a,a1) . a2)) is set
[a1,((G,M,M,M,A,a,a1) . a2)] is set
{a1,((G,M,M,M,A,a,a1) . a2)} is non empty finite set
{{a1,((G,M,M,M,A,a,a1) . a2)},{a1}} is non empty finite V46() set
A . [a1,((G,M,M,M,A,a,a1) . a2)] is set
(G,M,M,M,A,B,(G,M,M,M,A,a,a1)) . a2 is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
A is Element of M
B is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
a is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
(G,M,M,M,B,A,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
(G,M,M,M,B,a,A) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom a is Element of bool G
bool G is non empty set
dom (G,M,M,M,B,A,a) is Element of bool G
a1 is set
a . a1 is set
rng a is Element of bool M
bool M is non empty set
(G,M,M,M,B,A,a) . a1 is set
a2 is Element of M
B . (A,a2) is Element of M
[A,a2] is set
{A,a2} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,a2},{A}} is non empty finite V46() set
B . [A,a2] is set
dom (G,M,M,M,B,a,A) is Element of bool G
a1 is set
a . a1 is set
(G,M,M,M,B,a,A) . a1 is set
a2 is Element of M
B . (a2,A) is Element of M
[a2,A] is set
{a2,A} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,A},{a2}} is non empty finite V46() set
B . [a2,A] is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
B is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
(G,M,M,M,A,B,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
dom (G,M,M,M,A,B,B) is Element of bool G
bool G is non empty set
a is set
B . a is set
(G,M,M,M,A,B,B) . a is set
a1 is Element of M
A . (a1,a1) is Element of M
[a1,a1] is set
{a1,a1} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a1},{a1}} is non empty finite V46() set
A . [a1,a1] is set
dom B is Element of bool G
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (a,a1) is Relation-like Function-like Element of Funcs (G,M)
[a,a1] is set
{a,a1} is functional non empty finite set
{a} is functional non empty trivial finite 1 -element set
{{a,a1},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,a1] is Relation-like Function-like set
(M,M,M,A,G) . (a1,a) is Relation-like Function-like Element of Funcs (G,M)
[a1,a] is set
{a1,a} is functional non empty finite set
{a1} is functional non empty trivial finite 1 -element set
{{a1,a},{a1}} is non empty finite V46() set
(M,M,M,A,G) . [a1,a] is Relation-like Function-like set
(M,M,M,A,G) . (a,a1) is Relation-like Function-like Element of Funcs (G,M)
(G,M,M,M,A,a,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,a1,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (a1,a) is Relation-like Function-like Element of Funcs (G,M)
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a2 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (a1,a2) is Relation-like Function-like Element of Funcs (G,M)
[a1,a2] is set
{a1,a2} is functional non empty finite set
{a1} is functional non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
(M,M,M,A,G) . [a1,a2] is Relation-like Function-like set
(M,M,M,A,G) . (a,((M,M,M,A,G) . (a1,a2))) is Relation-like Function-like Element of Funcs (G,M)
[a,((M,M,M,A,G) . (a1,a2))] is set
{a,((M,M,M,A,G) . (a1,a2))} is functional non empty finite set
{a} is functional non empty trivial finite 1 -element set
{{a,((M,M,M,A,G) . (a1,a2))},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,((M,M,M,A,G) . (a1,a2))] is Relation-like Function-like set
(M,M,M,A,G) . (a,a1) is Relation-like Function-like Element of Funcs (G,M)
[a,a1] is set
{a,a1} is functional non empty finite set
{{a,a1},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,a1] is Relation-like Function-like set
(M,M,M,A,G) . (((M,M,M,A,G) . (a,a1)),a2) is Relation-like Function-like Element of Funcs (G,M)
[((M,M,M,A,G) . (a,a1)),a2] is set
{((M,M,M,A,G) . (a,a1)),a2} is functional non empty finite set
{((M,M,M,A,G) . (a,a1))} is functional non empty trivial finite 1 -element set
{{((M,M,M,A,G) . (a,a1)),a2},{((M,M,M,A,G) . (a,a1))}} is non empty finite V46() set
(M,M,M,A,G) . [((M,M,M,A,G) . (a,a1)),a2] is Relation-like Function-like set
(M,M,M,A,G) . (a,a1) is Relation-like Function-like Element of Funcs (G,M)
(M,M,M,A,G) . (((M,M,M,A,G) . (a,a1)),a2) is Relation-like Function-like Element of Funcs (G,M)
[((M,M,M,A,G) . (a,a1)),a2] is set
{((M,M,M,A,G) . (a,a1)),a2} is functional non empty finite set
{((M,M,M,A,G) . (a,a1))} is functional non empty trivial finite 1 -element set
{{((M,M,M,A,G) . (a,a1)),a2},{((M,M,M,A,G) . (a,a1))}} is non empty finite V46() set
(M,M,M,A,G) . [((M,M,M,A,G) . (a,a1)),a2] is Relation-like Function-like set
(G,M,M,M,A,a,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . ((G,M,M,M,A,a,a1),a2) is Relation-like Function-like Element of Funcs (G,M)
[(G,M,M,M,A,a,a1),a2] is set
{(G,M,M,M,A,a,a1),a2} is functional non empty finite set
{(G,M,M,M,A,a,a1)} is functional non empty trivial finite 1 -element set
{{(G,M,M,M,A,a,a1),a2},{(G,M,M,M,A,a,a1)}} is non empty finite V46() set
(M,M,M,A,G) . [(G,M,M,M,A,a,a1),a2] is Relation-like Function-like set
(G,M,M,M,A,(G,M,M,M,A,a,a1),a2) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,a1,a2) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,a,(G,M,M,M,A,a1,a2)) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (a,(G,M,M,M,A,a1,a2)) is Relation-like Function-like Element of Funcs (G,M)
[a,(G,M,M,M,A,a1,a2)] is set
{a,(G,M,M,M,A,a1,a2)} is functional non empty finite set
{{a,(G,M,M,M,A,a1,a2)},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,(G,M,M,M,A,a1,a2)] is Relation-like Function-like set
(M,M,M,A,G) . (a1,a2) is Relation-like Function-like Element of Funcs (G,M)
(M,M,M,A,G) . (a,((M,M,M,A,G) . (a1,a2))) is Relation-like Function-like Element of Funcs (G,M)
[a,((M,M,M,A,G) . (a1,a2))] is set
{a,((M,M,M,A,G) . (a1,a2))} is functional non empty finite set
{{a,((M,M,M,A,G) . (a1,a2))},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,((M,M,M,A,G) . (a1,a2))] is Relation-like Function-like set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Element of M
(M,G,A) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)
B is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,B,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
a2 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom a2 is Element of bool G
bool G is non empty set
(M,M,M,B,G) . ((M,G,A),a2) is Relation-like Function-like Element of Funcs (G,M)
[(M,G,A),a2] is set
{(M,G,A),a2} is functional non empty finite set
{(M,G,A)} is functional non empty trivial finite 1 -element set
{{(M,G,A),a2},{(M,G,A)}} is non empty finite V46() set
(M,M,M,B,G) . [(M,G,A),a2] is Relation-like Function-like set
(G,M,M,M,B,(M,G,A),a2) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,B,A,a2) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,B,G) . (a2,(M,G,A)) is Relation-like Function-like Element of Funcs (G,M)
[a2,(M,G,A)] is set
{a2,(M,G,A)} is functional non empty finite set
{a2} is functional non empty trivial finite 1 -element set
{{a2,(M,G,A)},{a2}} is non empty finite V46() set
(M,M,M,B,G) . [a2,(M,G,A)] is Relation-like Function-like set
(G,M,M,M,B,a2,(M,G,A)) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,B,a2,A) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
the_unity_wrt (M,M,M,A,G) is Relation-like Function-like Element of Funcs (G,M)
the_unity_wrt A is Element of M
(M,G,(the_unity_wrt A)) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)
B is Element of M
(M,G,B) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
B is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (B,B) is Relation-like Function-like Element of Funcs (G,M)
[B,B] is set
{B,B} is functional non empty finite set
{B} is functional non empty trivial finite 1 -element set
{{B,B},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,B] is Relation-like Function-like set
(M,M,M,A,G) . (B,B) is Relation-like Function-like Element of Funcs (G,M)
(G,M,M,M,A,B,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
B is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a1 is set
B . a1 is set
a . a1 is set
a2 is Element of M
a1 is Element of M
a2 is Element of M
A . (a2,a2) is Element of M
[a2,a2] is set
{a2,a2} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a2},{a2}} is non empty finite V46() set
A . [a2,a2] is set
x is Element of M
A . (x,a2) is Element of M
[x,a2] is set
{x,a2} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,a2},{x}} is non empty finite V46() set
A . [x,a2] is set
A . ((B . a1),a2) is set
[(B . a1),a2] is set
{(B . a1),a2} is non empty finite set
{(B . a1)} is non empty trivial finite 1 -element set
{{(B . a1),a2},{(B . a1)}} is non empty finite V46() set
A . [(B . a1),a2] is set
[:G,M:] is Relation-like set
bool [:G,M:] is non empty set
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
a2 is set
B . a2 is set
a . a2 is set
a1 is Element of M
a2 is Element of M
x is Element of M
A . (a1,x) is Element of M
[a1,x] is set
{a1,x} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,x},{a1}} is non empty finite V46() set
A . [a1,x] is set
c is Element of M
A . (c,a1) is Element of M
[c,a1] is set
{c,a1} is non empty finite set
{c} is non empty trivial finite 1 -element set
{{c,a1},{c}} is non empty finite V46() set
A . [c,a1] is set
A . (c,(B . a2)) is set
[c,(B . a2)] is set
{c,(B . a2)} is non empty finite set
{{c,(B . a2)},{c}} is non empty finite V46() set
A . [c,(B . a2)] is set
a2 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]
dom a1 is Element of bool G
bool G is non empty set
dom a2 is Element of bool G
rng a1 is Element of bool M
bool M is non empty set
rng a2 is Element of bool M
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (B,a1) is Relation-like Function-like Element of Funcs (G,M)
[B,a1] is set
{B,a1} is functional non empty finite set
{B} is functional non empty trivial finite 1 -element set
{{B,a1},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,a1] is Relation-like Function-like set
a2 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (a2,B) is Relation-like Function-like Element of Funcs (G,M)
[a2,B] is set
{a2,B} is functional non empty finite set
{a2} is functional non empty trivial finite 1 -element set
{{a2,B},{a2}} is non empty finite V46() set
(M,M,M,A,G) . [a2,B] is Relation-like Function-like set
dom a is Element of bool G
(G,M,M,M,A,B,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,B,a1) is Element of bool G
x is set
(G,M,M,M,A,B,a1) . x is set
B . x is set
a1 . x is set
A . ((B . x),(a1 . x)) is set
[(B . x),(a1 . x)] is set
{(B . x),(a1 . x)} is non empty finite set
{(B . x)} is non empty trivial finite 1 -element set
{{(B . x),(a1 . x)},{(B . x)}} is non empty finite V46() set
A . [(B . x),(a1 . x)] is set
a . x is set
(G,M,M,M,A,a2,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,a2,B) is Element of bool G
x is set
(G,M,M,M,A,a2,B) . x is set
a2 . x is set
B . x is set
A . ((a2 . x),(B . x)) is set
[(a2 . x),(B . x)] is set
{(a2 . x),(B . x)} is non empty finite set
{(a2 . x)} is non empty trivial finite 1 -element set
{{(a2 . x),(B . x)},{(a2 . x)}} is non empty finite V46() set
A . [(a2 . x),(B . x)] is set
a . x is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
B is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (B,a) is Relation-like Function-like Element of Funcs (G,M)
[B,a] is set
{B,a} is functional non empty finite set
{B} is functional non empty trivial finite 1 -element set
{{B,a},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,a] is Relation-like Function-like set
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (B,a1) is Relation-like Function-like Element of Funcs (G,M)
[B,a1] is set
{B,a1} is functional non empty finite set
{{B,a1},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,a1] is Relation-like Function-like set
(M,M,M,A,G) . (a,B) is Relation-like Function-like Element of Funcs (G,M)
[a,B] is set
{a,B} is functional non empty finite set
{a} is functional non empty trivial finite 1 -element set
{{a,B},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,B] is Relation-like Function-like set
(M,M,M,A,G) . (a1,B) is Relation-like Function-like Element of Funcs (G,M)
[a1,B] is set
{a1,B} is functional non empty finite set
{a1} is functional non empty trivial finite 1 -element set
{{a1,B},{a1}} is non empty finite V46() set
(M,M,M,A,G) . [a1,B] is Relation-like Function-like set
(G,M,M,M,A,a,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,a,B) is Element of bool G
bool G is non empty set
(G,M,M,M,A,a1,B) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,a1,B) is Element of bool G
(G,M,M,M,A,B,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,B,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,B,a) is Element of bool G
dom (G,M,M,M,A,B,a1) is Element of bool G
a2 is set
B . a2 is set
a . a2 is set
a1 . a2 is set
(G,M,M,M,A,a,B) . a2 is set
a2 is Element of M
a1 is Element of M
A . (a2,a1) is Element of M
[a2,a1] is set
{a2,a1} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
A . [a2,a1] is set
(G,M,M,M,A,a1,B) . a2 is set
x is Element of M
A . (x,a1) is Element of M
[x,a1] is set
{x,a1} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,a1},{x}} is non empty finite V46() set
A . [x,a1] is set
(G,M,M,M,A,B,a) . a2 is set
A . (a1,a2) is Element of M
[a1,a2] is set
{a1,a2} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
A . [a1,a2] is set
(G,M,M,M,A,B,a1) . a2 is set
A . (a1,x) is Element of M
[a1,x] is set
{a1,x} is non empty finite set
{{a1,x},{a1}} is non empty finite V46() set
A . [a1,x] is set
dom a is Element of bool G
dom a1 is Element of bool G
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
the_unity_wrt A is Element of M
the_unity_wrt (M,M,M,A,G) is Relation-like Function-like Element of Funcs (G,M)
(M,G,(the_unity_wrt A)) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)
B is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,A,G) . (B,a) is Relation-like Function-like Element of Funcs (G,M)
[B,a] is set
{B,a} is functional non empty finite set
{B} is functional non empty trivial finite 1 -element set
{{B,a},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,a] is Relation-like Function-like set
(G,M,M,M,A,B,a) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,B,a) is Element of bool G
bool G is non empty set
a1 is set
B . a1 is set
a . a1 is set
(G,M,M,M,A,B,a) . a1 is set
a2 is Element of M
a1 is Element of M
A . (a2,a1) is Element of M
[a2,a1] is set
{a2,a1} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
A . [a2,a1] is set
(M,G,(the_unity_wrt A)) . a1 is set
a1 is set
B . a1 is set
a . a1 is set
(G,M,M,M,A,B,a) . a1 is set
a2 is Element of M
a1 is Element of M
A . (a2,a1) is Element of M
[a2,a1] is set
{a2,a1} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
A . [a2,a1] is set
(M,G,(the_unity_wrt A)) . a1 is set
dom a is Element of bool G
dom B is Element of bool G
dom (M,G,(the_unity_wrt A)) is Element of bool G
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,A,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
[:(Funcs (G,M)),(Funcs (G,M)):] is Relation-like non empty set
[:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):] is non empty set
B is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
(M,M,M,B,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,M)):] -defined Funcs (G,M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,M)):],(Funcs (G,M)):]
a is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(M,M,M,B,G) . (a,a1) is Relation-like Function-like Element of Funcs (G,M)
[a,a1] is set
{a,a1} is functional non empty finite set
{a} is functional non empty trivial finite 1 -element set
{{a,a1},{a}} is non empty finite V46() set
(M,M,M,B,G) . [a,a1] is Relation-like Function-like set
(M,M,M,A,G) . (a,((M,M,M,B,G) . (a,a1))) is Relation-like Function-like Element of Funcs (G,M)
[a,((M,M,M,B,G) . (a,a1))] is set
{a,((M,M,M,B,G) . (a,a1))} is functional non empty finite set
{{a,((M,M,M,B,G) . (a,a1))},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,((M,M,M,B,G) . (a,a1))] is Relation-like Function-like set
(G,M,M,M,B,a,a1) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
(G,M,M,M,A,a,(G,M,M,M,B,a,a1)) is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
dom (G,M,M,M,A,a,(G,M,M,M,B,a,a1)) is Element of bool G
bool G is non empty set
dom (G,M,M,M,B,a,a1) is Element of bool G
a2 is set
a . a2 is set
a1 . a2 is set
(G,M,M,M,A,a,(G,M,M,M,B,a,a1)) . a2 is set
a1 is Element of M
(G,M,M,M,B,a,a1) . a2 is set
A . (a1,((G,M,M,M,B,a,a1) . a2)) is set
[a1,((G,M,M,M,B,a,a1) . a2)] is set
{a1,((G,M,M,M,B,a,a1) . a2)} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,((G,M,M,M,B,a,a1) . a2)},{a1}} is non empty finite V46() set
A . [a1,((G,M,M,M,B,a,a1) . a2)] is set
a2 is Element of M
B . (a1,a2) is Element of M
[a1,a2] is set
{a1,a2} is non empty finite set
{{a1,a2},{a1}} is non empty finite V46() set
B . [a1,a2] is set
dom a is Element of bool G
(M,M,M,A,G) . (a,(G,M,M,M,B,a,a1)) is Relation-like Function-like Element of Funcs (G,M)
[a,(G,M,M,M,B,a,a1)] is set
{a,(G,M,M,M,B,a,a1)} is functional non empty finite set
{{a,(G,M,M,M,B,a,a1)},{a}} is non empty finite V46() set
(M,M,M,A,G) . [a,(G,M,M,M,B,a,a1)] is Relation-like Function-like set
G is set
M is non empty set
A is non empty set
[:M,A:] is Relation-like non empty set
B is non empty set
[:[:M,A:],B:] is Relation-like non empty set
bool [:[:M,A:],B:] is non empty set
a is non empty set
a1 is non empty set
[:a,a1:] is Relation-like non empty set
a2 is non empty set
[:[:a,a1:],a2:] is Relation-like non empty set
bool [:[:a,a1:],a2:] is non empty set
Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M
Funcs (G,A) is functional non empty FUNCTION_DOMAIN of G,A
[:(Funcs (G,M)),(Funcs (G,A)):] is Relation-like non empty set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B
a1 is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]
(M,A,B,a1,G) is Relation-like [:(Funcs (G,M)),(Funcs (G,A)):] -defined Funcs (G,B) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,M)),(Funcs (G,A)):],(Funcs (G,B)):]
[:[:(Funcs (G,M)),(Funcs (G,A)):],(Funcs (G,B)):] is Relation-like non empty set
bool [:[:(Funcs (G,M)),(Funcs (G,A)):],(Funcs (G,B)):] is non empty set
a2 is Relation-like [:a,a1:] -defined a2 -valued Function-like non empty total quasi_total Element of bool [:[:a,a1:],a2:]
(a,a1,a2,a2,G) is Relation-like [:(Funcs (G,a)),(Funcs (G,a1)):] -defined Funcs (G,a2) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,a)),(Funcs (G,a1)):],(Funcs (G,a2)):]
Funcs (G,a) is functional non empty FUNCTION_DOMAIN of G,a
Funcs (G,a1) is functional non empty FUNCTION_DOMAIN of G,a1
[:(Funcs (G,a)),(Funcs (G,a1)):] is Relation-like non empty set
Funcs (G,a2) is functional non empty FUNCTION_DOMAIN of G,a2
[:[:(Funcs (G,a)),(Funcs (G,a1)):],(Funcs (G,a2)):] is Relation-like non empty set
bool [:[:(Funcs (G,a)),(Funcs (G,a1)):],(Funcs (G,a2)):] is non empty set
dom a1 is Relation-like M -defined A -valued non empty Element of bool [:M,A:]
bool [:M,A:] is non empty set
dom a2 is Relation-like a -defined a1 -valued non empty Element of bool [:a,a1:]
bool [:a,a1:] is non empty set
x is set
dom (M,A,B,a1,G) is Relation-like Funcs (G,M) -defined Funcs (G,A) -valued non empty Element of bool [:(Funcs (G,M)),(Funcs (G,A)):]
bool [:(Funcs (G,M)),(Funcs (G,A)):] is non empty set
c is Element of [:(Funcs (G,M)),(Funcs (G,A)):]
c `2 is Relation-like Function-like Element of Funcs (G,A)
c `1 is Relation-like Function-like Element of Funcs (G,M)
f9 is Relation-like G -defined a -valued Function-like total quasi_total Element of Funcs (G,a)
y2 is Relation-like G -defined a1 -valued Function-like total quasi_total Element of Funcs (G,a1)
(G,a,a1,a2,a2,f9,y2) is Relation-like G -defined a2 -valued Function-like total quasi_total Element of Funcs (G,a2)
dom (G,a,a1,a2,a2,f9,y2) is Element of bool G
bool G is non empty set
g is Relation-like G -defined M -valued Function-like total quasi_total Element of Funcs (G,M)
y1 is Relation-like G -defined A -valued Function-like total quasi_total Element of Funcs (G,A)
(G,M,A,B,a1,g,y1) is Relation-like G -defined B -valued Function-like total quasi_total Element of Funcs (G,B)
dom (G,M,A,B,a1,g,y1) is Element of bool G
dom g is Element of bool G
dom y1 is Element of bool G
V9 is set
g . V9 is set
rng g is Element of bool M
bool M is non empty set
y1 . V9 is set
rng y1 is Element of bool A
bool A is non empty set
[(g . V9),(y1 . V9)] is set
{(g . V9),(y1 . V9)} is non empty finite set
{(g . V9)} is non empty trivial finite 1 -element set
{{(g . V9),(y1 . V9)},{(g . V9)}} is non empty finite V46() set
(G,a,a1,a2,a2,f9,y2) . V9 is set
f9 . V9 is set
y2 . V9 is set
a2 . ((f9 . V9),(y2 . V9)) is set
[(f9 . V9),(y2 . V9)] is set
{(f9 . V9),(y2 . V9)} is non empty finite set
{(f9 . V9)} is non empty trivial finite 1 -element set
{{(f9 . V9),(y2 . V9)},{(f9 . V9)}} is non empty finite V46() set
a2 . [(f9 . V9),(y2 . V9)] is set
(G,M,A,B,a1,g,y1) . V9 is set
a1 . ((g . V9),(y1 . V9)) is set
a1 . [(g . V9),(y1 . V9)] is set
[g,y1] is Element of [:(Funcs (G,M)),(Funcs (G,A)):]
{g,y1} is functional non empty finite set
{g} is functional non empty trivial finite 1 -element set
{{g,y1},{g}} is non empty finite V46() set
(M,A,B,a1,G) . (g,y1) is Relation-like Function-like Element of Funcs (G,B)
[g,y1] is set
(M,A,B,a1,G) . [g,y1] is Relation-like Function-like set
(a,a1,a2,a2,G) . (f9,y2) is Relation-like Function-like Element of Funcs (G,a2)
[f9,y2] is set
{f9,y2} is functional non empty finite set
{f9} is functional non empty trivial finite 1 -element set
{{f9,y2},{f9}} is non empty finite V46() set
(a,a1,a2,a2,G) . [f9,y2] is Relation-like Function-like set
(M,A,B,a1,G) . x is Relation-like Function-like set
(a,a1,a2,a2,G) . x is Relation-like Function-like set
dom (a,a1,a2,a2,G) is Relation-like Funcs (G,a) -defined Funcs (G,a1) -valued non empty Element of bool [:(Funcs (G,a)),(Funcs (G,a1)):]
bool [:(Funcs (G,a)),(Funcs (G,a1)):] is non empty set
G is non empty multMagma
M is set
the carrier of G is non empty set
Funcs (M, the carrier of G) is functional non empty FUNCTION_DOMAIN of M, the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like 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, the carrier of G, the carrier of G, the multF of G,M) is Relation-like [:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] -defined Funcs (M, the carrier of G) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):]
[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] is Relation-like non empty set
[:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is Relation-like non empty set
bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is non empty set
the_unity_wrt the multF of G is Element of the carrier of G
( the carrier of G,M,(the_unity_wrt the multF of G)) is Relation-like M -defined the carrier of G -valued Function-like constant total quasi_total Element of Funcs (M, the carrier of G)
multLoopStr(# (Funcs (M, the carrier of G)),( the carrier of G, the carrier of G, the carrier of G, the multF of G,M),( the carrier of G,M,(the_unity_wrt the multF of G)) #) is strict multLoopStr
multMagma(# (Funcs (M, the carrier of G)),( the carrier of G, the carrier of G, the carrier of G, the multF of G,M) #) is strict multMagma
G is non empty multMagma
M is set
(G,M) is multMagma
the carrier of G is non empty set
Funcs (M, the carrier of G) is functional non empty FUNCTION_DOMAIN of M, the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like 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, the carrier of G, the carrier of G, the multF of G,M) is Relation-like [:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] -defined Funcs (M, the carrier of G) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):]
[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] is Relation-like non empty set
[:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is Relation-like non empty set
bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is non empty set
the_unity_wrt the multF of G is Element of the carrier of G
( the carrier of G,M,(the_unity_wrt the multF of G)) is Relation-like M -defined the carrier of G -valued Function-like constant total quasi_total Element of Funcs (M, the carrier of G)
multLoopStr(# (Funcs (M, the carrier of G)),( the carrier of G, the carrier of G, the carrier of G, the multF of G,M),( the carrier of G,M,(the_unity_wrt the multF of G)) #) is strict multLoopStr
the carrier of (G,M) is set
the carrier of G is non empty set
Funcs (M, the carrier of G) is functional non empty FUNCTION_DOMAIN of M, the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like 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, the carrier of G, the carrier of G, the multF of G,M) is Relation-like [:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] -defined Funcs (M, the carrier of G) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):]
[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] is Relation-like non empty set
[:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is Relation-like non empty set
bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M, the carrier of G)):] is non empty set
multMagma(# (Funcs (M, the carrier of G)),( the carrier of G, the carrier of G, the carrier of G, the multF of G,M) #) is strict multMagma
the carrier of (G,M) is set
G is set
M is non empty multMagma
(M,G) is non empty multMagma
the carrier of (M,G) is non empty set
the carrier of M is non empty set
Funcs (G, the carrier of M) is functional non empty FUNCTION_DOMAIN of G, the carrier of M
[: the carrier of (M,G), the carrier of (M,G):] is Relation-like non empty set
[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] is Relation-like non empty set
the multF of (M,G) is Relation-like [: the carrier of (M,G), the carrier of (M,G):] -defined the carrier of (M,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):]
[:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is Relation-like non empty set
bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is non empty set
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
( the carrier of M, the carrier of M, the carrier of M, the multF of M,G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G, the carrier of M) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G, the carrier of M)):]
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G, the carrier of M)):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G, the carrier of M)):] is non empty set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
( the carrier of M, the carrier of M,H₃(M),H₁(M),G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G,H₃(M)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):]
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is non empty set
multMagma(# (Funcs (G,H₃(M))),( the carrier of M, the carrier of M,H₃(M),H₁(M),G) #) is strict multMagma
the_unity_wrt H₁(M) is Element of the carrier of M
( the carrier of M,G,(the_unity_wrt H₁(M))) is Relation-like G -defined the carrier of M -valued Function-like constant total quasi_total Element of Funcs (G, the carrier of M)
multLoopStr(# (Funcs (G,H₃(M))),( the carrier of M, the carrier of M,H₃(M),H₁(M),G),( the carrier of M,G,(the_unity_wrt H₁(M))) #) is strict multLoopStr
G is set
M is set
A is non empty multMagma
(A,M) is non empty multMagma
the carrier of (A,M) is non empty set
the carrier of A is non empty set
[:M, the carrier of A:] is Relation-like set
bool [:M, the carrier of A:] is non empty set
Funcs (M,H₃(A)) is functional non empty FUNCTION_DOMAIN of M,H₃(A)
[:M,H₃(A):] is Relation-like set
bool [:M,H₃(A):] is non empty set
B is Relation-like M -defined H₃(A) -valued Function-like total quasi_total Element of bool [:M,H₃(A):]
rng B is Element of bool H₃(A)
bool H₃(A) is non empty set
dom B is Element of bool M
bool M is non empty set
G is set
M is non empty multMagma
(M,G) is non empty multMagma
the carrier of (M,G) is non empty set
A is Element of the carrier of (M,G)
the carrier of M is non empty set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
G is non empty multMagma
M is set
(G,M) is non empty multMagma
G is set
M is non empty multMagma
(M,G) is non empty constituted-Functions multMagma
the carrier of (M,G) is non empty set
the carrier of M is non empty set
A is Relation-like Function-like Element of the carrier of (M,G)
dom A is set
rng A is set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
B is Relation-like G -defined H₃(M) -valued Function-like total quasi_total Element of Funcs (G,H₃(M))
G is set
M is non empty multMagma
(M,G) is non empty constituted-Functions multMagma
the carrier of (M,G) is non empty set
A is Relation-like Function-like Element of the carrier of (M,G)
B is Relation-like Function-like Element of the carrier of (M,G)
dom A is set
dom B is set
G is non empty multMagma
M is non empty set
(G,M) is non empty constituted-Functions multMagma
the carrier of (G,M) is non empty set
A is Relation-like Function-like Element of the carrier of (G,M)
B is Element of M
A . B is set
the carrier of G is non empty set
dom A is set
rng A is set
G is non empty multMagma
M is non empty set
(G,M) is non empty constituted-Functions multMagma
the carrier of (G,M) is non empty set
A is Relation-like Function-like Element of the carrier of (G,M)
rng A is set
the Element of M is Element of M
dom A is set
(G,M,A, the Element of M) is Element of the carrier of G
the carrier of G is non empty set
G is non empty set
M is non empty multMagma
(M,G) is non empty constituted-Functions multMagma
the carrier of (M,G) is non empty set
A is Relation-like Function-like Element of the carrier of (M,G)
B is Relation-like Function-like Element of the carrier of (M,G)
A [*] B is Relation-like Function-like Element of the carrier of (M,G)
the multF of (M,G) is Relation-like [: the carrier of (M,G), the carrier of (M,G):] -defined the carrier of (M,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):]
[: the carrier of (M,G), the carrier of (M,G):] is Relation-like non empty set
[:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is Relation-like non empty set
bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is non empty set
the multF of (M,G) . (A,B) is Relation-like Function-like Element of the carrier of (M,G)
[A,B] is set
{A,B} is functional non empty finite set
{A} is functional non empty trivial finite 1 -element set
{{A,B},{A}} is non empty finite V46() set
the multF of (M,G) . [A,B] is set
a is Element of G
(M,G,(A [*] B),a) is Element of the carrier of M
the carrier of M is non empty set
(M,G,A,a) is Element of the carrier of M
(M,G,B,a) is Element of the carrier of M
(M,G,A,a) [*] (M,G,B,a) is Element of the carrier of M
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
the multF of M . ((M,G,A,a),(M,G,B,a)) is Element of the carrier of M
[(M,G,A,a),(M,G,B,a)] is set
{(M,G,A,a),(M,G,B,a)} is non empty finite set
{(M,G,A,a)} is non empty trivial finite 1 -element set
{{(M,G,A,a),(M,G,B,a)},{(M,G,A,a)}} is non empty finite V46() set
the multF of M . [(M,G,A,a),(M,G,B,a)] is set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
Funcs (G, the carrier of M) is functional non empty FUNCTION_DOMAIN of G, the carrier of M
[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] is Relation-like non empty set
( the carrier of M, the carrier of M,H₃(M),H₁(M),G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G,H₃(M)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):]
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is non empty set
a1 is Relation-like G -defined H₃(M) -valued Function-like total quasi_total Element of Funcs (G,H₃(M))
a2 is Relation-like G -defined H₃(M) -valued Function-like total quasi_total Element of Funcs (G,H₃(M))
(G,H₃(M),H₃(M), the carrier of M,H₁(M),a1,a2) is Relation-like G -defined the carrier of M -valued Function-like total quasi_total Element of Funcs (G, the carrier of M)
dom (G,H₃(M),H₃(M), the carrier of M,H₁(M),a1,a2) is Element of bool G
bool G is non empty set
G is non empty unital multMagma
M is set
(G,M) is non empty constituted-Functions multMagma
the carrier of G is non empty set
Funcs (M,H₃(G)) is functional non empty FUNCTION_DOMAIN of M,H₃(G)
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G,H₃(G),H₁(G),M) is Relation-like [:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] -defined Funcs (M,H₃(G)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):]
Funcs (M, the carrier of G) is functional non empty FUNCTION_DOMAIN of M, the carrier of G
[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] is Relation-like non empty set
[:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):] is Relation-like non empty set
bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):] is non empty set
the_unity_wrt H₁(G) is Element of the carrier of G
( the carrier of G,M,(the_unity_wrt H₁(G))) is Relation-like M -defined the carrier of G -valued Function-like constant total quasi_total Element of Funcs (M, the carrier of G)
multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #) is strict multLoopStr
B is Element of the carrier of G
1. multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #) is Element of the carrier of multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #)
the carrier of multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #) is set
the OneF of multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #) is Element of the carrier of multLoopStr(# (Funcs (M,H₃(G))),( the carrier of G, the carrier of G,H₃(G),H₁(G),M),( the carrier of G,M,(the_unity_wrt H₁(G))) #)
the_unity_wrt the multF of G is Element of the carrier of G
( the carrier of G,M,(the_unity_wrt the multF of G)) is Relation-like M -defined the carrier of G -valued Function-like constant total quasi_total Element of Funcs (M, the carrier of G)
( the carrier of G,M,B) is Relation-like M -defined the carrier of G -valued Function-like constant total quasi_total Element of Funcs (M, the carrier of G)
G is set
M is non empty unital multMagma
(M,G) is non empty strict well-unital constituted-Functions multLoopStr
1. (M,G) is Relation-like Function-like Element of the carrier of (M,G)
the carrier of (M,G) is non empty set
the OneF of (M,G) is Relation-like Function-like Element of the carrier of (M,G)
the carrier of M is non empty set
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
the_unity_wrt the multF of M is Element of the carrier of M
( the carrier of M,G,(the_unity_wrt the multF of M)) is Relation-like G -defined the carrier of M -valued Function-like constant total quasi_total Element of Funcs (G, the carrier of M)
Funcs (G, the carrier of M) is functional non empty FUNCTION_DOMAIN of G, the carrier of M
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
( the carrier of M, the carrier of M,H₃(M),H₁(M),G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G,H₃(M)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):]
[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] is Relation-like non empty set
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is non empty set
the_unity_wrt H₁(M) is Element of the carrier of M
( the carrier of M,G,(the_unity_wrt H₁(M))) is Relation-like G -defined the carrier of M -valued Function-like constant total quasi_total Element of Funcs (G, the carrier of M)
multLoopStr(# (Funcs (G,H₃(M))),( the carrier of M, the carrier of M,H₃(M),H₁(M),G),( the carrier of M,G,(the_unity_wrt H₁(M))) #) is strict multLoopStr
G is non empty multMagma
M is set
(G,M) is non empty constituted-Functions multMagma
the carrier of (G,M) is non empty set
[: the carrier of (G,M), the carrier of (G,M):] is Relation-like non empty set
the carrier of G is non empty set
Funcs (M, the carrier of G) is functional non empty FUNCTION_DOMAIN of M, the carrier of G
[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] is Relation-like non empty set
Funcs (M,H₃(G)) is functional non empty FUNCTION_DOMAIN of M,H₃(G)
the multF of (G,M) is Relation-like [: the carrier of (G,M), the carrier of (G,M):] -defined the carrier of (G,M) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (G,M), the carrier of (G,M):], the carrier of (G,M):]
[:[: the carrier of (G,M), the carrier of (G,M):], the carrier of (G,M):] is Relation-like non empty set
bool [:[: the carrier of (G,M), the carrier of (G,M):], the carrier of (G,M):] is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G,H₃(G),H₁(G),M) is Relation-like [:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):] -defined Funcs (M,H₃(G)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):]
[:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):] is Relation-like non empty set
bool [:[:(Funcs (M, the carrier of G)),(Funcs (M, the carrier of G)):],(Funcs (M,H₃(G))):] is non empty set
G is set
M is non empty multMagma
(M,G) is non empty constituted-Functions multMagma
A is non empty SubStr of M
(A,G) is non empty constituted-Functions multMagma
the carrier of (A,G) is non empty set
[: the carrier of (A,G), the carrier of (A,G):] is Relation-like non empty set
the carrier of A is non empty set
Funcs (G, the carrier of A) is functional non empty FUNCTION_DOMAIN of G, the carrier of A
[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):] is Relation-like non empty set
Funcs (G,H₃(A)) is functional non empty FUNCTION_DOMAIN of G,H₃(A)
the multF of (A,G) is Relation-like [: the carrier of (A,G), the carrier of (A,G):] -defined the carrier of (A,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):]
[:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):] is Relation-like non empty set
bool [:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):] is non empty set
the multF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
( the carrier of A, the carrier of A,H₃(A),H₁(A),G) is Relation-like [:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):] -defined Funcs (G,H₃(A)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):]
[:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):] is non empty set
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
the carrier of M is non empty set
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
the carrier of (M,G) is non empty set
[: the carrier of (M,G), the carrier of (M,G):] is Relation-like non empty set
Funcs (G, the carrier of M) is functional non empty FUNCTION_DOMAIN of G, the carrier of M
[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] is Relation-like non empty set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
the multF of (M,G) is Relation-like [: the carrier of (M,G), the carrier of (M,G):] -defined the carrier of (M,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):]
[:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is Relation-like non empty set
bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is non empty set
( the carrier of M, the carrier of M,H₃(M),H₁(M),G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G,H₃(M)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):]
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is non empty set
G is set
M is non empty unital multMagma
the carrier of M is non empty set
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
the_unity_wrt the multF of M is Element of the carrier of M
(M,G) is non empty strict well-unital constituted-Functions multLoopStr
A is non empty SubStr of M
the carrier of A is non empty set
(A,G) is non empty constituted-Functions multMagma
a is non empty unital multMagma
the carrier of a is non empty set
the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is Relation-like non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the_unity_wrt H₁(a) is Element of the carrier of a
B is non empty unital multMagma
the carrier of B is non empty set
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
the_unity_wrt H₁(B) is Element of the carrier of B
the carrier of (A,G) is non empty set
[: the carrier of (A,G), the carrier of (A,G):] is Relation-like non empty set
Funcs (G, the carrier of A) is functional non empty FUNCTION_DOMAIN of G, the carrier of A
[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):] is Relation-like non empty set
Funcs (G,H₃(A)) is functional non empty FUNCTION_DOMAIN of G,H₃(A)
the multF of (A,G) is Relation-like [: the carrier of (A,G), the carrier of (A,G):] -defined the carrier of (A,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):]
[:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):] is Relation-like non empty set
bool [:[: the carrier of (A,G), the carrier of (A,G):], the carrier of (A,G):] is non empty set
the multF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is Relation-like non empty set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is Relation-like non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
( the carrier of A, the carrier of A,H₃(A),H₁(A),G) is Relation-like [:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):] -defined Funcs (G,H₃(A)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):]
[:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of A)),(Funcs (G, the carrier of A)):],(Funcs (G,H₃(A))):] is non empty set
the carrier of (M,G) is non empty set
[: the carrier of (M,G), the carrier of (M,G):] is Relation-like non empty set
Funcs (G, the carrier of M) is functional non empty FUNCTION_DOMAIN of G, the carrier of M
[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] is Relation-like non empty set
Funcs (G,H₃(M)) is functional non empty FUNCTION_DOMAIN of G,H₃(M)
the multF of (M,G) is Relation-like [: the carrier of (M,G), the carrier of (M,G):] -defined the carrier of (M,G) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):]
[:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is Relation-like non empty set
bool [:[: the carrier of (M,G), the carrier of (M,G):], the carrier of (M,G):] is non empty set
( the carrier of M, the carrier of M,H₃(M),H₁(M),G) is Relation-like [:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):] -defined Funcs (G,H₃(M)) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):]
[:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is Relation-like non empty set
bool [:[:(Funcs (G, the carrier of M)),(Funcs (G, the carrier of M)):],(Funcs (G,H₃(M))):] is non empty set
(B,G) is non empty strict well-unital constituted-Functions multLoopStr
1. (B,G) is Relation-like Function-like Element of the carrier of (B,G)
the carrier of (B,G) is non empty set
the OneF of (B,G) is Relation-like Function-like Element of the carrier of (B,G)
the_unity_wrt H₁(M) is Element of the carrier of M
( the carrier of M,G,(the_unity_wrt H₁(M))) is Relation-like G -defined the carrier of M -valued Function-like constant total quasi_total Element of Funcs (G, the carrier of M)
(a,G) is non empty strict well-unital constituted-Functions multLoopStr
1. (a,G) is Relation-like Function-like Element of the carrier of (a,G)
the carrier of (a,G) is non empty set
the OneF of (a,G) is Relation-like Function-like Element of the carrier of (a,G)
the_unity_wrt H₁(A) is Element of the carrier of A
( the carrier of A,G,(the_unity_wrt H₁(A))) is Relation-like G -defined the carrier of A -valued Function-like constant total quasi_total Element of Funcs (G, the carrier of A)
G is non empty unital associative commutative left-cancelable right-cancelable cancelable uniquely-decomposable multMagma
M is set
(G,M) is non empty constituted-Functions multMagma
(G,M) is non empty strict well-unital constituted-Functions multLoopStr
G is set
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
G is set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
Funcs (G,NAT) is functional non empty FUNCTION_DOMAIN of G, NAT
[: the carrier of (G), the carrier of (G):] is Relation-like non empty set
[:(Funcs (G,NAT)),(Funcs (G,NAT)):] is Relation-like non empty set
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued 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
(NAT,NAT,NAT,addnat,G) is Relation-like [:(Funcs (G,NAT)),(Funcs (G,NAT)):] -defined Funcs (G,NAT) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:(Funcs (G,NAT)),(Funcs (G,NAT)):],(Funcs (G,NAT)):]
[:[:(Funcs (G,NAT)),(Funcs (G,NAT)):],(Funcs (G,NAT)):] is Relation-like non empty set
bool [:[:(Funcs (G,NAT)),(Funcs (G,NAT)):],(Funcs (G,NAT)):] is non empty 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)
(NAT,G,0) is Relation-like G -defined NAT -valued Function-like constant total quasi_total Function-yielding V41() Element of Funcs (G,NAT)
the multF of <NAT,+,0> is Relation-like [: the carrier of <NAT,+,0>, the carrier of <NAT,+,0>:] -defined the carrier of <NAT,+,0> -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of <NAT,+,0>, the carrier of <NAT,+,0>:], the carrier of <NAT,+,0>:]
[: the carrier of <NAT,+,0>, the carrier of <NAT,+,0>:] is Relation-like non empty set
[:[: the carrier of <NAT,+,0>, the carrier of <NAT,+,0>:], the carrier of <NAT,+,0>:] is Relation-like non empty set
bool [:[: the carrier of <NAT,+,0>, the carrier of <NAT,+,0>:], the carrier of <NAT,+,0>:] is non empty set
multMagma(# the carrier of <NAT,+,0>, the multF of <NAT,+,0> #) is strict multMagma
the_unity_wrt H₁( <NAT,+> ) is Element of the carrier of <NAT,+>
G is set
M is set
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (M) is non empty set
[:M,NAT:] is Relation-like set
bool [:M,NAT:] is non empty set
A is Relation-like M -defined NAT -valued Function-like total quasi_total Element of bool [:M,NAT:]
dom A is Element of bool M
bool M is non empty set
rng A is Element of bool NAT
Funcs (M,NAT) is functional non empty FUNCTION_DOMAIN of M, NAT
G is set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Relation-like Function-like Element of the carrier of (G)
dom M is set
rng M is set
[:G,NAT:] is Relation-like set
bool [:G,NAT:] is non empty set
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Relation-like Function-like Element of the carrier of (G)
rng M is set
A is Element of G
M . A is set
dom M is set
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
A is Relation-like Function-like Element of the carrier of (G)
B is Relation-like Function-like Element of the carrier of (G)
A [*] B is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . (A,B) is Relation-like Function-like Element of the carrier of (G)
[A,B] is set
{A,B} is functional non empty finite set
{A} is functional non empty trivial finite 1 -element set
{{A,B},{A}} is non empty finite V46() set
the multF of (G) . [A,B] is set
a is Element of G
(G,(A [*] B),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,A,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,B,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,A,a) + (G,B,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M is non empty multMagma
(M,G) is non empty constituted-Functions multMagma
the carrier of (M,G) is non empty set
a1 is Relation-like Function-like Element of the carrier of (M,G)
(M,G,a1,a) is Element of the carrier of M
the carrier of M is non empty set
a2 is Relation-like Function-like Element of the carrier of (M,G)
(M,G,a2,a) is Element of the carrier of M
(M,G,a1,a) [*] (M,G,a2,a) is Element of the carrier of M
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty set
the multF of M . ((M,G,a1,a),(M,G,a2,a)) is Element of the carrier of M
[(M,G,a1,a),(M,G,a2,a)] is set
{(M,G,a1,a),(M,G,a2,a)} is non empty finite set
{(M,G,a1,a)} is non empty trivial finite 1 -element set
{{(M,G,a1,a),(M,G,a2,a)},{(M,G,a1,a)}} is non empty finite V46() set
the multF of M . [(M,G,a1,a),(M,G,a2,a)] is set
G is set
M is set
chi (G,M) is Relation-like M -defined {{},1} -valued Function-like total quasi_total Element of bool [:M,{{},1}:]
[:M,{{},1}:] is Relation-like set
bool [:M,{{},1}:] is non empty set
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (M) is non empty set
rng (chi (G,M)) is finite V46() Element of bool {{},1}
bool {{},1} is non empty finite V46() set
{0,1} is non empty finite V46() Element of bool NAT
dom (chi (G,M)) is Element of bool M
bool M is non empty set
Funcs (M,NAT) is functional non empty FUNCTION_DOMAIN of M, NAT
G is set
M is set
chi (G,M) is Relation-like Function-like set
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (M) is non empty set
G is set
M is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G --> M is Relation-like G -defined NAT -valued Function-like constant total set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
(NAT,G,M) is Relation-like G -defined NAT -valued Function-like constant total quasi_total Element of Funcs (G,NAT)
Funcs (G,NAT) is functional non empty FUNCTION_DOMAIN of G, NAT
G is non empty set
M is Element of G
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
({M},G) is Relation-like Function-like Element of the carrier of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
G is non empty set
M is Element of G
(G,M) is Relation-like Function-like Element of the carrier of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
({M},G) is Relation-like Function-like Element of the carrier of (G)
(G,(G,M),M) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
A is Element of G
(G,(G,M),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Relation-like Function-like Element of the carrier of (G)
A is Relation-like Function-like Element of the carrier of (G)
B is set
M . B is set
A . B is set
G is set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
{0} is functional non empty trivial finite V46() 1 -element Element of bool NAT
NAT \ {0} is Element of bool REAL
[:G,NAT:] is Relation-like set
bool [:G,NAT:] is non empty set
(G,0) is Relation-like G -defined NAT -valued Function-like constant total Function-yielding V41() Element of the carrier of (G)
A is Relation-like Function-like Element of the carrier of (G)
B is Relation-like Function-like Element of the carrier of (G)
A [*] B is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . (A,B) is Relation-like Function-like Element of the carrier of (G)
[A,B] is set
{A,B} is functional non empty finite set
{A} is functional non empty trivial finite 1 -element set
{{A,B},{A}} is non empty finite V46() set
the multF of (G) . [A,B] is set
a1 is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
a1 " (NAT \ {0}) is Element of bool G
bool G is non empty set
a2 is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
a2 " (NAT \ {0}) is Element of bool G
a is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
a " (NAT \ {0}) is Element of bool G
dom a1 is Element of bool G
dom a2 is Element of bool G
(a1 " (NAT \ {0})) \/ (a2 " (NAT \ {0})) is Element of bool G
a1 is set
a . a1 is set
a1 . a1 is set
rng a1 is Element of bool NAT
a2 . a1 is set
rng a2 is Element of bool NAT
a2 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
x is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a2 + x is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
dom M is Element of bool G
bool G is non empty set
M " (NAT \ {0}) is Element of bool G
the Element of M " (NAT \ {0}) is Element of M " (NAT \ {0})
M . the Element of M " (NAT \ {0}) is 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)
A is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
the carrier of A is non empty set
B is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
the carrier of B is non empty set
a is Relation-like Function-like Element of the carrier of (G)
a " (NAT \ {0}) is set
a1 is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
a1 " (NAT \ {0}) is Element of bool G
a1 is Relation-like G -defined NAT -valued Function-like total quasi_total Element of bool [:G,NAT:]
a1 " (NAT \ {0}) is Element of bool G
A is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
the carrier of A is non empty set
B is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
the carrier of B is non empty set
a is set
a1 is Relation-like Function-like Element of the carrier of (G)
a1 " (NAT \ {0}) is set
a is set
a1 is Relation-like Function-like Element of the carrier of (G)
a1 " (NAT \ {0}) is set
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Element of G
(G,M) is Relation-like Function-like Element of the carrier of (G)
the carrier of (G) is non empty set
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
({M},G) is Relation-like Function-like Element of the carrier of (G)
(G,M) " (NAT \ {0}) is set
A is set
dom (G,M) is set
(G,M) . A is set
B is Element of G
(G,(G,M),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G is set
{G} is non empty trivial finite 1 -element set
<*G*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
M is non empty set
A is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
A ^ <*G*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
{G} |` (A ^ <*G*>) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom ({G} |` (A ^ <*G*>)) is finite Element of bool NAT
{G} |` A is Relation-like NAT -defined {G} -valued M -valued Function-like finite FinSubsequence-like Element of bool [:NAT,M:]
[:NAT,M:] is Relation-like non empty non trivial non finite set
bool [:NAT,M:] is non empty non trivial non finite set
dom ({G} |` A) is finite Element of bool NAT
len A is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(len A) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{((len A) + 1)} is non empty trivial finite V46() 1 -element Element of bool NAT
(dom ({G} |` A)) \/ {((len A) + 1)} is non empty finite Element of bool NAT
B is set
len <*G*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg (len A) is finite len A -element Element of bool NAT
dom A is finite Element of bool NAT
dom (A ^ <*G*>) is non empty finite Element of bool NAT
(len A) + (len <*G*>) is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg ((len A) + (len <*G*>)) is non empty finite (len A) + (len <*G*>) -element Element of bool NAT
(Seg (len A)) \/ {((len A) + 1)} is non empty finite Element of bool NAT
(A ^ <*G*>) . B is set
a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(A ^ <*G*>) . a is set
A . a is set
B is set
len <*G*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
dom (A ^ <*G*>) is non empty finite Element of bool NAT
Seg ((len A) + 1) is non empty finite (len A) + 1 -element Element of bool NAT
dom A is finite Element of bool NAT
A . B is set
Seg (len A) is finite len A -element Element of bool NAT
(Seg (len A)) \/ {((len A) + 1)} is non empty finite Element of bool NAT
(A ^ <*G*>) . ((len A) + 1) is set
a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(A ^ <*G*>) . a is set
A . a is set
G is set
{G} is non empty trivial finite 1 -element set
M is set
<*M*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
A is non empty set
B is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
B ^ <*M*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
{G} |` (B ^ <*M*>) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom ({G} |` (B ^ <*M*>)) is finite Element of bool NAT
{G} |` B is Relation-like NAT -defined {G} -valued A -valued Function-like finite FinSubsequence-like Element of bool [:NAT,A:]
[:NAT,A:] is Relation-like non empty non trivial non finite set
bool [:NAT,A:] is non empty non trivial non finite set
dom ({G} |` B) is finite Element of bool NAT
a is set
len <*M*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
len B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg (len B) is finite len B -element Element of bool NAT
dom B is finite Element of bool NAT
dom (B ^ <*M*>) is non empty finite Element of bool NAT
(len B) + (len <*M*>) is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg ((len B) + (len <*M*>)) is non empty finite (len B) + (len <*M*>) -element Element of bool NAT
(len B) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{((len B) + 1)} is non empty trivial finite V46() 1 -element Element of bool NAT
(Seg (len B)) \/ {((len B) + 1)} is non empty finite Element of bool NAT
(B ^ <*M*>) . a is set
(B ^ <*M*>) . ((len B) + 1) is set
a1 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(B ^ <*M*>) . a1 is set
B . a1 is set
a is set
dom B is finite Element of bool NAT
len <*M*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
dom (B ^ <*M*>) is non empty finite Element of bool NAT
len B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(len B) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
Seg ((len B) + 1) is non empty finite (len B) + 1 -element Element of bool NAT
Seg (len B) is finite len B -element Element of bool NAT
{((len B) + 1)} is non empty trivial finite V46() 1 -element Element of bool NAT
(Seg (len B)) \/ {((len B) + 1)} is non empty finite Element of bool NAT
B . a is set
a1 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(B ^ <*M*>) . a1 is set
B . a1 is set
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
[:G,NAT:] is Relation-like non empty non trivial non finite set
bool [:G,NAT:] is non empty non trivial non finite set
A is Relation-like G -defined NAT -valued Function-like non empty total quasi_total Element of bool [:G,NAT:]
A is Relation-like Function-like Element of the carrier of (G)
B is Relation-like Function-like Element of the carrier of (G)
a is Element of G
(G,A,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{a} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
{a} |` M is Relation-like NAT -defined G -valued {a} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
[:NAT,G:] is Relation-like non empty non trivial non finite set
bool [:NAT,G:] is non empty non trivial non finite set
dom ({a} |` M) is finite Element of bool NAT
card (dom ({a} |` M)) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,B,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G 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 V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of G
[:NAT,G:] is Relation-like non empty non trivial non finite set
(G,(<*> G)) is Relation-like Function-like Element of the carrier of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Element of G
(G,(G,(<*> G)),M) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
{M} |` {} is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom ({M} |` {}) is finite Element of bool NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() Element of bool NAT
{M} |` (<*> G) is Relation-like NAT -defined G -valued {M} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
bool [:NAT,G:] is non empty non trivial non finite set
dom ({M} |` (<*> G)) is finite Element of bool NAT
G 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 V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of G
[:NAT,G:] is Relation-like non empty non trivial non finite set
(G,(<*> G)) is Relation-like Function-like Element of the carrier of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
(G,0) is Relation-like G -defined NAT -valued Function-like constant non empty total Function-yielding V41() Element of the carrier of (G)
M is set
(G,(<*> G)) . M is set
A is Element of G
{A} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
{A} |` {} is Relation-like NAT -defined Function-like finite FinSubsequence-like set
dom ({A} |` {}) is finite Element of bool NAT
card (dom ({A} |` {})) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
dom (G,(<*> G)) is set
G is non empty set
M is Element of G
<*M*> is Relation-like NAT -defined G -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of G
(G,<*M*>) is Relation-like Function-like Element of the carrier of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
(G,M) is Relation-like Function-like Element of the carrier of (G)
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
({M},G) is Relation-like Function-like Element of the carrier of (G)
rng <*M*> is non empty trivial finite 1 -element Element of bool G
A is Element of G
dom <*M*> is non empty trivial finite 1 -element Element of bool NAT
card (Seg 1) is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{A} is non empty trivial finite 1 -element Element of bool G
{A} /\ {M} is finite Element of bool G
(G,(G,M),M) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{M} |` <*M*> is Relation-like NAT -defined G -valued {M} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
[:NAT,G:] is Relation-like non empty non trivial non finite set
bool [:NAT,G:] is non empty non trivial non finite set
(rng <*M*>) |` <*M*> is Relation-like NAT -defined G -valued rng <*M*> -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
{A} |` <*M*> is Relation-like NAT -defined G -valued {A} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
{A} /\ (rng <*M*>) is finite Element of bool G
({A} /\ (rng <*M*>)) |` <*M*> is Relation-like NAT -defined G -valued {A} /\ (rng <*M*>) -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
(G,(G,M),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,(G,<*M*>),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
M is Element of G
<*M*> is Relation-like NAT -defined G -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of G
(G,M) is Relation-like Function-like Element of the carrier of (G)
the carrier of (G) is non empty set
{M} is non empty trivial finite 1 -element Element of bool G
bool G is non empty set
({M},G) is Relation-like Function-like Element of the carrier of (G)
A is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
A ^ <*M*> is Relation-like NAT -defined G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of G *
G * is functional non empty FinSequence-membered FinSequenceSet of G
(G,(A ^ <*M*>)) is Relation-like Function-like Element of the carrier of (G)
(G,A) is Relation-like Function-like Element of the carrier of (G)
(G,A) [*] (G,M) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . ((G,A),(G,M)) is Relation-like Function-like Element of the carrier of (G)
[(G,A),(G,M)] is set
{(G,A),(G,M)} is functional non empty finite set
{(G,A)} is functional non empty trivial finite 1 -element set
{{(G,A),(G,M)},{(G,A)}} is non empty finite V46() set
the multF of (G) . [(G,A),(G,M)] is set
len A is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(len A) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is Element of G
{a} is non empty trivial finite 1 -element Element of bool G
{a} |` A is Relation-like NAT -defined G -valued {a} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
[:NAT,G:] is Relation-like non empty non trivial non finite set
bool [:NAT,G:] is non empty non trivial non finite set
dom ({a} |` A) is finite Element of bool NAT
dom A is finite Element of bool NAT
(G,(G,(A ^ <*M*>)),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
{a} |` B is Relation-like NAT -defined G -valued {a} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
dom ({a} |` B) is finite Element of bool NAT
card (dom ({a} |` B)) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,(G,A),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
card (dom ({a} |` A)) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{a} |` (A ^ <*M*>) is Relation-like NAT -defined G -valued {a} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
dom ({a} |` (A ^ <*M*>)) is finite Element of bool NAT
(G,(G,M),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,((G,A) [*] (G,M)),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,(G,A),a) + (G,(G,M),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{M} |` (A ^ <*M*>) is Relation-like NAT -defined G -valued {M} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
dom ({M} |` (A ^ <*M*>)) is finite Element of bool NAT
{M} |` A is Relation-like NAT -defined G -valued {M} -valued G -valued Function-like finite FinSubsequence-like Element of bool [:NAT,G:]
dom ({M} |` A) is finite Element of bool NAT
{((len A) + 1)} is non empty trivial finite V46() 1 -element Element of bool NAT
(dom ({M} |` A)) \/ {((len A) + 1)} is non empty finite Element of bool NAT
(G,(G,M),M) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
M is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
(G,M) is Relation-like Function-like Element of the carrier of (G)
the carrier of (G) is non empty set
A is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
M ^ A is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
G * is functional non empty FinSequence-membered FinSequenceSet of G
(G,(M ^ A)) is Relation-like Function-like Element of the carrier of (G)
(G,A) is Relation-like Function-like Element of the carrier of (G)
(G,M) [*] (G,A) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . ((G,M),(G,A)) is Relation-like Function-like Element of the carrier of (G)
[(G,M),(G,A)] is set
{(G,M),(G,A)} is functional non empty finite set
{(G,M)} is functional non empty trivial finite 1 -element set
{{(G,M),(G,A)},{(G,M)}} is non empty finite V46() set
the multF of (G) . [(G,M),(G,A)] is set
len A is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M ^ a is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
(G,(M ^ a)) is Relation-like Function-like Element of the carrier of (G)
(G,a) is Relation-like Function-like Element of the carrier of (G)
(G,M) [*] (G,a) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,M),(G,a)) is Relation-like Function-like Element of the carrier of (G)
[(G,M),(G,a)] is set
{(G,M),(G,a)} is functional non empty finite set
{{(G,M),(G,a)},{(G,M)}} is non empty finite V46() set
the multF of (G) . [(G,M),(G,a)] is set
a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a2 is set
<*a2*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
a1 ^ <*a2*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng <*a2*> is non empty trivial finite 1 -element set
{a2} is non empty trivial finite 1 -element set
rng a is finite Element of bool G
bool G is non empty set
len <*a2*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a1 is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len a1 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(len a1) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M ^ a1 is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
a2 is Element of G
<*a2*> is Relation-like NAT -defined G -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of G
(M ^ a1) ^ <*a2*> is Relation-like NAT -defined G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of G *
(G,((M ^ a1) ^ <*a2*>)) is Relation-like Function-like Element of the carrier of (G)
(G,(M ^ a1)) is Relation-like Function-like Element of the carrier of (G)
(G,a2) is Relation-like Function-like Element of the carrier of (G)
{a2} is non empty trivial finite 1 -element Element of bool G
({a2},G) is Relation-like Function-like Element of the carrier of (G)
(G,(M ^ a1)) [*] (G,a2) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,(M ^ a1)),(G,a2)) is Relation-like Function-like Element of the carrier of (G)
[(G,(M ^ a1)),(G,a2)] is set
{(G,(M ^ a1)),(G,a2)} is functional non empty finite set
{(G,(M ^ a1))} is functional non empty trivial finite 1 -element set
{{(G,(M ^ a1)),(G,a2)},{(G,(M ^ a1))}} is non empty finite V46() set
the multF of (G) . [(G,(M ^ a1)),(G,a2)] is set
(G,a1) is Relation-like Function-like Element of the carrier of (G)
(G,M) [*] (G,a1) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,M),(G,a1)) is Relation-like Function-like Element of the carrier of (G)
[(G,M),(G,a1)] is set
{(G,M),(G,a1)} is functional non empty finite set
{{(G,M),(G,a1)},{(G,M)}} is non empty finite V46() set
the multF of (G) . [(G,M),(G,a1)] is set
((G,M) [*] (G,a1)) [*] (G,a2) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . (((G,M) [*] (G,a1)),(G,a2)) is Relation-like Function-like Element of the carrier of (G)
[((G,M) [*] (G,a1)),(G,a2)] is set
{((G,M) [*] (G,a1)),(G,a2)} is functional non empty finite set
{((G,M) [*] (G,a1))} is functional non empty trivial finite 1 -element set
{{((G,M) [*] (G,a1)),(G,a2)},{((G,M) [*] (G,a1))}} is non empty finite V46() set
the multF of (G) . [((G,M) [*] (G,a1)),(G,a2)] is set
(G,a1) [*] (G,a2) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,a1),(G,a2)) is Relation-like Function-like Element of the carrier of (G)
[(G,a1),(G,a2)] is set
{(G,a1),(G,a2)} is functional non empty finite set
{(G,a1)} is functional non empty trivial finite 1 -element set
{{(G,a1),(G,a2)},{(G,a1)}} is non empty finite V46() set
the multF of (G) . [(G,a1),(G,a2)] is set
(G,M) [*] ((G,a1) [*] (G,a2)) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,M),((G,a1) [*] (G,a2))) is Relation-like Function-like Element of the carrier of (G)
[(G,M),((G,a1) [*] (G,a2))] is set
{(G,M),((G,a1) [*] (G,a2))} is functional non empty finite set
{{(G,M),((G,a1) [*] (G,a2))},{(G,M)}} is non empty finite V46() set
the multF of (G) . [(G,M),((G,a1) [*] (G,a2))] is set
B is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M ^ B is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
(G,(M ^ B)) is Relation-like Function-like Element of the carrier of (G)
(G,B) is Relation-like Function-like Element of the carrier of (G)
(G,M) [*] (G,B) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) . ((G,M),(G,B)) is Relation-like Function-like Element of the carrier of (G)
[(G,M),(G,B)] is set
{(G,M),(G,B)} is functional non empty finite set
{{(G,M),(G,B)},{(G,M)}} is non empty finite V46() set
the multF of (G) . [(G,M),(G,B)] is set
<*> G is Relation-like non-empty empty-yielding NAT -defined G -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of G
[:NAT,G:] is Relation-like non empty non trivial non finite set
(G,(<*> G)) is Relation-like Function-like Element of the carrier of (G)
(G,0) is Relation-like G -defined NAT -valued Function-like constant non empty total Function-yielding V41() Element of the carrier of (G)
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)
G is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
M is non empty set
A is Element of M
(M,G,A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,G,A)) is Relation-like Function-like Element of the carrier of (M)
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (M) is non empty set
(M,(M,(M,G,A)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,0,A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
<*> M is Relation-like non-empty empty-yielding NAT -defined M -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of M
[:NAT,M:] is Relation-like non empty non trivial non finite set
B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,B,A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,B,A)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,(M,B,A)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(B + 1),A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,(B + 1),A)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,(M,(B + 1),A)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
<*A*> is Relation-like NAT -defined M -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of M
(M,B,A) ^ <*A*> is Relation-like NAT -defined M -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of M *
M * is functional non empty FinSequence-membered FinSequenceSet of M
(M,((M,B,A) ^ <*A*>)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,((M,B,A) ^ <*A*>)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,A) is Relation-like Function-like Element of the carrier of (M)
{A} is non empty trivial finite 1 -element Element of bool M
bool M is non empty set
({A},M) is Relation-like Function-like Element of the carrier of (M)
(M,(M,B,A)) [*] (M,A) is Relation-like Function-like Element of the carrier of (M)
the multF of (M) is Relation-like [: the carrier of (M), the carrier of (M):] -defined the carrier of (M) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):]
[: the carrier of (M), the carrier of (M):] is Relation-like non empty set
[:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is Relation-like non empty set
bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is non empty set
the multF of (M) . ((M,(M,B,A)),(M,A)) is Relation-like Function-like Element of the carrier of (M)
[(M,(M,B,A)),(M,A)] is set
{(M,(M,B,A)),(M,A)} is functional non empty finite set
{(M,(M,B,A))} is functional non empty trivial finite 1 -element set
{{(M,(M,B,A)),(M,A)},{(M,(M,B,A))}} is non empty finite V46() set
the multF of (M) . [(M,(M,B,A)),(M,A)] is set
(M,((M,(M,B,A)) [*] (M,A)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,A),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B + (M,(M,A),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,0) is Relation-like M -defined NAT -valued Function-like constant non empty total Function-yielding V41() Element of the carrier of (M)
(M,(M,0),A) is Relation-like Function-like V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,0,A)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,(M,0,A)),A) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B is Element of M
(M,(M,(M,G,A)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,a,A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,a,A)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,(M,a,A)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(a + 1),A) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,(a + 1),A)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,(M,(a + 1),A)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
<*A*> is Relation-like NAT -defined M -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of M
(M,a,A) ^ <*A*> is Relation-like NAT -defined M -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of M *
M * is functional non empty FinSequence-membered FinSequenceSet of M
(M,((M,a,A) ^ <*A*>)) is Relation-like Function-like Element of the carrier of (M)
(M,(M,((M,a,A) ^ <*A*>)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,A) is Relation-like Function-like Element of the carrier of (M)
{A} is non empty trivial finite 1 -element Element of bool M
bool M is non empty set
({A},M) is Relation-like Function-like Element of the carrier of (M)
(M,(M,a,A)) [*] (M,A) is Relation-like Function-like Element of the carrier of (M)
the multF of (M) is Relation-like [: the carrier of (M), the carrier of (M):] -defined the carrier of (M) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):]
[: the carrier of (M), the carrier of (M):] is Relation-like non empty set
[:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is Relation-like non empty set
bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is non empty set
the multF of (M) . ((M,(M,a,A)),(M,A)) is Relation-like Function-like Element of the carrier of (M)
[(M,(M,a,A)),(M,A)] is set
{(M,(M,a,A)),(M,A)} is functional non empty finite set
{(M,(M,a,A))} is functional non empty trivial finite 1 -element set
{{(M,(M,a,A)),(M,A)},{(M,(M,a,A))}} is non empty finite V46() set
the multF of (M) . [(M,(M,a,A)),(M,A)] is set
(M,((M,(M,a,A)) [*] (M,A)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,A),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
0 + (M,(M,A),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,0),B) is Relation-like Function-like V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,(M,0,A)),B) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
G is non empty set
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (G)
(G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,G) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (G) is non empty set
M is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
(G,M) is Relation-like Function-like Element of the carrier of (G)
the carrier of (G) is non empty set
len M is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
B + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,a) is Relation-like Function-like Element of the carrier of (G)
a1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a2 is set
<*a2*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
a1 ^ <*a2*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng <*a2*> is non empty trivial finite 1 -element set
{a2} is non empty trivial finite 1 -element set
rng a is finite Element of bool G
bool G is non empty set
len <*a2*> is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a1 is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len a1 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(len a1) + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,a1) is Relation-like Function-like Element of the carrier of (G)
a2 is Element of G
(G,a2) is Relation-like Function-like Element of the carrier of (G)
{a2} is non empty trivial finite 1 -element Element of bool G
({a2},G) is Relation-like Function-like Element of the carrier of (G)
x is Relation-like Function-like Element of the carrier of (G)
c is Relation-like Function-like Element of the carrier of (G)
x [*] c is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . (x,c) is Relation-like Function-like Element of the carrier of (G)
[x,c] is set
{x,c} is functional non empty finite set
{x} is functional non empty trivial finite 1 -element set
{{x,c},{x}} is non empty finite V46() set
the multF of (G) . [x,c] is set
(G,a1) [*] (G,a2) is Relation-like Function-like Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like 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) . ((G,a1),(G,a2)) is Relation-like Function-like Element of the carrier of (G)
[(G,a1),(G,a2)] is set
{(G,a1),(G,a2)} is functional non empty finite set
{(G,a1)} is functional non empty trivial finite 1 -element set
{{(G,a1),(G,a2)},{(G,a1)}} is non empty finite V46() set
the multF of (G) . [(G,a1),(G,a2)] is set
A is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
len A is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(G,A) is Relation-like Function-like Element of the carrier of (G)
<*> G is Relation-like non-empty empty-yielding NAT -defined G -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of G
[:NAT,G:] is Relation-like non empty non trivial non finite set
(G,0) is Relation-like G -defined NAT -valued Function-like constant non empty total Function-yielding V41() Element of the carrier of (G)
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)
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)
G is set
M is non empty set
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of (M)
(M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
(<NAT,+,0>,M) is non empty strict associative commutative well-unital constituted-Functions left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr
the carrier of (M) is non empty set
the carrier of (M) is non empty set
A is Relation-like Function-like Element of the carrier of (M)
A " (NAT \ {0}) is set
B is finite set
card B is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is finite set
card a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a + 1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a1 is Relation-like Function-like Element of the carrier of (M)
a1 " (NAT \ {0}) is set
the Element of a1 " (NAT \ {0}) is Element of a1 " (NAT \ {0})
a1 is Relation-like Function-like Element of the carrier of (M)
a1 " (NAT \ {0}) is set
a2 is finite set
card a2 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
dom a1 is set
x is Element of M
c is Relation-like Function-like set
dom c is set
rng c is set
y2 is set
y1 is set
c . y1 is set
f9 is Element of M
(M,a1,f9) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
[:M,NAT:] is Relation-like non empty non trivial non finite set
bool [:M,NAT:] is non empty non trivial non finite set
y2 is Relation-like M -defined NAT -valued Function-like non empty total quasi_total Element of bool [:M,NAT:]
y1 is Relation-like Function-like Element of the carrier of (M)
y1 " (NAT \ {0}) is set
{x} is non empty trivial finite 1 -element Element of bool M
bool M is non empty set
(a1 " (NAT \ {0})) \ {x} is Element of bool (a1 " (NAT \ {0}))
bool (a1 " (NAT \ {0})) is non empty set
f9 is set
y1 . f9 is set
g is Element of M
(M,y1,g) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
a1 . g is set
f9 is set
dom a1 is set
a1 . f9 is set
y1 . f9 is set
(M,a1,x) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,a1,x),x) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,(M,(M,a1,x),x)) is Relation-like Function-like Element of the carrier of (M)
card {x} is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
f9 is Relation-like Function-like Element of the carrier of (M)
f9 " (NAT \ {0}) is set
V9 is finite set
card V9 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(a + 1) - 1 is V36() V37() V145() Element of REAL
p is finite set
card p is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
p is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of M
(M,p) is Relation-like Function-like Element of the carrier of (M)
M * is functional non empty FinSequence-membered FinSequenceSet of M
p ^ (M,(M,a1,x),x) is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like Element of M *
q is Relation-like NAT -defined M -valued Function-like finite FinSequence-like FinSubsequence-like Element of M *
(M,q) is Relation-like Function-like Element of the carrier of (M)
a is Element of M
(M,a1,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
0 + (M,a1,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,y1,a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,(M,(M,a1,x),x)),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,y1,x) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
(M,(M,(M,(M,a1,x),x)),x) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
y1 [*] (M,(M,(M,a1,x),x)) is Relation-like Function-like Element of the carrier of (M)
the multF of (M) is Relation-like [: the carrier of (M), the carrier of (M):] -defined the carrier of (M) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):]
[: the carrier of (M), the carrier of (M):] is Relation-like non empty set
[:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is Relation-like non empty set
bool [:[: the carrier of (M), the carrier of (M):], the carrier of (M):] is non empty set
the multF of (M) . (y1,(M,(M,(M,a1,x),x))) is Relation-like Function-like Element of the carrier of (M)
[y1,(M,(M,(M,a1,x),x))] is set
{y1,(M,(M,(M,a1,x),x))} is functional non empty finite set
{y1} is functional non empty trivial finite 1 -element set
{{y1,(M,(M,(M,a1,x),x))},{y1}} is non empty finite V46() set
the multF of (M) . [y1,(M,(M,(M,a1,x),x))] is set
(M,(y1 [*] (M,(M,(M,a1,x),x))),a) is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
the Element of M is Element of M
a1 is Relation-like Function-like Element of the carrier of (M)
a1 " (NAT \ {0}) is set
a2 is Relation-like Function-like Element of the carrier of (M)
a2 " (NAT \ {0}) is set
a1 is finite set
card a1 is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
rng a1 is set
(rng a1) /\ (NAT \ {0}) is Element of bool REAL
(rng a1) /\ NAT is Element of bool REAL
((rng a1) /\ NAT) \ {0} is Element of bool REAL
[:NAT,M:] is Relation-like non empty non trivial non finite set
<*> M is Relation-like non-empty empty-yielding NAT -defined M -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of M
a2 is Relation-like non-empty empty-yielding NAT -defined M -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() FinSequence of M
(M,a2) is Relation-like Function-like Element of the carrier of (M)
(M,a2) is Element of bool NAT
dom a2 is set
a1 . the Element of M is set
(M,0) is Relation-like M -defined NAT -valued Function-like constant non empty total Function-yielding V41() Element of the carrier of (M)
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
bool G is non empty set
bool M is non empty set
[:(bool G),(bool M):] is Relation-like non empty set
bool A is non empty set
[:[:(bool G),(bool M):],(bool A):] is Relation-like non empty set
bool [:[:(bool G),(bool M):],(bool A):] is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
a is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
a is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
a1 is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
a2 is Element of [:(bool G),(bool M):]
a . a2 is Element of bool A
a2 `1 is Element of bool G
a2 `2 is Element of bool M
[:(a2 `1),(a2 `2):] is Relation-like set
B .: [:(a2 `1),(a2 `2):] is Element of bool A
a1 . a2 is Element of bool A
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
bool G is non empty set
bool M is non empty set
bool A is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
(G,M,A,B) is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
[:(bool G),(bool M):] is Relation-like non empty set
[:[:(bool G),(bool M):],(bool A):] is Relation-like non empty set
bool [:[:(bool G),(bool M):],(bool A):] is non empty set
a is Element of bool G
a1 is Element of bool M
(G,M,A,B) . (a,a1) is Element of bool A
[a,a1] is set
{a,a1} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,a1},{a}} is non empty finite V46() set
(G,M,A,B) . [a,a1] is set
[:a,a1:] is Relation-like set
B .: [:a,a1:] is Element of bool A
[a,a1] is Element of [:(bool G),(bool M):]
[a,a1] `1 is Element of bool G
[a,a1] `2 is Element of bool M
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
bool G is non empty set
bool M is non empty set
bool A is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
(G,M,A,B) is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
[:(bool G),(bool M):] is Relation-like non empty set
[:[:(bool G),(bool M):],(bool A):] is Relation-like non empty set
bool [:[:(bool G),(bool M):],(bool A):] is non empty set
a is Element of bool G
a1 is Element of bool M
(G,M,A,B) . (a,a1) is Element of bool A
[a,a1] is set
{a,a1} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,a1},{a}} is non empty finite V46() set
(G,M,A,B) . [a,a1] is set
a2 is set
a1 is set
B . (a2,a1) is set
[a2,a1] is set
{a2,a1} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,a1},{a2}} is non empty finite V46() set
B . [a2,a1] is set
[:a,a1:] is Relation-like set
B .: [:a,a1:] is Element of bool A
dom B is Relation-like G -defined M -valued non empty Element of bool [:G,M:]
bool [:G,M:] is non empty set
x is Element of G
a2 is Element of M
[x,a2] is Element of [:G,M:]
{x,a2} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,a2},{x}} is non empty finite V46() set
G is non empty set
M is non empty set
[:G,M:] is Relation-like non empty set
A is non empty set
[:[:G,M:],A:] is Relation-like non empty set
bool [:[:G,M:],A:] is non empty set
bool G is non empty set
bool M is non empty set
bool A is non empty set
B is Relation-like [:G,M:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:G,M:],A:]
(G,M,A,B) is Relation-like [:(bool G),(bool M):] -defined bool A -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool M):],(bool A):]
[:(bool G),(bool M):] is Relation-like non empty set
[:[:(bool G),(bool M):],(bool A):] is Relation-like non empty set
bool [:[:(bool G),(bool M):],(bool A):] is non empty set
a is Element of bool G
a1 is Element of bool M
(G,M,A,B) . (a,a1) is Element of bool A
[a,a1] is set
{a,a1} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,a1},{a}} is non empty finite V46() set
(G,M,A,B) . [a,a1] is set
{ (B . (b₁,b₂)) where b₁ is Element of G, b₂ is Element of M : ( b₁ in a & b₂ in a1 ) } is set
[:a,a1:] is Relation-like set
B .: [:a,a1:] is Element of bool A
a1 is set
dom B is Relation-like G -defined M -valued non empty Element of bool [:G,M:]
bool [:G,M:] is non empty set
a2 is set
B . a2 is set
x is set
c is set
[x,c] is set
{x,c} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,c},{x}} is non empty finite V46() set
y1 is Element of G
y2 is Element of M
B . (y1,y2) is Element of A
[y1,y2] is set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite 1 -element set
{{y1,y2},{y1}} is non empty finite V46() set
B . [y1,y2] is set
a1 is set
a2 is Element of G
x is Element of M
B . (a2,x) is Element of A
[a2,x] is set
{a2,x} is non empty finite set
{a2} is non empty trivial finite 1 -element set
{{a2,x},{a2}} is non empty finite V46() set
B . [a2,x] is set
G is set
M is set
[:G,M:] is Relation-like set
[:M,G:] is Relation-like set
A is non empty set
[:A,A:] is Relation-like non empty set
[:[:A,A:],A:] is Relation-like non empty set
bool [:[:A,A:],A:] is non empty set
B is Relation-like [:A,A:] -defined A -valued Function-like non empty total quasi_total Element of bool [:[:A,A:],A:]
B .: [:G,M:] is Element of bool A
bool A is non empty set
B .: [:M,G:] is Element of bool A
a is set
a1 is set
[:a,a1:] is Relation-like set
B .: [:a,a1:] is Element of bool A
[:a1,a:] is Relation-like set
B .: [:a1,a:] is Element of bool A
a2 is set
dom B is Relation-like A -defined A -valued non empty Element of bool [:A,A:]
bool [:A,A:] is non empty set
a1 is set
B . a1 is set
a2 is Element of [:A,A:]
a2 `1 is Element of A
a2 `2 is Element of A
[(a2 `1),(a2 `2)] is Element of [:A,A:]
{(a2 `1),(a2 `2)} is non empty finite set
{(a2 `1)} is non empty trivial finite 1 -element set
{{(a2 `1),(a2 `2)},{(a2 `1)}} is non empty finite V46() set
[(a2 `2),(a2 `1)] is Element of [:A,A:]
{(a2 `2),(a2 `1)} is non empty finite set
{(a2 `2)} is non empty trivial finite 1 -element set
{{(a2 `2),(a2 `1)},{(a2 `2)}} is non empty finite V46() set
B . ((a2 `1),(a2 `2)) is Element of A
[(a2 `1),(a2 `2)] is set
B . [(a2 `1),(a2 `2)] is set
B . ((a2 `2),(a2 `1)) is Element of A
[(a2 `2),(a2 `1)] is set
B . [(a2 `2),(a2 `1)] is set
G is set
M is set
[:G,M:] is Relation-like set
A is set
[:M,A:] is Relation-like set
B is non empty set
[:B,B:] is Relation-like non empty set
[:[:B,B:],B:] is Relation-like non empty set
bool [:[:B,B:],B:] is non empty set
a is Relation-like [:B,B:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:B,B:],B:]
a .: [:G,M:] is Element of bool B
bool B is non empty set
[:(a .: [:G,M:]),A:] is Relation-like set
a .: [:(a .: [:G,M:]),A:] is Element of bool B
a .: [:M,A:] is Element of bool B
[:G,(a .: [:M,A:]):] is Relation-like set
a .: [:G,(a .: [:M,A:]):] is Element of bool B
dom a is Relation-like B -defined B -valued non empty Element of bool [:B,B:]
bool [:B,B:] is non empty set
a1 is set
a2 is set
a . a2 is set
a1 is Element of [:B,B:]
a1 `1 is Element of B
a1 `2 is Element of B
[(a1 `1),(a1 `2)] is Element of [:B,B:]
{(a1 `1),(a1 `2)} is non empty finite set
{(a1 `1)} is non empty trivial finite 1 -element set
{{(a1 `1),(a1 `2)},{(a1 `1)}} is non empty finite V46() set
a2 is set
a . a2 is set
x is Element of [:B,B:]
x `1 is Element of B
x `2 is Element of B
a . ((x `1),(x `2)) is Element of B
[(x `1),(x `2)] is set
{(x `1),(x `2)} is non empty finite set
{(x `1)} is non empty trivial finite 1 -element set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V46() set
a . [(x `1),(x `2)] is set
[(x `1),(x `2)] is Element of [:B,B:]
[(x `2),(a1 `2)] is Element of [:B,B:]
{(x `2),(a1 `2)} is non empty finite set
{(x `2)} is non empty trivial finite 1 -element set
{{(x `2),(a1 `2)},{(x `2)}} is non empty finite V46() set
a . ((x `2),(a1 `2)) is Element of B
[(x `2),(a1 `2)] is set
a . [(x `2),(a1 `2)] is set
[(x `1),(a . ((x `2),(a1 `2)))] is Element of [:B,B:]
{(x `1),(a . ((x `2),(a1 `2)))} is non empty finite set
{{(x `1),(a . ((x `2),(a1 `2)))},{(x `1)}} is non empty finite V46() set
a . ((a1 `1),(a1 `2)) is Element of B
[(a1 `1),(a1 `2)] is set
a . [(a1 `1),(a1 `2)] is set
a . ((x `1),(a . ((x `2),(a1 `2)))) is Element of B
[(x `1),(a . ((x `2),(a1 `2)))] is set
a . [(x `1),(a . ((x `2),(a1 `2)))] is set
a1 is set
a2 is set
a . a2 is set
a1 is Element of [:B,B:]
a1 `1 is Element of B
a1 `2 is Element of B
[(a1 `1),(a1 `2)] is Element of [:B,B:]
{(a1 `1),(a1 `2)} is non empty finite set
{(a1 `1)} is non empty trivial finite 1 -element set
{{(a1 `1),(a1 `2)},{(a1 `1)}} is non empty finite V46() set
a2 is set
a . a2 is set
x is Element of [:B,B:]
x `1 is Element of B
x `2 is Element of B
a . ((x `1),(x `2)) is Element of B
[(x `1),(x `2)] is set
{(x `1),(x `2)} is non empty finite set
{(x `1)} is non empty trivial finite 1 -element set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V46() set
a . [(x `1),(x `2)] is set
[(x `1),(x `2)] is Element of [:B,B:]
[(a1 `1),(x `1)] is Element of [:B,B:]
{(a1 `1),(x `1)} is non empty finite set
{{(a1 `1),(x `1)},{(a1 `1)}} is non empty finite V46() set
a . ((a1 `1),(x `1)) is Element of B
[(a1 `1),(x `1)] is set
a . [(a1 `1),(x `1)] is set
[(a . ((a1 `1),(x `1))),(x `2)] is Element of [:B,B:]
{(a . ((a1 `1),(x `1))),(x `2)} is non empty finite set
{(a . ((a1 `1),(x `1)))} is non empty trivial finite 1 -element set
{{(a . ((a1 `1),(x `1))),(x `2)},{(a . ((a1 `1),(x `1)))}} is non empty finite V46() set
a . ((a1 `1),(a1 `2)) is Element of B
[(a1 `1),(a1 `2)] is set
a . [(a1 `1),(a1 `2)] is set
a . ((a . ((a1 `1),(x `1))),(x `2)) is Element of B
[(a . ((a1 `1),(x `1))),(x `2)] is set
a . [(a . ((a1 `1),(x `1))),(x `2)] 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
bool G is non empty set
M is Relation-like [:G,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]
(G,G,G,M) is Relation-like [:(bool G),(bool G):] -defined bool G -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool G):],(bool G):]
[:(bool G),(bool G):] is Relation-like non empty set
[:[:(bool G),(bool G):],(bool G):] is Relation-like non empty set
bool [:[:(bool G),(bool G):],(bool G):] is non empty set
A is Element of bool G
B is Element of bool G
(G,G,G,M) . (A,B) is Element of bool G
[A,B] is set
{A,B} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,B},{A}} is non empty finite V46() set
(G,G,G,M) . [A,B] is set
(G,G,G,M) . (B,A) is Element of bool G
[B,A] is set
{B,A} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,A},{B}} is non empty finite V46() set
(G,G,G,M) . [B,A] is set
(G,G,G,M) . (A,B) is Element of bool G
[:A,B:] is Relation-like set
M .: [:A,B:] is Element of bool G
[:B,A:] is Relation-like set
M .: [:B,A:] is Element of bool G
(G,G,G,M) . (B,A) is Element of bool 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
bool G is non empty set
M is Relation-like [:G,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]
(G,G,G,M) is Relation-like [:(bool G),(bool G):] -defined bool G -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool G):],(bool G):]
[:(bool G),(bool G):] is Relation-like non empty set
[:[:(bool G),(bool G):],(bool G):] is Relation-like non empty set
bool [:[:(bool G),(bool G):],(bool G):] is non empty set
A is Element of bool G
B is Element of bool G
a is Element of bool G
(G,G,G,M) . (B,a) is Element of bool G
[B,a] is set
{B,a} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,a},{B}} is non empty finite V46() set
(G,G,G,M) . [B,a] is set
(G,G,G,M) . (A,((G,G,G,M) . (B,a))) is Element of bool G
[A,((G,G,G,M) . (B,a))] is set
{A,((G,G,G,M) . (B,a))} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,((G,G,G,M) . (B,a))},{A}} is non empty finite V46() set
(G,G,G,M) . [A,((G,G,G,M) . (B,a))] is set
(G,G,G,M) . (A,B) is Element of bool G
[A,B] is set
{A,B} is non empty finite set
{{A,B},{A}} is non empty finite V46() set
(G,G,G,M) . [A,B] is set
(G,G,G,M) . (((G,G,G,M) . (A,B)),a) is Element of bool G
[((G,G,G,M) . (A,B)),a] is set
{((G,G,G,M) . (A,B)),a} is non empty finite set
{((G,G,G,M) . (A,B))} is non empty trivial finite 1 -element set
{{((G,G,G,M) . (A,B)),a},{((G,G,G,M) . (A,B))}} is non empty finite V46() set
(G,G,G,M) . [((G,G,G,M) . (A,B)),a] is set
(G,G,G,M) . (A,B) is Element of bool G
(G,G,G,M) . (((G,G,G,M) . (A,B)),a) is Element of bool G
[((G,G,G,M) . (A,B)),a] is set
{((G,G,G,M) . (A,B)),a} is non empty finite set
{((G,G,G,M) . (A,B))} is non empty trivial finite 1 -element set
{{((G,G,G,M) . (A,B)),a},{((G,G,G,M) . (A,B))}} is non empty finite V46() set
(G,G,G,M) . [((G,G,G,M) . (A,B)),a] is set
[:A,B:] is Relation-like set
M .: [:A,B:] is Element of bool G
(G,G,G,M) . ((M .: [:A,B:]),a) is Element of bool G
[(M .: [:A,B:]),a] is set
{(M .: [:A,B:]),a} is non empty finite set
{(M .: [:A,B:])} is non empty trivial finite 1 -element set
{{(M .: [:A,B:]),a},{(M .: [:A,B:])}} is non empty finite V46() set
(G,G,G,M) . [(M .: [:A,B:]),a] is set
[:(M .: [:A,B:]),a:] is Relation-like set
M .: [:(M .: [:A,B:]),a:] is Element of bool G
[:B,a:] is Relation-like set
M .: [:B,a:] is Element of bool G
[:A,(M .: [:B,a:]):] is Relation-like set
M .: [:A,(M .: [:B,a:]):] is Element of bool G
(G,G,G,M) . (A,(M .: [:B,a:])) is Element of bool G
[A,(M .: [:B,a:])] is set
{A,(M .: [:B,a:])} is non empty finite set
{{A,(M .: [:B,a:])},{A}} is non empty finite V46() set
(G,G,G,M) . [A,(M .: [:B,a:])] is set
(G,G,G,M) . (B,a) is Element of bool G
(G,G,G,M) . (A,((G,G,G,M) . (B,a))) is Element of bool G
[A,((G,G,G,M) . (B,a))] is set
{A,((G,G,G,M) . (B,a))} is non empty finite set
{{A,((G,G,G,M) . (B,a))},{A}} is non empty finite V46() set
(G,G,G,M) . [A,((G,G,G,M) . (B,a))] is set
G is set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty set
M /\ G is set
A is Relation-like [:M,M:] -defined M -valued Function-like non empty total quasi_total Element of bool [:[:M,M:],M:]
B is Element of M
{B} is non empty trivial finite 1 -element Element of bool M
bool M is non empty set
[:{B},G:] is Relation-like set
A .: [:{B},G:] is Element of bool M
[:G,{B}:] is Relation-like set
A .: [:G,{B}:] is Element of bool M
a is set
dom A is Relation-like M -defined M -valued non empty Element of bool [:M,M:]
bool [:M,M:] is non empty set
a1 is set
A . a1 is set
a2 is Element of [:M,M:]
a2 `1 is Element of M
a2 `2 is Element of M
A . ((a2 `1),(a2 `2)) is Element of M
[(a2 `1),(a2 `2)] is set
{(a2 `1),(a2 `2)} is non empty finite set
{(a2 `1)} is non empty trivial finite 1 -element set
{{(a2 `1),(a2 `2)},{(a2 `1)}} is non empty finite V46() set
A . [(a2 `1),(a2 `2)] is set
[(a2 `1),(a2 `2)] is Element of [:M,M:]
A . (B,(a2 `2)) is Element of M
[B,(a2 `2)] is set
{B,(a2 `2)} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,(a2 `2)},{B}} is non empty finite V46() set
A . [B,(a2 `2)] is set
dom A is Relation-like M -defined M -valued non empty Element of bool [:M,M:]
bool [:M,M:] is non empty set
a is set
a1 is Element of M
A . (B,a1) is Element of M
[B,a1] is set
{B,a1} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,a1},{B}} is non empty finite V46() set
A . [B,a1] is set
[B,a] is set
{B,a} is non empty finite set
{{B,a},{B}} is non empty finite V46() set
A . [B,a] is set
[B,a1] is Element of [:M,M:]
a is set
a1 is set
A . a1 is set
a2 is Element of [:M,M:]
a2 `1 is Element of M
a2 `2 is Element of M
A . ((a2 `1),(a2 `2)) is Element of M
[(a2 `1),(a2 `2)] is set
{(a2 `1),(a2 `2)} is non empty finite set
{(a2 `1)} is non empty trivial finite 1 -element set
{{(a2 `1),(a2 `2)},{(a2 `1)}} is non empty finite V46() set
A . [(a2 `1),(a2 `2)] is set
[(a2 `1),(a2 `2)] is Element of [:M,M:]
A . ((a2 `1),B) is Element of M
[(a2 `1),B] is set
{(a2 `1),B} is non empty finite set
{{(a2 `1),B},{(a2 `1)}} is non empty finite V46() set
A . [(a2 `1),B] is set
a is set
a1 is Element of M
A . (a1,B) is Element of M
[a1,B] is set
{a1,B} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,B},{a1}} is non empty finite V46() set
A . [a1,B] is set
[a,B] is set
{a,B} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,B},{a}} is non empty finite V46() set
A . [a,B] is set
[a1,B] is Element of [:M,M:]
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
bool G is non empty set
M is Relation-like [:G,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]
(G,G,G,M) is Relation-like [:(bool G),(bool G):] -defined bool G -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool G):],(bool G):]
[:(bool G),(bool G):] is Relation-like non empty set
[:[:(bool G),(bool G):],(bool G):] is Relation-like non empty set
bool [:[:(bool G),(bool G):],(bool G):] is non empty set
the_unity_wrt (G,G,G,M) is Element of bool G
A is Element of G
{A} is non empty trivial finite 1 -element Element of bool G
B is Element of bool G
(G,G,G,M) . ({A},B) is Element of bool G
[{A},B] is set
{{A},B} is non empty finite set
{{A}} is non empty trivial finite V46() 1 -element set
{{{A},B},{{A}}} is non empty finite V46() set
(G,G,G,M) . [{A},B] is set
[:{A},B:] is Relation-like set
M .: [:{A},B:] is Element of bool G
G /\ B is Element of bool G
(G,G,G,M) . (B,{A}) is Element of bool G
[B,{A}] is set
{B,{A}} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,{A}},{B}} is non empty finite V46() set
(G,G,G,M) . [B,{A}] is set
[:B,{A}:] is Relation-like set
M .: [:B,{A}:] is Element of bool 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
bool G is non empty set
M is Relation-like [:G,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]
(G,G,G,M) is Relation-like [:(bool G),(bool G):] -defined bool G -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool G):],(bool G):]
[:(bool G),(bool G):] is Relation-like non empty set
[:[:(bool G),(bool G):],(bool G):] is Relation-like non empty set
bool [:[:(bool G),(bool G):],(bool G):] is non empty set
the_unity_wrt M is Element of G
{(the_unity_wrt M)} is non empty trivial finite 1 -element Element of bool G
the_unity_wrt (G,G,G,M) is Element of bool G
A is Element 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
bool G is non empty set
M is Relation-like [:G,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:G,G:],G:]
(G,G,G,M) is Relation-like [:(bool G),(bool G):] -defined bool G -valued Function-like non empty total quasi_total Element of bool [:[:(bool G),(bool G):],(bool G):]
[:(bool G),(bool G):] is Relation-like non empty set
[:[:(bool G),(bool G):],(bool G):] is Relation-like non empty set
bool [:[:(bool G),(bool G):],(bool G):] is non empty set
the_unity_wrt M is Element of G
the_unity_wrt (G,G,G,M) is Element of bool G
A is Element of bool G
B is Element of bool G
(G,G,G,M) . (A,B) is Element of bool G
[A,B] is set
{A,B} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,B},{A}} is non empty finite V46() set
(G,G,G,M) . [A,B] is set
{(the_unity_wrt M)} is non empty trivial finite 1 -element Element of bool G
the Element of A is Element of A
the Element of B is Element of B
[:A,B:] is Relation-like set
M .: [:A,B:] is Element of bool G
dom M is Relation-like G -defined G -valued non empty Element of bool [:G,G:]
bool [:G,G:] is non empty set
(dom M) /\ [:A,B:] is Relation-like G -defined G -valued Element of bool [:G,G:]
a1 is Element of G
{a1} is non empty trivial finite 1 -element Element of bool G
a2 is Element of G
M . (a1,a2) is Element of G
[a1,a2] is set
{a1,a2} is non empty finite set
{a1} is non empty trivial finite 1 -element set
{{a1,a2},{a1}} is non empty finite V46() set
M . [a1,a2] is set
x is set
c is Element of G
M . (c,a2) is Element of G
[c,a2] is set
{c,a2} is non empty finite set
{c} is non empty trivial finite 1 -element set
{{c,a2},{c}} is non empty finite V46() set
M . [c,a2] is set
x is set
c is Element of G
M . (a1,c) is Element of G
[a1,c] is set
{a1,c} is non empty finite set
{{a1,c},{a1}} is non empty finite V46() set
M . [a1,c] is set
{a2} is non empty trivial finite 1 -element Element of bool G
G is non empty multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G, the multF of G) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool 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 the multF of G)} is non empty trivial finite 1 -element Element of bool the carrier of G
multLoopStr(# (bool the carrier of G),( the carrier of G, the carrier of G, the carrier of G, the multF of G),{(the_unity_wrt the multF of G)} #) is strict multLoopStr
multMagma(# (bool the carrier of G),( the carrier of G, the carrier of G, the carrier of G, the multF of G) #) is strict multMagma
G is non empty multMagma
(G) is multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G, the multF of G) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool 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 the multF of G)} is non empty trivial finite 1 -element Element of bool the carrier of G
multLoopStr(# (bool the carrier of G),( the carrier of G, the carrier of G, the carrier of G, the multF of G),{(the_unity_wrt the multF of G)} #) is strict multLoopStr
the carrier of (G) is set
the carrier of G is non empty set
bool the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G, the multF of G) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is non empty set
multMagma(# (bool the carrier of G),( the carrier of G, the carrier of G, the carrier of G, the multF of G) #) is strict multMagma
the carrier of (G) is set
G is non empty unital multMagma
(G) is non empty multMagma
the carrier of G is non empty set
bool H₃(G) is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G,H₁(G)) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
bool the carrier of G is non empty set
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is non empty set
the_unity_wrt H₁(G) is Element of the carrier of G
{(the_unity_wrt H₁(G))} is non empty trivial finite 1 -element Element of bool the carrier of G
multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is strict multLoopStr
1. multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is Element of the carrier of multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #)
the carrier of multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is set
the OneF of multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is Element of the carrier of multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #)
G is non empty multMagma
(G) is non empty multMagma
the carrier of (G) is non empty set
the carrier of G is non empty set
bool the carrier of G is non empty set
[: the carrier of (G), the carrier of (G):] is Relation-like non empty set
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued 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
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G, the multF of G) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is non empty set
bool H₃(G) is non empty set
( the carrier of G, the carrier of G, the carrier of G,H₁(G)) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
the_unity_wrt H₁(G) is Element of the carrier of G
{(the_unity_wrt H₁(G))} is non empty trivial finite 1 -element Element of bool the carrier of G
multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is strict multLoopStr
multMagma(# (bool the carrier of G),( the carrier of G, the carrier of G, the carrier of G,H₁(G)) #) is strict multMagma
G is non empty unital multMagma
(G) is non empty strict 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)
the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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 the multF of G)} is non empty trivial finite 1 -element Element of bool the carrier of G
bool the carrier of G is non empty set
bool H₃(G) is non empty set
( the carrier of G, the carrier of G, the carrier of G,H₁(G)) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is non empty set
the_unity_wrt H₁(G) is Element of the carrier of G
{(the_unity_wrt H₁(G))} is non empty trivial finite 1 -element Element of bool the carrier of G
multLoopStr(# (bool H₃(G)),( the carrier of G, the carrier of G, the carrier of G,H₁(G)),{(the_unity_wrt H₁(G))} #) is strict multLoopStr
G is non empty 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 carrier of G is non empty set
bool the carrier of G is non empty set
[:(bool the carrier of G),(bool the carrier of G):] is Relation-like non empty set
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued 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
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued 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, the carrier of G, the carrier of G,H₁(G)) is Relation-like [:(bool the carrier of G),(bool the carrier of G):] -defined bool the carrier of G -valued Function-like non empty total quasi_total Element of bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):]
[:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is Relation-like non empty set
bool [:[:(bool the carrier of G),(bool the carrier of G):],(bool the carrier of G):] is non empty set
bool H₃(G) is non empty set