:: 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₁ where b₁ is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty finite countable set
Seg 2 is non empty finite V43(2) countable Element of bool NAT
{ b₁ where b₁ is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty finite countable set
Seg 3 is non empty finite V43(3) countable Element of bool NAT
{ b₁ where b₁ is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b₁ & b₁ <= 3 ) } is set
{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₄ 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
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₄ is 1-sorted
the carrier of c₄ is set
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₄ is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
c₄ . 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
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₄ is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
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₄ . n1 is set
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₄ . lF is set
m1 . lF is set
the multF of (G,p,lF) . ((c₄ . lF),(m1 . lF)) is set
[(c₄ . lF),(m1 . lF)] is set
{(c₄ . lF),(m1 . lF)} is non empty finite countable set
{(c₄ . lF)} is non empty finite countable set
{{(c₄ . lF),(m1 . lF)},{(c₄ . lF)}} is non empty finite V40() countable set
the multF of (G,p,lF) . [(c₄ . lF),(m1 . lF)] is set
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₄ . G is set
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₄ . 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 . ((c₄ . G),(m1 . G)) is set
[(c₄ . G),(m1 . G)] is set
{(c₄ . G),(m1 . G)} is non empty finite countable set
{(c₄ . G)} is non empty finite countable set
{{(c₄ . G),(m1 . G)},{(c₄ . G)}} is non empty finite V40() countable set
the multF of H . [(c₄ . G),(m1 . G)] is set
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₄ . 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 . ((c₄ . lF),(m1 . lF)) is set
[(c₄ . lF),(m1 . lF)] is set
{(c₄ . lF),(m1 . lF)} is non empty finite countable set
{(c₄ . lF)} is non empty finite countable set
{{(c₄ . lF),(m1 . lF)},{(c₄ . lF)}} is non empty finite V40() countable set
the multF of p . [(c₄ . lF),(m1 . lF)] is set
[:(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₄ is Relation-like [:(product (Carrier f)),(product (Carrier f)):] -defined product (Carrier f) -valued Function-like quasi_total Function-yielding V166() Element of bool [:[:(product (Carrier f)),(product (Carrier f)):],(product (Carrier f)):]
multMagma(# (product (Carrier f)),c₄ #) is strict multMagma
the carrier of multMagma(# (product (Carrier f)),c₄ #) is set
the multF of multMagma(# (product (Carrier f)),c₄ #) is Relation-like [: the carrier of multMagma(# (product (Carrier f)),c₄ #), the carrier of multMagma(# (product (Carrier f)),c₄ #):] -defined the carrier of multMagma(# (product (Carrier f)),c₄ #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (product (Carrier f)),c₄ #), the carrier of multMagma(# (product (Carrier f)),c₄ #):], the carrier of multMagma(# (product (Carrier f)),c₄ #):]
[: the carrier of multMagma(# (product (Carrier f)),c₄ #), the carrier of multMagma(# (product (Carrier f)),c₄ #):] is Relation-like set
[:[: the carrier of multMagma(# (product (Carrier f)),c₄ #), the carrier of multMagma(# (product (Carrier f)),c₄ #):], the carrier of multMagma(# (product (Carrier f)),c₄ #):] is Relation-like set
bool [:[: the carrier of multMagma(# (product (Carrier f)),c₄ #), the carrier of multMagma(# (product (Carrier f)),c₄ #):], the carrier of multMagma(# (product (Carrier f)),c₄ #):] is non empty set
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 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₄ #) . [m1,n1] is set
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₄ is strict multMagma
the carrier of c₄ is set
the multF of c₄ is Relation-like [: the carrier of c₄, the carrier of c₄:] -defined the carrier of c₄ -valued Function-like quasi_total Element of bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:]
[: the carrier of c₄, the carrier of c₄:] is Relation-like set
[:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is Relation-like set
bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] 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 c₄ . (n1,G) is set
the multF of c₄ . [n1,G] is set
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₄ . [lF,p] is set
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,p) is set
lF . z is set
p . z is set
the multF of f . (lF,p) is set
c₁₃ is non empty multMagma
lpp is Relation-like Function-like set
lpp . z is set
the multF of c₁₃ is Relation-like [: the carrier of c₁₃, the carrier of c₁₃:] -defined the carrier of c₁₃ -valued Function-like quasi_total Element of bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:]
the carrier of c₁₃ is non empty set
[: the carrier of c₁₃, the carrier of c₁₃:] is Relation-like non empty set
[:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is Relation-like non empty set
bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is non empty set
the multF of c₁₃ . ((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 c₁₃ . [(lF . z),(p . z)] is set
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₄ is Relation-like Function-like set
c₄ . f is set
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₄) is set
[f,c₄] is set
{f,c₄} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,c₄},{f}} is non empty finite V40() countable set
the multF of (G1,n1) . [f,c₄] is set
c₁₃ is non empty multMagma
lpp is Relation-like Function-like set
lpp . f is set
the multF of c₁₃ is Relation-like [: the carrier of c₁₃, the carrier of c₁₃:] -defined the carrier of c₁₃ -valued Function-like quasi_total Element of bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:]
the carrier of c₁₃ is non empty set
[: the carrier of c₁₃, the carrier of c₁₃:] is Relation-like non empty set
[:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is Relation-like non empty set
bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is non empty set
the multF of c₁₃ . ((f . f),(c₄ . f)) is set
[(f . f),(c₄ . f)] is set
{(f . f),(c₄ . f)} is non empty finite countable set
{(f . f)} is non empty finite countable set
{{(f . f),(c₄ . f)},{(f . f)}} is non empty finite V40() countable set
the multF of c₁₃ . [(f . f),(c₄ . f)] is set
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₄ is non empty unital Group-like multMagma
f is set
f . f is set
c₄ is Element of G1
(G1,f,c₄) is non empty multMagma
m1 is non empty unital Group-like multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c₄ is non empty associative multMagma
f is set
f . f is set
c₄ is Element of G1
(G1,f,c₄) is non empty multMagma
m1 is non empty associative multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c₄ is non empty commutative multMagma
f is set
f . f is set
c₄ is Element of G1
(G1,f,c₄) is non empty multMagma
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₄ is 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 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₄ is Relation-like G1 -defined Function-like total 1-sorted-yielding () set
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
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
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 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₄ is set
f . c₄ is set
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₄ is Relation-like Function-like set
dom c₄ is set
rng c₄ is set
m1 is set
f . m1 is set
(Carrier f) . m1 is set
c₄ . 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
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₄ . 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} 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₁₃ is Element of the carrier of H
c₁₃ * 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 . (c₁₃,z) is Element of the carrier of H
[c₁₃,z] is set
{c₁₃,z} is non empty finite countable set
{c₁₃} is non empty finite countable set
{{c₁₃,z},{c₁₃}} is non empty finite V40() countable set
the multF of H . [c₁₃,z] is set
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₄ . i)) is set
[(G . i),(c₄ . i)] is set
{(G . i),(c₄ . i)} is non empty finite countable set
{(G . i)} is non empty finite countable set
{{(G . i),(c₄ . i)},{(G . i)}} is non empty finite V40() countable set
the multF of lpp . [(G . i),(c₄ . i)] is set
dom lF is Element of bool G1
i is set
f . i is set
c₄ . 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
c₁₃ is Element of the carrier of H
z * c₁₃ 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,c₁₃) is Element of the carrier of H
[z,c₁₃] is set
{z,c₁₃} is non empty finite countable set
{z} is non empty finite countable set
{{z,c₁₃},{z}} is non empty finite V40() countable set
the multF of H . [z,c₁₃] 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 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₄ . i),(G . i)) is set
[(c₄ . i),(G . i)] is set
{(c₄ . i),(G . i)} is non empty finite countable set
{(c₄ . i)} is non empty finite countable set
{{(c₄ . i),(G . i)},{(c₄ . i)}} is non empty finite V40() countable set
the multF of lpp . [(c₄ . i),(G . i)] is set
i is set
f . i is set
G . i is set
c₄ . i is set
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₁₃ is Element of the carrier of H
lpp is Element of the carrier of H
c₁₃ * 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 . (c₁₃,lpp) is Element of the carrier of H
[c₁₃,lpp] is set
{c₁₃,lpp} is non empty finite countable set
{c₁₃} is non empty finite countable set
{{c₁₃,lpp},{c₁₃}} is non empty finite V40() countable set
the multF of H . [c₁₃,lpp] is set
lpp * c₁₃ is Element of the carrier of H
the multF of H . (lpp,c₁₃) is Element of the carrier of H
[lpp,c₁₃] is set
{lpp,c₁₃} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c₁₃},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c₁₃] is set
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₄ . H is set
i . H is set
z is non empty multMagma
the carrier of z is non empty set
c₁₃ is Element of the carrier of z
lpp is Element of the carrier of z
c₁₃ * 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 . (c₁₃,lpp) is Element of the carrier of z
[c₁₃,lpp] is set
{c₁₃,lpp} is non empty finite countable set
{c₁₃} is non empty finite countable set
{{c₁₃,lpp},{c₁₃}} is non empty finite V40() countable set
the multF of z . [c₁₃,lpp] is set
lpp * c₁₃ is Element of the carrier of z
the multF of z . (lpp,c₁₃) is Element of the carrier of z
[lpp,c₁₃] is set
{lpp,c₁₃} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c₁₃},{lpp}} is non empty finite V40() countable set
the multF of z . [lpp,c₁₃] 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} 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₄ . lpp is set
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₄ . lpp is set
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₁₃ is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
c₁₃ . 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 . ((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₁₃ 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₄ 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)
c₄ * 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) . (c₄,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c₄,m1] is set
{c₄,m1} is functional non empty finite countable set
{c₄} is functional non empty finite with_common_domain countable set
{{c₄,m1},{c₄}} is non empty finite V40() countable set
the multF of (G1,f) . [c₄,m1] is set
n1 is Relation-like Function-like Element of the carrier of (G1,f)
(c₄ * m1) * n1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((c₄ * m1),n1) is Relation-like Function-like Element of the carrier of (G1,f)
[(c₄ * m1),n1] is set
{(c₄ * m1),n1} is functional non empty finite countable set
{(c₄ * m1)} is functional non empty finite with_common_domain countable set
{{(c₄ * m1),n1},{(c₄ * m1)}} is non empty finite V40() countable set
the multF of (G1,f) . [(c₄ * 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} 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₄ * (m1 * n1) is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c₄,(m1 * n1)) is Relation-like Function-like Element of the carrier of (G1,f)
[c₄,(m1 * n1)] is set
{c₄,(m1 * n1)} is functional non empty finite countable set
{{c₄,(m1 * n1)},{c₄}} is non empty finite V40() countable set
the multF of (G1,f) . [c₄,(m1 * n1)] 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
the multF of (G1,f) . (( 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) . (c₄,m1)),n1] is set
{( the multF of (G1,f) . (c₄,m1)),n1} is functional non empty finite countable set
{( the multF of (G1,f) . (c₄,m1))} is functional non empty finite with_common_domain countable set
{{( the multF of (G1,f) . (c₄,m1)),n1},{( the multF of (G1,f) . (c₄,m1))}} is non empty finite V40() countable set
the multF of (G1,f) . [( the multF of (G1,f) . (c₄,m1)),n1] is set
the multF of (G1,f) . (c₄,( the multF of (G1,f) . (m1,n1))) is Relation-like Function-like Element of the carrier of (G1,f)
[c₄,( the multF of (G1,f) . (m1,n1))] is set
{c₄,( the multF of (G1,f) . (m1,n1))} is functional non empty finite countable set
{{c₄,( the multF of (G1,f) . (m1,n1))},{c₄}} is non empty finite V40() countable set
the multF of (G1,f) . [c₄,( the multF of (G1,f) . (m1,n1))] is set
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₂₃ is non empty multMagma
K is Relation-like Function-like set
K . i is set
the multF of c₂₃ is Relation-like [: the carrier of c₂₃, the carrier of c₂₃:] -defined the carrier of c₂₃ -valued Function-like quasi_total Element of bool [:[: the carrier of c₂₃, the carrier of c₂₃:], the carrier of c₂₃:]
the carrier of c₂₃ is non empty set
[: the carrier of c₂₃, the carrier of c₂₃:] is Relation-like non empty set
[:[: the carrier of c₂₃, the carrier of c₂₃:], the carrier of c₂₃:] is Relation-like non empty set
bool [:[: the carrier of c₂₃, the carrier of c₂₃:], the carrier of c₂₃:] is non empty set
the multF of c₂₃ . ((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 c₂₃ . [(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
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
the multF of (G1,f) . (c₄,k) is set
[c₄,k] is set
{c₄,k} is functional non empty finite countable set
{{c₄,k},{c₄}} is non empty finite V40() countable set
the multF of (G1,f) . [c₄,k] is set
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 Element of the carrier 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,ff] is set
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 Element of the carrier 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,ff] is set
J * (j * ff) is Element of the carrier of c₂₃
the multF of c₂₃ . (J,(j * ff)) is Element of the carrier 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₂₃ . [J,(j * ff)] is set
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₄ 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)
c₄ * 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) . (c₄,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c₄,m1] is set
{c₄,m1} is functional non empty finite countable set
{c₄} is functional non empty finite with_common_domain countable set
{{c₄,m1},{c₄}} is non empty finite V40() countable set
the multF of (G1,f) . [c₄,m1] is set
m1 * c₄ is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (m1,c₄) is Relation-like Function-like Element of the carrier of (G1,f)
[m1,c₄] is set
{m1,c₄} is functional non empty finite countable set
{m1} is functional non empty finite with_common_domain countable set
{{m1,c₄},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,c₄] 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
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₁₃ is Element of the carrier of H
lpp is Element of the carrier of H
c₁₃ * lpp is Element of the carrier of H
the multF of H . (c₁₃,lpp) is Element of the carrier of H
[c₁₃,lpp] is set
{c₁₃,lpp} is non empty finite countable set
{c₁₃} is non empty finite countable set
{{c₁₃,lpp},{c₁₃}} is non empty finite V40() countable set
the multF of H . [c₁₃,lpp] is set
lpp * c₁₃ is Element of the carrier of H
the multF of H . (lpp,c₁₃) is Element of the carrier of H
[lpp,c₁₃] is set
{lpp,c₁₃} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c₁₃},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c₁₃] is set
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₄ 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)
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₄ is non empty set
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₄ is Relation-like [: the carrier of c₄, the carrier of c₄:] -defined the carrier of c₄ -valued Function-like quasi_total Element of bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:]
[: the carrier of c₄, the carrier of c₄:] is Relation-like non empty set
[:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is Relation-like non empty set
bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is non empty set
the multF of c₄ . (p,lF) is Element of the carrier 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₄ . [p,lF] is set
lF * p is Element of the carrier of c₄
the multF of c₄ . (lF,p) is Element of the carrier 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₄ . [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
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₁₃ is Element of the carrier of z
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₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
z * c₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (z,c₁₃) is Relation-like Function-like Element of the carrier of (G1,f)
[z,c₁₃] is set
{z,c₁₃} is functional non empty finite countable set
{{z,c₁₃},{z}} is non empty finite V40() countable set
the multF of (G1,f) . [z,c₁₃] is set
c₁₃ * z is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c₁₃,z) is Relation-like Function-like Element of the carrier of (G1,f)
[c₁₃,z] is set
{c₁₃,z} is functional non empty finite countable set
{c₁₃} is functional non empty finite with_common_domain countable set
{{c₁₃,z},{c₁₃}} is non empty finite V40() countable set
the multF of (G1,f) . [c₁₃,z] is set
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 Element of the carrier 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₄ . [p,k] is set
k * p is Element of the carrier of c₄
the multF of c₄ . (k,p) is Element of the carrier 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₄ . [k,p] is set
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₄ is non empty multMagma
the carrier of (G1,f) is non empty set
the carrier of c₄ is non empty set
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₄ is Relation-like [: the carrier of c₄, the carrier of c₄:] -defined the carrier of c₄ -valued Function-like quasi_total Element of bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:]
[: the carrier of c₄, the carrier of c₄:] is Relation-like non empty set
[:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is Relation-like non empty set
bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is non empty set
the multF of c₄ . (m1,n1) is Element of the carrier 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 set
the multF of c₄ . [m1,n1] is set
G is Element of the carrier of c₄
(m1 * n1) * G is Element of the carrier of c₄
the multF of c₄ . ((m1 * n1),G) is Element of the carrier of c₄
[(m1 * n1),G] is set
{(m1 * n1),G} is non empty finite countable set
{(m1 * n1)} is non empty finite countable set
{{(m1 * n1),G},{(m1 * n1)}} is non empty finite V40() countable set
the multF of c₄ . [(m1 * n1),G] is set
n1 * G is Element of the carrier of c₄
the multF of c₄ . (n1,G) is Element of the carrier of c₄
[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 c₄ . [n1,G] is set
m1 * (n1 * G) is Element of the carrier of c₄
the multF of c₄ . (m1,(n1 * G)) is Element of the carrier of c₄
[m1,(n1 * G)] is set
{m1,(n1 * G)} is non empty finite countable set
{{m1,(n1 * G)},{m1}} is non empty finite V40() countable set
the multF of c₄ . [m1,(n1 * G)] is set
lF is set
f . lF is set
dom f is Element of bool G1
bool G1 is non empty set
rng f is set
p is non empty multMagma
the carrier of p is non empty set
the Element of the carrier of p is Element of the carrier of p
lF is Relation-like G1 -defined Function-like total set
dom lF is Element of bool G1
bool G1 is non empty set
p is set
f . p is set
Carrier f is Relation-like non-empty G1 -defined Function-like total set
(Carrier f) . p is set
lF . p is set
i is 1-sorted
the carrier of i is set
lF . p is set
i is non empty multMagma
the carrier of i is non empty set
H is Element of the carrier of i
z is 1-sorted
the carrier of z is set
p is set
f . p is set
dom f is Element of bool G1
rng f is set
i is non empty multMagma
the carrier of i is non empty set
the Element of the carrier of i is Element of the carrier of i
p is Relation-like G1 -defined Function-like total set
H is set
f . H is set
dom f is Element of bool G1
rng f is set
z is non empty multMagma
the carrier of z is non empty set
the Element of the carrier of z is Element of the carrier of z
H is Relation-like G1 -defined Function-like total set
dom H is Element of bool G1
z is set
f . z is set
(Carrier f) . z is set
H . z is set
c₁₃ is 1-sorted
the carrier of c₁₃ is set
H . z is set
c₁₃ is non empty multMagma
the carrier of c₁₃ is non empty set
lpp is Element of the carrier of c₁₃
k is 1-sorted
the carrier of k is set
dom p is Element of bool G1
z is set
f . z is set
(Carrier f) . z is set
p . z is set
c₁₃ is 1-sorted
the carrier of c₁₃ is set
p . z is set
c₁₃ is non empty multMagma
the carrier of c₁₃ is non empty set
lpp is Element of the carrier of c₁₃
k is 1-sorted
the carrier of k is set
dom (Carrier f) is Element of bool G1
product (Carrier f) is functional non empty with_common_domain product-like set
z is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
c₁₃ is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
k is Relation-like Function-like Element of the carrier of (G1,f)
f is Relation-like Function-like Element of the carrier of (G1,f)
k * f 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) . (k,f) is Relation-like Function-like Element of the carrier of (G1,f)
[k,f] is set
{k,f} is functional non empty finite countable set
{k} is functional non empty finite with_common_domain countable set
{{k,f},{k}} is non empty finite V40() countable set
the multF of (G1,f) . [k,f] is set
gf is Relation-like Function-like Element of the carrier of (G1,f)
(k * f) * gf is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((k * f),gf) is Relation-like Function-like Element of the carrier of (G1,f)
[(k * f),gf] is set
{(k * f),gf} is functional non empty finite countable set
{(k * f)} is functional non empty finite with_common_domain countable set
{{(k * f),gf},{(k * f)}} is non empty finite V40() countable set
the multF of (G1,f) . [(k * f),gf] is set
f * gf is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (f,gf) is Relation-like Function-like Element of the carrier of (G1,f)
[f,gf] is set
{f,gf} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,gf},{f}} is non empty finite V40() countable set
the multF of (G1,f) . [f,gf] is set
k * (f * gf) is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (k,(f * gf)) is Relation-like Function-like Element of the carrier of (G1,f)
[k,(f * gf)] is set
{k,(f * gf)} is functional non empty finite countable set
{{k,(f * gf)},{k}} is non empty finite V40() countable set
the multF of (G1,f) . [k,(f * gf)] is set
i is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
i . f is set
j is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
j . f is set
z . f is set
c₂₃ is Element of the carrier of c₄
m1 * c₂₃ is Element of the carrier of c₄
the multF of c₄ . (m1,c₂₃) is Element of the carrier of c₄
[m1,c₂₃] is set
{m1,c₂₃} is non empty finite countable set
{{m1,c₂₃},{m1}} is non empty finite V40() countable set
the multF of c₄ . [m1,c₂₃] is set
G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
G . f is set
c₁₃ . f is set
m is Element of the carrier of c₄
m * G is Element of the carrier of c₄
the multF of c₄ . (m,G) is Element of the carrier of c₄
[m,G] is set
{m,G} is non empty finite countable set
{m} is non empty finite countable set
{{m,G},{m}} is non empty finite V40() countable set
the multF of c₄ . [m,G] is set
G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
G . f is set
lpp . f is set
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₄ is non empty multMagma
the carrier of (G1,f) is non empty set
the carrier of c₄ is non empty set
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₄ is Relation-like [: the carrier of c₄, the carrier of c₄:] -defined the carrier of c₄ -valued Function-like quasi_total Element of bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:]
[: the carrier of c₄, the carrier of c₄:] is Relation-like non empty set
[:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is Relation-like non empty set
bool [:[: the carrier of c₄, the carrier of c₄:], the carrier of c₄:] is non empty set
the multF of c₄ . (m1,n1) is Element of the carrier 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 set
the multF of c₄ . [m1,n1] is set
n1 * m1 is Element of the carrier of c₄
the multF of c₄ . (n1,m1) is Element of the carrier of c₄
[n1,m1] is set
{n1,m1} is non empty finite countable set
{n1} is non empty finite countable set
{{n1,m1},{n1}} is non empty finite V40() countable set
the multF of c₄ . [n1,m1] is set
G is set
f . G is set
dom f is Element of bool G1
bool G1 is non empty set
rng f is set
lF is non empty multMagma
the carrier of lF is non empty set
the Element of the carrier of lF is Element of the carrier of lF
G is Relation-like G1 -defined Function-like total set
p is set
f . p is set
dom f is Element of bool G1
bool G1 is non empty set
rng f is set
i is non empty multMagma
the carrier of i is non empty set
the Element of the carrier of i is Element of the carrier of i
p is Relation-like G1 -defined Function-like total set
dom G is Element of bool G1
bool G1 is non empty set
i is set
f . i is set
Carrier f is Relation-like non-empty G1 -defined Function-like total set
(Carrier f) . i is set
G . i is set
H is 1-sorted
the carrier of H is set
G . i is set
H is non empty multMagma
the carrier of H is non empty set
z is Element of the carrier of H
c₁₃ is 1-sorted
the carrier of c₁₃ is set
dom (Carrier f) is Element of bool G1
product (Carrier f) is functional non empty with_common_domain product-like set
i is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
i . f is set
dom p is Element of bool G1
H is set
f . H is set
(Carrier f) . H is set
p . H is set
z is 1-sorted
the carrier of z is set
p . H is set
z is non empty multMagma
the carrier of z is non empty set
c₁₃ is Element of the carrier of z
lpp is 1-sorted
the carrier of lpp is set
H is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
z is Relation-like Function-like Element of the carrier of (G1,f)
c₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
z * c₁₃ 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) . (z,c₁₃) is Relation-like Function-like Element of the carrier of (G1,f)
[z,c₁₃] is set
{z,c₁₃} is functional non empty finite countable set
{z} is functional non empty finite with_common_domain countable set
{{z,c₁₃},{z}} is non empty finite V40() countable set
the multF of (G1,f) . [z,c₁₃] is set
c₁₃ * z is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c₁₃,z) is Relation-like Function-like Element of the carrier of (G1,f)
[c₁₃,z] is set
{c₁₃,z} is functional non empty finite countable set
{c₁₃} is functional non empty finite with_common_domain countable set
{{c₁₃,z},{c₁₃}} is non empty finite V40() countable set
the multF of (G1,f) . [c₁₃,z] is set
H . f is set
lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
lpp . f is set
G1 is set
f is Relation-like G1 -defined Function-like total set
f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) set
(G1,f) is non empty strict unital Group-like constituted-Functions multMagma
1_ (G1,f) is Relation-like Function-like Element of the carrier of (G1,f)
the carrier of (G1,f) is non empty set
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
dom f is Element of bool G1
m1 is set
f . m1 is set
(Carrier f) . m1 is set
f . m1 is set
n1 is non empty unital Group-like multMagma
1_ n1 is Element of the carrier of n1
the carrier of n1 is non empty set
G is 1-sorted
the carrier of G is set
product (Carrier f) is functional non empty with_common_domain product-like set
n1 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)
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
f . i is set
H is non empty unital Group-like multMagma
1_ H is Element of the carrier of H
the carrier of H is non empty set
G . i is set
the multF of (G1,f) . (n1,f) is set
[n1,f] is set
{n1,f} is functional non empty finite countable set
{{n1,f},{n1}} is non empty finite V40() countable set
the multF of (G1,f) . [n1,f] is set
z is Element of the carrier of H
c₁₃ is Element of the carrier of H
z * c₁₃ 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,c₁₃) is Element of the carrier of H
[z,c₁₃] is set
{z,c₁₃} is non empty finite countable set
{z} is non empty finite countable set
{{z,c₁₃},{z}} is non empty finite V40() countable set
the multF of H . [z,c₁₃] is set
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),(f . i)) is set
[(G . i),(f . i)] is set
{(G . i),(f . i)} is non empty finite countable set
{(G . i)} is non empty finite countable set
{{(G . i),(f . i)},{(G . i)}} is non empty finite V40() countable set
the multF of lpp . [(G . i),(f . i)] is set
dom lF is Element of bool G1
i is set
f . i is set
f . i is set
H is non empty unital Group-like multMagma
1_ H is Element of the carrier of H
the carrier of H is non empty set
G . i is set
the multF of (G1,f) . (f,n1) is set
[f,n1] is set
{f,n1} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,n1},{f}} is non empty finite V40() countable set
the multF of (G1,f) . [f,n1] is set
c₁₃ is Element of the carrier of H
z is Element of the carrier of H
c₁₃ * 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 . (c₁₃,z) is Element of the carrier of H
[c₁₃,z] is set
{c₁₃,z} is non empty finite countable set
{c₁₃} is non empty finite countable set
{{c₁₃,z},{c₁₃}} is non empty finite V40() countable set
the multF of H . [c₁₃,z] 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 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 . ((f . i),(G . i)) is set
[(f . i),(G . i)] is set
{(f . i),(G . i)} is non empty finite countable set
{(f . i)} is non empty finite countable set
{{(f . i),(G . i)},{(f . i)}} is non empty finite V40() countable set
the multF of lpp . [(f . i),(G . i)] is set
dom p is Element of bool G1
G1 is set
f is set
f is Relation-like Function-like set
f . f is set
c₄ is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) set
c₄ . f is set
(G1,c₄) is non empty strict unital Group-like constituted-Functions multMagma
1_ (G1,c₄) is Relation-like Function-like Element of the carrier of (G1,c₄)
the carrier of (G1,c₄) is non empty set
m1 is non empty unital Group-like multMagma
1_ m1 is Element of the carrier of m1
the carrier of m1 is non empty set
Carrier c₄ is Relation-like non-empty G1 -defined Function-like total set
product (Carrier c₄) is functional non empty with_common_domain product-like set
lF is Element of the carrier of m1
p is set
c₄ . p is set
i is non empty unital Group-like multMagma
1_ i is Element of the carrier of i
the carrier of i is non empty set
p is Relation-like G1 -defined Function-like total set
dom p is Element of bool G1
bool G1 is non empty set
i is set
c₄ . i is set
(Carrier c₄) . i is set
p . i is set
H is 1-sorted
the carrier of H is set
p . i is set
H is non empty unital Group-like multMagma
1_ H is Element of the carrier of H
the carrier of H is non empty set
z is 1-sorted
the carrier of z is set
dom (Carrier c₄) is Element of bool G1
i is Relation-like Function-like Element of the carrier of (G1,c₄)
i * (1_ (G1,c₄)) is Relation-like Function-like Element of the carrier of (G1,c₄)
the multF of (G1,c₄) is Relation-like [: the carrier of (G1,c₄), the carrier of (G1,c₄):] -defined the carrier of (G1,c₄) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):]
[: the carrier of (G1,c₄), the carrier of (G1,c₄):] is Relation-like non empty set
[:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):] is Relation-like non empty set
bool [:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):] is non empty set
the multF of (G1,c₄) . (i,(1_ (G1,c₄))) is Relation-like Function-like Element of the carrier of (G1,c₄)
[i,(1_ (G1,c₄))] is set
{i,(1_ (G1,c₄))} is functional non empty finite countable set
{i} is functional non empty finite with_common_domain countable set
{{i,(1_ (G1,c₄))},{i}} is non empty finite V40() countable set
the multF of (G1,c₄) . [i,(1_ (G1,c₄))] is set
p . f is set
the multF of (G1,c₄) . (p,f) is set
[p,f] is set
{p,f} is functional non empty finite countable set
{p} is functional non empty finite with_common_domain countable set
{{p,f},{p}} is non empty finite V40() countable set
the multF of (G1,c₄) . [p,f] is set
G is Element of the carrier of m1
lF * G is Element of the carrier of m1
the multF of m1 is Relation-like [: the carrier of m1, the carrier of m1:] -defined the carrier of m1 -valued Function-like quasi_total Element of bool [:[: the carrier of m1, the carrier of m1:], the carrier of m1:]
[: the carrier of m1, the carrier of m1:] is Relation-like non empty set
[:[: the carrier of m1, the carrier of m1:], the carrier of m1:] is Relation-like non empty set
bool [:[: the carrier of m1, the carrier of m1:], the carrier of m1:] is non empty set
the multF of m1 . (lF,G) is Element of the carrier of m1
[lF,G] is set
{lF,G} is non empty finite countable set
{lF} is non empty finite countable set
{{lF,G},{lF}} is non empty finite V40() countable set
the multF of m1 . [lF,G] is set
H is non empty multMagma
z is Relation-like Function-like set
z . f 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 . ((p . f),(f . f)) is set
[(p . f),(f . f)] is set
{(p . f),(f . f)} is non empty finite countable set
{(p . f)} is non empty finite countable set
{{(p . f),(f . f)},{(p . f)}} is non empty finite V40() countable set
the multF of H . [(p . f),(f . f)] is set
(1_ (G1,c₄)) * i is Relation-like Function-like Element of the carrier of (G1,c₄)
the multF of (G1,c₄) . ((1_ (G1,c₄)),i) is Relation-like Function-like Element of the carrier of (G1,c₄)
[(1_ (G1,c₄)),i] is set
{(1_ (G1,c₄)),i} is functional non empty finite countable set
{(1_ (G1,c₄))} is functional non empty finite with_common_domain countable set
{{(1_ (G1,c₄)),i},{(1_ (G1,c₄))}} is non empty finite V40() countable set
the multF of (G1,c₄) . [(1_ (G1,c₄)),i] is set
the multF of (G1,c₄) . (f,p) is set
[f,p] is set
{f,p} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,p},{f}} is non empty finite V40() countable set
the multF of (G1,c₄) . [f,p] is set
G * lF is Element of the carrier of m1
the multF of m1 . (G,lF) is Element of the carrier of m1
[G,lF] is set
{G,lF} is non empty finite countable set
{G} is non empty finite countable set
{{G,lF},{G}} is non empty finite V40() countable set
the multF of m1 . [G,lF] is set
H is non empty multMagma
z is Relation-like Function-like set
z . f 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 . ((f . f),(p . f)) is set
[(f . f),(p . f)] is set
{(f . f),(p . f)} is non empty finite countable set
{(f . f)} is non empty finite countable set
{{(f . f),(p . f)},{(f . f)}} is non empty finite V40() countable set
the multF of H . [(f . f),(p . f)] is set
G1 is set
f is Relation-like Function-like set
f is Relation-like G1 -defined Function-like total set
c₄ is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) (G1) set
(G1,c₄) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of (G1,c₄) is non empty set
m1 is Relation-like Function-like Element of the carrier of (G1,c₄)
m1 " is Relation-like Function-like Element of the carrier of (G1,c₄)
Carrier c₄ is Relation-like non-empty G1 -defined Function-like total set
dom (Carrier c₄) is Element of bool G1
bool G1 is non empty set
dom f is Element of bool G1
G is set
c₄ . G is set
(Carrier c₄) . G is set
f . G is set
f . G is set
lF is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of lF is non empty set
p is Element of the carrier of lF
p " is Element of the carrier of lF
i is 1-sorted
the carrier of i is set
product (Carrier c₄) is functional non empty with_common_domain product-like set
1_ (G1,c₄) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G1,c₄)
G is Relation-like Function-like Element of the carrier of (G1,c₄)
m1 * G is Relation-like Function-like Element of the carrier of (G1,c₄)
the multF of (G1,c₄) is Relation-like [: the carrier of (G1,c₄), the carrier of (G1,c₄):] -defined the carrier of (G1,c₄) -valued Function-like quasi_total associative Element of bool [:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):]
[: the carrier of (G1,c₄), the carrier of (G1,c₄):] is Relation-like non empty set
[:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):] is Relation-like non empty set
bool [:[: the carrier of (G1,c₄), the carrier of (G1,c₄):], the carrier of (G1,c₄):] is non empty set
the multF of (G1,c₄) . (m1,G) is Relation-like Function-like Element of the carrier of (G1,c₄)
[m1,G] is set
{m1,G} is functional non empty finite countable set
{m1} is functional non empty finite with_common_domain countable set
{{m1,G},{m1}} is non empty finite V40() countable set
the multF of (G1,c₄) . [m1,G] is set
G * m1 is Relation-like Function-like Element of the carrier of (G1,c₄)
the multF of (G1,c₄) . (G,m1) is Relation-like Function-like Element of the carrier of (G1,c₄)
[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,c₄) . [G,m1] is set
lF is Relation-like G1 -defined Function-like Carrier c₄ -compatible total Element of product (Carrier c₄)
dom lF is Element of bool G1
z is set
c₄ . z is set
f . z is set
f . z is set
c₁₃ is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of c₁₃ is non empty set
lpp is Element of the carrier of c₁₃
lpp " is Element of the carrier of c₁₃
the multF of (G1,c₄) . (f,m1) is set
[f,m1] is set
{f,m1} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,m1},{f}} is non empty finite V40() countable set
the multF of (G1,c₄) . [f,m1] is set
H is Relation-like G1 -defined Function-like Carrier c₄ -compatible total Element of product (Carrier c₄)
H . z is set
(lpp ") * lpp is Element of the carrier of c₁₃
the multF of c₁₃ is Relation-like [: the carrier of c₁₃, the carrier of c₁₃:] -defined the carrier of c₁₃ -valued Function-like quasi_total associative Element of bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:]
[: the carrier of c₁₃, the carrier of c₁₃:] is Relation-like non empty set
[:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is Relation-like non empty set
bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is non empty set
the multF of c₁₃ . ((lpp "),lpp) is Element of the carrier of c₁₃
[(lpp "),lpp] is set
{(lpp "),lpp} is non empty finite countable set
{(lpp ")} is non empty finite countable set
{{(lpp "),lpp},{(lpp ")}} is non empty finite V40() countable set
the multF of c₁₃ . [(lpp "),lpp] is set
1_ c₁₃ is non being_of_order_0 Element of the carrier of c₁₃
i is Relation-like G1 -defined Function-like Carrier c₄ -compatible total Element of product (Carrier c₄)
i . z is set
lF . z is set
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 . ((f . z),(H . z)) is set
[(f . z),(H . z)] is set
{(f . z),(H . z)} is non empty finite countable set
{(f . z)} is non empty finite countable set
{{(f . z),(H . z)},{(f . z)}} is non empty finite V40() countable set
the multF of k . [(f . z),(H . z)] is set
dom i is Element of bool G1
z is set
c₄ . z is set
f . z is set
f . z is set
c₁₃ is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of c₁₃ is non empty set
lpp is Element of the carrier of c₁₃
lpp " is Element of the carrier of c₁₃
the multF of (G1,c₄) . (m1,f) is set
[m1,f] is set
{m1,f} is functional non empty finite countable set
{{m1,f},{m1}} is non empty finite V40() countable set
the multF of (G1,c₄) . [m1,f] is set
H . z is set
lpp * (lpp ") is Element of the carrier of c₁₃
the multF of c₁₃ is Relation-like [: the carrier of c₁₃, the carrier of c₁₃:] -defined the carrier of c₁₃ -valued Function-like quasi_total associative Element of bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:]
[: the carrier of c₁₃, the carrier of c₁₃:] is Relation-like non empty set
[:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is Relation-like non empty set
bool [:[: the carrier of c₁₃, the carrier of c₁₃:], the carrier of c₁₃:] is non empty set
the multF of c₁₃ . (lpp,(lpp ")) is Element of the carrier of c₁₃
[lpp,(lpp ")] is set
{lpp,(lpp ")} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,(lpp ")},{lpp}} is non empty finite V40() countable set
the multF of c₁₃ . [lpp,(lpp ")] is set
1_ c₁₃ is non being_of_order_0 Element of the carrier of c₁₃
p is Relation-like G1 -defined Function-like Carrier c₄ -compatible total Element of product (Carrier c₄)
p . z is set
lF . z is set
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 . ((H . z),(f . z)) is set
[(H . z),(f . z)] is set
{(H . z),(f . z)} is non empty finite countable set
{(H . z)} is non empty finite countable set
{{(H . z),(f . z)},{(H . z)}} is non empty finite V40() countable set
the multF of k . [(H . z),(f . z)] is set
dom p is Element of bool G1
G1 is set
f is set
f is Relation-like Function-like set
f . f is set
c₄ is Relation-like Function-like set
c₄ . f is set
m1 is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) (G1) set
(G1,m1) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of (G1,m1) is non empty set
m1 . f is set
n1 is Relation-like Function-like Element of the carrier of (G1,m1)
n1 " is Relation-like Function-like Element of the carrier of (G1,m1)
G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G is non empty set
lF is Element of the carrier of G
lF " is Element of the carrier of G
the multF of (G1,m1) is Relation-like [: the carrier of (G1,m1), the carrier of (G1,m1):] -defined the carrier of (G1,m1) -valued Function-like quasi_total associative Element of bool [:[: the carrier of (G1,m1), the carrier of (G1,m1):], the carrier of (G1,m1):]
[: the carrier of (G1,m1), the carrier of (G1,m1):] is Relation-like non empty set
[:[: the carrier of (G1,m1), the carrier of (G1,m1):], the carrier of (G1,m1):] is Relation-like non empty set
bool [:[: the carrier of (G1,m1), the carrier of (G1,m1):], the carrier of (G1,m1):] is non empty set
the multF of (G1,m1) . (c₄,f) is set
[c₄,f] is set
{c₄,f} is functional non empty finite countable set
{c₄} is functional non empty finite with_common_domain countable set
{{c₄,f},{c₄}} is non empty finite V40() countable set
the multF of (G1,m1) . [c₄,f] is set
(n1 ") * n1 is Relation-like Function-like Element of the carrier of (G1,m1)
the multF of (G1,m1) . ((n1 "),n1) is Relation-like Function-like Element of the carrier of (G1,m1)
[(n1 "),n1] is set
{(n1 "),n1} is functional non empty finite countable set
{(n1 ")} is functional non empty finite with_common_domain countable set
{{(n1 "),n1},{(n1 ")}} is non empty finite V40() countable set
the multF of (G1,m1) . [(n1 "),n1] is set
1_ (G1,m1) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G1,m1)
Carrier m1 is Relation-like non-empty G1 -defined Function-like total set
product (Carrier m1) is functional non empty with_common_domain product-like set
i is Element of the carrier of G
i * lF 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 associative 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,lF) is Element of the carrier of G
[i,lF] is set
{i,lF} is non empty finite countable set
{i} is non empty finite countable set
{{i,lF},{i}} is non empty finite V40() countable set
the multF of G . [i,lF] is set
1_ G is non being_of_order_0 Element of the carrier of G
H is non empty multMagma
z is Relation-like Function-like set
z . f 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 . ((c₄ . f),(f . f)) is set
[(c₄ . f),(f . f)] is set
{(c₄ . f),(f . f)} is non empty finite countable set
{(c₄ . f)} is non empty finite countable set
{{(c₄ . f),(f . f)},{(c₄ . f)}} is non empty finite V40() countable set
the multF of H . [(c₄ . f),(f . f)] is set
the multF of (G1,m1) . (f,c₄) is set
[f,c₄] is set
{f,c₄} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,c₄},{f}} is non empty finite V40() countable set
the multF of (G1,m1) . [f,c₄] is set
n1 * (n1 ") is Relation-like Function-like Element of the carrier of (G1,m1)
the multF of (G1,m1) . (n1,(n1 ")) is Relation-like Function-like Element of the carrier of (G1,m1)
[n1,(n1 ")] is set
{n1,(n1 ")} is functional non empty finite countable set
{n1} is functional non empty finite with_common_domain countable set
{{n1,(n1 ")},{n1}} is non empty finite V40() countable set
the multF of (G1,m1) . [n1,(n1 ")] is set
lF * i is Element of the carrier of G
the multF of G . (lF,i) is Element of the carrier of G
[lF,i] is set
{lF,i} is non empty finite countable set
{lF} is non empty finite countable set
{{lF,i},{lF}} is non empty finite V40() countable set
the multF of G . [lF,i] is set
H is non empty multMagma
z is Relation-like Function-like set
z . f 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 . ((f . f),(c₄ . f)) is set
[(f . f),(c₄ . f)] is set
{(f . f),(c₄ . f)} is non empty finite countable set
{(f . f)} is non empty finite countable set
{{(f . f),(c₄ . f)},{(f . f)}} is non empty finite V40() countable set
the multF of H . [(f . f),(c₄ . f)] is set
G1 is set
f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) (G1) set
(G1,f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
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
bool G1 is non empty set
1_ (G1,f) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G1,f)
the carrier of (G1,f) is non empty set
dom (Carrier f) is Element of bool G1
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
dom m1 is Element of bool G1
n1 is set
G is set
{} G1 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() Element of bool G1
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper 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() Element of bool NAT
lF is Relation-like non-empty empty-yielding {} G1 -defined Function-like one-to-one constant functional empty total 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
m1 +* lF is Relation-like Function-like set
m1 +* {} is Relation-like Function-like set
p is set
f . p is set
lF . p 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
lF is finite countable Element of bool G1
p is Relation-like lF -defined Function-like total set
m1 +* p is Relation-like Function-like set
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 associative 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
G is non empty set
the multF of (G1,f) || G is Relation-like Function-like set
[:G,G:] is Relation-like non empty set
the multF of (G1,f) | [:G,G:] is Relation-like [:G,G:] -defined [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like 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
dom ( the multF of (G1,f) || G) is set
rng ( the multF of (G1,f) || G) is set
dom the multF of (G1,f) is Relation-like the carrier of (G1,f) -defined the carrier of (G1,f) -valued Element of bool [: the carrier of (G1,f), the carrier of (G1,f):]
bool [: the carrier of (G1,f), the carrier of (G1,f):] is non empty set
p is set
i is set
( the multF of (G1,f) || G) . i is set
H is set
z is set
[H,z] is set
{H,z} is non empty finite countable set
{H} is non empty finite countable set
{{H,z},{H}} is non empty finite V40() countable set
c₁₃ is finite countable Element of bool G1
lpp is Relation-like c₁₃ -defined Function-like total set
m1 +* lpp is Relation-like Function-like set
k is finite countable Element of bool G1
f is Relation-like k -defined Function-like total set
m1 +* f is Relation-like Function-like set
dom lpp is finite countable Element of bool c₁₃
bool c₁₃ is non empty finite V40() countable set
G is set
f . G is set
(Carrier f) . G is set
lpp . G is set
gf is Relation-like Function-like set
gf . G is set
j is non empty unital Group-like multMagma
the carrier of j is non empty set
1_ j is Element of the carrier of j
G is 1-sorted
the carrier of G is set
j is non empty unital Group-like multMagma
gf is Relation-like Function-like set
gf . G is set
m1 . G is set
1_ j is Element of the carrier of j
the carrier of j is non empty set
G is 1-sorted
the carrier of G is set
gf is Relation-like Function-like set
gf is Relation-like Function-like set
dom f is finite countable Element of bool k
bool k is non empty finite V40() countable set
G is set
f . G is set
(Carrier f) . G is set
f . G is set
i is Relation-like Function-like set
i . G is set
j is non empty unital Group-like multMagma
the carrier of j is non empty set
1_ j is Element of the carrier of j
G is 1-sorted
the carrier of G is set
j is non empty unital Group-like multMagma
i is Relation-like Function-like set
i . G is set
m1 . G is set
1_ j is Element of the carrier of j
the carrier of j is non empty set
G is 1-sorted
the carrier of G is set
i is Relation-like Function-like set
i is Relation-like Function-like set
dom gf is set
(dom m1) \/ (dom lpp) is set
dom i is set
(dom m1) \/ (dom f) is set
j is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
[j,G] is set
{j,G} is functional non empty finite countable set
{j} is functional non empty finite with_common_domain countable set
{{j,G},{j}} is non empty finite V40() countable set
G is Relation-like Function-like Element of the carrier of (G1,f)
m is Relation-like Function-like Element of the carrier of (G1,f)
G * m is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (G,m) is Relation-like Function-like Element of the carrier of (G1,f)
[G,m] is set
{G,m} is functional non empty finite countable set
{G} is functional non empty finite with_common_domain countable set
{{G,m},{G}} is non empty finite V40() countable set
the multF of (G1,f) . [G,m] is set
K is set
c₁₃ \/ k is finite countable Element of bool G1
(c₁₃ \/ k) \ K is finite countable Element of bool G1
ff is finite countable Element of bool G1
c₂₃ is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
dom c₂₃ is Element of bool G1
J is set
f . J is set
j . J is set
G . J is set
J is non empty unital Group-like multMagma
the carrier of J is non empty set
j is Element of the carrier of J
G is Element of the carrier of J
j * G is Element of the carrier of J
the multF of J is Relation-like [: the carrier of J, the carrier of J:] -defined the carrier of J -valued Function-like quasi_total Element of bool [:[: the carrier of J, the carrier of J:], the carrier of J:]
[: the carrier of J, the carrier of J:] is Relation-like non empty set
[:[: the carrier of J, the carrier of J:], the carrier of J:] is Relation-like non empty set
bool [:[: the carrier of J, the carrier of J:], the carrier of J:] is non empty set
the multF of J . (j,G) is Element of the carrier of J
[j,G] is set
{j,G} is non empty finite countable set
{j} is non empty finite countable set
{{j,G},{j}} is non empty finite V40() countable set
the multF of J . [j,G] is set
J is Relation-like ff -defined Function-like total set
m1 +* J is Relation-like Function-like set
dom J is finite countable Element of bool ff
bool ff is non empty finite V40() countable set
j is set
f . j is set
the multF of (G1,f) . (j,G) is set
the multF of (G1,f) . [j,G] is set
j . j is set
G . j is set
G is non empty multMagma
k1 is Relation-like Function-like set
k1 . j 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 . ((j . j),(G . j)) is set
[(j . j),(G . j)] is set
{(j . j),(G . j)} is non empty finite countable set
{(j . j)} is non empty finite countable set
{{(j . j),(G . j)},{(j . j)}} is non empty finite V40() countable set
the multF of G . [(j . j),(G . j)] is set
k2 is non empty unital Group-like multMagma
G2 is non empty unital Group-like multMagma
the carrier of G2 is non empty set
c₂₃ . j is set
x1i is Element of the carrier of G2
x2i is Element of the carrier of G2
x1i * x2i is Element of the carrier of G2
the multF of G2 is Relation-like [: the carrier of G2, the carrier of G2:] -defined the carrier of G2 -valued Function-like quasi_total Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
[: the carrier of G2, the carrier of G2:] is Relation-like non empty set
[:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is Relation-like non empty set
bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is non empty set
the multF of G2 . (x1i,x2i) is Element of the carrier of G2
[x1i,x2i] is set
{x1i,x2i} is non empty finite countable set
{x1i} is non empty finite countable set
{{x1i,x2i},{x1i}} is non empty finite V40() countable set
the multF of G2 . [x1i,x2i] is set
J . j is set
(m1 +* J) . j is set
c₃₅ is non empty unital Group-like multMagma
the carrier of c₃₅ is non empty set
c₃₆ is Element of the carrier of c₃₅
c₃₇ is Element of the carrier of c₃₅
c₃₆ * c₃₇ is Element of the carrier of c₃₅
the multF of c₃₅ is Relation-like [: the carrier of c₃₅, the carrier of c₃₅:] -defined the carrier of c₃₅ -valued Function-like quasi_total Element of bool [:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:]
[: the carrier of c₃₅, the carrier of c₃₅:] is Relation-like non empty set
[:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:] is Relation-like non empty set
bool [:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:] is non empty set
the multF of c₃₅ . (c₃₆,c₃₇) is Element of the carrier of c₃₅
[c₃₆,c₃₇] is set
{c₃₆,c₃₇} is non empty finite countable set
{c₃₆} is non empty finite countable set
{{c₃₆,c₃₇},{c₃₆}} is non empty finite V40() countable set
the multF of c₃₅ . [c₃₆,c₃₇] is set
(m1 +* J) . j is set
m1 . j is set
1_ k2 is Element of the carrier of k2
the carrier of k2 is non empty set
lpp . j is set
f . j is set
c₃₅ is non empty unital Group-like multMagma
the carrier of c₃₅ is non empty set
c₃₆ is Element of the carrier of c₃₅
c₃₇ is Element of the carrier of c₃₅
c₃₆ * c₃₇ is Element of the carrier of c₃₅
the multF of c₃₅ is Relation-like [: the carrier of c₃₅, the carrier of c₃₅:] -defined the carrier of c₃₅ -valued Function-like quasi_total Element of bool [:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:]
[: the carrier of c₃₅, the carrier of c₃₅:] is Relation-like non empty set
[:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:] is Relation-like non empty set
bool [:[: the carrier of c₃₅, the carrier of c₃₅:], the carrier of c₃₅:] is non empty set
the multF of c₃₅ . (c₃₆,c₃₇) is Element of the carrier of c₃₅
[c₃₆,c₃₇] is set
{c₃₆,c₃₇} is non empty finite countable set
{c₃₆} is non empty finite countable set
{{c₃₆,c₃₇},{c₃₆}} is non empty finite V40() countable set
the multF of c₃₅ . [c₃₆,c₃₇] is set
1_ c₃₅ is Element of the carrier of c₃₅
dom (m1 +* J) is set
(dom m1) \/ (dom J) is set
j is set
f . j is set
J . j is set
j . j is set
G . j is set
G is non empty unital Group-like multMagma
the carrier of G is non empty set
k1 is Element of the carrier of G
k2 is Element of the carrier of G
k1 * k2 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 . (k1,k2) is Element of the carrier of G
[k1,k2] is set
{k1,k2} is non empty finite countable set
{k1} is non empty finite countable set
{{k1,k2},{k1}} is non empty finite V40() countable set
the multF of G . [k1,k2] is set
1_ G is Element of the carrier of G
lpp . j is set
G2 is non empty unital Group-like multMagma
the carrier of G2 is non empty set
1_ G2 is Element of the carrier of G2
m1 . j is set
f . j is set
G2 is non empty unital Group-like multMagma
the carrier of G2 is non empty set
1_ G2 is Element of the carrier of G2
m1 . j is set
f . j is set
lpp . j is set
G2 is non empty unital Group-like multMagma
the carrier of G2 is non empty set
1_ G2 is Element of the carrier of G2
x1i is non empty unital Group-like multMagma
the carrier of x1i is non empty set
1_ x1i is Element of the carrier of x1i
J is finite countable Element of bool G1
J is finite countable Element of bool G1
ff is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
j is set
f . j is set
ff . j is set
J is finite countable Element of bool G1
J is finite countable Element of bool G1
j is Relation-like J -defined Function-like total set
m1 +* j is Relation-like Function-like set
[:[:G,G:],G:] is Relation-like non empty set
bool [:[:G,G:],G:] is non empty set
p is Relation-like [:G,G:] -defined G -valued Function-like quasi_total Element of bool [:[:G,G:],G:]
multMagma(# G,p #) is strict multMagma
the carrier of multMagma(# G,p #) is set
z is finite countable Element of bool G1
c₁₃ is Relation-like z -defined Function-like total set
m1 +* c₁₃ is Relation-like Function-like set
H is Element of the carrier of multMagma(# G,p #)
z is Element of the carrier of multMagma(# G,p #)
z * H is Element of the carrier of multMagma(# G,p #)
the multF of multMagma(# G,p #) is Relation-like [: the carrier of multMagma(# G,p #), the carrier of multMagma(# G,p #):] -defined the carrier of multMagma(# G,p #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# G,p #), the carrier of multMagma(# G,p #):], the carrier of multMagma(# G,p #):]
[: the carrier of multMagma(# G,p #), the carrier of multMagma(# G,p #):] is Relation-like set
[:[: the carrier of multMagma(# G,p #), the carrier of multMagma(# G,p #):], the carrier of multMagma(# G,p #):] is Relation-like set
bool [:[: the carrier of multMagma(# G,p #), the carrier of multMagma(# G,p #):], the carrier of multMagma(# G,p #):] is non empty set
the multF of multMagma(# G,p #) . (z,H) is Element of the carrier of multMagma(# G,p #)
[z,H] is set
{z,H} is non empty finite countable set
{z} is non empty finite countable set
{{z,H},{z}} is non empty finite V40() countable set
the multF of multMagma(# G,p #) . [z,H] is set
H * z is Element of the carrier of multMagma(# G,p #)
the multF of multMagma(# G,p #) . (H,z) is Element of the carrier of multMagma(# G,p #)
[H,z] is set
{H,z} is non empty finite countable set
{H} is non empty finite countable set
{{H,z},{H}} is non empty finite V40() countable set
the multF of multMagma(# G,p #) . [H,z] is set
c₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
c₁₃ * (1_ (G1,f)) is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c₁₃,(1_ (G1,f))) is Relation-like Function-like Element of the carrier of (G1,f)
[c₁₃,(1_ (G1,f))] is set
{c₁₃,(1_ (G1,f))} is functional non empty finite countable set
{c₁₃} is functional non empty finite with_common_domain countable set
{{c₁₃,(1_ (G1,f))},{c₁₃}} is non empty finite V40() countable set
the multF of (G1,f) . [c₁₃,(1_ (G1,f))] is set
(1_ (G1,f)) * c₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((1_ (G1,f)),c₁₃) is Relation-like Function-like Element of the carrier of (G1,f)
[(1_ (G1,f)),c₁₃] is set
{(1_ (G1,f)),c₁₃} is functional non empty finite countable set
{(1_ (G1,f))} is functional non empty finite with_common_domain countable set
{{(1_ (G1,f)),c₁₃},{(1_ (G1,f))}} is non empty finite V40() countable set
the multF of (G1,f) . [(1_ (G1,f)),c₁₃] is set
c₁₃ " is Relation-like Function-like Element of the carrier of (G1,f)
f is finite countable Element of bool G1
gf is Relation-like f -defined Function-like total set
m1 +* gf is Relation-like Function-like set
i is set
f . i is set
gf . i is set
G is non empty unital Group-like multMagma
G is non empty associative multMagma
j is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of j is non empty set
m is non empty unital Group-like multMagma
the carrier of m is non empty set
1_ m is Element of the carrier of m
G is Element of the carrier of j
G " is Element of the carrier of j
i is Relation-like f -defined Function-like total set
m1 +* i is Relation-like Function-like set
dom i is finite countable Element of bool f
bool f is non empty finite V40() countable set
dom gf is finite countable Element of bool f
j is set
f . j is set
G is non empty unital Group-like multMagma
m is non empty associative multMagma
m is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
(m1 +* i) . j is set
i . j is set
gf . j is set
lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
lpp . j is set
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
k . j is set
c₂₃ is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of c₂₃ is non empty set
K is Element of the carrier of c₂₃
K " is Element of the carrier of c₂₃
(m1 +* i) . j is set
m1 . j is set
1_ G is Element of the carrier of G
the carrier of G is non empty set
1_ m is non being_of_order_0 Element of the carrier of m
the carrier of m is non empty set
(1_ m) " is Element of the carrier of m
lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
lpp . j is set
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
k . j is set
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
dom k is Element of bool G1
dom (m1 +* i) is set
(dom m1) \/ (dom i) is set
j is set
f . j is set
i . j is set
gf . j is set
G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G is non empty set
m is Element of the carrier of G
m " is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
c₂₃ is non empty unital Group-like multMagma
the carrier of c₂₃ is non empty set
1_ c₂₃ is Element of the carrier of c₂₃
gf is finite countable Element of bool G1
i is Relation-like gf -defined Function-like total set
m1 +* i is Relation-like Function-like set
f is Element of the carrier of multMagma(# G,p #)
z * f is Element of the carrier of multMagma(# G,p #)
the multF of multMagma(# G,p #) . (z,f) is Element of the carrier of multMagma(# G,p #)
[z,f] is set
{z,f} is non empty finite countable set
{{z,f},{z}} is non empty finite V40() countable set
the multF of multMagma(# G,p #) . [z,f] is set
f * z is Element of the carrier of multMagma(# G,p #)
the multF of multMagma(# G,p #) . (f,z) is Element of the carrier of multMagma(# G,p #)
[f,z] is set
{f,z} is non empty finite countable set
{f} is non empty finite countable set
{{f,z},{f}} is non empty finite V40() countable set
the multF of multMagma(# G,p #) . [f,z] is set
c₁₃ * (c₁₃ ") is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c₁₃,(c₁₃ ")) is Relation-like Function-like Element of the carrier of (G1,f)
[c₁₃,(c₁₃ ")] is set
{c₁₃,(c₁₃ ")} is functional non empty finite countable set
{{c₁₃,(c₁₃ ")},{c₁₃}} is non empty finite V40() countable set
the multF of (G1,f) . [c₁₃,(c₁₃ ")] is set
(c₁₃ ") * c₁₃ is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((c₁₃ "),c₁₃) is Relation-like Function-like Element of the carrier of (G1,f)
[(c₁₃ "),c₁₃] is set
{(c₁₃ "),c₁₃} is functional non empty finite countable set
{(c₁₃ ")} is functional non empty finite with_common_domain countable set
{{(c₁₃ "),c₁₃},{(c₁₃ ")}} is non empty finite V40() countable set
the multF of (G1,f) . [(c₁₃ "),c₁₃] is set
H is non empty unital Group-like multMagma
z is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() Subgroup of (G1,f)
the carrier of z is non empty set
c₁₃ is set
lpp is finite countable Element of bool G1
k is Relation-like lpp -defined Function-like total set
m1 +* k is Relation-like Function-like set
k is finite countable Element of bool G1
lpp is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
f is Relation-like k -defined Function-like total set
lpp +* f is Relation-like Function-like set
dom lpp is Element of bool G1
dom f is finite countable Element of bool k
bool k is non empty finite V40() countable set
i is set
f . i is set
(Carrier f) . i is set
f . i is set
(lpp +* f) . i is set
G is non empty unital Group-like multMagma
the carrier of G is non empty set
1_ G is Element of the carrier of G
j is 1-sorted
the carrier of j is set
G is non empty unital Group-like multMagma
(lpp +* f) . i is set
lpp . i is set
1_ G is Element of the carrier of G
the carrier of G is non empty set
j is 1-sorted
the carrier of j is set
dom (lpp +* f) is set
(dom lpp) \/ (dom f) is set
f is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() Subgroup of (G1,f)
the carrier of f is non empty set
c₄ is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() Subgroup of (G1,f)
the carrier of c₄ is non empty set
G1 is set
f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) (G1) set
(G1,f) is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() Subgroup of (G1,f)
(G1,f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of (G1,f) is non empty set
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 associative 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
f is Element of the carrier of (G1,f)
c₄ is Element of the carrier of (G1,f)
the multF of (G1,f) . (f,c₄) is Element of the carrier of (G1,f)
[f,c₄] is set
{f,c₄} is non empty finite countable set
{f} is non empty finite countable set
{{f,c₄},{f}} is non empty finite V40() countable set
the multF of (G1,f) . [f,c₄] is set
the carrier of (G1,f) is non empty 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
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
G1 is finite countable set
f is Relation-like G1 -defined Function-like total 1-sorted-yielding () (G1) (G1) set
(G1,f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
(G1,f) is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() Subgroup of (G1,f)
the carrier of (G1,f) is non empty set
the carrier of (G1,f) is non empty 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
1_ (G1,f) is Relation-like Function-like non being_of_order_0 Element of the carrier of (G1,f)
n1 is set
lF is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
dom lF is finite countable Element of bool G1
bool G1 is non empty finite V40() countable set
G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
dom G is finite countable Element of bool G1
bool G1 is non empty finite V40() countable set
lF is Relation-like G1 -defined Function-like total set
p is set
i is set
i is finite countable Element of bool G1
H is Relation-like i -defined Function-like total set
dom H is finite countable Element of bool i
bool i is non empty finite V40() countable set
z is set
lF . z is set
H . z is set
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
m1 +* H is Relation-like Function-like set
(m1 +* H) . z is set
f . z is set
c₁₃ is non empty unital Group-like multMagma
lF . z is set
the carrier of c₁₃ is non empty set
1_ c₁₃ is Element of the carrier of c₁₃
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
m1 . z is set
m1 +* H is Relation-like Function-like set
(m1 +* H) . z is set
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
m1 +* H is Relation-like Function-like set
m1 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
m1 +* H is Relation-like Function-like set
dom m1 is finite countable Element of bool G1
dom (m1 +* H) is set
(dom m1) \/ (dom H) is finite countable set
z is set
f . z is set
H . z is set
lF . z is set
c₁₃ is non empty unital Group-like multMagma
the carrier of c₁₃ is non empty set
lpp is Element of the carrier of c₁₃
1_ c₁₃ is Element of the carrier of c₁₃
i is finite countable Element of bool G1
p is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
H is Relation-like i -defined Function-like total set
p +* H is Relation-like Function-like set
G1 is non empty multMagma
<*G1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
dom <*G1*> is non empty finite countable Element of bool NAT
f is Relation-like {1} -defined Function-like total set
f is set
rng f is set
dom f is finite countable Element of bool {1}
bool {1} is non empty finite V40() countable set
c₄ is set
f . c₄ is set
G1 is non empty multMagma
<*G1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty unital Group-like multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
f is Relation-like {1} -defined Function-like total 1-sorted-yielding () set
f is Element of {1}
({1},f,f) is non empty multMagma
G1 is non empty unital Group-like multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty associative multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
f is Relation-like {1} -defined Function-like total 1-sorted-yielding () set
f is Element of {1}
({1},f,f) is non empty multMagma
G1 is non empty associative multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty commutative multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
f is Relation-like {1} -defined Function-like total 1-sorted-yielding () set
f is Element of {1}
({1},f,f) is non empty multMagma
G1 is non empty commutative multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
G1 is non empty multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
Carrier <*G1*> is Relation-like non-empty {1} -defined Function-like total set
product (Carrier <*G1*>) is functional non empty with_common_domain product-like set
f is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total Element of product (Carrier <*G1*>)
dom f is set
dom f is finite countable Element of bool {1}
bool {1} is non empty finite V40() countable set
dom (Carrier <*G1*>) is finite countable Element of bool {1}
G1 is non empty multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict constituted-Functions multMagma
the carrier of ({1},<*G1*>) is non empty set
f is Relation-like Function-like Element of the carrier of ({1},<*G1*>)
Carrier <*G1*> is Relation-like non-empty {1} -defined Function-like total set
product (Carrier <*G1*>) is functional non empty with_common_domain product-like set
f is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1*>)
G1 is non empty multMagma
the carrier of G1 is non empty set
f is Element of the carrier of G1
<*f*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict constituted-Functions multMagma
the carrier of ({1},<*G1*>) is non empty set
<*f*> is Relation-like NAT -defined the carrier of G1 -valued Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G1
Carrier <*G1*> is Relation-like non-empty {1} -defined Function-like total set
dom (Carrier <*G1*>) is finite countable Element of bool {1}
bool {1} is non empty finite V40() countable set
<*G1*> . 1 is set
<*f*> . 1 is set
m1 is set
<*f*> . m1 is set
(Carrier <*G1*>) . m1 is set
(Carrier <*G1*>) . 1 is set
n1 is 1-sorted
the carrier of n1 is set
dom <*f*> is non empty finite countable Element of bool NAT
product (Carrier <*G1*>) is functional non empty with_common_domain product-like set
G1 is non empty multMagma
f is non empty multMagma
<*G1,f*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
K247(1,1) is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
dom <*G1,f*> is non empty finite countable Element of bool NAT
f is Relation-like {1,2} -defined Function-like total set
c₄ is set
rng f is set
dom f is finite countable Element of bool {1,2}
bool {1,2} is non empty finite V40() countable set
m1 is set
f . m1 is set
G1 is non empty multMagma
f is non empty multMagma
<*G1,f*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
K247(1,1) is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
G1 is non empty multMagma
f is non empty multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
f is Relation-like {1,2} -defined Function-like total 1-sorted-yielding () set
c₄ is Element of {1,2}
({1,2},f,c₄) is non empty multMagma
G1 is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty associative multMagma
f is non empty associative multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
f is Relation-like {1,2} -defined Function-like total 1-sorted-yielding () set
c₄ is Element of {1,2}
({1,2},f,c₄) is non empty multMagma
G1 is non empty associative multMagma
f is non empty associative multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty commutative multMagma
f is non empty commutative multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
f is Relation-like {1,2} -defined Function-like total 1-sorted-yielding () set
c₄ is Element of {1,2}
({1,2},f,c₄) is non empty multMagma
G1 is non empty commutative multMagma
f is non empty commutative multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2}) ({1,2}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2}) ({1,2}) ({1,2}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty multMagma
f is non empty multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
Carrier <*G1,f*> is Relation-like non-empty {1,2} -defined Function-like total set
product (Carrier <*G1,f*>) is functional non empty with_common_domain product-like set
f is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total Element of product (Carrier <*G1,f*>)
dom f is set
dom f is finite countable Element of bool {1,2}
bool {1,2} is non empty finite V40() countable set
dom (Carrier <*G1,f*>) is finite countable Element of bool {1,2}
G1 is non empty multMagma
f is non empty multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
({1,2},<*G1,f*>) is non empty strict constituted-Functions multMagma
the carrier of ({1,2},<*G1,f*>) is non empty set
f is Relation-like Function-like Element of the carrier of ({1,2},<*G1,f*>)
Carrier <*G1,f*> is Relation-like non-empty {1,2} -defined Function-like total set
product (Carrier <*G1,f*>) is functional non empty with_common_domain product-like set
c₄ is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
G1 is non empty multMagma
the carrier of G1 is non empty set
f is non empty multMagma
the carrier of f is non empty set
f is Element of the carrier of G1
c₄ is Element of the carrier of f
<*f,c₄*> is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
K230(<*f*>,<*c₄*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
({1,2},<*G1,f*>) is non empty strict constituted-Functions multMagma
the carrier of ({1,2},<*G1,f*>) is non empty set
Carrier <*G1,f*> is Relation-like non-empty {1,2} -defined Function-like total set
dom (Carrier <*G1,f*>) is finite countable Element of bool {1,2}
bool {1,2} is non empty finite V40() countable set
<*f,c₄*> . 2 is set
<*G1,f*> . 2 is set
<*G1,f*> . 1 is set
<*f,c₄*> . 1 is set
G is set
<*f,c₄*> . G is set
(Carrier <*G1,f*>) . G is set
(Carrier <*G1,f*>) . 1 is set
lF is 1-sorted
the carrier of lF is set
(Carrier <*G1,f*>) . 2 is set
lF is 1-sorted
the carrier of lF is set
dom <*f,c₄*> is non empty finite countable Element of bool NAT
product (Carrier <*G1,f*>) is functional non empty with_common_domain product-like set
G1 is non empty multMagma
f is non empty multMagma
f is non empty multMagma
<*G1,f,f*> is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
K247(K247(1,1),1) is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
dom <*G1,f,f*> is non empty finite countable Element of bool NAT
c₄ is Relation-like {1,2,3} -defined Function-like total set
m1 is set
rng c₄ is set
dom c₄ is finite countable Element of bool {1,2,3}
bool {1,2,3} is non empty finite V40() countable set
n1 is set
c₄ . n1 is set
G1 is non empty multMagma
f is non empty multMagma
f is non empty multMagma
<*G1,f,f*> is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
K247(K247(1,1),1) is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
G1 is non empty multMagma
f is non empty multMagma
f is non empty multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
c₄ is Relation-like {1,2,3} -defined Function-like total 1-sorted-yielding () set
m1 is Element of {1,2,3}
({1,2,3},c₄,m1) is non empty multMagma
G1 is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
f is non empty unital Group-like multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty associative multMagma
f is non empty associative multMagma
f is non empty associative multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
c₄ is Relation-like {1,2,3} -defined Function-like total 1-sorted-yielding () set
m1 is Element of {1,2,3}
({1,2,3},c₄,m1) is non empty multMagma
G1 is non empty associative multMagma
f is non empty associative multMagma
f is non empty associative multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty commutative multMagma
f is non empty commutative multMagma
f is non empty commutative multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
c₄ is Relation-like {1,2,3} -defined Function-like total 1-sorted-yielding () set
m1 is Element of {1,2,3}
({1,2,3},c₄,m1) is non empty multMagma
G1 is non empty commutative multMagma
f is non empty commutative multMagma
f is non empty commutative multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2,3}) ({1,2,3}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2,3}) ({1,2,3}) ({1,2,3}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
G1 is non empty multMagma
f is non empty multMagma
f is non empty multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
Carrier <*G1,f,f*> is Relation-like non-empty {1,2,3} -defined Function-like total set
product (Carrier <*G1,f,f*>) is functional non empty with_common_domain product-like set
c₄ is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total Element of product (Carrier <*G1,f,f*>)
dom c₄ is set
dom c₄ is finite countable Element of bool {1,2,3}
bool {1,2,3} is non empty finite V40() countable set
dom (Carrier <*G1,f,f*>) is finite countable Element of bool {1,2,3}
G1 is non empty multMagma
f is non empty multMagma
f is non empty multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
({1,2,3},<*G1,f,f*>) is non empty strict constituted-Functions multMagma
the carrier of ({1,2,3},<*G1,f,f*>) is non empty set
c₄ is Relation-like Function-like Element of the carrier of ({1,2,3},<*G1,f,f*>)
Carrier <*G1,f,f*> is Relation-like non-empty {1,2,3} -defined Function-like total set
product (Carrier <*G1,f,f*>) is functional non empty with_common_domain product-like set
m1 is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
G1 is non empty multMagma
the carrier of G1 is non empty set
f is non empty multMagma
the carrier of f is non empty set
f is non empty multMagma
the carrier of f is non empty set
c₄ is Element of the carrier of G1
m1 is Element of the carrier of f
n1 is Element of the carrier of f
<*c₄,m1,n1*> is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable set
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
<*m1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
K230(<*c₄*>,<*m1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*n1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,n1] is set
{1,n1} is non empty finite countable set
{{1,n1},{1}} is non empty finite V40() countable set
{[1,n1]} is Relation-like Function-like non empty finite countable set
K230(K230(<*c₄*>,<*m1*>),<*n1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
({1,2,3},<*G1,f,f*>) is non empty strict constituted-Functions multMagma
the carrier of ({1,2,3},<*G1,f,f*>) is non empty set
Carrier <*G1,f,f*> is Relation-like non-empty {1,2,3} -defined Function-like total set
dom (Carrier <*G1,f,f*>) is finite countable Element of bool {1,2,3}
bool {1,2,3} is non empty finite V40() countable set
<*c₄,m1,n1*> . 2 is set
<*G1,f,f*> . 1 is set
<*c₄,m1,n1*> . 3 is set
<*G1,f,f*> . 3 is set
<*G1,f,f*> . 2 is set
<*c₄,m1,n1*> . 1 is set
p is set
<*c₄,m1,n1*> . p is set
(Carrier <*G1,f,f*>) . p is set
(Carrier <*G1,f,f*>) . 1 is set
i is 1-sorted
the carrier of i is set
(Carrier <*G1,f,f*>) . 2 is set
i is 1-sorted
the carrier of i is set
(Carrier <*G1,f,f*>) . 3 is set
i is 1-sorted
the carrier of i is set
dom <*c₄,m1,n1*> is non empty finite countable Element of bool NAT
product (Carrier <*G1,f,f*>) is functional non empty with_common_domain product-like set
G1 is non empty multMagma
the carrier of G1 is non empty set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict constituted-Functions multMagma
f is Element of the carrier of G1
(G1,f) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the carrier of ({1},<*G1*>) is non empty set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
f is Element of the carrier of G1
(G1,f) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
(G1,f) * (G1,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the multF of ({1},<*G1*>) is Relation-like [: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):] -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total Element of bool [:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):]
[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):] is Relation-like non empty set
[:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):] is Relation-like non empty set
bool [:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):] is non empty set
the multF of ({1},<*G1*>) . ((G1,f),(G1,f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[(G1,f),(G1,f)] is set
{(G1,f),(G1,f)} is functional non empty finite V40() countable set
{(G1,f)} is functional non empty finite V40() with_common_domain countable set
{{(G1,f),(G1,f)},{(G1,f)}} is non empty finite V40() countable set
the multF of ({1},<*G1*>) . [(G1,f),(G1,f)] is set
f * f is Element of the carrier of G1
the multF of G1 is Relation-like [: the carrier of G1, the carrier of G1:] -defined the carrier of G1 -valued Function-like quasi_total Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is Relation-like non empty set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is Relation-like non empty set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is non empty set
the multF of G1 . (f,f) is Element of the carrier of G1
[f,f] is set
{f,f} is non empty finite countable set
{f} is non empty finite countable set
{{f,f},{f}} is non empty finite V40() countable set
the multF of G1 . [f,f] is set
(G1,(f * f)) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,(f * f)] is set
{1,(f * f)} is non empty finite countable set
{{1,(f * f)},{1}} is non empty finite V40() countable set
{[1,(f * f)]} is Relation-like Function-like non empty finite countable set
<*G1*> . 1 is set
Carrier <*G1*> is Relation-like non-empty {1} -defined Function-like total set
product (Carrier <*G1*>) is functional non empty with_common_domain product-like set
m1 is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1*>)
m1 . 1 is set
n1 is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1*>)
n1 . 1 is set
lF is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1*>)
lF . 1 is set
G is Relation-like {1} -defined Function-like Carrier <*G1*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1*>)
p is ext-real V27() V28() V29() V33() V34() V103() set
G . p is set
lF . p is set
dom G is finite countable Element of bool {1}
bool {1} is non empty finite V40() countable set
dom (Carrier <*G1*>) is finite countable Element of bool {1}
len G is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
len lF is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
G1 is non empty multMagma
the carrier of G1 is non empty set
f is non empty multMagma
the carrier of f is non empty set
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
({1,2},<*G1,f*>) is non empty strict constituted-Functions multMagma
f is Element of the carrier of G1
c₄ is Element of the carrier of G1
f * c₄ is Element of the carrier of G1
the multF of G1 is Relation-like [: the carrier of G1, the carrier of G1:] -defined the carrier of G1 -valued Function-like quasi_total Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is Relation-like non empty set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is Relation-like non empty set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is non empty set
the multF of G1 . (f,c₄) is Element of the carrier of G1
[f,c₄] is set
{f,c₄} is non empty finite countable set
{f} is non empty finite countable set
{{f,c₄},{f}} is non empty finite V40() countable set
the multF of G1 . [f,c₄] is set
m1 is Element of the carrier of f
(G1,f,f,m1) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
the carrier of ({1,2},<*G1,f*>) is non empty set
<*f*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
<*m1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
K230(<*f*>,<*m1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
n1 is Element of the carrier of f
(G1,f,c₄,n1) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
<*n1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,n1] is set
{1,n1} is non empty finite countable set
{{1,n1},{1}} is non empty finite V40() countable set
{[1,n1]} is Relation-like Function-like non empty finite countable set
K230(<*c₄*>,<*n1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
(G1,f,f,m1) * (G1,f,c₄,n1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
the multF of ({1,2},<*G1,f*>) is Relation-like [: the carrier of ({1,2},<*G1,f*>), the carrier of ({1,2},<*G1,f*>):] -defined the carrier of ({1,2},<*G1,f*>) -valued Function-like quasi_total Element of bool [:[: the carrier of ({1,2},<*G1,f*>), the carrier of ({1,2},<*G1,f*>):], the carrier of ({1,2},<*G1,f*>):]
[: the carrier of ({1,2},<*G1,f*>), the carrier of ({1,2},<*G1,f*>):] is Relation-like non empty set
[:[: the carrier of ({1,2},<*G1,f*>), the carrier of ({1,2},<*G1,f*>):], the carrier of ({1,2},<*G1,f*>):] is Relation-like non empty set
bool [:[: the carrier of ({1,2},<*G1,f*>), the carrier of ({1,2},<*G1,f*>):], the carrier of ({1,2},<*G1,f*>):] is non empty set
the multF of ({1,2},<*G1,f*>) . ((G1,f,f,m1),(G1,f,c₄,n1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
[(G1,f,f,m1),(G1,f,c₄,n1)] is set
{(G1,f,f,m1),(G1,f,c₄,n1)} is functional non empty finite V40() countable set
{(G1,f,f,m1)} is functional non empty finite V40() with_common_domain countable set
{{(G1,f,f,m1),(G1,f,c₄,n1)},{(G1,f,f,m1)}} is non empty finite V40() countable set
the multF of ({1,2},<*G1,f*>) . [(G1,f,f,m1),(G1,f,c₄,n1)] is set
m1 * n1 is Element of the carrier of f
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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of f . (m1,n1) is Element of the carrier of f
[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 set
the multF of f . [m1,n1] is set
(G1,f,(f * c₄),(m1 * n1)) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
<*(f * c₄)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(f * c₄)] is set
{1,(f * c₄)} is non empty finite countable set
{{1,(f * c₄)},{1}} is non empty finite V40() countable set
{[1,(f * c₄)]} is Relation-like Function-like non empty finite countable set
<*(m1 * n1)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(m1 * n1)] is set
{1,(m1 * n1)} is non empty finite countable set
{{1,(m1 * n1)},{1}} is non empty finite V40() countable set
{[1,(m1 * n1)]} is Relation-like Function-like non empty finite countable set
K230(<*(f * c₄)*>,<*(m1 * n1)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*G1,f*> . 1 is set
<*G1,f*> . 2 is set
Carrier <*G1,f*> is Relation-like non-empty {1,2} -defined Function-like total set
product (Carrier <*G1,f*>) is functional non empty with_common_domain product-like set
lF is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
lF . 1 is set
H is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
H . 1 is set
p is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
p . 2 is set
H . 2 is set
p . 1 is set
lF . 2 is set
i is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
z is ext-real V27() V28() V29() V33() V34() V103() set
i . z is set
H . z is set
dom i is finite countable Element of bool {1,2}
bool {1,2} is non empty finite V40() countable set
dom (Carrier <*G1,f*>) is finite countable Element of bool {1,2}
len i is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
len H is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
G1 is non empty multMagma
the carrier of G1 is non empty set
f is non empty multMagma
the carrier of f is non empty set
f is non empty multMagma
the carrier of f is non empty set
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
({1,2,3},<*G1,f,f*>) is non empty strict constituted-Functions multMagma
c₄ is Element of the carrier of G1
m1 is Element of the carrier of G1
c₄ * m1 is Element of the carrier of G1
the multF of G1 is Relation-like [: the carrier of G1, the carrier of G1:] -defined the carrier of G1 -valued Function-like quasi_total Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is Relation-like non empty set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is Relation-like non empty set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is non empty set
the multF of G1 . (c₄,m1) is Element of the carrier of G1
[c₄,m1] is set
{c₄,m1} is non empty finite countable set
{c₄} is non empty finite countable set
{{c₄,m1},{c₄}} is non empty finite V40() countable set
the multF of G1 . [c₄,m1] is set
n1 is Element of the carrier of f
G is Element of the carrier of f
n1 * G is Element of the carrier of f
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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of f . (n1,G) is Element of the carrier of f
[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
lF is Element of the carrier of f
(G1,f,f,c₄,n1,lF) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
the carrier of ({1,2,3},<*G1,f,f*>) is non empty set
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
<*n1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,n1] is set
{1,n1} is non empty finite countable set
{{1,n1},{1}} is non empty finite V40() countable set
{[1,n1]} is Relation-like Function-like non empty finite countable set
K230(<*c₄*>,<*n1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*lF*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,lF] is set
{1,lF} is non empty finite countable set
{{1,lF},{1}} is non empty finite V40() countable set
{[1,lF]} is Relation-like Function-like non empty finite countable set
K230(K230(<*c₄*>,<*n1*>),<*lF*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
p is Element of the carrier of f
(G1,f,f,m1,G,p) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
<*m1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
<*G*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,G] is set
{1,G} is non empty finite countable set
{{1,G},{1}} is non empty finite V40() countable set
{[1,G]} is Relation-like Function-like non empty finite countable set
K230(<*m1*>,<*G*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*p*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,p] is set
{1,p} is non empty finite countable set
{{1,p},{1}} is non empty finite V40() countable set
{[1,p]} is Relation-like Function-like non empty finite countable set
K230(K230(<*m1*>,<*G*>),<*p*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
(G1,f,f,c₄,n1,lF) * (G1,f,f,m1,G,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
the multF of ({1,2,3},<*G1,f,f*>) is Relation-like [: the carrier of ({1,2,3},<*G1,f,f*>), the carrier of ({1,2,3},<*G1,f,f*>):] -defined the carrier of ({1,2,3},<*G1,f,f*>) -valued Function-like quasi_total Element of bool [:[: the carrier of ({1,2,3},<*G1,f,f*>), the carrier of ({1,2,3},<*G1,f,f*>):], the carrier of ({1,2,3},<*G1,f,f*>):]
[: the carrier of ({1,2,3},<*G1,f,f*>), the carrier of ({1,2,3},<*G1,f,f*>):] is Relation-like non empty set
[:[: the carrier of ({1,2,3},<*G1,f,f*>), the carrier of ({1,2,3},<*G1,f,f*>):], the carrier of ({1,2,3},<*G1,f,f*>):] is Relation-like non empty set
bool [:[: the carrier of ({1,2,3},<*G1,f,f*>), the carrier of ({1,2,3},<*G1,f,f*>):], the carrier of ({1,2,3},<*G1,f,f*>):] is non empty set
the multF of ({1,2,3},<*G1,f,f*>) . ((G1,f,f,c₄,n1,lF),(G1,f,f,m1,G,p)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
[(G1,f,f,c₄,n1,lF),(G1,f,f,m1,G,p)] is set
{(G1,f,f,c₄,n1,lF),(G1,f,f,m1,G,p)} is functional non empty finite V40() countable set
{(G1,f,f,c₄,n1,lF)} is functional non empty finite V40() with_common_domain countable set
{{(G1,f,f,c₄,n1,lF),(G1,f,f,m1,G,p)},{(G1,f,f,c₄,n1,lF)}} is non empty finite V40() countable set
the multF of ({1,2,3},<*G1,f,f*>) . [(G1,f,f,c₄,n1,lF),(G1,f,f,m1,G,p)] is set
lF * p is Element of the carrier of f
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 non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of f . (lF,p) is Element of the carrier of f
[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 f . [lF,p] is set
(G1,f,f,(c₄ * m1),(n1 * G),(lF * p)) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
<*(c₄ * m1)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(c₄ * m1)] is set
{1,(c₄ * m1)} is non empty finite countable set
{{1,(c₄ * m1)},{1}} is non empty finite V40() countable set
{[1,(c₄ * m1)]} is Relation-like Function-like non empty finite countable set
<*(n1 * G)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(n1 * G)] is set
{1,(n1 * G)} is non empty finite countable set
{{1,(n1 * G)},{1}} is non empty finite V40() countable set
{[1,(n1 * G)]} is Relation-like Function-like non empty finite countable set
K230(<*(c₄ * m1)*>,<*(n1 * G)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*(lF * p)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(lF * p)] is set
{1,(lF * p)} is non empty finite countable set
{{1,(lF * p)},{1}} is non empty finite V40() countable set
{[1,(lF * p)]} is Relation-like Function-like non empty finite countable set
K230(K230(<*(c₄ * m1)*>,<*(n1 * G)*>),<*(lF * p)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
<*G1,f,f*> . 1 is set
<*G1,f,f*> . 3 is set
<*G1,f,f*> . 2 is set
Carrier <*G1,f,f*> is Relation-like non-empty {1,2,3} -defined Function-like total set
product (Carrier <*G1,f,f*>) is functional non empty with_common_domain product-like set
H is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
H . 1 is set
H . 3 is set
H . 2 is set
lpp is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
lpp . 3 is set
lpp . 2 is set
lpp . 1 is set
z is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
z . 3 is set
z . 2 is set
z . 1 is set
c₁₃ is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
k is ext-real V27() V28() V29() V33() V34() V103() set
c₁₃ . k is set
lpp . k is set
dom c₁₃ is finite countable Element of bool {1,2,3}
bool {1,2,3} is non empty finite V40() countable set
dom (Carrier <*G1,f,f*>) is finite countable Element of bool {1,2,3}
len c₁₃ is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
len lpp is ext-real V27() V28() V29() V33() V34() V103() Element of NAT
G1 is non empty unital Group-like multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict unital Group-like constituted-Functions multMagma
1_ ({1},<*G1*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the carrier of ({1},<*G1*>) is non empty set
1_ G1 is Element of the carrier of G1
the carrier of G1 is non empty set
(G1,(1_ G1)) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,(1_ G1)] is set
{1,(1_ G1)} is non empty finite countable set
{{1,(1_ G1)},{1}} is non empty finite V40() countable set
{[1,(1_ G1)]} is Relation-like Function-like non empty finite countable set
dom (G1,(1_ G1)) is non empty finite countable Element of bool NAT
c₄ is Relation-like {1} -defined Function-like total set
m1 is set
<*G1*> . m1 is set
c₄ . m1 is set
n1 is non empty unital Group-like multMagma
1_ n1 is Element of the carrier of n1
the carrier of n1 is non empty set
G1 is non empty unital Group-like multMagma
1_ G1 is Element of the carrier of G1
the carrier of G1 is non empty set
f is non empty unital Group-like multMagma
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
({1,2},<*G1,f*>) is non empty strict unital Group-like constituted-Functions multMagma
1_ ({1,2},<*G1,f*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
the carrier of ({1,2},<*G1,f*>) is non empty set
1_ f is Element of the carrier of f
the carrier of f is non empty set
(G1,f,(1_ G1),(1_ f)) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
<*(1_ G1)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(1_ G1)] is set
{1,(1_ G1)} is non empty finite countable set
{{1,(1_ G1)},{1}} is non empty finite V40() countable set
{[1,(1_ G1)]} is Relation-like Function-like non empty finite countable set
<*(1_ f)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(1_ f)] is set
{1,(1_ f)} is non empty finite countable set
{{1,(1_ f)},{1}} is non empty finite V40() countable set
{[1,(1_ f)]} is Relation-like Function-like non empty finite countable set
K230(<*(1_ G1)*>,<*(1_ f)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
dom (G1,f,(1_ G1),(1_ f)) is non empty finite countable Element of bool NAT
m1 is Relation-like {1,2} -defined Function-like total set
n1 is set
<*G1,f*> . n1 is set
m1 . n1 is set
G is non empty unital Group-like multMagma
1_ G is Element of the carrier of G
the carrier of G is non empty set
G is non empty unital Group-like multMagma
1_ G is Element of the carrier of G
the carrier of G is non empty set
G1 is non empty unital Group-like multMagma
1_ G1 is Element of the carrier of G1
the carrier of G1 is non empty set
f is non empty unital Group-like multMagma
1_ f is Element of the carrier of f
the carrier of f is non empty set
f is non empty unital Group-like multMagma
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2,3}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
({1,2,3},<*G1,f,f*>) is non empty strict unital Group-like constituted-Functions multMagma
1_ ({1,2,3},<*G1,f,f*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
the carrier of ({1,2,3},<*G1,f,f*>) is non empty set
1_ f is Element of the carrier of f
the carrier of f is non empty set
(G1,f,f,(1_ G1),(1_ f),(1_ f)) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
<*(1_ G1)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(1_ G1)] is set
{1,(1_ G1)} is non empty finite countable set
{{1,(1_ G1)},{1}} is non empty finite V40() countable set
{[1,(1_ G1)]} is Relation-like Function-like non empty finite countable set
<*(1_ f)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(1_ f)] is set
{1,(1_ f)} is non empty finite countable set
{{1,(1_ f)},{1}} is non empty finite V40() countable set
{[1,(1_ f)]} is Relation-like Function-like non empty finite countable set
K230(<*(1_ G1)*>,<*(1_ f)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*(1_ f)*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(1_ f)] is set
{1,(1_ f)} is non empty finite countable set
{{1,(1_ f)},{1}} is non empty finite V40() countable set
{[1,(1_ f)]} is Relation-like Function-like non empty finite countable set
K230(K230(<*(1_ G1)*>,<*(1_ f)*>),<*(1_ f)*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
dom (G1,f,f,(1_ G1),(1_ f),(1_ f)) is non empty finite countable Element of bool NAT
n1 is Relation-like {1,2,3} -defined Function-like total set
G is set
<*G1,f,f*> . G is set
n1 . G is set
lF is non empty unital Group-like multMagma
1_ lF is Element of the carrier of lF
the carrier of lF is non empty set
lF is non empty unital Group-like multMagma
1_ lF is Element of the carrier of lF
the carrier of lF is non empty set
lF is non empty unital Group-like multMagma
1_ lF is Element of the carrier of lF
the carrier of lF is non empty set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is Element of the carrier of G1
(G1,f) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the carrier of ({1},<*G1*>) is non empty set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
(G1,f) " is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
f " is Element of the carrier of G1
(G1,(f ")) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,(f ")] is set
{1,(f ")} is non empty finite countable set
{{1,(f ")},{1}} is non empty finite V40() countable set
{[1,(f ")]} is Relation-like Function-like non empty finite countable set
f is Relation-like {1} -defined Function-like total 1-sorted-yielding () ({1}) ({1}) set
Carrier f is Relation-like non-empty {1} -defined Function-like total set
product (Carrier f) is functional non empty with_common_domain product-like set
m1 is Relation-like {1} -defined Function-like Carrier f -compatible total Element of product (Carrier f)
m1 . 1 is set
f . 1 is set
c₄ is Relation-like {1} -defined Function-like Carrier f -compatible total Element of product (Carrier f)
n1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of n1 is non empty set
lF is set
f . lF is set
m1 . lF is set
c₄ . lF is set
G is Element of the carrier of n1
G " is Element of the carrier of n1
(G ") " is Element of the carrier of n1
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of f is non empty set
<*G1,f*> is Relation-like NAT -defined {1,2} -defined Function-like non empty total finite V43(2) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2}) ({1,2}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
({1,2},<*G1,f*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
f is Element of the carrier of G1
f " is Element of the carrier of G1
c₄ is Element of the carrier of f
(G1,f,f,c₄) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
the carrier of ({1,2},<*G1,f*>) is non empty set
<*f*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
K230(<*f*>,<*c₄*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
(G1,f,f,c₄) " is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
c₄ " is Element of the carrier of f
(G1,f,(f "),(c₄ ")) is Relation-like NAT -defined Function-like non empty finite V43(2) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2},<*G1,f*>)
<*(f ")*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(f ")] is set
{1,(f ")} is non empty finite countable set
{{1,(f ")},{1}} is non empty finite V40() countable set
{[1,(f ")]} is Relation-like Function-like non empty finite countable set
<*(c₄ ")*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(c₄ ")] is set
{1,(c₄ ")} is non empty finite countable set
{{1,(c₄ ")},{1}} is non empty finite V40() countable set
{[1,(c₄ ")]} is Relation-like Function-like non empty finite countable set
K230(<*(f ")*>,<*(c₄ ")*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*G1,f*> . 2 is set
Carrier <*G1,f*> is Relation-like non-empty {1,2} -defined Function-like total set
product (Carrier <*G1,f*>) is functional non empty with_common_domain product-like set
G is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
G . 1 is set
G . 2 is set
<*G1,f*> . 1 is set
n1 is Relation-like {1,2} -defined Function-like Carrier <*G1,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f*>)
lF is set
<*G1,f*> . lF is set
G . lF is set
n1 . lF is set
p is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of p is non empty set
i is Element of the carrier of p
i " is Element of the carrier of p
(i ") " is Element of the carrier of p
p is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of p is non empty set
i is Element of the carrier of p
i " is Element of the carrier of p
(i ") " is Element of the carrier of p
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of f is non empty set
f is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of f is non empty set
<*G1,f,f*> is Relation-like NAT -defined {1,2,3} -defined Function-like non empty total finite V43(3) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1,2,3}) ({1,2,3}) set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(<*G1*>,<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*f*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
K230(K230(<*G1*>,<*f*>),<*f*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
({1,2,3},<*G1,f,f*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
c₄ is Element of the carrier of G1
c₄ " is Element of the carrier of G1
m1 is Element of the carrier of f
m1 " is Element of the carrier of f
n1 is Element of the carrier of f
(G1,f,f,c₄,m1,n1) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
the carrier of ({1,2,3},<*G1,f,f*>) is non empty set
<*c₄*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
<*m1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
K230(<*c₄*>,<*m1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*n1*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,n1] is set
{1,n1} is non empty finite countable set
{{1,n1},{1}} is non empty finite V40() countable set
{[1,n1]} is Relation-like Function-like non empty finite countable set
K230(K230(<*c₄*>,<*m1*>),<*n1*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
(G1,f,f,c₄,m1,n1) " is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
n1 " is Element of the carrier of f
(G1,f,f,(c₄ "),(m1 "),(n1 ")) is Relation-like NAT -defined Function-like non empty finite V43(3) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1,2,3},<*G1,f,f*>)
<*(c₄ ")*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(c₄ ")] is set
{1,(c₄ ")} is non empty finite countable set
{{1,(c₄ ")},{1}} is non empty finite V40() countable set
{[1,(c₄ ")]} is Relation-like Function-like non empty finite countable set
<*(m1 ")*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(m1 ")] is set
{1,(m1 ")} is non empty finite countable set
{{1,(m1 ")},{1}} is non empty finite V40() countable set
{[1,(m1 ")]} is Relation-like Function-like non empty finite countable set
K230(<*(c₄ ")*>,<*(m1 ")*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(1,1)) FinSequence-like FinSubsequence-like countable set
<*(n1 ")*> is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable set
[1,(n1 ")] is set
{1,(n1 ")} is non empty finite countable set
{{1,(n1 ")},{1}} is non empty finite V40() countable set
{[1,(n1 ")]} is Relation-like Function-like non empty finite countable set
K230(K230(<*(c₄ ")*>,<*(m1 ")*>),<*(n1 ")*>) is Relation-like NAT -defined Function-like non empty finite V43(K247(K247(1,1),1)) FinSequence-like FinSubsequence-like countable set
<*G1,f,f*> . 2 is set
<*G1,f,f*> . 3 is set
Carrier <*G1,f,f*> is Relation-like non-empty {1,2,3} -defined Function-like total set
product (Carrier <*G1,f,f*>) is functional non empty with_common_domain product-like set
p is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
p . 1 is set
p . 3 is set
p . 2 is set
<*G1,f,f*> . 1 is set
lF is Relation-like {1,2,3} -defined Function-like Carrier <*G1,f,f*> -compatible total finite FinSequence-like FinSubsequence-like countable Element of product (Carrier <*G1,f,f*>)
i is set
<*G1,f,f*> . i is set
p . i is set
lF . i is set
H is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of H is non empty set
z is Element of the carrier of H
z " is Element of the carrier of H
(z ") " is Element of the carrier of H
H is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of H is non empty set
z is Element of the carrier of H
z " is Element of the carrier of H
(z ") " is Element of the carrier of H
H is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of H is non empty set
z is Element of the carrier of H
z " is Element of the carrier of H
(z ") " is Element of the carrier of H
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of ({1},<*G1*>) is non empty set
[: the carrier of G1, the carrier of ({1},<*G1*>):] is Relation-like non empty set
bool [: the carrier of G1, the carrier of ({1},<*G1*>):] is non empty set
f is Relation-like the carrier of G1 -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total Element of bool [: the carrier of G1, the carrier of ({1},<*G1*>):]
f is Element of the carrier of G1
c₄ is Element of the carrier of G1
f * c₄ is Element of the carrier of G1
the multF of G1 is Relation-like [: the carrier of G1, the carrier of G1:] -defined the carrier of G1 -valued Function-like quasi_total associative Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is Relation-like non empty set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is Relation-like non empty set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is non empty set
the multF of G1 . (f,c₄) is Element of the carrier of G1
[f,c₄] is set
{f,c₄} is non empty finite countable set
{f} is non empty finite countable set
{{f,c₄},{f}} is non empty finite V40() countable set
the multF of G1 . [f,c₄] is set
f . (f * c₄) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
(G1,(f * c₄)) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,(f * c₄)] is set
{1,(f * c₄)} is non empty finite countable set
{{1,(f * c₄)},{1}} is non empty finite V40() countable set
{[1,(f * c₄)]} is Relation-like Function-like non empty finite countable set
(G1,f) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,f] is set
{1,f} is non empty finite countable set
{{1,f},{1}} is non empty finite V40() countable set
{[1,f]} is Relation-like Function-like non empty finite countable set
(G1,c₄) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,c₄] is set
{1,c₄} is non empty finite countable set
{{1,c₄},{1}} is non empty finite V40() countable set
{[1,c₄]} is Relation-like Function-like non empty finite countable set
(G1,f) * (G1,c₄) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the multF of ({1},<*G1*>) is Relation-like [: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):] -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total associative Element of bool [:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):]
[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):] is Relation-like non empty set
[:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):] is Relation-like non empty set
bool [:[: the carrier of ({1},<*G1*>), the carrier of ({1},<*G1*>):], the carrier of ({1},<*G1*>):] is non empty set
the multF of ({1},<*G1*>) . ((G1,f),(G1,c₄)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[(G1,f),(G1,c₄)] is set
{(G1,f),(G1,c₄)} is functional non empty finite V40() countable set
{(G1,f)} is functional non empty finite V40() with_common_domain countable set
{{(G1,f),(G1,c₄)},{(G1,f)}} is non empty finite V40() countable set
the multF of ({1},<*G1*>) . [(G1,f),(G1,c₄)] is set
f . c₄ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
(G1,f) * (f . c₄) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the multF of ({1},<*G1*>) . ((G1,f),(f . c₄)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[(G1,f),(f . c₄)] is set
{(G1,f),(f . c₄)} is functional non empty finite V40() countable set
{{(G1,f),(f . c₄)},{(G1,f)}} is non empty finite V40() countable set
the multF of ({1},<*G1*>) . [(G1,f),(f . c₄)] is set
f . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
(f . f) * (f . c₄) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
the multF of ({1},<*G1*>) . ((f . f),(f . c₄)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[(f . f),(f . c₄)] is set
{(f . f),(f . c₄)} is functional non empty finite V40() countable set
{(f . f)} is functional non empty finite V40() with_common_domain countable set
{{(f . f),(f . c₄)},{(f . f)}} is non empty finite V40() countable set
the multF of ({1},<*G1*>) . [(f . f),(f . c₄)] is set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of ({1},<*G1*>) is non empty set
[: the carrier of G1, the carrier of ({1},<*G1*>):] is Relation-like non empty set
bool [: the carrier of G1, the carrier of ({1},<*G1*>):] is non empty set
f is Relation-like the carrier of G1 -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total V102(G1,({1},<*G1*>)) Element of bool [: the carrier of G1, the carrier of ({1},<*G1*>):]
dom f is Element of bool the carrier of G1
bool the carrier of G1 is non empty set
rng f is Element of bool the carrier of ({1},<*G1*>)
bool the carrier of ({1},<*G1*>) is non empty set
f is set
<*G1*> . 1 is set
Carrier <*G1*> is Relation-like non-empty {1} -defined Function-like total set
(Carrier <*G1*>) . 1 is set
c₄ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
product (Carrier <*G1*>) is functional non empty with_common_domain product-like set
dom c₄ is finite countable Element of bool NAT
dom (Carrier <*G1*>) is finite countable Element of bool {1}
bool {1} is non empty finite V40() countable set
c₄ . 1 is set
n1 is 1-sorted
the carrier of n1 is set
m1 is Element of the carrier of G1
f . m1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
(G1,m1) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
f is set
dom f is set
c₄ is set
f . f is set
f . c₄ is set
m1 is Element of the carrier of G1
(G1,m1) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,m1] is set
{1,m1} is non empty finite countable set
{{1,m1},{1}} is non empty finite V40() countable set
{[1,m1]} is Relation-like Function-like non empty finite countable set
f . m1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
n1 is Element of the carrier of G1
(G1,n1) is Relation-like NAT -defined Function-like non empty finite V43(1) FinSequence-like FinSubsequence-like countable Element of the carrier of ({1},<*G1*>)
[1,n1] is set
{1,n1} is non empty finite countable set
{{1,n1},{1}} is non empty finite V40() countable set
{[1,n1]} is Relation-like Function-like non empty finite countable set
G1 is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
<*G1*> is Relation-like NAT -defined {1} -defined Function-like non empty total finite V43(1) FinSequence-like FinSubsequence-like countable 1-sorted-yielding () ({1}) ({1}) set
[1,G1] is set
{1,G1} is non empty finite countable set
{{1,G1},{1}} is non empty finite V40() countable set
{[1,G1]} is Relation-like Function-like non empty finite countable set
({1},<*G1*>) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V158() multMagma
the carrier of G1 is non empty set
the carrier of ({1},<*G1*>) is non empty set
[: the carrier of G1, the carrier of ({1},<*G1*>):] is Relation-like non empty set
bool [: the carrier of G1, the carrier of ({1},<*G1*>):] is non empty set
f is Relation-like the carrier of G1 -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total Element of bool [: the carrier of G1, the carrier of ({1},<*G1*>):]
f is Relation-like the carrier of G1 -defined the carrier of ({1},<*G1*>) -valued Function-like quasi_total V102(G1,({1},<*G1*>)) Element of bool [: the carrier of G1, the carrier of ({1},<*G1*>):]