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
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()
G is Relation-like Function-like set
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
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