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

(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

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

(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

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

(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

(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

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

(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

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

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

(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

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

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

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

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

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

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

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

(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

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

(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

(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

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

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

(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

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

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

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

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

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

Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)

{ b

(x1 | t) . k0 is set

Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)

{ b

Seg (len (x1 | t)) is V33() V40( len (x1 | t)) countable Element of K19(NAT)

{ b

(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

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

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

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

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

Seg (len (t | F)) is V33() V40( len (t | F)) countable Element of K19(NAT)

{ b

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

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

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

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