:: GROUP_12 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() V33() V38() V39() countable denumerable Element of K19(REAL)
K19(REAL) is set
NAT is non empty V24() V25() V26() V33() V38() V39() countable denumerable set
K19(NAT) is V33() set
K19(NAT) is V33() set
COMPLEX is set
RAT is set
INT is set
K20(REAL,REAL) is set
K19(K20(REAL,REAL)) is set
K361() is non empty strict multMagma
the carrier of K361() is non empty set
K366() is non empty strict unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma
K367() is non empty strict associative commutative V156() V157() V158() M18(K366())
K368() is non empty strict unital associative commutative V156() V157() V158() V159() M21(K366(),K367())
K370() is non empty strict unital associative commutative multMagma
K371() is non empty strict unital associative commutative V159() M18(K370())
K430() is set
{} is functional empty V24() V25() V26() V28() V29() V30() V31() V33() V38() V40( {} ) V100() FinSequence-membered ext-real non positive non negative countable set
{{}} is non empty V12() V40(1) set
1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable Element of NAT
K332({{}}) is functional non empty FinSequence-membered M15({{}})
K20(K332({{}}),{{}}) is set
K19(K20(K332({{}}),{{}})) is set
PFuncs (K332({{}}),{{}}) is set
{1} is non empty V12() V40(1) set
2 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable Element of NAT
{1,2} is non empty set
3 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable Element of NAT
K89(1,2,3) is set
0 is functional empty V24() V25() V26() V28() V29() V30() V31() V33() V38() V40( {} ) V100() FinSequence-membered ext-real non positive non negative countable Element of NAT
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like set
F is Element of n
G . F is non empty multMagma
s is multMagma
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding associative set
F is Element of n
G . F is non empty multMagma
s is multMagma
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding commutative set
F is Element of n
G . F is non empty multMagma
s is multMagma
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
the carrier of (product G) is non empty set
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
s is Relation-like Function-like set
dom s is set
s . F is set
t is Element of the carrier of (G . F)
(1_ (product G)) +* (F,t) is Relation-like Function-like set
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (1_ (product G)) is set
k is Element of n
s . k is set
G . k is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . k) is Element of the carrier of (G . k)
the carrier of (G . k) is non empty set
(1_ (product G)) . k is set
dom ((1_ (product G)) +* (F,t)) is set
x1 is set
x2 is Element of n
s . x2 is set
G . x2 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x2) is Element of the carrier of (G . x2)
the carrier of (G . x2) is non empty set
s . x1 is set
(1_ (product G)) . x2 is set
((1_ (product G)) +* (F,t)) . x1 is set
x2 is Element of n
s . x1 is set
((1_ (product G)) +* (F,t)) . x1 is set
x2 is Element of n
k is Element of n
s . k is set
G . k is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . k) is Element of the carrier of (G . k)
the carrier of (G . k) is non empty set
x1 is Element of n
s . x1 is set
G . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x1) is Element of the carrier of (G . x1)
the carrier of (G . x1) is non empty set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
K19( the carrier of (product G)) is set
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
t is Element of K19( the carrier of (product G))
x1 is set
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
(Carrier G) . F is set
x2 is 1-sorted
the carrier of x2 is set
s is Element of the carrier of (G . F)
(1_ (product G)) +* (F,s) is Relation-like Function-like set
x1 is set
x2 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,x2) is Relation-like Function-like set
x2 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,x2) is Relation-like Function-like set
s is Element of the carrier of (G . F)
(1_ (product G)) +* (F,s) is Relation-like Function-like set
s is Element of K19( the carrier of (product G))
t is Element of K19( the carrier of (product G))
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
F is Element of n
(n,G,F) is Element of K19( the carrier of (product G))
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
K19( the carrier of (product G)) is set
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
dom (1_ (product G)) is set
1_ (G . F) is Element of the carrier of (G . F)
the carrier of (G . F) is non empty set
(1_ (product G)) +* (F,(1_ (G . F))) is Relation-like Function-like set
dom ((1_ (product G)) +* (F,(1_ (G . F)))) is set
x1 is Element of n
k is Relation-like n -defined Function-like set
k . x1 is set
(1_ (product G)) . x1 is set
G . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x1) is Element of the carrier of (G . x1)
the carrier of (G . x1) is non empty set
x1 is Element of n
k is Relation-like n -defined Function-like set
k . x1 is set
G . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x1) is Element of the carrier of (G . x1)
the carrier of (G . x1) is non empty set
x1 is Element of n
k is Relation-like n -defined Function-like set
k is Relation-like n -defined Function-like set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
F is Element of n
(n,G,F) is non empty Element of K19( the carrier of (product G))
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
K19( the carrier of (product G)) is set
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
s is set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
t is Element of the carrier of (G . F)
(1_ (product G)) +* (F,t) is Relation-like Function-like set
k is Relation-like Function-like set
x1 is Relation-like Function-like set
dom x1 is set
x1 . F is set
x2 is Element of the carrier of (G . F)
s is Element of n
x1 . s is set
G . s is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . s) is Element of the carrier of (G . s)
the carrier of (G . s) is non empty set
t is Relation-like Function-like set
dom t is set
t . F is set
k is Element of the carrier of (G . F)
t is Relation-like Function-like set
dom t is set
t . F is set
k is Element of the carrier of (G . F)
(1_ (product G)) +* (F,k) is Relation-like Function-like set
t is Relation-like Function-like set
dom t is set
t . F is set
k is Element of the carrier of (G . F)
x1 is Relation-like Function-like set
dom x1 is set
x1 . F is set
x2 is Element of the carrier of (G . F)
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like Function-like Element of the carrier of (product G)
s * t is Relation-like Function-like Element of the carrier of (product G)
k is Element of the carrier of (G . F)
(1_ (product G)) +* (F,k) is Relation-like Function-like set
x1 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,x1) is Relation-like Function-like set
k * x1 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,(k * x1)) is Relation-like Function-like set
dom s is set
s . F is set
t is Element of n
s . t is set
G . t is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . t) is Element of the carrier of (G . t)
the carrier of (G . t) is non empty set
dom t is set
t . F is set
t is Element of n
t . t is set
G . t is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . t) is Element of the carrier of (G . t)
the carrier of (G . t) is non empty set
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (s * t) is set
(s * t) . F is set
k is Element of n
(s * t) . k is set
G . k is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . k) is Element of the carrier of (G . k)
the carrier of (G . k) is non empty set
s . k is set
t . k is set
(1_ (G . k)) * (1_ (G . k)) is Element of the carrier of (G . k)
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
s is Relation-like Function-like Element of the carrier of (product G)
s " is Relation-like Function-like Element of the carrier of (product G)
t is Element of the carrier of (G . F)
(1_ (product G)) +* (F,t) is Relation-like Function-like set
t " is Element of the carrier of (G . F)
(1_ (product G)) +* (F,(t ")) is Relation-like Function-like set
dom s is set
s . F is set
x1 is Element of n
s . x1 is set
G . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x1) is Element of the carrier of (G . x1)
the carrier of (G . x1) is non empty set
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (s ") is set
(s ") . F is set
x2 is Element of n
(s ") . x2 is set
G . x2 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x2) is Element of the carrier of (G . x2)
the carrier of (G . x2) is non empty set
s . x2 is set
(1_ (G . x2)) " is Element of the carrier of (G . x2)
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is Element of n
(n,G,F) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like Function-like Element of the carrier of (product G)
s * t is Relation-like Function-like Element of the carrier of (product G)
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
k is Element of the carrier of (G . F)
(1_ (product G)) +* (F,k) is Relation-like Function-like set
x1 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,x1) is Relation-like Function-like set
k * x1 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,(k * x1)) is Relation-like Function-like set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is Element of n
(n,G,F) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
s is Relation-like Function-like Element of the carrier of (product G)
s " is Relation-like Function-like Element of the carrier of (product G)
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
t is Element of the carrier of (G . F)
(1_ (product G)) +* (F,t) is Relation-like Function-like set
t " is Element of the carrier of (G . F)
(1_ (product G)) +* (F,(t ")) is Relation-like Function-like set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
F is Element of n
(n,G,F) is non empty Element of K19( the carrier of (product G))
the carrier of (product G) is non empty set
K19( the carrier of (product G)) is set
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like Function-like Element of the carrier of (product G)
s * t is Relation-like Function-like Element of the carrier of (product G)
k is Relation-like Function-like Element of the carrier of (product G)
k " is Relation-like Function-like Element of the carrier of (product G)
s is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of s is non empty set
t is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of t is non empty set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
the carrier of (product G) is non empty set
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
(n,G,F) is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of (n,G,F) is non empty set
K20( the carrier of (G . F), the carrier of (n,G,F)) is set
K19(K20( the carrier of (G . F), the carrier of (n,G,F))) is set
(n,G,F) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
s is Element of the carrier of (G . F)
(1_ (product G)) +* (F,s) is Relation-like Function-like set
s is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
t is Element of the carrier of (G . F)
k is Element of the carrier of (G . F)
t * k is Element of the carrier of (G . F)
s . (t * k) is Element of the carrier of (n,G,F)
s . t is Element of the carrier of (n,G,F)
s . k is Element of the carrier of (n,G,F)
(s . t) * (s . k) is Element of the carrier of (n,G,F)
(1_ (product G)) +* (F,t) is Relation-like Function-like set
(1_ (product G)) +* (F,k) is Relation-like Function-like set
(1_ (product G)) +* (F,(t * k)) is Relation-like Function-like set
x1 is Relation-like Function-like Element of the carrier of (product G)
x2 is Relation-like Function-like Element of the carrier of (product G)
x1 * x2 is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
k is set
x1 is Element of the carrier of (G . F)
(1_ (product G)) +* (F,x1) is Relation-like Function-like set
t . x1 is Element of the carrier of (n,G,F)
rng t is Element of K19( the carrier of (n,G,F))
K19( the carrier of (n,G,F)) is set
k is set
x1 is set
t . k is set
t . x1 is set
x2 is Element of the carrier of (G . F)
t . x2 is Element of the carrier of (n,G,F)
(1_ (product G)) +* (F,x2) is Relation-like Function-like set
s is Element of the carrier of (G . F)
(1_ (product G)) +* (F,s) is Relation-like Function-like set
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (1_ (product G)) is set
F .--> x2 is Relation-like n -defined {F} -defined the carrier of (G . F) -valued Function-like one-to-one set
{F} is non empty V12() V40(1) set
(1_ (product G)) +* (F .--> x2) is Relation-like Function-like set
((1_ (product G)) +* (F .--> x2)) . F is set
((1_ (product G)) +* (F,x2)) . F is set
F .--> s is Relation-like n -defined {F} -defined the carrier of (G . F) -valued Function-like one-to-one set
(1_ (product G)) +* (F .--> s) is Relation-like Function-like set
((1_ (product G)) +* (F .--> s)) . F is set
k is Element of the carrier of (G . F)
t . k is Element of the carrier of (n,G,F)
(1_ (product G)) +* (F,k) is Relation-like Function-like set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
(n,G,F) is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (n,G,F) is non empty set
K20( the carrier of (G . F), the carrier of (n,G,F)) is set
K19(K20( the carrier of (G . F), the carrier of (n,G,F))) is set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
the carrier of (product G) is non empty set
s is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
s is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
t is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
k is Element of the carrier of (G . F)
s . k is Element of the carrier of (n,G,F)
(1_ (product G)) +* (F,k) is Relation-like Function-like set
t . k is Element of the carrier of (n,G,F)
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
F is Element of n
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
(n,G,F) is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (n,G,F) is non empty set
(n,G,F) is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
K20( the carrier of (G . F), the carrier of (n,G,F)) is set
K19(K20( the carrier of (G . F), the carrier of (n,G,F))) is set
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
the carrier of (product G) is non empty set
s is Relation-like the carrier of (G . F) -defined the carrier of (n,G,F) -valued Function-like non empty total quasi_total V99(G . F,(n,G,F)) Element of K19(K20( the carrier of (G . F), the carrier of (n,G,F)))
k is Element of the carrier of (G . F)
s . k is Element of the carrier of (n,G,F)
(n,G,F) . k is Element of the carrier of (n,G,F)
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
F is Element of n
(n,G,F) is non empty strict unital Group-like associative V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of (product G) is non empty set
the carrier of (n,G,F) is non empty set
k is Relation-like Function-like Element of the carrier of (product G)
k " is Relation-like Function-like Element of the carrier of (product G)
k * (n,G,F) is Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
carr (n,G,F) is Element of K19( the carrier of (product G))
k * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in carr (n,G,F) ) } is set
(k * (n,G,F)) * (k ") is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k ")) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
(k * (n,G,F)) * K102( the carrier of (product G),(k ")) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in k * (n,G,F) & b₂ in K102( the carrier of (product G),(k ")) ) } is set
x1 is set
x2 is Relation-like Function-like Element of the carrier of (product G)
x2 * (k ") is Relation-like Function-like Element of the carrier of (product G)
s is Relation-like Function-like Element of the carrier of (product G)
k * s is Relation-like Function-like Element of the carrier of (product G)
(n,G,F) is non empty Element of K19( the carrier of (product G))
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
t is Relation-like Function-like set
dom t is set
t . F is set
k is Element of the carrier of (G . F)
(k * s) * (k ") is Relation-like Function-like Element of the carrier of (product G)
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (Carrier G) is Element of K19(n)
K19(n) is set
dom ((k * s) * (k ")) is set
(Carrier G) . F is set
bb is 1-sorted
the carrier of bb is set
k . F is set
s . F is set
(k * s) . F is set
tii is Element of the carrier of (G . F)
xk is Element of the carrier of (G . F)
tii * xk is Element of the carrier of (G . F)
(k ") . F is set
tii " is Element of the carrier of (G . F)
((k * s) * (k ")) . F is set
(tii * xk) * (tii ") is Element of the carrier of (G . F)
j is Element of n
t . j is set
G . j is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . j) is Element of the carrier of (G . j)
the carrier of (G . j) is non empty set
(Carrier G) . j is set
Rj is 1-sorted
the carrier of Rj is set
k . j is set
s . j is set
(k * s) . j is set
xa is Element of the carrier of (G . j)
xk is Element of the carrier of (G . j)
xa * xk is Element of the carrier of (G . j)
(k ") . j is set
xa " is Element of the carrier of (G . j)
((k * s) * (k ")) . j is set
(xa * xk) * (xa ") is Element of the carrier of (G . j)
xa * (xa ") is Element of the carrier of (G . j)
k is Relation-like Function-like Element of the carrier of (product G)
k * (n,G,F) is Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
carr (n,G,F) is Element of K19( the carrier of (product G))
k * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in carr (n,G,F) ) } is set
(n,G,F) * k is Element of K19( the carrier of (product G))
(carr (n,G,F)) * k is Element of K19( the carrier of (product G))
(carr (n,G,F)) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in carr (n,G,F) & b₂ in K102( the carrier of (product G),k) ) } is set
k " is Relation-like Function-like Element of the carrier of (product G)
(k * (n,G,F)) * (k ") is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k ")) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
(k * (n,G,F)) * K102( the carrier of (product G),(k ")) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in k * (n,G,F) & b₂ in K102( the carrier of (product G),(k ")) ) } is set
(k ") * k is Relation-like Function-like Element of the carrier of (product G)
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
((k * (n,G,F)) * (k ")) * k is Element of K19( the carrier of (product G))
((k * (n,G,F)) * (k ")) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in (k * (n,G,F)) * (k ") & b₂ in K102( the carrier of (product G),k) ) } is set
(n,G,F) * (k ") is Element of K19( the carrier of (product G))
(carr (n,G,F)) * (k ") is Element of K19( the carrier of (product G))
(carr (n,G,F)) * K102( the carrier of (product G),(k ")) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in carr (n,G,F) & b₂ in K102( the carrier of (product G),(k ")) ) } is set
k * ((n,G,F) * (k ")) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * ((n,G,F) * (k ")) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in (n,G,F) * (k ") ) } is set
(k * ((n,G,F) * (k "))) * k is Element of K19( the carrier of (product G))
(k * ((n,G,F) * (k "))) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in k * ((n,G,F) * (k ")) & b₂ in K102( the carrier of (product G),k) ) } is set
((n,G,F) * (k ")) * k is Element of K19( the carrier of (product G))
((n,G,F) * (k ")) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in (n,G,F) * (k ") & b₂ in K102( the carrier of (product G),k) ) } is set
k * (((n,G,F) * (k ")) * k) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (((n,G,F) * (k ")) * k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in ((n,G,F) * (k ")) * k ) } is set
(n,G,F) * ((k ") * k) is Element of K19( the carrier of (product G))
(carr (n,G,F)) * ((k ") * k) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),((k ") * k)) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
(carr (n,G,F)) * K102( the carrier of (product G),((k ") * k)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in carr (n,G,F) & b₂ in K102( the carrier of (product G),((k ") * k)) ) } is set
k * ((n,G,F) * ((k ") * k)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * ((n,G,F) * ((k ") * k)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in (n,G,F) * ((k ") * k) ) } is set
k is Relation-like Function-like Element of the carrier of (product G)
(n,G,F) * k is Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
carr (n,G,F) is Element of K19( the carrier of (product G))
(carr (n,G,F)) * k is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
(carr (n,G,F)) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in carr (n,G,F) & b₂ in K102( the carrier of (product G),k) ) } is set
k * (n,G,F) is Element of K19( the carrier of (product G))
k * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in carr (n,G,F) ) } is set
k " is Relation-like Function-like Element of the carrier of (product G)
(k ") " is Relation-like Function-like Element of the carrier of (product G)
(k ") * (n,G,F) is Element of K19( the carrier of (product G))
(k ") * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k ")) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k ")) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),(k ")) & b₂ in carr (n,G,F) ) } is set
((k ") * (n,G,F)) * ((k ") ") is Element of K19( the carrier of (product G))
K102( the carrier of (product G),((k ") ")) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
((k ") * (n,G,F)) * K102( the carrier of (product G),((k ") ")) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in (k ") * (n,G,F) & b₂ in K102( the carrier of (product G),((k ") ")) ) } is set
k * (k ") is Relation-like Function-like Element of the carrier of (product G)
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
((k ") * (n,G,F)) * k is Element of K19( the carrier of (product G))
((k ") * (n,G,F)) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in (k ") * (n,G,F) & b₂ in K102( the carrier of (product G),k) ) } is set
k * (((k ") * (n,G,F)) * k) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (((k ") * (n,G,F)) * k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in ((k ") * (n,G,F)) * k ) } is set
(k ") * ((n,G,F) * k) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k ")) * ((n,G,F) * k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),(k ")) & b₂ in (n,G,F) * k ) } is set
k * ((k ") * ((n,G,F) * k)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * ((k ") * ((n,G,F) * k)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in (k ") * ((n,G,F) * k) ) } is set
(k * (k ")) * ((n,G,F) * k) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k * (k "))) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k * (k "))) * ((n,G,F) * k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),(k * (k "))) & b₂ in (n,G,F) * k ) } is set
(k * (k ")) * (n,G,F) is Element of K19( the carrier of (product G))
(k * (k ")) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),(k * (k "))) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),(k * (k "))) & b₂ in carr (n,G,F) ) } is set
((k * (k ")) * (n,G,F)) * k is Element of K19( the carrier of (product G))
((k * (k ")) * (n,G,F)) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in (k * (k ")) * (n,G,F) & b₂ in K102( the carrier of (product G),k) ) } is set
k is Relation-like Function-like Element of the carrier of (product G)
k * (n,G,F) is Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
carr (n,G,F) is Element of K19( the carrier of (product G))
k * (carr (n,G,F)) is Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) is non empty V12() V40(1) with_common_domain Element of K19( the carrier of (product G))
K102( the carrier of (product G),k) * (carr (n,G,F)) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in K102( the carrier of (product G),k) & b₂ in carr (n,G,F) ) } is set
(n,G,F) * k is Element of K19( the carrier of (product G))
(carr (n,G,F)) * k is Element of K19( the carrier of (product G))
(carr (n,G,F)) * K102( the carrier of (product G),k) is Element of K19( the carrier of (product G))
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of (product G) : ( b₁ in carr (n,G,F) & b₂ in K102( the carrier of (product G),k) ) } is set
n is non empty set
G is Relation-like n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is Element of n
(n,G,F) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
s is Element of n
(n,G,s) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
k is Relation-like Function-like Element of the carrier of (product G)
x1 is Relation-like Function-like Element of the carrier of (product G)
k * x1 is Relation-like Function-like Element of the carrier of (product G)
x1 * k is Relation-like Function-like Element of the carrier of (product G)
the carrier of (n,G,F) is non empty set
(n,G,F) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
the carrier of (n,G,s) is non empty set
(n,G,s) is non empty Element of K19( the carrier of (product G))
G . F is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . F) is non empty set
x2 is Relation-like Function-like set
dom x2 is set
x2 . F is set
s is Element of the carrier of (G . F)
G . s is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . s) is non empty set
t is Relation-like Function-like set
dom t is set
t . s is set
k is Element of the carrier of (G . s)
Carrier G is Relation-like non-empty n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (k * x1) is set
dom (x1 * k) is set
bb is set
(k * x1) . bb is set
(x1 * k) . bb is set
x is Element of n
x2 . x is set
G . x is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x) is Element of the carrier of (G . x)
the carrier of (G . x) is non empty set
t . x is set
(k * x1) . x is set
(1_ (G . x)) * (1_ (G . x)) is Element of the carrier of (G . x)
(x1 * k) . x is set
x is Element of n
t . x is set
G . x is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x) is Element of the carrier of (G . x)
the carrier of (G . x) is non empty set
(k * x1) . x is set
j is Element of the carrier of (G . x)
j * (1_ (G . x)) is Element of the carrier of (G . x)
(1_ (G . x)) * j is Element of the carrier of (G . x)
(x1 * k) . x is set
x is Element of n
x2 . x is set
G . x is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x) is Element of the carrier of (G . x)
the carrier of (G . x) is non empty set
(k * x1) . x is set
j is Element of the carrier of (G . x)
(1_ (G . x)) * j is Element of the carrier of (G . x)
j * (1_ (G . x)) is Element of the carrier of (G . x)
(x1 * k) . x is set
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
G is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
G . F is set
s is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ s is Element of the carrier of s
the carrier of s is non empty set
t is Relation-like Function-like Element of the carrier of (product G)
t . F is set
k is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
dom k is countable Element of K19(NAT)
Product k is Relation-like Function-like Element of the carrier of (product G)
<*> the carrier of (product G) is Relation-like NAT -defined the carrier of (product G) -valued Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V33() V38() V40( {} ) V100() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Cardinal-yielding countable Function-yielding V166() FinSequence of the carrier of (product G)
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
t + 1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
k is Relation-like Function-like Element of the carrier of (product G)
k . F is set
x1 is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len x1 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
dom x1 is countable Element of K19(NAT)
Product x1 is Relation-like Function-like Element of the carrier of (product G)
x1 | t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
Seg t is V33() V40(t) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= t ) } is set
x1 | (Seg t) is Relation-like FinSubsequence-like set
t is Element of Seg n
dom (x1 | t) is countable Element of K19(NAT)
(x1 | t) . t is set
x1 . t is set
((Seg n),G,t) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
Product (x1 | t) is Relation-like Function-like Element of the carrier of (product G)
Seg (t + 1) is non empty V33() V40(t + 1) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= t + 1 ) } is set
len (x1 | t) is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
(len x1) - 1 is V31() V100() ext-real set
(Product (x1 | t)) . F is set
Seg (len x1) is V33() V40( len x1) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len x1 ) } is set
x1 . (len x1) is set
(len (x1 | t)) + 1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
k is Relation-like Function-like Element of the carrier of (product G)
<*k*> is Relation-like NAT -defined Function-like non empty V12() V33() V40(1) FinSequence-like FinSubsequence-like countable Element of the carrier of (product <*(product G)*>)
<*(product G)*> is Relation-like NAT -defined {1} -defined Function-like non empty V12() total V33() V40(1) FinSequence-like FinSubsequence-like countable V178() multMagma-yielding Group-like associative set
[1,(product G)] is set
{[1,(product G)]} is non empty V12() V40(1) set
product <*(product G)*> is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product <*(product G)*>) is non empty set
[1,k] is set
{[1,k]} is non empty V12() V40(1) set
(x1 | t) ^ <*k*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like countable set
len ((x1 | t) ^ <*k*>) is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable Element of NAT
dom ((x1 | t) ^ <*k*>) is countable Element of K19(NAT)
k0 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
x1 . k0 is set
((x1 | t) ^ <*k*>) . k0 is set
Seg ((len (x1 | t)) + 1) is non empty V33() V40((len (x1 | t)) + 1) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= (len (x1 | t)) + 1 ) } is set
Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len (x1 | t) ) } is set
(x1 | t) . k0 is set
Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len (x1 | t) ) } is set
Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len (x1 | t) ) } is set
(Product (x1 | t)) * k is Relation-like Function-like Element of the carrier of (product G)
x2 is Element of Seg n
((Seg n),G,x2) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of ((Seg n),G,x2) is non empty set
((Seg n),G,x2) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
G . x2 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . x2) is non empty set
k0 is Relation-like Function-like set
dom k0 is set
k0 . x2 is set
aa is Element of the carrier of (G . x2)
bb is Element of Seg n
k0 . bb is set
G . bb is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . bb) is Element of the carrier of (G . bb)
the carrier of (G . bb) is non empty set
(1_ (G . bb)) * (1_ (G . bb)) is Element of the carrier of (G . bb)
k is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
dom k is countable Element of K19(NAT)
t is Relation-like Function-like Element of the carrier of (product G)
Product k is Relation-like Function-like Element of the carrier of (product G)
t . F is set
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
G is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
s is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len s is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
dom s is countable Element of K19(NAT)
F is Relation-like Function-like Element of the carrier of (product G)
Product s is Relation-like Function-like Element of the carrier of (product G)
t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
s . t is set
F . t is set
F is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
F + 1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
dom t is countable Element of K19(NAT)
Product t is Relation-like Function-like Element of the carrier of (product G)
t . 1 is set
<*(t . 1)*> is Relation-like NAT -defined Function-like non empty V12() V33() V40(1) FinSequence-like FinSubsequence-like countable set
[1,(t . 1)] is set
{[1,(t . 1)]} is non empty V12() V40(1) set
k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
t . k is set
s . k is set
Seg (len t) is V33() V40( len t) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len t ) } is set
x1 is Relation-like Function-like Element of the carrier of (product G)
x1 . k is set
(F + 1) - 1 is V31() V100() ext-real set
n - 0 is non empty V31() V100() ext-real positive non negative set
k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
t . k is set
s . k is set
t | F is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
Seg F is V33() V40(F) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= F ) } is set
t | (Seg F) is Relation-like FinSubsequence-like set
Seg (F + 1) is non empty V33() V40(F + 1) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= F + 1 ) } is set
dom (t | F) is countable Element of K19(NAT)
len (t | F) is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
(F + 1) - 1 is V31() V100() ext-real set
n - 0 is non empty V31() V100() ext-real positive non negative set
Seg (len t) is V33() V40( len t) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len t ) } is set
Seg (len (t | F)) is V33() V40( len (t | F)) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= len (t | F) ) } is set
x2 is Element of Seg n
(t | F) . x2 is set
t . x2 is set
((Seg n),G,x2) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
Product (t | F) is Relation-like Function-like Element of the carrier of (product G)
t . (len t) is set
s is Relation-like Function-like Element of the carrier of (product G)
<*s*> is Relation-like NAT -defined Function-like non empty V12() V33() V40(1) FinSequence-like FinSubsequence-like countable Element of the carrier of (product <*(product G)*>)
<*(product G)*> is Relation-like NAT -defined {1} -defined Function-like non empty V12() total V33() V40(1) FinSequence-like FinSubsequence-like countable V178() multMagma-yielding Group-like associative set
[1,(product G)] is set
{[1,(product G)]} is non empty V12() V40(1) set
product <*(product G)*> is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product <*(product G)*>) is non empty set
[1,s] is set
{[1,s]} is non empty V12() V40(1) set
(t | F) ^ <*s*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like countable set
(Product (t | F)) * s is Relation-like Function-like Element of the carrier of (product G)
k is Element of Seg n
((Seg n),G,k) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
the carrier of ((Seg n),G,k) is non empty set
((Seg n),G,k) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
G . k is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . k) is non empty set
k is Relation-like Function-like set
dom k is set
k . k is set
k0 is Element of the carrier of (G . k)
aa is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
t . aa is set
s . aa is set
len <*s*> is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable Element of NAT
(len (t | F)) + (len <*s*>) is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
(len (t | F)) + 1 is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
(t | F) . aa is set
(Product (t | F)) . aa is set
bb is Relation-like Function-like Element of the carrier of (product G)
bb . aa is set
x is Element of Seg n
s . x is set
G . x is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . x) is Element of the carrier of (G . x)
the carrier of (G . x) is non empty set
Carrier G is Relation-like non-empty Seg n -defined Function-like total set
(Carrier G) . x is set
j is 1-sorted
the carrier of j is set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (Carrier G) is countable Element of K19((Seg n))
K19((Seg n)) is set
tii is Element of the carrier of (G . x)
tii * (1_ (G . x)) is Element of the carrier of (G . x)
(Product (t | F)) . aa is set
1_ (G . k) is Element of the carrier of (G . k)
(1_ (G . k)) * k0 is Element of the carrier of (G . k)
s . aa is set
k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
t . k is set
s . k is set
F is Relation-like Function-like Element of the carrier of (product G)
s is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len s is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product s is Relation-like Function-like Element of the carrier of (product G)
dom s is countable Element of K19(NAT)
t is Element of Seg n
((Seg n),G,t) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
s . t is set
t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
s . t is set
F . t is set
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
G is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is Relation-like Function-like Element of the carrier of (product G)
s is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len s is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product t is Relation-like Function-like Element of the carrier of (product G)
x1 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
s . x1 is set
F . x1 is set
s is Relation-like Function-like Element of the carrier of (product G)
s . x1 is set
t . x1 is set
t is Relation-like Function-like Element of the carrier of (product G)
t . x1 is set
x2 is Element of Seg n
((Seg n),G,x2) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
s . x2 is set
the carrier of ((Seg n),G,x2) is non empty set
((Seg n),G,x2) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
G . x2 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . x2) is non empty set
k is Relation-like Function-like set
dom k is set
k . x2 is set
k0 is Element of the carrier of (G . x2)
t . x2 is set
aa is Relation-like Function-like set
dom aa is set
aa . x2 is set
bb is Element of the carrier of (G . x2)
x is set
j is Element of Seg n
k . x is set
aa . x is set
j is Element of Seg n
k . j is set
G . j is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
1_ (G . j) is Element of the carrier of (G . j)
the carrier of (G . j) is non empty set
k . x is set
aa . x is set
j is Element of Seg n
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
G is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative set
product G is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
F is Relation-like Function-like Element of the carrier of (product G)
1_ (product G) is Relation-like Function-like Element of the carrier of (product G)
t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
Carrier G is Relation-like non-empty Seg n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom (Carrier G) is countable Element of K19((Seg n))
K19((Seg n)) is set
k is Element of Seg n
G . k is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
(Carrier G) . k is set
x1 is 1-sorted
the carrier of x1 is set
the carrier of (G . k) is non empty set
F . k is set
x2 is Element of the carrier of (G . k)
(1_ (product G)) +* (k,x2) is Relation-like Function-like set
((Seg n),G,k) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
dom t is countable Element of K19(NAT)
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product t is Relation-like Function-like Element of the carrier of (product G)
k is Element of Seg n
((Seg n),G,k) is non empty strict unital Group-like associative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
t . k is set
((Seg n),G,k) is non empty Element of K19( the carrier of (product G))
K19( the carrier of (product G)) is set
x1 is Element of Seg n
G . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . x1) is non empty set
F . x1 is set
x2 is Element of the carrier of (G . x1)
(1_ (product G)) +* (x1,x2) is Relation-like Function-like set
the carrier of ((Seg n),G,k) is non empty set
Carrier G is Relation-like non-empty Seg n -defined Function-like total set
product (Carrier G) is functional non empty with_common_domain product-like set
dom F is set
dom (Product t) is set
dom (1_ (product G)) is set
x1 is set
x2 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
t . x2 is set
(Product t) . x2 is set
F . x1 is set
(Product t) . x1 is set
s is Element of Seg n
G . s is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (G . s) is non empty set
F . s is set
t is Element of the carrier of (G . s)
(1_ (product G)) +* (s,t) is Relation-like Function-like set
k is Relation-like Function-like Element of the carrier of (product G)
k . x2 is set
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
G is non empty unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma
the carrier of G is non empty set
F is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative set
product F is non empty strict unital Group-like associative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product F) is non empty set
K20( the carrier of (product F), the carrier of G) is set
K19(K20( the carrier of (product F), the carrier of G)) is set
Carrier F is Relation-like non-empty Seg n -defined Function-like total set
dom (Carrier F) is countable Element of K19((Seg n))
K19((Seg n)) is set
t is Relation-like Function-like Element of the carrier of (product F)
dom t is set
product (Carrier F) is functional non empty with_common_domain product-like set
x1 is Element of Seg n
t . x1 is set
F . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (F . x1) is non empty set
(Carrier F) . x1 is set
x2 is 1-sorted
the carrier of x2 is set
k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like countable set
dom k is countable Element of K19(NAT)
x1 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable set
k . x1 is set
x2 is Element of Seg n
k . x2 is set
F . x2 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (F . x2) is non empty set
x1 is set
t . x1 is set
(Carrier F) . x1 is set
t is Relation-like Function-like Element of the carrier of (product F)
dom t is set
k is set
t . k is set
(Carrier F) . k is set
x1 is Element of Seg n
t . x1 is set
F . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (F . x1) is non empty set
(Carrier F) . x1 is set
x2 is 1-sorted
the carrier of x2 is set
k is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
x1 is Element of Seg n
k . x1 is set
F . x1 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
the carrier of (F . x1) is non empty set
Product k is Element of the carrier of G
t is Relation-like the carrier of (product F) -defined the carrier of G -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (product F), the carrier of G))
k is Relation-like Function-like Element of the carrier of (product F)
x1 is Relation-like Function-like Element of the carrier of (product F)
k * x1 is Relation-like Function-like Element of the carrier of (product F)
t . (k * x1) is Element of the carrier of G
t . k is Element of the carrier of G
t . x1 is Element of the carrier of G
(t . k) * (t . x1) is Element of the carrier of G
dom k is set
x2 is set
k . x2 is set
(Carrier F) . x2 is set
dom x1 is set
s is set
x1 . s is set
(Carrier F) . s is set
k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
t is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
dom t is countable Element of K19(NAT)
k0 is Element of Seg n
F . k0 is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
(Carrier F) . k0 is set
the carrier of (F . k0) is non empty set
k . k0 is set
bb is 1-sorted
the carrier of bb is set
x1 . k0 is set
x is 1-sorted
the carrier of x is set
aa is Element of the carrier of (F . k0)
x2 is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
x2 /. k0 is Element of the carrier of G
bb is Element of the carrier of (F . k0)
s is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
s /. k0 is Element of the carrier of G
t . k is set
aa * bb is Element of the carrier of (F . k0)
x2 /. k is Element of the carrier of G
s /. k is Element of the carrier of G
(x2 /. k) * (s /. k) is Element of the carrier of G
k is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len k is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product k is Element of the carrier of G
k0 is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len k0 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product k0 is Element of the carrier of G
aa is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len aa is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product aa is Element of the carrier of G
k is Relation-like the carrier of (product F) -defined the carrier of G -valued Function-like non empty total quasi_total V99( product F,G) Element of K19(K20( the carrier of (product F), the carrier of G))
x1 is set
x2 is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len x2 is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product x2 is Element of the carrier of G
product (Carrier F) is functional non empty with_common_domain product-like set
dom x2 is countable Element of K19(NAT)
s is set
x2 . s is set
(Carrier F) . s is set
t is Element of Seg n
F . t is non empty unital Group-like associative V153() V154() V155() V156() V157() V158() multMagma
x2 . t is set
(Carrier F) . t is set
k is 1-sorted
the carrier of k is set
s is Relation-like Function-like Element of the carrier of (product F)
k . s is Element of the carrier of G
rng k is Element of K19( the carrier of G)
K19( the carrier of G) is set
t is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product t is Element of the carrier of G
x1 is set
x2 is set
k . x1 is set
k . x2 is set
s is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len s is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product s is Element of the carrier of G
t is Relation-like NAT -defined the carrier of G -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product t is Element of the carrier of G
x1 is Relation-like Function-like Element of the carrier of (product F)
k . x1 is Element of the carrier of G
n is non empty V24() V25() V26() V30() V31() V33() V38() V100() ext-real positive non negative countable set
Seg n is non empty V33() V40(n) countable Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
F is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative commutative set
G is Relation-like Seg n -defined Function-like total V178() multMagma-yielding Group-like associative commutative set
product F is non empty strict unital Group-like associative commutative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product F) is non empty set
product G is non empty strict unital Group-like associative commutative V143() V153() V154() V155() V156() V157() V158() multMagma
the carrier of (product G) is non empty set
K20( the carrier of (product F), the carrier of (product G)) is set
K19(K20( the carrier of (product F), the carrier of (product G))) is set
s is Element of Seg n
F . s is non empty unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma
((Seg n),G,s) is non empty strict unital Group-like associative commutative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
s is Relation-like Function-like Element of the carrier of (product G)
t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product t is Relation-like Function-like Element of the carrier of (product G)
k is Element of Seg n
F . k is non empty unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma
t . k is set
((Seg n),G,k) is non empty strict unital Group-like associative commutative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
k is Element of Seg n
F . k is non empty unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma
t . k is set
s is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len s is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
t is Relation-like NAT -defined the carrier of (product G) -valued Function-like V33() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (product G)
len t is V24() V25() V26() V30() V31() V33() V38() V100() ext-real non negative countable Element of NAT
Product s is Relation-like Function-like Element of the carrier of (product G)
Product t is Relation-like Function-like Element of the carrier of (product G)
k is Element of Seg n
((Seg n),G,k) is non empty strict unital Group-like associative commutative normal V153() V154() V155() V156() V157() V158() Subgroup of product G
t . k is set
s . k is set
F . k is non empty unital Group-like associative commutative V153() V154() V155() V156() V157() V158() multMagma