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

RAT is set
INT is set

bool is non empty set
K354() is non empty strict multMagma
the carrier of K354() is non empty set

K423() is set

bool 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
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty finite countable set
Seg 2 is non empty finite V43(2) countable Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite countable set
Seg 3 is non empty finite V43(3) countable Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
{1,2,3} is non empty finite countable 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
c4 is set
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

G1 is non empty 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 set
() . f is set
dom f is Element of bool G1
bool G1 is non empty set
f . f is set
rng f is set
c4 is 1-sorted
the carrier of c4 is set
G1 is non empty set

dom () is Element of bool G1
bool G1 is non empty set
f is Element of G1
(G1,f,f) is non empty multMagma
() . f is set

c4 . f is set
the carrier of (G1,f,f) is non empty set
m1 is 1-sorted
the carrier of m1 is set
G1 is set

dom () is Element of bool G1
bool G1 is non empty set

rng () is set
union (rng ()) is set
n1 is set
f . n1 is set
c4 . n1 is set
m1 . n1 is set
G is non empty 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
c4 . lF is set
m1 . lF is set
the multF of (G,p,lF) . ((c4 . lF),(m1 . lF)) is set
[(c4 . lF),(m1 . lF)] is set
{(c4 . lF),(m1 . lF)} is non empty finite countable set
{(c4 . lF)} is non empty finite countable set
{{(c4 . lF),(m1 . lF)},{(c4 . lF)}} is non empty finite V40() countable set
the multF of (G,p,lF) . [(c4 . lF),(m1 . lF)] is set
i is set
() . lF is set
f . lF is set

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

dom n1 is set
rng n1 is set
G is set
n1 . G is set
() . G is set
f . G is set
c4 . G is set
m1 . G is set
lF is non empty set
p is Element of lF
m1 . p is 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
c4 . p is set
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 . ((c4 . G),(m1 . G)) is set
[(c4 . G),(m1 . G)] is set
{(c4 . G),(m1 . G)} is non empty finite countable set
{(c4 . G)} is non empty finite countable set
{{(c4 . G),(m1 . G)},{(c4 . G)}} is non empty finite V40() countable set
the multF of H . [(c4 . G),(m1 . G)] is set
z is 1-sorted
the carrier of z is set

lF is set
f . lF is set
c4 . lF is set
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 . ((c4 . lF),(m1 . lF)) is set
[(c4 . lF),(m1 . lF)] is set
{(c4 . lF),(m1 . lF)} is non empty finite countable set
{(c4 . lF)} is non empty finite countable set
{{(c4 . lF),(m1 . lF)},{(c4 . lF)}} is non empty finite V40() countable set
the multF of p . [(c4 . lF),(m1 . lF)] is set
[:(product ()),(product ()):] is Relation-like non empty set
[:[:(product ()),(product ()):],(product ()):] is Relation-like non empty set
bool [:[:(product ()),(product ()):],(product ()):] is non empty set
c4 is Relation-like [:(product ()),(product ()):] -defined product () -valued Function-like quasi_total Function-yielding V166() Element of bool [:[:(product ()),(product ()):],(product ()):]
multMagma(# (product ()),c4 #) is strict multMagma
the carrier of multMagma(# (product ()),c4 #) is set
the multF of multMagma(# (product ()),c4 #) is Relation-like [: the carrier of multMagma(# (product ()),c4 #), the carrier of multMagma(# (product ()),c4 #):] -defined the carrier of multMagma(# (product ()),c4 #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (product ()),c4 #), the carrier of multMagma(# (product ()),c4 #):], the carrier of multMagma(# (product ()),c4 #):]
[: the carrier of multMagma(# (product ()),c4 #), the carrier of multMagma(# (product ()),c4 #):] is Relation-like set
[:[: the carrier of multMagma(# (product ()),c4 #), the carrier of multMagma(# (product ()),c4 #):], the carrier of multMagma(# (product ()),c4 #):] is Relation-like set
bool [:[: the carrier of multMagma(# (product ()),c4 #), the carrier of multMagma(# (product ()),c4 #):], the carrier of multMagma(# (product ()),c4 #):] is non empty set

the multF of multMagma(# (product ()),c4 #) . (m1,n1) is set
[m1,n1] is set
{m1,n1} is functional non empty finite countable set

{{m1,n1},{m1}} is non empty finite V40() countable set
the multF of multMagma(# (product ()),c4 #) . [m1,n1] is set
G is set
f . G is set
m1 . G is set
n1 . G is set

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
c4 is strict multMagma
the carrier of c4 is set
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
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 c4 . (n1,G) is set
the multF of c4 . [n1,G] is set

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

{{lF,p},{lF}} is non empty finite V40() countable set
the multF of f . [lF,p] is set
the multF of c4 . [lF,p] is set
dom () is Element of bool G1
bool G1 is non empty set

dom H is Element of bool G1

z is set
i . z is set
H . z is set
f . z is set
the multF of c4 . (lF,p) is set
lF . z is set
p . z is set
the multF of f . (lF,p) is set
c13 is non empty multMagma

lpp . z is set
the multF of c13 is Relation-like [: the carrier of c13, the carrier of c13:] -defined the carrier of c13 -valued Function-like quasi_total Element of bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:]
the carrier of c13 is non empty set
[: the carrier of c13, the carrier of c13:] is Relation-like non empty set
[:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is Relation-like non empty set
bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is non empty set
the multF of c13 . ((lF . z),(p . z)) is set
[(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 c13 . [(lF . z),(p . z)] is set
k is non empty multMagma

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

(G1,f) is strict multMagma
the carrier of (G1,f) is set

G1 is set
f is set

f . f is set

c4 . f is set

m1 . f is 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,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

the multF of (G1,n1) . (f,c4) is set
[f,c4] is set
{f,c4} is functional non empty finite countable set

{{f,c4},{f}} is non empty finite V40() countable set
the multF of (G1,n1) . [f,c4] is set
c13 is non empty multMagma

lpp . f is set
the multF of c13 is Relation-like [: the carrier of c13, the carrier of c13:] -defined the carrier of c13 -valued Function-like quasi_total Element of bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:]
the carrier of c13 is non empty set
[: the carrier of c13, the carrier of c13:] is Relation-like non empty set
[:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is Relation-like non empty set
bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is non empty set
the multF of c13 . ((f . f),(c4 . f)) is set
[(f . f),(c4 . f)] is set
{(f . f),(c4 . f)} is non empty finite countable set
{(f . f)} is non empty finite countable set
{{(f . f),(c4 . f)},{(f . f)}} is non empty finite V40() countable set
the multF of c13 . [(f . f),(c4 . f)] is set
G1 is set
G1 is non empty set

f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty unital Group-like multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty unital Group-like multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty associative multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty associative multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty commutative multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty commutative multMagma
G1 is set

{} is non empty finite countable set
[:G1,{}:] is Relation-like set
bool [:G1,{}:] is non empty set
c4 is set
rng () is trivial finite countable set
rng () is trivial finite countable Element of bool {}
bool {} is non empty finite V40() countable set
dom () is Element of bool G1
bool G1 is non empty set
m1 is set
() . m1 is set

m1 is set
n1 is non empty 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
c4 . m1 is set
m1 is set
n1 is non empty 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
c4 . m1 is set
m1 is set
c4 . m1 is set
n1 is non empty set

G is Element of n1
(n1,lF,G) is non empty multMagma
p is non empty commutative multMagma
G1 is set

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

dom () is Element of bool G1
bool G1 is non empty set
rng () is set
union (rng ()) is set
c4 is set
f . c4 is set
m1 is non empty set
n1 is Element of m1
f . n1 is set

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

dom c4 is set
rng c4 is set
m1 is set
f . m1 is set
() . m1 is set
c4 . m1 is set
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

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,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,n1},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,n1] is set

dom G is Element of bool G1
i is set
f . i is set
c4 . i is set
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,m1},{G}} is non empty finite V40() countable set
the multF of (G1,f) . [G,m1] is set
c13 is Element of the carrier of H
c13 * z is Element of the carrier of H
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 . (c13,z) is Element of the carrier of H
[c13,z] is set
{c13,z} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,z},{c13}} is non empty finite V40() countable set
the multF of H . [c13,z] is set

lF . i is set
lpp is non empty multMagma

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),(c4 . i)) is set
[(G . i),(c4 . i)] is set
{(G . i),(c4 . i)} is non empty finite countable set
{(G . i)} is non empty finite countable set
{{(G . i),(c4 . i)},{(G . i)}} is non empty finite V40() countable set
the multF of lpp . [(G . i),(c4 . i)] is set
dom lF is Element of bool G1
i is set
f . i is set
c4 . i is set
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
c13 is Element of the carrier of H
z * c13 is Element of the carrier of H
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,c13) is Element of the carrier of H
[z,c13] is set
{z,c13} is non empty finite countable set
{z} is non empty finite countable set
{{z,c13},{z}} is non empty finite V40() countable set
the multF of H . [z,c13] is set

p . i is set
lpp is non empty multMagma

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 . ((c4 . i),(G . i)) is set
[(c4 . i),(G . i)] is set
{(c4 . i),(G . i)} is non empty finite countable set
{(c4 . i)} is non empty finite countable set
{{(c4 . i),(G . i)},{(c4 . i)}} is non empty finite V40() countable set
the multF of lpp . [(c4 . i),(G . i)] is set
i is set
f . i is set
G . i is set
c4 . i is set
H is non empty multMagma
the carrier of H is non empty set
z is Element of the carrier of H
() . i is set
c13 is Element of the carrier of H
lpp is Element of the carrier of H
c13 * lpp is Element of the carrier of H
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 . (c13,lpp) is Element of the carrier of H
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of H . [c13,lpp] is set
lpp * c13 is Element of the carrier of H
the multF of H . (lpp,c13) is Element of the carrier of H
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c13] is set
k is 1-sorted
the carrier of k is set

dom i is set
rng i is set
H is set
f . H is set
() . H is set
G . H is set
c4 . H is set
i . H is set
z is non empty multMagma
the carrier of z is non empty set
c13 is Element of the carrier of z
lpp is Element of the carrier of z
c13 * lpp is Element of the carrier of z
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 . (c13,lpp) is Element of the carrier of z
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of z . [c13,lpp] is set
lpp * c13 is Element of the carrier of z
the multF of z . (lpp,c13) is Element of the carrier of z
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of z . [lpp,c13] is set
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,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
c4 . lpp is set
i . lpp is set
the multF of (G1,f) . (G,i) is set
[G,i] is set

{{G,i},{G}} is non empty finite V40() countable set
the multF of (G1,f) . [G,i] is set

z . lpp is set
gf is non empty multMagma
the carrier of gf is non empty set
k is non empty multMagma

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
c4 . lpp is set
i . lpp is set
the multF of (G1,f) . (i,G) is set
[i,G] is set

{{i,G},{i}} is non empty finite V40() countable set
the multF of (G1,f) . [i,G] is set

c13 . lpp is set
gf is non empty multMagma
the carrier of gf is non empty set
k is non empty multMagma

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 c13 is Element of bool G1
G1 is set

(G1,f) is non empty strict constituted-Functions multMagma
the carrier of (G1,f) is non empty set
c4 is Relation-like Function-like Element of the carrier of (G1,f)
m1 is Relation-like Function-like Element of the carrier of (G1,f)
c4 * 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) . (c4,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,m1] is set
{c4,m1} is functional non empty finite countable set

{{c4,m1},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,m1] is set
n1 is Relation-like Function-like Element of the carrier of (G1,f)
(c4 * m1) * n1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((c4 * m1),n1) is Relation-like Function-like Element of the carrier of (G1,f)
[(c4 * m1),n1] is set
{(c4 * m1),n1} is functional non empty finite countable set

{{(c4 * m1),n1},{(c4 * m1)}} is non empty finite V40() countable set
the multF of (G1,f) . [(c4 * m1),n1] 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,n1},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,n1] is set
c4 * (m1 * n1) is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c4,(m1 * n1)) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,(m1 * n1)] is set
{c4,(m1 * n1)} is functional non empty finite countable set
{{c4,(m1 * n1)},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,(m1 * n1)] is set

the multF of (G1,f) . (( the multF of (G1,f) . (c4,m1)),n1) is Relation-like Function-like Element of the carrier of (G1,f)
[( the multF of (G1,f) . (c4,m1)),n1] is set
{( the multF of (G1,f) . (c4,m1)),n1} is functional non empty finite countable set
{( the multF of (G1,f) . (c4,m1))} is functional non empty finite with_common_domain countable set
{{( the multF of (G1,f) . (c4,m1)),n1},{( the multF of (G1,f) . (c4,m1))}} is non empty finite V40() countable set
the multF of (G1,f) . [( the multF of (G1,f) . (c4,m1)),n1] is set
the multF of (G1,f) . (c4,( the multF of (G1,f) . (m1,n1))) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,( the multF of (G1,f) . (m1,n1))] is set
{c4,( the multF of (G1,f) . (m1,n1))} is functional non empty finite countable set
{{c4,( the multF of (G1,f) . (m1,n1))},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,( the multF of (G1,f) . (m1,n1))] is set
dom () is Element of bool G1
bool G1 is non empty set

dom gf is Element of bool G1
i is set
f . i is set

G . i is set

lF . i is set
G is non empty multMagma

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 . i is set

the multF of (G1,f) . (lpp,n1) is set
[lpp,n1] is set
{lpp,n1} is functional non empty finite 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
c23 is non empty multMagma

K . i is set
the multF of c23 is Relation-like [: the carrier of c23, the carrier of c23:] -defined the carrier of c23 -valued Function-like quasi_total Element of bool [:[: the carrier of c23, the carrier of c23:], the carrier of c23:]
the carrier of c23 is non empty set
[: the carrier of c23, the carrier of c23:] is Relation-like non empty set
[:[: the carrier of c23, the carrier of c23:], the carrier of c23:] is Relation-like non empty set
bool [:[: the carrier of c23, the carrier of c23:], the carrier of c23:] is non empty set
the multF of c23 . ((lpp . i),(p . i)) is set
[(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 c23 . [(lpp . i),(p . i)] is set
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

the multF of (G1,f) . (c4,k) is set
[c4,k] is set
{c4,k} is functional non empty finite countable set
{{c4,k},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,k] is set
k . i is set

f . i is set
J is Element of the carrier of c23
ff is Element of the carrier of c23
J * ff is Element of the carrier of c23
the multF of c23 . (J,ff) is Element of the carrier of c23
[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 c23 . [J,ff] is set
J is Element of the carrier of c23
j is Element of the carrier of c23
j * ff is Element of the carrier of c23
the multF of c23 . (j,ff) is Element of the carrier of c23
[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 c23 . [j,ff] is set
J * (j * ff) is Element of the carrier of c23
the multF of c23 . (J,(j * ff)) is Element of the carrier of c23
[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 c23 . [J,(j * ff)] is set
gf . i is set
G is non empty multMagma

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

(G1,f) is non empty strict constituted-Functions multMagma
the carrier of (G1,f) is non empty set
c4 is Relation-like Function-like Element of the carrier of (G1,f)
m1 is Relation-like Function-like Element of the carrier of (G1,f)
c4 * 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) . (c4,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,m1] is set
{c4,m1} is functional non empty finite countable set

{{c4,m1},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,m1] is set
m1 * c4 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (m1,c4) is Relation-like Function-like Element of the carrier of (G1,f)
[m1,c4] is set
{m1,c4} is functional non empty finite countable set

{{m1,c4},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,c4] is set

dom () is Element of bool G1
bool G1 is non empty set

dom p is Element of bool G1
i is set
f . i is set

n1 . i is set

G . i is set
H is non empty multMagma

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 . i is set
c13 is Element of the carrier of H
lpp is Element of the carrier of H
c13 * lpp is Element of the carrier of H
the multF of H . (c13,lpp) is Element of the carrier of H
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of H . [c13,lpp] is set
lpp * c13 is Element of the carrier of H
the multF of H . (lpp,c13) is Element of the carrier of H
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c13] is set
p . i is set
k is non empty commutative multMagma
k is non empty multMagma

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 . f is set
(G1,f) is non empty strict constituted-Functions multMagma
c4 is non empty multMagma
the carrier of (G1,f) is non empty set
n1 is Relation-like Function-like Element of the carrier of (G1,f)

the carrier of c4 is non empty set

G . f is set
lF is Element of the carrier of c4
p is Element of the carrier of c4
p * lF is Element of the carrier of c4
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like non empty set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like non empty set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
the multF of c4 . (p,lF) is Element of the carrier of c4
[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 c4 . [p,lF] is set
lF * p is Element of the carrier of c4
the multF of c4 . (lF,p) is Element of the carrier of c4
[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 c4 . [lF,p] is set
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

dom i is Element of bool G1
bool G1 is non empty set
H is set
f . H is set
() . 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
c13 is Element of the carrier of z
lpp is 1-sorted
the carrier of lpp is set
dom () is Element of bool G1

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,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,n1},{z}} is non empty finite V40() countable set
the multF of (G1,f) . [z,n1] is set
c13 is Relation-like Function-like Element of the carrier of (G1,f)
z * c13 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (z,c13) is Relation-like Function-like Element of the carrier of (G1,f)
[z,c13] is set
{z,c13} is functional non empty finite countable set
{{z,c13},{z}} is non empty finite V40() countable set
the multF of (G1,f) . [z,c13] is set
c13 * z is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c13,z) is Relation-like Function-like Element of the carrier of (G1,f)
[c13,z] is set
{c13,z} is functional non empty finite countable set

{{c13,z},{c13}} is non empty finite V40() countable set
the multF of (G1,f) . [c13,z] is set

lpp . f is set
k is Element of the carrier of c4
p * k is Element of the carrier of c4
the multF of c4 . (p,k) is Element of the carrier of c4
[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 c4 . [p,k] is set
k * p is Element of the carrier of c4
the multF of c4 . (k,p) is Element of the carrier of c4
[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 c4 . [k,p] is set
G1 is set
f is set

f . f is set
(G1,f) is non empty strict constituted-Functions multMagma
c4 is non empty multMagma
the carrier of (G1,f) is non empty set
the carrier of c4 is non empty set
m1 is Element of the carrier of c4
n1 is Element of the carrier of c4
m1 * n1 is Element of the carrier of c4
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like non empty set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like non empty set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
the multF of c4 . (m1,n1) is Element of the carrier of c4
[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