:: MONOID_1 semantic presentation

REAL is set

NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set

1 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT

{{},1} is non empty finite V46() set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is Relation-like non empty non trivial non finite set

[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

[:1,1:] is Relation-like non empty finite set

bool [:1,1:] is non empty finite V46() set

[:[:1,1:],1:] is Relation-like non empty finite set

bool [:[:1,1:],1:] is non empty finite V46() set

NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

K452() is non empty strict multMagma

the carrier of K452() is non empty set

<REAL,+> is non empty strict unital V127() associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable cancelable multMagma

K215() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total Element of bool [:[:REAL,REAL:],REAL:]

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

K458() is non empty strict associative commutative left-cancelable right-cancelable cancelable SubStr of <REAL,+>

<NAT,+> is non empty strict unital associative commutative left-cancelable right-cancelable cancelable uniquely-decomposable SubStr of K458()

<REAL,*> is non empty strict unital associative commutative multMagma

K217() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total Element of bool [:[:REAL,REAL:],REAL:]

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

<NAT,*> is non empty strict unital associative commutative uniquely-decomposable SubStr of <REAL,*>

2 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT

3 is non empty V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() Element of NAT

<NAT,+,0> is non empty strict unital associative commutative well-unital left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalExtension of <NAT,+>

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

addnat is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total Element of bool [:[:NAT,NAT:],NAT:]

the multF of <NAT,+> is Relation-like [: the carrier of <NAT,+>, the carrier of <NAT,+>:] -defined the carrier of <NAT,+> -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:]

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

[: the carrier of <NAT,+>, the carrier of <NAT,+>:] is Relation-like non empty set

[:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:] is Relation-like non empty set

bool [:[: the carrier of <NAT,+>, the carrier of <NAT,+>:], the carrier of <NAT,+>:] is non empty set

multLoopStr(# NAT,addnat,0 #) is strict multLoopStr

dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set

rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial V29() V30() V31() V33() V34() V35() V36() V37() Function-yielding V41() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V145() V147() set

G is Relation-like Function-like set

M is set

A is set

[M,A] is set

{M,A} is non empty finite set

{M} is non empty trivial finite 1 -element set

{{M,A},{M}} is non empty finite V46() set

B is set

G .. ([M,A],B) is set

K232(G) is Relation-like Function-like set

K232(G) . ([M,A],B) is set

[[M,A],B] is set

{[M,A],B} is non empty finite set

{[M,A]} is Relation-like Function-like constant non empty trivial finite 1 -element set

{{[M,A],B},{[M,A]}} is non empty finite V46() set

K232(G) . [[M,A],B] is set

M is non empty set

A is non empty set

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

G is non empty set

B is non empty set

Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B

[:[:M,A:],(Funcs (G,B)):] is Relation-like non empty set

bool [:[:M,A:],(Funcs (G,B)):] is non empty set

a is Relation-like [:M,A:] -defined Funcs (G,B) -valued Function-like non empty total quasi_total Function-yielding V41() Element of bool [:[:M,A:],(Funcs (G,B)):]

a1 is Element of M

a2 is Element of A

a1 is Element of G

(a,a1,a2,a1) is set

[a1,a2] is set

{a1,a2} is non empty finite set

{a1} is non empty trivial finite 1 -element set

{{a1,a2},{a1}} is non empty finite V46() set

a .. ([a1,a2],a1) is set

K232(a) is Relation-like Function-like set

K232(a) . ([a1,a2],a1) is set

[[a1,a2],a1] is set

{[a1,a2],a1} is non empty finite set

{[a1,a2]} is Relation-like Function-like constant non empty trivial finite 1 -element set

{{[a1,a2],a1},{[a1,a2]}} is non empty finite V46() set

K232(a) . [[a1,a2],a1] is set

a . (a1,a2) is Relation-like Function-like Element of Funcs (G,B)

a . [a1,a2] is Relation-like Function-like set

[a1,a2] is Element of [:M,A:]

dom a is Relation-like M -defined A -valued non empty Element of bool [:M,A:]

bool [:M,A:] is non empty set

a2 is Relation-like G -defined B -valued Function-like total quasi_total Element of Funcs (G,B)

dom a2 is Element of bool G

bool G is non empty set

a2 . a1 is Element of B

M is non empty set

A is non empty set

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

B is non empty set

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

bool [:[:M,A:],B:] is non empty set

G is set

[:G,M:] is Relation-like set

bool [:G,M:] is non empty set

[:G,A:] is Relation-like set

bool [:G,A:] is non empty set

a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]

a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]

a2 is Relation-like G -defined A -valued Function-like total quasi_total Element of bool [:G,A:]

a .: (a1,a2) is Relation-like Function-like set

Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B

<:a1,a2:> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]

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

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

a * <:a1,a2:> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]

[:G,B:] is Relation-like set

bool [:G,B:] is non empty set

dom (a .: (a1,a2)) is set

rng (a .: (a1,a2)) is set

G is non empty set

G is non empty set

M is V29() V30() V31() V35() V36() V37() finite cardinal V145() V147() Element of NAT

A is Element of G

M |-> A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

G is non empty set

M is set

A is Element of G

M --> A is Relation-like M -defined G -valued Function-like constant total set

Funcs (M,G) is functional non empty FUNCTION_DOMAIN of M,G

M --> A is Relation-like M -defined G -valued Function-like constant total quasi_total Element of bool [:M,G:]

[:M,G:] is Relation-like set

bool [:M,G:] is non empty set

dom (M --> A) is Element of bool M

bool M is non empty set

rng (M --> A) is trivial finite Element of bool G

bool G is non empty set

{A} is non empty trivial finite 1 -element Element of bool G

M is non empty set

A is non empty set

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

B is non empty set

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

bool [:[:M,A:],B:] is non empty set

G is set

[:G,A:] is Relation-like set

bool [:G,A:] is non empty set

a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]

a1 is Element of M

a2 is Relation-like G -defined A -valued Function-like total quasi_total Element of bool [:G,A:]

a [;] (a1,a2) is Relation-like Function-like set

Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B

dom a2 is Element of bool G

bool G is non empty set

(M,G,a1) is Relation-like G -defined M -valued Function-like constant total quasi_total Element of Funcs (G,M)

Funcs (G,M) is functional non empty FUNCTION_DOMAIN of G,M

<:(M,G,a1),a2:> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]

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

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

a * <:(M,G,a1),a2:> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]

[:G,B:] is Relation-like set

bool [:G,B:] is non empty set

dom (a [;] (a1,a2)) is set

rng (a [;] (a1,a2)) is set

M is non empty set

A is non empty set

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

B is non empty set

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

bool [:[:M,A:],B:] is non empty set

G is set

[:G,M:] is Relation-like set

bool [:G,M:] is non empty set

a is Relation-like [:M,A:] -defined B -valued Function-like non empty total quasi_total Element of bool [:[:M,A:],B:]

a1 is Relation-like G -defined M -valued Function-like total quasi_total Element of bool [:G,M:]

a2 is Element of A

a [:] (a1,a2) is Relation-like Function-like set

Funcs (G,B) is functional non empty FUNCTION_DOMAIN of G,B

dom a1 is Element of bool G

bool G is non empty set

(A,G,a2) is Relation-like G -defined A -valued Function-like constant total quasi_total Element of Funcs (G,A)

Funcs (G,A) is functional non empty FUNCTION_DOMAIN of G,A

<:a1,(A,G,a2):> is Relation-like G -defined [:M,A:] -valued Function-like total quasi_total Element of bool [:G,[:M,A:]:]

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

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

a * <:a1,(A,G,a2):> is Relation-like G -defined B -valued Function-like total quasi_total Element of bool [:G,B:]

[:G,B:] is Relation-like set

bool [:G,B:] is non empty set

dom (a [:] (a1,a2)) is set

rng (a [:] (a1,a2)) is set

M is Relation-like Function-like set

G is Relation-like Function-like set

A is set

G | A is Relation-like Function-like set

M * (G | A) is Relation-like Function-like set

A |` M is Relation-like Function-like set

(A |` M) * G is Relation-like Function-like set

dom (G | A) is set

dom G is set

(dom G) /\ A is set

dom (M * (G | A)) is set

dom ((A |` M) * G) is set

B is set

dom M is set

M . B is set

dom (A |` M) is set

(A |` M) . B is set

B is set

dom (A |` M) is set

dom M is set

(A |` M) . B is set

M . B is set

B is set

(M * (G | A)) . B is set

M . B is set

(G | A) . (M . B) is set

G . (M . B) is set

((A |` M) * G) . B is set

(A |` M) . B is set

G . ((A |` M) . B) is set

dom (A |` M) is set

F

F

[:F

bool [:F

G is set

M is Element of F

G is Relation-like Function-like set

dom G is set

rng G is set

M is Relation-like F

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