:: GROUP_7 semantic presentation

REAL is set

NAT is non empty non trivial V27() V28() V29() non finite countable denumerable Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial V27() V28() V29() non finite countable denumerable set

bool NAT is non empty set

bool NAT is non empty set

COMPLEX is set

RAT is set

INT is set

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

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

K354() is non empty strict multMagma

the carrier of K354() is non empty set

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

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

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

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

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

K423() is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V31() V32() V33() V34() finite finite-yielding V40() V103() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V166() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V31() V32() V33() V34() finite finite-yielding V40() V103() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V166() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V27() V28() V29() V31() V32() V33() V34() finite finite-yielding V40() V103() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V166() set

{{}} is functional non empty finite V40() with_common_domain countable set

K325({{}}) is functional non empty FinSequence-membered M15({{}})

[:K325({{}}),{{}}:] is Relation-like non empty set

bool [:K325({{}}),{{}}:] is non empty set

PFuncs (K325({{}}),{{}}) is set

1 is non empty ext-real V27() V28() V29() V33() V34() V103() Element of NAT

2 is non empty ext-real V27() V28() V29() V33() V34() V103() Element of NAT

3 is non empty ext-real V27() V28() V29() V33() V34() V103() Element of NAT

Seg 1 is non empty finite V43(1) countable Element of bool NAT

{ b

{1} is non empty finite countable set

Seg 2 is non empty finite V43(2) countable Element of bool NAT

{ b

{1,2} is non empty finite countable set

Seg 3 is non empty finite V43(3) countable Element of bool NAT

{ b

{1,2,3} is non empty finite countable set

G1 is Relation-like Function-like set

f is set

dom G1 is set

G1 . f is set

rng G1 is set

G1 is set

the non empty multMagma is non empty multMagma

G1 --> the non empty multMagma is Relation-like G1 -defined { the non empty multMagma } -valued Function-like constant total quasi_total Element of bool [:G1,{ the non empty multMagma }:]

{ the non empty multMagma } is non empty finite countable set

[:G1,{ the non empty multMagma }:] is Relation-like set

bool [:G1,{ the non empty multMagma }:] is non empty set

c

rng (G1 --> the non empty multMagma ) is trivial finite countable set

rng (G1 --> the non empty multMagma ) is trivial finite countable Element of bool { the non empty multMagma }

bool { the non empty multMagma } is non empty finite V40() countable set

dom (G1 --> the non empty multMagma ) is Element of bool G1

bool G1 is non empty set

m1 is set

(G1 --> the non empty multMagma ) . m1 is set

the set is set

the Relation-like the set -defined Function-like total 1-sorted-yielding () set is Relation-like the set -defined Function-like total 1-sorted-yielding () set

G1 is non empty set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

f is Element of G1

f . f is set

dom f is Element of bool G1

bool G1 is non empty set

f . f is 1-sorted

rng f is set

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

Carrier f is Relation-like G1 -defined Function-like total set

f is set

(Carrier f) . f is set

dom f is Element of bool G1

bool G1 is non empty set

f . f is set

rng f is set

c

the carrier of c

G1 is non empty set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

f is Element of G1

(G1,f,f) is non empty multMagma

(Carrier f) . f is set

c

c

the carrier of (G1,f,f) is non empty set

m1 is 1-sorted

the carrier of m1 is set

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

c

m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

rng (Carrier f) is set

union (rng (Carrier f)) is set

n1 is set

f . n1 is set

c

m1 . n1 is set

G is non empty set

p is Relation-like G -defined Function-like total 1-sorted-yielding () set

lF is Element of G

(G,p,lF) is non empty multMagma

the multF of (G,p,lF) is Relation-like [: the carrier of (G,p,lF), the carrier of (G,p,lF):] -defined the carrier of (G,p,lF) -valued Function-like quasi_total Element of bool [:[: the carrier of (G,p,lF), the carrier of (G,p,lF):], the carrier of (G,p,lF):]

the carrier of (G,p,lF) is non empty set

[: the carrier of (G,p,lF), the carrier of (G,p,lF):] is Relation-like non empty set

[:[: the carrier of (G,p,lF), the carrier of (G,p,lF):], the carrier of (G,p,lF):] is Relation-like non empty set

bool [:[: the carrier of (G,p,lF), the carrier of (G,p,lF):], the carrier of (G,p,lF):] is non empty set

c

m1 . lF is set

the multF of (G,p,lF) . ((c

[(c

{(c

{(c

{{(c

the multF of (G,p,lF) . [(c

i is set

(Carrier f) . lF is set

f . lF is set

Carrier p is Relation-like non-empty G -defined Function-like total set

(Carrier p) . lF is set

H is 1-sorted

the carrier of H is set

H is 1-sorted

the carrier of H is set

H is 1-sorted

the carrier of H is set

n1 is Relation-like Function-like set

dom n1 is set

rng n1 is set

G is set

n1 . G is set

(Carrier f) . G is set

f . G is set

c

m1 . G is set

lF is non empty set

p is Element of lF

m1 . p is set

i is Relation-like lF -defined Function-like total 1-sorted-yielding () set

(lF,i,p) is non empty multMagma

the carrier of (lF,i,p) is non empty set

H is 1-sorted

the carrier of H is set

c

H is 1-sorted

the carrier of H is set

H is non empty multMagma

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

the carrier of H is non empty set

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

the multF of H . ((c

[(c

{(c

{(c

{{(c

the multF of H . [(c

z is 1-sorted

the carrier of z is set

G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

lF is set

f . lF is set

c

m1 . lF is set

G . lF is set

p is non empty multMagma

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

the carrier of p is non empty set

[: the carrier of p, the carrier of p:] is Relation-like non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is Relation-like non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

the multF of p . ((c

[(c

{(c

{(c

{{(c

the multF of p . [(c

[:(product (Carrier f)),(product (Carrier f)):] is Relation-like non empty set

[:[:(product (Carrier f)),(product (Carrier f)):],(product (Carrier f)):] is Relation-like non empty set

bool [:[:(product (Carrier f)),(product (Carrier f)):],(product (Carrier f)):] is non empty set

c

multMagma(# (product (Carrier f)),c

the carrier of multMagma(# (product (Carrier f)),c

the multF of multMagma(# (product (Carrier f)),c

[: the carrier of multMagma(# (product (Carrier f)),c

[:[: the carrier of multMagma(# (product (Carrier f)),c

bool [:[: the carrier of multMagma(# (product (Carrier f)),c

m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

n1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

the multF of multMagma(# (product (Carrier f)),c

[m1,n1] is set

{m1,n1} is functional non empty finite countable set

{m1} is functional non empty finite with_common_domain countable set

{{m1,n1},{m1}} is non empty finite V40() countable set

the multF of multMagma(# (product (Carrier f)),c

G is set

f . G is set

m1 . G is set

n1 . G is set

f is strict multMagma

the carrier of f is set

the multF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]

[: the carrier of f, the carrier of f:] is Relation-like set

[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like set

bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set

c

the carrier of c

the multF of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

n1 is set

G is set

the multF of f . (n1,G) is set

[n1,G] is set

{n1,G} is non empty finite countable set

{n1} is non empty finite countable set

{{n1,G},{n1}} is non empty finite V40() countable set

the multF of f . [n1,G] is set

the multF of c

the multF of c

lF is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

p is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

[lF,p] is set

{lF,p} is functional non empty finite countable set

{lF} is functional non empty finite with_common_domain countable set

{{lF,p},{lF}} is non empty finite V40() countable set

the multF of f . [lF,p] is set

the multF of c

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

H is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

dom H is Element of bool G1

i is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

z is set

i . z is set

H . z is set

f . z is set

the multF of c

lF . z is set

p . z is set

the multF of f . (lF,p) is set

c

lpp is Relation-like Function-like set

lpp . z is set

the multF of c

the carrier of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the multF of c

[(lF . z),(p . z)] is set

{(lF . z),(p . z)} is non empty finite countable set

{(lF . z)} is non empty finite countable set

{{(lF . z),(p . z)},{(lF . z)}} is non empty finite V40() countable set

the multF of c

k is non empty multMagma

f is Relation-like Function-like set

f . z is set

the multF of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like quasi_total Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]

the carrier of k is non empty set

[: the carrier of k, the carrier of k:] is Relation-like non empty set

[:[: the carrier of k, the carrier of k:], the carrier of k:] is Relation-like non empty set

bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set

the multF of k . ((lF . z),(p . z)) is set

the multF of k . [(lF . z),(p . z)] is set

dom i is Element of bool G1

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

(G1,f) is strict multMagma

the carrier of (G1,f) is set

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

G1 is set

f is set

f is Relation-like Function-like set

f . f is set

c

c

m1 is Relation-like Function-like set

m1 . f is set

n1 is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

(G1,n1) is non empty strict constituted-Functions multMagma

the carrier of (G1,n1) is non empty set

n1 . f is set

G is non empty multMagma

the carrier of G is non empty set

lF is Relation-like Function-like Element of the carrier of (G1,n1)

p is Relation-like Function-like Element of the carrier of (G1,n1)

lF * p is Relation-like Function-like Element of the carrier of (G1,n1)

the multF of (G1,n1) is Relation-like [: the carrier of (G1,n1), the carrier of (G1,n1):] -defined the carrier of (G1,n1) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,n1), the carrier of (G1,n1):], the carrier of (G1,n1):]

[: the carrier of (G1,n1), the carrier of (G1,n1):] is Relation-like non empty set

[:[: the carrier of (G1,n1), the carrier of (G1,n1):], the carrier of (G1,n1):] is Relation-like non empty set

bool [:[: the carrier of (G1,n1), the carrier of (G1,n1):], the carrier of (G1,n1):] is non empty set

the multF of (G1,n1) . (lF,p) is Relation-like Function-like Element of the carrier of (G1,n1)

[lF,p] is set

{lF,p} is functional non empty finite countable set

{lF} is functional non empty finite with_common_domain countable set

{{lF,p},{lF}} is non empty finite V40() countable set

the multF of (G1,n1) . [lF,p] is set

i is Element of the carrier of G

H is Element of the carrier of G

i * H is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G . (i,H) is Element of the carrier of G

[i,H] is set

{i,H} is non empty finite countable set

{i} is non empty finite countable set

{{i,H},{i}} is non empty finite V40() countable set

the multF of G . [i,H] is set

Carrier n1 is Relation-like non-empty G1 -defined Function-like total set

product (Carrier n1) is functional non empty with_common_domain product-like set

the multF of (G1,n1) . (f,c

[f,c

{f,c

{f} is functional non empty finite with_common_domain countable set

{{f,c

the multF of (G1,n1) . [f,c

c

lpp is Relation-like Function-like set

lpp . f is set

the multF of c

the carrier of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the multF of c

[(f . f),(c

{(f . f),(c

{(f . f)} is non empty finite countable set

{{(f . f),(c

the multF of c

G1 is set

G1 is non empty set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

f is Element of G1

(G1,f,f) is non empty multMagma

c

f is set

f . f is set

c

(G1,f,c

m1 is non empty unital Group-like multMagma

f is Element of G1

(G1,f,f) is non empty multMagma

c

f is set

f . f is set

c

(G1,f,c

m1 is non empty associative multMagma

f is Element of G1

(G1,f,f) is non empty multMagma

c

f is set

f . f is set

c

(G1,f,c

m1 is non empty commutative multMagma

G1 is set

the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma

G1 --> the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma is Relation-like G1 -defined { the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma } -valued Function-like constant total quasi_total Element of bool [:G1,{ the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma }:]

{ the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma } is non empty finite countable set

[:G1,{ the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma }:] is Relation-like set

bool [:G1,{ the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma }:] is non empty set

c

rng (G1 --> the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma ) is trivial finite countable set

rng (G1 --> the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma ) is trivial finite countable Element of bool { the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma }

bool { the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma } is non empty finite V40() countable set

dom (G1 --> the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma ) is Element of bool G1

bool G1 is non empty set

m1 is set

(G1 --> the non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma ) . m1 is set

c

m1 is set

n1 is non empty set

lF is Relation-like n1 -defined Function-like total 1-sorted-yielding () set

G is Element of n1

(n1,lF,G) is non empty multMagma

p is non empty unital Group-like multMagma

i is non empty unital Group-like multMagma

c

m1 is set

n1 is non empty set

lF is Relation-like n1 -defined Function-like total 1-sorted-yielding () set

G is Element of n1

(n1,lF,G) is non empty multMagma

p is non empty associative multMagma

i is non empty associative multMagma

c

m1 is set

c

n1 is non empty set

lF is Relation-like n1 -defined Function-like total 1-sorted-yielding () set

G is Element of n1

(n1,lF,G) is non empty multMagma

p is non empty commutative multMagma

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) set

(G1,f) is non empty strict constituted-Functions multMagma

Carrier f is Relation-like non-empty G1 -defined Function-like total set

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

rng (Carrier f) is set

union (rng (Carrier f)) is set

c

f . c

m1 is non empty set

n1 is Element of m1

f . n1 is set

G is Relation-like m1 -defined Function-like total 1-sorted-yielding () (m1) set

Carrier G is Relation-like non-empty m1 -defined Function-like total set

(Carrier G) . n1 is set

(m1,G,n1) is non empty multMagma

the carrier of (m1,G,n1) is non empty set

lF is Element of the carrier of (m1,G,n1)

(Carrier f) . n1 is set

p is 1-sorted

the carrier of p is set

p is Element of the carrier of (m1,G,n1)

p * lF is Element of the carrier of (m1,G,n1)

the multF of (m1,G,n1) is Relation-like [: the carrier of (m1,G,n1), the carrier of (m1,G,n1):] -defined the carrier of (m1,G,n1) -valued Function-like quasi_total Element of bool [:[: the carrier of (m1,G,n1), the carrier of (m1,G,n1):], the carrier of (m1,G,n1):]

[: the carrier of (m1,G,n1), the carrier of (m1,G,n1):] is Relation-like non empty set

[:[: the carrier of (m1,G,n1), the carrier of (m1,G,n1):], the carrier of (m1,G,n1):] is Relation-like non empty set

bool [:[: the carrier of (m1,G,n1), the carrier of (m1,G,n1):], the carrier of (m1,G,n1):] is non empty set

the multF of (m1,G,n1) . (p,lF) is Element of the carrier of (m1,G,n1)

[p,lF] is set

{p,lF} is non empty finite countable set

{p} is non empty finite countable set

{{p,lF},{p}} is non empty finite V40() countable set

the multF of (m1,G,n1) . [p,lF] is set

lF * p is Element of the carrier of (m1,G,n1)

the multF of (m1,G,n1) . (lF,p) is Element of the carrier of (m1,G,n1)

[lF,p] is set

{lF,p} is non empty finite countable set

{lF} is non empty finite countable set

{{lF,p},{lF}} is non empty finite V40() countable set

the multF of (m1,G,n1) . [lF,p] is set

c

dom c

rng c

m1 is set

f . m1 is set

(Carrier f) . m1 is set

c

n1 is non empty multMagma

the carrier of n1 is non empty set

G is Element of the carrier of n1

lF is 1-sorted

the carrier of lF is set

product (Carrier f) is functional non empty with_common_domain product-like set

the carrier of (G1,f) is non empty set

m1 is Relation-like Function-like Element of the carrier of (G1,f)

n1 is Relation-like Function-like Element of the carrier of (G1,f)

n1 * m1 is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]

[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set

[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set

bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set

the multF of (G1,f) . (n1,m1) is Relation-like Function-like Element of the carrier of (G1,f)

[n1,m1] is set

{n1,m1} is functional non empty finite countable set

{n1} is functional non empty finite with_common_domain countable set

{{n1,m1},{n1}} is non empty finite V40() countable set

the multF of (G1,f) . [n1,m1] is set

m1 * n1 is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) . (m1,n1) is Relation-like Function-like Element of the carrier of (G1,f)

[m1,n1] is set

{m1,n1} is functional non empty finite countable set

{m1} is functional non empty finite with_common_domain countable set

{{m1,n1},{m1}} is non empty finite V40() countable set

the multF of (G1,f) . [m1,n1] is set

G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

dom G is Element of bool G1

i is set

f . i is set

c

H is non empty multMagma

the carrier of H is non empty set

z is Element of the carrier of H

G . i is set

the multF of (G1,f) . (G,m1) is set

[G,m1] is set

{G,m1} is functional non empty finite countable set

{G} is functional non empty finite with_common_domain countable set

{{G,m1},{G}} is non empty finite V40() countable set

the multF of (G1,f) . [G,m1] is set

c

c

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

the multF of H . (c

[c

{c

{c

{{c

the multF of H . [c

lF is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

lF . i is set

lpp is non empty multMagma

k is Relation-like Function-like set

k . i is set

the multF of lpp is Relation-like [: the carrier of lpp, the carrier of lpp:] -defined the carrier of lpp -valued Function-like quasi_total Element of bool [:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:]

the carrier of lpp is non empty set

[: the carrier of lpp, the carrier of lpp:] is Relation-like non empty set

[:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:] is Relation-like non empty set

bool [:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:] is non empty set

the multF of lpp . ((G . i),(c

[(G . i),(c

{(G . i),(c

{(G . i)} is non empty finite countable set

{{(G . i),(c

the multF of lpp . [(G . i),(c

dom lF is Element of bool G1

i is set

f . i is set

c

H is non empty multMagma

the carrier of H is non empty set

z is Element of the carrier of H

G . i is set

the multF of (G1,f) . (m1,G) is set

[m1,G] is set

{m1,G} is functional non empty finite countable set

{{m1,G},{m1}} is non empty finite V40() countable set

the multF of (G1,f) . [m1,G] is set

c

z * c

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

the multF of H . (z,c

[z,c

{z,c

{z} is non empty finite countable set

{{z,c

the multF of H . [z,c

p is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

p . i is set

lpp is non empty multMagma

k is Relation-like Function-like set

k . i is set

the multF of lpp is Relation-like [: the carrier of lpp, the carrier of lpp:] -defined the carrier of lpp -valued Function-like quasi_total Element of bool [:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:]

the carrier of lpp is non empty set

[: the carrier of lpp, the carrier of lpp:] is Relation-like non empty set

[:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:] is Relation-like non empty set

bool [:[: the carrier of lpp, the carrier of lpp:], the carrier of lpp:] is non empty set

the multF of lpp . ((c

[(c

{(c

{(c

{{(c

the multF of lpp . [(c

i is set

f . i is set

G . i is set

c

H is non empty multMagma

the carrier of H is non empty set

z is Element of the carrier of H

(Carrier f) . i is set

c

lpp is Element of the carrier of H

c

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

the multF of H . (c

[c

{c

{c

{{c

the multF of H . [c

lpp * c

the multF of H . (lpp,c

[lpp,c

{lpp,c

{lpp} is non empty finite countable set

{{lpp,c

the multF of H . [lpp,c

k is 1-sorted

the carrier of k is set

i is Relation-like Function-like set

dom i is set

rng i is set

H is set

f . H is set

(Carrier f) . H is set

G . H is set

c

i . H is set

z is non empty multMagma

the carrier of z is non empty set

c

lpp is Element of the carrier of z

c

the multF of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like quasi_total Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]

[: the carrier of z, the carrier of z:] is Relation-like non empty set

[:[: the carrier of z, the carrier of z:], the carrier of z:] is Relation-like non empty set

bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set

the multF of z . (c

[c

{c

{c

{{c

the multF of z . [c

lpp * c

the multF of z . (lpp,c

[lpp,c

{lpp,c

{lpp} is non empty finite countable set

{{lpp,c

the multF of z . [lpp,c

k is 1-sorted

the carrier of k is set

dom p is Element of bool G1

H is Relation-like Function-like Element of the carrier of (G1,f)

n1 * H is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) . (n1,H) is Relation-like Function-like Element of the carrier of (G1,f)

[n1,H] is set

{n1,H} is functional non empty finite countable set

{{n1,H},{n1}} is non empty finite V40() countable set

the multF of (G1,f) . [n1,H] is set

H * n1 is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) . (H,n1) is Relation-like Function-like Element of the carrier of (G1,f)

[H,n1] is set

{H,n1} is functional non empty finite countable set

{H} is functional non empty finite with_common_domain countable set

{{H,n1},{H}} is non empty finite V40() countable set

the multF of (G1,f) . [H,n1] is set

lpp is set

f . lpp is set

G . lpp is set

c

i . lpp is set

the multF of (G1,f) . (G,i) is set

[G,i] is set

{G,i} is functional non empty finite countable set

{{G,i},{G}} is non empty finite V40() countable set

the multF of (G1,f) . [G,i] is set

z is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

z . lpp is set

gf is non empty multMagma

the carrier of gf is non empty set

k is non empty multMagma

f is Relation-like Function-like set

f . lpp is set

the multF of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like quasi_total Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]

the carrier of k is non empty set

[: the carrier of k, the carrier of k:] is Relation-like non empty set

[:[: the carrier of k, the carrier of k:], the carrier of k:] is Relation-like non empty set

bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set

the multF of k . ((G . lpp),(i . lpp)) is set

[(G . lpp),(i . lpp)] is set

{(G . lpp),(i . lpp)} is non empty finite countable set

{(G . lpp)} is non empty finite countable set

{{(G . lpp),(i . lpp)},{(G . lpp)}} is non empty finite V40() countable set

the multF of k . [(G . lpp),(i . lpp)] is set

i is Element of the carrier of gf

G is Element of the carrier of gf

i * G is Element of the carrier of gf

the multF of gf is Relation-like [: the carrier of gf, the carrier of gf:] -defined the carrier of gf -valued Function-like quasi_total Element of bool [:[: the carrier of gf, the carrier of gf:], the carrier of gf:]

[: the carrier of gf, the carrier of gf:] is Relation-like non empty set

[:[: the carrier of gf, the carrier of gf:], the carrier of gf:] is Relation-like non empty set

bool [:[: the carrier of gf, the carrier of gf:], the carrier of gf:] is non empty set

the multF of gf . (i,G) is Element of the carrier of gf

[i,G] is set

{i,G} is non empty finite countable set

{i} is non empty finite countable set

{{i,G},{i}} is non empty finite V40() countable set

the multF of gf . [i,G] is set

G * i is Element of the carrier of gf

the multF of gf . (G,i) is Element of the carrier of gf

[G,i] is set

{G,i} is non empty finite countable set

{G} is non empty finite countable set

{{G,i},{G}} is non empty finite V40() countable set

the multF of gf . [G,i] is set

lpp is set

f . lpp is set

G . lpp is set

c

i . lpp is set

the multF of (G1,f) . (i,G) is set

[i,G] is set

{i,G} is functional non empty finite countable set

{i} is functional non empty finite with_common_domain countable set

{{i,G},{i}} is non empty finite V40() countable set

the multF of (G1,f) . [i,G] is set

c

c

gf is non empty multMagma

the carrier of gf is non empty set

k is non empty multMagma

f is Relation-like Function-like set

f . lpp is set

the multF of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like quasi_total Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]

the carrier of k is non empty set

[: the carrier of k, the carrier of k:] is Relation-like non empty set

[:[: the carrier of k, the carrier of k:], the carrier of k:] is Relation-like non empty set

bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set

the multF of k . ((i . lpp),(G . lpp)) is set

[(i . lpp),(G . lpp)] is set

{(i . lpp),(G . lpp)} is non empty finite countable set

{(i . lpp)} is non empty finite countable set

{{(i . lpp),(G . lpp)},{(i . lpp)}} is non empty finite V40() countable set

the multF of k . [(i . lpp),(G . lpp)] is set

i is Element of the carrier of gf

G is Element of the carrier of gf

i * G is Element of the carrier of gf

the multF of gf is Relation-like [: the carrier of gf, the carrier of gf:] -defined the carrier of gf -valued Function-like quasi_total Element of bool [:[: the carrier of gf, the carrier of gf:], the carrier of gf:]

[: the carrier of gf, the carrier of gf:] is Relation-like non empty set

[:[: the carrier of gf, the carrier of gf:], the carrier of gf:] is Relation-like non empty set

bool [:[: the carrier of gf, the carrier of gf:], the carrier of gf:] is non empty set

the multF of gf . (i,G) is Element of the carrier of gf

[i,G] is set

{i,G} is non empty finite countable set

{i} is non empty finite countable set

{{i,G},{i}} is non empty finite V40() countable set

the multF of gf . [i,G] is set

G * i is Element of the carrier of gf

the multF of gf . (G,i) is Element of the carrier of gf

[G,i] is set

{G,i} is non empty finite countable set

{G} is non empty finite countable set

{{G,i},{G}} is non empty finite V40() countable set

the multF of gf . [G,i] is set

dom z is Element of bool G1

dom c

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) set

(G1,f) is non empty strict constituted-Functions multMagma

the carrier of (G1,f) is non empty set

c

m1 is Relation-like Function-like Element of the carrier of (G1,f)

c

the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]

[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set

[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set

bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set

the multF of (G1,f) . (c

[c

{c

{c

{{c

the multF of (G1,f) . [c

n1 is Relation-like Function-like Element of the carrier of (G1,f)

(c

the multF of (G1,f) . ((c

[(c

{(c

{(c

{{(c

the multF of (G1,f) . [(c

m1 * n1 is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) . (m1,n1) is Relation-like Function-like Element of the carrier of (G1,f)

[m1,n1] is set

{m1,n1} is functional non empty finite countable set

{m1} is functional non empty finite with_common_domain countable set

{{m1,n1},{m1}} is non empty finite V40() countable set

the multF of (G1,f) . [m1,n1] is set

c

the multF of (G1,f) . (c

[c

{c

{{c

the multF of (G1,f) . [c

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

the multF of (G1,f) . (( the multF of (G1,f) . (c

[( the multF of (G1,f) . (c

{( the multF of (G1,f) . (c

{( the multF of (G1,f) . (c

{{( the multF of (G1,f) . (c

the multF of (G1,f) . [( the multF of (G1,f) . (c

the multF of (G1,f) . (c

[c

{c

{{c

the multF of (G1,f) . [c

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

gf is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

dom gf is Element of bool G1

i is set

f . i is set

G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

G . i is set

lF is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

lF . i is set

G is non empty multMagma

j is Relation-like Function-like set

j . i is set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

the carrier of G is non empty set

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G . ((G . i),(lF . i)) is set

[(G . i),(lF . i)] is set

{(G . i),(lF . i)} is non empty finite countable set

{(G . i)} is non empty finite countable set

{{(G . i),(lF . i)},{(G . i)}} is non empty finite V40() countable set

the multF of G . [(G . i),(lF . i)] is set

p is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

p . i is set

lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

the multF of (G1,f) . (lpp,n1) is set

[lpp,n1] is set

{lpp,n1} is functional non empty finite countable set

{lpp} is functional non empty finite with_common_domain countable set

{{lpp,n1},{lpp}} is non empty finite V40() countable set

the multF of (G1,f) . [lpp,n1] is set

lpp . i is set

c

K is Relation-like Function-like set

K . i is set

the multF of c

the carrier of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the multF of c

[(lpp . i),(p . i)] is set

{(lpp . i),(p . i)} is non empty finite countable set

{(lpp . i)} is non empty finite countable set

{{(lpp . i),(p . i)},{(lpp . i)}} is non empty finite V40() countable set

the multF of c

G is Element of the carrier of G

m is Element of the carrier of G

G * m is Element of the carrier of G

the multF of G . (G,m) is Element of the carrier of G

[G,m] is set

{G,m} is non empty finite countable set

{G} is non empty finite countable set

{{G,m},{G}} is non empty finite V40() countable set

the multF of G . [G,m] is set

k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

the multF of (G1,f) . (c

[c

{c

{{c

the multF of (G1,f) . [c

k . i is set

f is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

f . i is set

J is Element of the carrier of c

ff is Element of the carrier of c

J * ff is Element of the carrier of c

the multF of c

[J,ff] is set

{J,ff} is non empty finite countable set

{J} is non empty finite countable set

{{J,ff},{J}} is non empty finite V40() countable set

the multF of c

J is Element of the carrier of c

j is Element of the carrier of c

j * ff is Element of the carrier of c

the multF of c

[j,ff] is set

{j,ff} is non empty finite countable set

{j} is non empty finite countable set

{{j,ff},{j}} is non empty finite V40() countable set

the multF of c

J * (j * ff) is Element of the carrier of c

the multF of c

[J,(j * ff)] is set

{J,(j * ff)} is non empty finite countable set

{J} is non empty finite countable set

{{J,(j * ff)},{J}} is non empty finite V40() countable set

the multF of c

gf . i is set

G is non empty multMagma

k1 is Relation-like Function-like set

k1 . i is set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

the carrier of G is non empty set

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G . ((lF . i),(p . i)) is set

[(lF . i),(p . i)] is set

{(lF . i),(p . i)} is non empty finite countable set

{(lF . i)} is non empty finite countable set

{{(lF . i),(p . i)},{(lF . i)}} is non empty finite V40() countable set

the multF of G . [(lF . i),(p . i)] is set

k2 is non empty multMagma

G2 is Relation-like Function-like set

G2 . i is set

the multF of k2 is Relation-like [: the carrier of k2, the carrier of k2:] -defined the carrier of k2 -valued Function-like quasi_total Element of bool [:[: the carrier of k2, the carrier of k2:], the carrier of k2:]

the carrier of k2 is non empty set

[: the carrier of k2, the carrier of k2:] is Relation-like non empty set

[:[: the carrier of k2, the carrier of k2:], the carrier of k2:] is Relation-like non empty set

bool [:[: the carrier of k2, the carrier of k2:], the carrier of k2:] is non empty set

the multF of k2 . ((G . i),(k . i)) is set

[(G . i),(k . i)] is set

{(G . i),(k . i)} is non empty finite countable set

{{(G . i),(k . i)},{(G . i)}} is non empty finite V40() countable set

the multF of k2 . [(G . i),(k . i)] is set

dom f is Element of bool G1

G1 is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) set

(G1,f) is non empty strict constituted-Functions multMagma

the carrier of (G1,f) is non empty set

c

m1 is Relation-like Function-like Element of the carrier of (G1,f)

c

the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]

[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set

[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set

bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set

the multF of (G1,f) . (c

[c

{c

{c

{{c

the multF of (G1,f) . [c

m1 * c

the multF of (G1,f) . (m1,c

[m1,c

{m1,c

{m1} is functional non empty finite with_common_domain countable set

{{m1,c

the multF of (G1,f) . [m1,c

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

dom (Carrier f) is Element of bool G1

bool G1 is non empty set

p is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

dom p is Element of bool G1

i is set

f . i is set

n1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

n1 . i is set

G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

G . i is set

H is non empty multMagma

z is Relation-like Function-like set

z . i is set

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

the carrier of H is non empty set

[: the carrier of H, the carrier of H:] is Relation-like non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

the multF of H . ((n1 . i),(G . i)) is set

[(n1 . i),(G . i)] is set

{(n1 . i),(G . i)} is non empty finite countable set

{(n1 . i)} is non empty finite countable set

{{(n1 . i),(G . i)},{(n1 . i)}} is non empty finite V40() countable set

the multF of H . [(n1 . i),(G . i)] is set

lF is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

lF . i is set

c

lpp is Element of the carrier of H

c

the multF of H . (c

[c

{c

{c

{{c

the multF of H . [c

lpp * c

the multF of H . (lpp,c

[lpp,c

{lpp,c

{lpp} is non empty finite countable set

{{lpp,c

the multF of H . [lpp,c

p . i is set

k is non empty commutative multMagma

k is non empty multMagma

f is Relation-like Function-like set

f . i is set

the multF of k is Relation-like [: the carrier of k, the carrier of k:] -defined the carrier of k -valued Function-like quasi_total Element of bool [:[: the carrier of k, the carrier of k:], the carrier of k:]

the carrier of k is non empty set

[: the carrier of k, the carrier of k:] is Relation-like non empty set

[:[: the carrier of k, the carrier of k:], the carrier of k:] is Relation-like non empty set

bool [:[: the carrier of k, the carrier of k:], the carrier of k:] is non empty set

the multF of k . ((G . i),(n1 . i)) is set

[(G . i),(n1 . i)] is set

{(G . i),(n1 . i)} is non empty finite countable set

{(G . i)} is non empty finite countable set

{{(G . i),(n1 . i)},{(G . i)}} is non empty finite V40() countable set

the multF of k . [(G . i),(n1 . i)] is set

dom lF is Element of bool G1

G1 is set

f is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

f . f is set

(G1,f) is non empty strict constituted-Functions multMagma

c

the carrier of (G1,f) is non empty set

n1 is Relation-like Function-like Element of the carrier of (G1,f)

Carrier f is Relation-like non-empty G1 -defined Function-like total set

product (Carrier f) is functional non empty with_common_domain product-like set

the carrier of c

G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

G . f is set

lF is Element of the carrier of c

p is Element of the carrier of c

p * lF is Element of the carrier of c

the multF of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the multF of c

[p,lF] is set

{p,lF} is non empty finite countable set

{p} is non empty finite countable set

{{p,lF},{p}} is non empty finite V40() countable set

the multF of c

lF * p is Element of the carrier of c

the multF of c

[lF,p] is set

{lF,p} is non empty finite countable set

{lF} is non empty finite countable set

{{lF,p},{lF}} is non empty finite V40() countable set

the multF of c

i is set

f . i is set

dom f is Element of bool G1

bool G1 is non empty set

rng f is set

H is non empty multMagma

the carrier of H is non empty set

the Element of the carrier of H is Element of the carrier of H

i is Relation-like G1 -defined Function-like total set

dom i is Element of bool G1

bool G1 is non empty set

H is set

f . H is set

(Carrier f) . H is set

i . H is set

z is 1-sorted

the carrier of z is set

i . H is set

z is non empty multMagma

the carrier of z is non empty set

c

lpp is 1-sorted

the carrier of lpp is set

dom (Carrier f) is Element of bool G1

H is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

H . f is set

z is Relation-like Function-like Element of the carrier of (G1,f)

n1 * z is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]

[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set

[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set

bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set

the multF of (G1,f) . (n1,z) is Relation-like Function-like Element of the carrier of (G1,f)

[n1,z] is set

{n1,z} is functional non empty finite countable set

{n1} is functional non empty finite with_common_domain countable set

{{n1,z},{n1}} is non empty finite V40() countable set

the multF of (G1,f) . [n1,z] is set

z * n1 is Relation-like Function-like Element of the carrier of (G1,f)

the multF of (G1,f) . (z,n1) is Relation-like Function-like Element of the carrier of (G1,f)

[z,n1] is set

{z,n1} is functional non empty finite countable set

{z} is functional non empty finite with_common_domain countable set

{{z,n1},{z}} is non empty finite V40() countable set

the multF of (G1,f) . [z,n1] is set

c

z * c

the multF of (G1,f) . (z,c

[z,c

{z,c

{{z,c

the multF of (G1,f) . [z,c

c

the multF of (G1,f) . (c

[c

{c

{c

{{c

the multF of (G1,f) . [c

lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)

lpp . f is set

k is Element of the carrier of c

p * k is Element of the carrier of c

the multF of c

[p,k] is set

{p,k} is non empty finite countable set

{{p,k},{p}} is non empty finite V40() countable set

the multF of c

k * p is Element of the carrier of c

the multF of c

[k,p] is set

{k,p} is non empty finite countable set

{k} is non empty finite countable set

{{k,p},{k}} is non empty finite V40() countable set

the multF of c

G1 is set

f is set

f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set

f . f is set

(G1,f) is non empty strict constituted-Functions multMagma

c

the carrier of (G1,f) is non empty set

the carrier of c

m1 is Element of the carrier of c

n1 is Element of the carrier of c

m1 * n1 is Element of the carrier of c

the multF of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the multF of c

[m1,n1] is set

{m1,n1} is non empty finite countable set

{m1} is non empty finite countable set

{{m1,n1},{m1}} is non empty finite V40() countable