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

1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT
{{},1} is non empty finite V46() set

RAT is set
INT is set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is Relation-like non empty non trivial non finite set
is Relation-like non empty non trivial non finite set
bool 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

multMagma(# REAL,K215() #) is strict multMagma

multMagma(# REAL,K217() #) is strict multMagma

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

the carrier of <NAT,+,0> is non empty set

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

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) . ([M,A],B) is set
[[M,A],B] is set
{[M,A],B} is non empty finite 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) . ([a1,a2],a1) is set
[[a1,a2],a1] is set
{[a1,a2],a1} is non empty finite 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

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 .: (a1,a2) is Relation-like Function-like set
Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B

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

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

G is non empty set
M is set
A is Element of G

Funcs (M,G) is functional non empty FUNCTION_DOMAIN of 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

a1 is Element of M

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

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

A is set

M * (G | A) 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
F1() is set
F2() is non empty set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
G is set
M is Element of F2()

dom G is set
rng G is set
M is Relation-like F1() -defined F2() -valued Function-like total quasi_total Element of bool [:F1(),F2():]
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

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

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,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 . (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,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

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

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

(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,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,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],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

(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

(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,(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

(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

(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

(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

(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) . (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,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

(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

(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,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,((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,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

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,(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

(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

B is Element of 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

(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

(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,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

(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

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

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

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

(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) . (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,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

(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

(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,a},{B}} is non empty finite V46() set
(M,M,M,A,G) . [B,a] is Relation-like Function-like set

(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,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,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

(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,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,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,()) . 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,()) . a1 is set
dom a is Element of bool G
dom B is Element of bool G
dom (M,G,()) 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

(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

(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)):]

(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,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

(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