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
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty finite countable set
Seg 2 is non empty finite V43(2) countable Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite countable set
Seg 3 is non empty finite V43(3) countable Element of bool NAT
{ b1 where b1 is ext-real V27() V28() V29() V33() V34() V103() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
{1,2,3} is non empty finite countable set
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
c4 is set
rng (G1 --> the non empty multMagma ) is trivial finite countable set
rng (G1 --> the non empty multMagma ) is trivial finite countable Element of bool { the non empty multMagma }
bool { the non empty multMagma } is non empty finite V40() countable set
dom (G1 --> the non empty multMagma ) is Element of bool G1
bool G1 is non empty set
m1 is set
(G1 --> the non empty multMagma ) . m1 is set
the set is set
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
c4 is 1-sorted
the carrier of c4 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
c4 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
c4 . f is set
the carrier of (G1,f,f) is non empty set
m1 is 1-sorted
the carrier of m1 is set
G1 is set
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
c4 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
c4 . 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
c4 . lF is set
m1 . lF is set
the multF of (G,p,lF) . ((c4 . lF),(m1 . lF)) is set
[(c4 . lF),(m1 . lF)] is set
{(c4 . lF),(m1 . lF)} is non empty finite countable set
{(c4 . lF)} is non empty finite countable set
{{(c4 . lF),(m1 . lF)},{(c4 . lF)}} is non empty finite V40() countable set
the multF of (G,p,lF) . [(c4 . lF),(m1 . lF)] is set
i is set
(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
c4 . 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
c4 . p is set
H is 1-sorted
the carrier of H is set
H is non empty multMagma
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
the carrier of H is non empty set
[: the carrier of H, the carrier of H:] is Relation-like non empty set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of H . ((c4 . G),(m1 . G)) is set
[(c4 . G),(m1 . G)] is set
{(c4 . G),(m1 . G)} is non empty finite countable set
{(c4 . G)} is non empty finite countable set
{{(c4 . G),(m1 . G)},{(c4 . G)}} is non empty finite V40() countable set
the multF of H . [(c4 . G),(m1 . G)] is set
z is 1-sorted
the carrier of z is set
G is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
lF is set
f . lF is set
c4 . lF is set
m1 . lF is set
G . lF is set
p is non empty multMagma
the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]
the carrier of p is non empty set
[: the carrier of p, the carrier of p:] is Relation-like non empty set
[:[: the carrier of p, the carrier of p:], the carrier of p:] is Relation-like non empty set
bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set
the multF of p . ((c4 . lF),(m1 . lF)) is set
[(c4 . lF),(m1 . lF)] is set
{(c4 . lF),(m1 . lF)} is non empty finite countable set
{(c4 . lF)} is non empty finite countable set
{{(c4 . lF),(m1 . lF)},{(c4 . lF)}} is non empty finite V40() countable set
the multF of p . [(c4 . lF),(m1 . lF)] is set
[:(product (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
c4 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)),c4 #) is strict multMagma
the carrier of multMagma(# (product (Carrier f)),c4 #) is set
the multF of multMagma(# (product (Carrier f)),c4 #) is Relation-like [: the carrier of multMagma(# (product (Carrier f)),c4 #), the carrier of multMagma(# (product (Carrier f)),c4 #):] -defined the carrier of multMagma(# (product (Carrier f)),c4 #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (product (Carrier f)),c4 #), the carrier of multMagma(# (product (Carrier f)),c4 #):], the carrier of multMagma(# (product (Carrier f)),c4 #):]
[: the carrier of multMagma(# (product (Carrier f)),c4 #), the carrier of multMagma(# (product (Carrier f)),c4 #):] is Relation-like set
[:[: the carrier of multMagma(# (product (Carrier f)),c4 #), the carrier of multMagma(# (product (Carrier f)),c4 #):], the carrier of multMagma(# (product (Carrier f)),c4 #):] is Relation-like set
bool [:[: the carrier of multMagma(# (product (Carrier f)),c4 #), the carrier of multMagma(# (product (Carrier f)),c4 #):], the carrier of multMagma(# (product (Carrier f)),c4 #):] 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)),c4 #) . (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)),c4 #) . [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
c4 is strict multMagma
the carrier of c4 is set
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
n1 is set
G is set
the multF of f . (n1,G) is set
[n1,G] is set
{n1,G} is non empty finite countable set
{n1} is non empty finite countable set
{{n1,G},{n1}} is non empty finite V40() countable set
the multF of f . [n1,G] is set
the multF of c4 . (n1,G) is set
the multF of c4 . [n1,G] is set
lF 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 c4 . [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 c4 . (lF,p) is set
lF . z is set
p . z is set
the multF of f . (lF,p) is set
c13 is non empty multMagma
lpp is Relation-like Function-like set
lpp . z is set
the multF of c13 is Relation-like [: the carrier of c13, the carrier of c13:] -defined the carrier of c13 -valued Function-like quasi_total Element of bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:]
the carrier of c13 is non empty set
[: the carrier of c13, the carrier of c13:] is Relation-like non empty set
[:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is Relation-like non empty set
bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is non empty set
the multF of c13 . ((lF . z),(p . z)) is set
[(lF . z),(p . z)] is set
{(lF . z),(p . z)} is non empty finite countable set
{(lF . z)} is non empty finite countable set
{{(lF . z),(p . z)},{(lF . z)}} is non empty finite V40() countable set
the multF of c13 . [(lF . z),(p . z)] is set
k is non empty multMagma
f 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
c4 is Relation-like Function-like set
c4 . 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,c4) is set
[f,c4] is set
{f,c4} is functional non empty finite countable set
{f} is functional non empty finite with_common_domain countable set
{{f,c4},{f}} is non empty finite V40() countable set
the multF of (G1,n1) . [f,c4] is set
c13 is non empty multMagma
lpp is Relation-like Function-like set
lpp . f is set
the multF of c13 is Relation-like [: the carrier of c13, the carrier of c13:] -defined the carrier of c13 -valued Function-like quasi_total Element of bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:]
the carrier of c13 is non empty set
[: the carrier of c13, the carrier of c13:] is Relation-like non empty set
[:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is Relation-like non empty set
bool [:[: the carrier of c13, the carrier of c13:], the carrier of c13:] is non empty set
the multF of c13 . ((f . f),(c4 . f)) is set
[(f . f),(c4 . f)] is set
{(f . f),(c4 . f)} is non empty finite countable set
{(f . f)} is non empty finite countable set
{{(f . f),(c4 . f)},{(f . f)}} is non empty finite V40() countable set
the multF of c13 . [(f . f),(c4 . f)] is set
G1 is set
G1 is non empty set
f is Relation-like G1 -defined Function-like total 1-sorted-yielding () set
f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty unital Group-like multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty unital Group-like multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty associative multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty associative multMagma
f is Element of G1
(G1,f,f) is non empty multMagma
c4 is non empty commutative multMagma
f is set
f . f is set
c4 is Element of G1
(G1,f,c4) is non empty multMagma
m1 is non empty commutative multMagma
G1 is set
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
c4 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
c4 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
c4 . 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
c4 . m1 is set
m1 is set
c4 . 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
c4 is set
f . c4 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
c4 is Relation-like Function-like set
dom c4 is set
rng c4 is set
m1 is set
f . m1 is set
(Carrier f) . m1 is set
c4 . m1 is set
n1 is non empty multMagma
the carrier of n1 is non empty set
G is Element of the carrier of n1
lF is 1-sorted
the carrier of lF is set
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
c4 . i is set
H is non empty multMagma
the carrier of H is non empty set
z is Element of the carrier of H
G . i is set
the multF of (G1,f) . (G,m1) is set
[G,m1] is set
{G,m1} is functional non empty finite countable set
{G} 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
c13 is Element of the carrier of H
c13 * z is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is Relation-like non empty set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of H . (c13,z) is Element of the carrier of H
[c13,z] is set
{c13,z} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,z},{c13}} is non empty finite V40() countable set
the multF of H . [c13,z] is set
lF 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),(c4 . i)) is set
[(G . i),(c4 . i)] is set
{(G . i),(c4 . i)} is non empty finite countable set
{(G . i)} is non empty finite countable set
{{(G . i),(c4 . i)},{(G . i)}} is non empty finite V40() countable set
the multF of lpp . [(G . i),(c4 . i)] is set
dom lF is Element of bool G1
i is set
f . i is set
c4 . i is set
H is non empty multMagma
the carrier of H is non empty set
z is Element of the carrier of H
G . i is set
the multF of (G1,f) . (m1,G) is set
[m1,G] is set
{m1,G} is functional non empty finite countable set
{{m1,G},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,G] is set
c13 is Element of the carrier of H
z * c13 is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is Relation-like non empty set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of H . (z,c13) is Element of the carrier of H
[z,c13] is set
{z,c13} is non empty finite countable set
{z} is non empty finite countable set
{{z,c13},{z}} is non empty finite V40() countable set
the multF of H . [z,c13] is set
p 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 . ((c4 . i),(G . i)) is set
[(c4 . i),(G . i)] is set
{(c4 . i),(G . i)} is non empty finite countable set
{(c4 . i)} is non empty finite countable set
{{(c4 . i),(G . i)},{(c4 . i)}} is non empty finite V40() countable set
the multF of lpp . [(c4 . i),(G . i)] is set
i is set
f . i is set
G . i is set
c4 . i is set
H is non empty multMagma
the carrier of H is non empty set
z is Element of the carrier of H
(Carrier f) . i is set
c13 is Element of the carrier of H
lpp is Element of the carrier of H
c13 * lpp is Element of the carrier of H
the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like quasi_total Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is Relation-like non empty set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is Relation-like non empty set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of H . (c13,lpp) is Element of the carrier of H
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of H . [c13,lpp] is set
lpp * c13 is Element of the carrier of H
the multF of H . (lpp,c13) is Element of the carrier of H
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c13] is set
k is 1-sorted
the carrier of k is set
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
c4 . H is set
i . H is set
z is non empty multMagma
the carrier of z is non empty set
c13 is Element of the carrier of z
lpp is Element of the carrier of z
c13 * lpp is Element of the carrier of z
the multF of z is Relation-like [: the carrier of z, the carrier of z:] -defined the carrier of z -valued Function-like quasi_total Element of bool [:[: the carrier of z, the carrier of z:], the carrier of z:]
[: the carrier of z, the carrier of z:] is Relation-like non empty set
[:[: the carrier of z, the carrier of z:], the carrier of z:] is Relation-like non empty set
bool [:[: the carrier of z, the carrier of z:], the carrier of z:] is non empty set
the multF of z . (c13,lpp) is Element of the carrier of z
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of z . [c13,lpp] is set
lpp * c13 is Element of the carrier of z
the multF of z . (lpp,c13) is Element of the carrier of z
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of z . [lpp,c13] is set
k is 1-sorted
the carrier of k is set
dom p is Element of bool G1
H is Relation-like Function-like Element of the carrier of (G1,f)
n1 * H is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (n1,H) is Relation-like Function-like Element of the carrier of (G1,f)
[n1,H] is set
{n1,H} is functional non empty finite countable set
{{n1,H},{n1}} is non empty finite V40() countable set
the multF of (G1,f) . [n1,H] is set
H * n1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (H,n1) is Relation-like Function-like Element of the carrier of (G1,f)
[H,n1] is set
{H,n1} is functional non empty finite countable set
{H} 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
c4 . 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
c4 . 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
c13 is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
c13 . 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 c13 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
c4 is Relation-like Function-like Element of the carrier of (G1,f)
m1 is Relation-like Function-like Element of the carrier of (G1,f)
c4 * m1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]
[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set
[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set
bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set
the multF of (G1,f) . (c4,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,m1] is set
{c4,m1} is functional non empty finite countable set
{c4} is functional non empty finite with_common_domain countable set
{{c4,m1},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,m1] is set
n1 is Relation-like Function-like Element of the carrier of (G1,f)
(c4 * m1) * n1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . ((c4 * m1),n1) is Relation-like Function-like Element of the carrier of (G1,f)
[(c4 * m1),n1] is set
{(c4 * m1),n1} is functional non empty finite countable set
{(c4 * m1)} is functional non empty finite with_common_domain countable set
{{(c4 * m1),n1},{(c4 * m1)}} is non empty finite V40() countable set
the multF of (G1,f) . [(c4 * m1),n1] is set
m1 * n1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (m1,n1) is Relation-like Function-like Element of the carrier of (G1,f)
[m1,n1] is set
{m1,n1} is functional non empty finite countable set
{m1} 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
c4 * (m1 * n1) is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c4,(m1 * n1)) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,(m1 * n1)] is set
{c4,(m1 * n1)} is functional non empty finite countable set
{{c4,(m1 * n1)},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,(m1 * n1)] is set
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) . (c4,m1)),n1) is Relation-like Function-like Element of the carrier of (G1,f)
[( the multF of (G1,f) . (c4,m1)),n1] is set
{( the multF of (G1,f) . (c4,m1)),n1} is functional non empty finite countable set
{( the multF of (G1,f) . (c4,m1))} is functional non empty finite with_common_domain countable set
{{( the multF of (G1,f) . (c4,m1)),n1},{( the multF of (G1,f) . (c4,m1))}} is non empty finite V40() countable set
the multF of (G1,f) . [( the multF of (G1,f) . (c4,m1)),n1] is set
the multF of (G1,f) . (c4,( the multF of (G1,f) . (m1,n1))) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,( the multF of (G1,f) . (m1,n1))] is set
{c4,( the multF of (G1,f) . (m1,n1))} is functional non empty finite countable set
{{c4,( the multF of (G1,f) . (m1,n1))},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,( the multF of (G1,f) . (m1,n1))] is set
dom (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
c23 is non empty multMagma
K is Relation-like Function-like set
K . i is set
the multF of c23 is Relation-like [: the carrier of c23, the carrier of c23:] -defined the carrier of c23 -valued Function-like quasi_total Element of bool [:[: the carrier of c23, the carrier of c23:], the carrier of c23:]
the carrier of c23 is non empty set
[: the carrier of c23, the carrier of c23:] is Relation-like non empty set
[:[: the carrier of c23, the carrier of c23:], the carrier of c23:] is Relation-like non empty set
bool [:[: the carrier of c23, the carrier of c23:], the carrier of c23:] is non empty set
the multF of c23 . ((lpp . i),(p . i)) is set
[(lpp . i),(p . i)] is set
{(lpp . i),(p . i)} is non empty finite countable set
{(lpp . i)} is non empty finite countable set
{{(lpp . i),(p . i)},{(lpp . i)}} is non empty finite V40() countable set
the multF of c23 . [(lpp . i),(p . i)] is set
G is Element of the carrier of G
m is Element of the carrier of G
G * m is Element of the carrier of G
the multF of G . (G,m) is Element of the carrier of G
[G,m] is set
{G,m} is non empty finite countable set
{G} is non empty finite countable set
{{G,m},{G}} is non empty finite V40() countable set
the multF of G . [G,m] is set
k is Relation-like G1 -defined Function-like Carrier f -compatible total Element of product (Carrier f)
the multF of (G1,f) . (c4,k) is set
[c4,k] is set
{c4,k} is functional non empty finite countable set
{{c4,k},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,k] is set
k . i is set
f 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 c23
ff is Element of the carrier of c23
J * ff is Element of the carrier of c23
the multF of c23 . (J,ff) is Element of the carrier of c23
[J,ff] is set
{J,ff} is non empty finite countable set
{J} is non empty finite countable set
{{J,ff},{J}} is non empty finite V40() countable set
the multF of c23 . [J,ff] is set
J is Element of the carrier of c23
j is Element of the carrier of c23
j * ff is Element of the carrier of c23
the multF of c23 . (j,ff) is Element of the carrier of c23
[j,ff] is set
{j,ff} is non empty finite countable set
{j} is non empty finite countable set
{{j,ff},{j}} is non empty finite V40() countable set
the multF of c23 . [j,ff] is set
J * (j * ff) is Element of the carrier of c23
the multF of c23 . (J,(j * ff)) is Element of the carrier of c23
[J,(j * ff)] is set
{J,(j * ff)} is non empty finite countable set
{J} is non empty finite countable set
{{J,(j * ff)},{J}} is non empty finite V40() countable set
the multF of c23 . [J,(j * ff)] is set
gf . i is set
G is non empty multMagma
k1 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
c4 is Relation-like Function-like Element of the carrier of (G1,f)
m1 is Relation-like Function-like Element of the carrier of (G1,f)
c4 * m1 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) is Relation-like [: the carrier of (G1,f), the carrier of (G1,f):] -defined the carrier of (G1,f) -valued Function-like quasi_total Element of bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):]
[: the carrier of (G1,f), the carrier of (G1,f):] is Relation-like non empty set
[:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is Relation-like non empty set
bool [:[: the carrier of (G1,f), the carrier of (G1,f):], the carrier of (G1,f):] is non empty set
the multF of (G1,f) . (c4,m1) is Relation-like Function-like Element of the carrier of (G1,f)
[c4,m1] is set
{c4,m1} is functional non empty finite countable set
{c4} is functional non empty finite with_common_domain countable set
{{c4,m1},{c4}} is non empty finite V40() countable set
the multF of (G1,f) . [c4,m1] is set
m1 * c4 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (m1,c4) is Relation-like Function-like Element of the carrier of (G1,f)
[m1,c4] is set
{m1,c4} is functional non empty finite countable set
{m1} is functional non empty finite with_common_domain countable set
{{m1,c4},{m1}} is non empty finite V40() countable set
the multF of (G1,f) . [m1,c4] 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
c13 is Element of the carrier of H
lpp is Element of the carrier of H
c13 * lpp is Element of the carrier of H
the multF of H . (c13,lpp) is Element of the carrier of H
[c13,lpp] is set
{c13,lpp} is non empty finite countable set
{c13} is non empty finite countable set
{{c13,lpp},{c13}} is non empty finite V40() countable set
the multF of H . [c13,lpp] is set
lpp * c13 is Element of the carrier of H
the multF of H . (lpp,c13) is Element of the carrier of H
[lpp,c13] is set
{lpp,c13} is non empty finite countable set
{lpp} is non empty finite countable set
{{lpp,c13},{lpp}} is non empty finite V40() countable set
the multF of H . [lpp,c13] is set
p . i is set
k is non empty commutative multMagma
k is non empty multMagma
f 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
c4 is non empty multMagma
the carrier of (G1,f) is non empty set
n1 is Relation-like Function-like Element of the carrier of (G1,f)
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 c4 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 c4
p is Element of the carrier of c4
p * lF is Element of the carrier of c4
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like non empty set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like non empty set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
the multF of c4 . (p,lF) is Element of the carrier of c4
[p,lF] is set
{p,lF} is non empty finite countable set
{p} is non empty finite countable set
{{p,lF},{p}} is non empty finite V40() countable set
the multF of c4 . [p,lF] is set
lF * p is Element of the carrier of c4
the multF of c4 . (lF,p) is Element of the carrier of c4
[lF,p] is set
{lF,p} is non empty finite countable set
{lF} is non empty finite countable set
{{lF,p},{lF}} is non empty finite V40() countable set
the multF of c4 . [lF,p] is set
i is set
f . i is set
dom f is Element of bool G1
bool G1 is non empty set
rng f is set
H is non empty multMagma
the carrier of H is non empty set
the Element of the carrier of H is Element of the carrier of H
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
c13 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
c13 is Relation-like Function-like Element of the carrier of (G1,f)
z * c13 is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (z,c13) is Relation-like Function-like Element of the carrier of (G1,f)
[z,c13] is set
{z,c13} is functional non empty finite countable set
{{z,c13},{z}} is non empty finite V40() countable set
the multF of (G1,f) . [z,c13] is set
c13 * z is Relation-like Function-like Element of the carrier of (G1,f)
the multF of (G1,f) . (c13,z) is Relation-like Function-like Element of the carrier of (G1,f)
[c13,z] is set
{c13,z} is functional non empty finite countable set
{c13} is functional non empty finite with_common_domain countable set
{{c13,z},{c13}} is non empty finite V40() countable set
the multF of (G1,f) . [c13,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 c4
p * k is Element of the carrier of c4
the multF of c4 . (p,k) is Element of the carrier of c4
[p,k] is set
{p,k} is non empty finite countable set
{{p,k},{p}} is non empty finite V40() countable set
the multF of c4 . [p,k] is set
k * p is Element of the carrier of c4
the multF of c4 . (k,p) is Element of the carrier of c4
[k,p] is set
{k,p} is non empty finite countable set
{k} is non empty finite countable set
{{k,p},{k}} is non empty finite V40() countable set
the multF of c4 . [k,p] is set
G1 is set
f is set
f 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
c4 is non empty multMagma
the carrier of (G1,f) is non empty set
the carrier of c4 is non empty set
m1 is Element of the carrier of c4
n1 is Element of the carrier of c4
m1 * n1 is Element of the carrier of c4
the multF of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined the carrier of c4 -valued Function-like quasi_total Element of bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:]
[: the carrier of c4, the carrier of c4:] is Relation-like non empty set
[:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is Relation-like non empty set
bool [:[: the carrier of c4, the carrier of c4:], the carrier of c4:] is non empty set
the multF of c4 . (m1,n1) is Element of the carrier of c4
[m1,n1] is set
{m1,n1} is non empty finite countable set
{m1} is non empty finite countable set
{{m1,n1},{m1}} is non empty finite V40() countable