:: GRSOLV_1 semantic presentation

REAL is set

NAT is non empty V28() V29() V30() Element of K19(REAL)

K19(REAL) is set

NAT is non empty V28() V29() V30() set

K19(NAT) is set

K19(NAT) is set

COMPLEX is set

RAT is set

INT is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K354() is non empty strict Group-like associative commutative cyclic multMagma

the carrier of K354() is non empty V126() set

{} is Function-like functional empty V28() V29() V30() V32() V33() V34() V35() ext-real V107() FinSequence-membered set

1 is non empty V28() V29() V30() V34() V35() ext-real positive V107() Element of NAT

2 is non empty V28() V29() V30() V34() V35() ext-real positive V107() Element of NAT

3 is non empty V28() V29() V30() V34() V35() ext-real positive V107() Element of NAT

Seg 1 is non empty V37() V44(1) Element of K19(NAT)

{1} is non empty set

Seg 2 is non empty V37() V44(2) Element of K19(NAT)

{1,2} is non empty set

0 is Function-like functional empty V28() V29() V30() V32() V33() V34() V35() ext-real V107() FinSequence-membered Element of NAT

the non empty Group-like associative multMagma is non empty Group-like associative multMagma

(1). the non empty Group-like associative multMagma is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of the non empty Group-like associative multMagma

H is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of the non empty Group-like associative multMagma

<*H*> is Relation-like NAT -defined Function-like non empty V37() V44(1) FinSequence-like FinSubsequence-like set

rng <*H*> is set

Subgroups H is non empty set

h is set

{H} is non empty set

h is Relation-like NAT -defined Subgroups H -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups H

len h is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h . 1 is set

(Omega). H is non empty V52() strict Group-like associative commutative normal Subgroup of H

the carrier of H is non empty V12() V37() set

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

multMagma(# the carrier of H, the multF of H #) is strict Group-like associative multMagma

h . (len h) is set

(1). H is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of H

dom h is Element of K19(NAT)

F is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h . F is set

h . (F + 1) is set

z is non empty V52() Group-like associative commutative Subgroup of H

c

G1 is non empty V52() Group-like associative commutative normal Subgroup of z

z ./. G1 is non empty strict Group-like associative multMagma

z is non empty V52() strict Group-like associative commutative Subgroup of H

F is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h . F is set

c

h . (F + 1) is set

G1 is non empty V52() Group-like associative commutative normal Subgroup of z

z ./. G1 is non empty strict Group-like associative multMagma

G is non empty strict Group-like associative multMagma

h is non empty strict Group-like associative Subgroup of G

F is non empty strict Group-like associative Subgroup of G

H is non empty strict Group-like associative Subgroup of G

h /\ H is non empty strict Group-like associative Subgroup of G

F /\ H is non empty strict Group-like associative Subgroup of G

h /\ F is non empty strict Group-like associative Subgroup of G

(h /\ F) /\ H is non empty strict Group-like associative Subgroup of G

h /\ (F /\ H) is non empty strict Group-like associative Subgroup of G

c

z is non empty Group-like associative Subgroup of F

c

G is non empty strict Group-like associative multMagma

H is non empty strict Group-like associative Subgroup of G

the carrier of H is non empty set

h is non empty strict Group-like associative normal Subgroup of H

F is Element of the carrier of H

F * h is Element of K19( the carrier of H)

K19( the carrier of H) is set

carr h is Element of K19( the carrier of H)

the carrier of h is non empty set

F * (carr h) is Element of K19( the carrier of H)

K107( the carrier of H,F) is non empty Element of K19( the carrier of H)

K107( the carrier of H,F) * (carr h) is Element of K19( the carrier of H)

{ (b

z is Element of the carrier of H

z * h is Element of K19( the carrier of H)

z * (carr h) is Element of K19( the carrier of H)

K107( the carrier of H,z) is non empty Element of K19( the carrier of H)

K107( the carrier of H,z) * (carr h) is Element of K19( the carrier of H)

{ (b

(F * h) * (z * h) is Element of K19( the carrier of H)

{ (b

F * z is Element of the carrier of H

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of H . (F,z) is Element of the carrier of H

(F * z) * h is Element of K19( the carrier of H)

(F * z) * (carr h) is Element of K19( the carrier of H)

K107( the carrier of H,(F * z)) is non empty Element of K19( the carrier of H)

K107( the carrier of H,(F * z)) * (carr h) is Element of K19( the carrier of H)

{ (b

H ./. h is non empty strict Group-like associative multMagma

the carrier of (H ./. h) is non empty set

nat_hom h is Relation-like the carrier of H -defined the carrier of (H ./. h) -valued Function-like quasi_total unity-preserving V103(H,H ./. h) Element of K19(K20( the carrier of H, the carrier of (H ./. h)))

K20( the carrier of H, the carrier of (H ./. h)) is set

K19(K20( the carrier of H, the carrier of (H ./. h))) is set

(nat_hom h) . F is Element of the carrier of (H ./. h)

(nat_hom h) . z is Element of the carrier of (H ./. h)

@ ((nat_hom h) . F) is Element of K19( the carrier of H)

@ ((nat_hom h) . z) is Element of K19( the carrier of H)

(nat_hom h) . (F * z) is Element of the carrier of (H ./. h)

((nat_hom h) . F) * ((nat_hom h) . z) is Element of the carrier of (H ./. h)

the multF of (H ./. h) is Relation-like K20( the carrier of (H ./. h), the carrier of (H ./. h)) -defined the carrier of (H ./. h) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (H ./. h), the carrier of (H ./. h)), the carrier of (H ./. h)))

K20( the carrier of (H ./. h), the carrier of (H ./. h)) is set

K20(K20( the carrier of (H ./. h), the carrier of (H ./. h)), the carrier of (H ./. h)) is set

K19(K20(K20( the carrier of (H ./. h), the carrier of (H ./. h)), the carrier of (H ./. h))) is set

the multF of (H ./. h) . (((nat_hom h) . F),((nat_hom h) . z)) is Element of the carrier of (H ./. h)

G is non empty strict Group-like associative multMagma

h is non empty strict Group-like associative Subgroup of G

H is non empty strict Group-like associative Subgroup of G

H /\ h is non empty strict Group-like associative Subgroup of G

F is non empty strict Group-like associative normal Subgroup of h

H /\ F is non empty strict Group-like associative Subgroup of G

h ./. F is non empty strict Group-like associative multMagma

the carrier of h is non empty set

the carrier of (h ./. F) is non empty set

nat_hom F is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like quasi_total unity-preserving V103(h,h ./. F) Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

K20( the carrier of h, the carrier of (h ./. F)) is set

K19(K20( the carrier of h, the carrier of (h ./. F))) is set

the carrier of H is non empty set

(nat_hom F) | the carrier of H is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

c

carr h is Element of K19( the carrier of G)

the carrier of G is non empty set

K19( the carrier of G) is set

carr H is Element of K19( the carrier of G)

G1 is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

dom G1 is Element of K19( the carrier of h)

K19( the carrier of h) is set

dom c

the carrier of h /\ the carrier of H is set

h /\ H is non empty strict Group-like associative Subgroup of G

carr (h /\ H) is Element of K19( the carrier of G)

the carrier of (h /\ H) is non empty set

the carrier of (H /\ h) is non empty set

rng ((nat_hom F) | the carrier of H) is Element of K19( the carrier of (h ./. F))

K19( the carrier of (h ./. F)) is set

rng (nat_hom F) is Element of K19( the carrier of (h ./. F))

K20( the carrier of (H /\ h), the carrier of (h ./. F)) is set

K19(K20( the carrier of (H /\ h), the carrier of (h ./. F))) is set

G2 is Relation-like the carrier of (H /\ h) -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20( the carrier of (H /\ h), the carrier of (h ./. F)))

A is Element of the carrier of (H /\ h)

B is Element of the carrier of (H /\ h)

A * B is Element of the carrier of (H /\ h)

the multF of (H /\ h) is Relation-like K20( the carrier of (H /\ h), the carrier of (H /\ h)) -defined the carrier of (H /\ h) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (H /\ h), the carrier of (H /\ h)), the carrier of (H /\ h)))

K20( the carrier of (H /\ h), the carrier of (H /\ h)) is set

K20(K20( the carrier of (H /\ h), the carrier of (H /\ h)), the carrier of (H /\ h)) is set

K19(K20(K20( the carrier of (H /\ h), the carrier of (H /\ h)), the carrier of (H /\ h))) is set

the multF of (H /\ h) . (A,B) is Element of the carrier of (H /\ h)

G2 . (A * B) is Element of the carrier of (h ./. F)

G2 . A is Element of the carrier of (h ./. F)

G2 . B is Element of the carrier of (h ./. F)

(G2 . A) * (G2 . B) is Element of the carrier of (h ./. F)

the multF of (h ./. F) is Relation-like K20( the carrier of (h ./. F), the carrier of (h ./. F)) -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F)))

K20( the carrier of (h ./. F), the carrier of (h ./. F)) is set

K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F)) is set

K19(K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F))) is set

the multF of (h ./. F) . ((G2 . A),(G2 . B)) is Element of the carrier of (h ./. F)

(carr H) /\ (carr h) is Element of K19( the carrier of G)

((nat_hom F) | the carrier of H) . B is set

(nat_hom F) . B is set

((nat_hom F) | the carrier of H) . (A * B) is set

(nat_hom F) . (A * B) is set

N is Element of the carrier of h

x is Element of the carrier of h

N * x is Element of the carrier of h

the multF of h is Relation-like K20( the carrier of h, the carrier of h) -defined the carrier of h -valued Function-like quasi_total Element of K19(K20(K20( the carrier of h, the carrier of h), the carrier of h))

K20( the carrier of h, the carrier of h) is set

K20(K20( the carrier of h, the carrier of h), the carrier of h) is set

K19(K20(K20( the carrier of h, the carrier of h), the carrier of h)) is set

the multF of h . (N,x) is Element of the carrier of h

((nat_hom F) | the carrier of H) . A is set

(nat_hom F) . A is set

the carrier of H /\ the carrier of h is set

carr (H /\ h) is Element of K19( the carrier of G)

A is Relation-like the carrier of (H /\ h) -defined the carrier of (h ./. F) -valued Function-like quasi_total unity-preserving V103(H /\ h,h ./. F) Element of K19(K20( the carrier of (H /\ h), the carrier of (h ./. F)))

Ker A is non empty strict Group-like associative normal Subgroup of H /\ h

B is non empty Group-like associative Subgroup of G

N is Element of the carrier of G

carr (Ker A) is Element of K19( the carrier of (H /\ h))

K19( the carrier of (H /\ h)) is set

the carrier of (Ker A) is non empty set

(carr H) /\ (carr h) is Element of K19( the carrier of G)

x is Element of the carrier of (H /\ h)

((nat_hom F) | the carrier of H) . x is set

(nat_hom F) . x is set

A . x is Element of the carrier of (h ./. F)

y is Element of the carrier of h

y * F is Element of K19( the carrier of h)

carr F is Element of K19( the carrier of h)

the carrier of F is non empty set

y * (carr F) is Element of K19( the carrier of h)

K107( the carrier of h,y) is non empty Element of K19( the carrier of h)

K107( the carrier of h,y) * (carr F) is Element of K19( the carrier of h)

{ (b

1_ (h ./. F) is Element of the carrier of (h ./. F)

the carrier of F is non empty set

the carrier of H /\ the carrier of F is set

x is non empty strict Group-like associative Subgroup of G

carr x is Element of K19( the carrier of G)

the carrier of x is non empty set

(carr H) /\ (carr x) is Element of K19( the carrier of G)

the carrier of (H /\ F) is non empty set

carr (H /\ F) is Element of K19( the carrier of G)

y is Element of the carrier of (H /\ h)

(carr H) /\ (carr h) is Element of K19( the carrier of G)

((nat_hom F) | the carrier of H) . y is set

(nat_hom F) . y is set

A . y is Element of the carrier of (h ./. F)

a is Element of the carrier of h

a * F is Element of K19( the carrier of h)

carr F is Element of K19( the carrier of h)

a * (carr F) is Element of K19( the carrier of h)

K107( the carrier of h,a) is non empty Element of K19( the carrier of h)

K107( the carrier of h,a) * (carr F) is Element of K19( the carrier of h)

{ (b

1_ (h ./. F) is Element of the carrier of (h ./. F)

z is non empty strict Group-like associative Subgroup of G

B is non empty strict Group-like associative normal Subgroup of z

z ./. B is non empty strict Group-like associative multMagma

Image A is non empty strict Group-like associative Subgroup of h ./. F

N is non empty strict Group-like associative Subgroup of G

x is non empty Group-like associative normal Subgroup of N

N ./. x is non empty strict Group-like associative multMagma

G is non empty strict Group-like associative multMagma

h is non empty strict Group-like associative Subgroup of G

H is non empty strict Group-like associative Subgroup of G

h /\ H is non empty strict Group-like associative Subgroup of G

F is non empty strict Group-like associative normal Subgroup of h

F /\ H is non empty strict Group-like associative Subgroup of G

h ./. F is non empty strict Group-like associative multMagma

the carrier of h is non empty set

the carrier of (h ./. F) is non empty set

nat_hom F is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like quasi_total unity-preserving V103(h,h ./. F) Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

K20( the carrier of h, the carrier of (h ./. F)) is set

K19(K20( the carrier of h, the carrier of (h ./. F))) is set

the carrier of H is non empty set

(nat_hom F) | the carrier of H is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

c

carr h is Element of K19( the carrier of G)

the carrier of G is non empty set

K19( the carrier of G) is set

carr H is Element of K19( the carrier of G)

G1 is Relation-like the carrier of h -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20( the carrier of h, the carrier of (h ./. F)))

dom G1 is Element of K19( the carrier of h)

K19( the carrier of h) is set

dom c

the carrier of h /\ the carrier of H is set

the carrier of (h /\ H) is non empty set

rng ((nat_hom F) | the carrier of H) is Element of K19( the carrier of (h ./. F))

K19( the carrier of (h ./. F)) is set

rng (nat_hom F) is Element of K19( the carrier of (h ./. F))

K20( the carrier of (h /\ H), the carrier of (h ./. F)) is set

K19(K20( the carrier of (h /\ H), the carrier of (h ./. F))) is set

G2 is Relation-like the carrier of (h /\ H) -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20( the carrier of (h /\ H), the carrier of (h ./. F)))

A is Element of the carrier of (h /\ H)

B is Element of the carrier of (h /\ H)

A * B is Element of the carrier of (h /\ H)

the multF of (h /\ H) is Relation-like K20( the carrier of (h /\ H), the carrier of (h /\ H)) -defined the carrier of (h /\ H) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (h /\ H), the carrier of (h /\ H)), the carrier of (h /\ H)))

K20( the carrier of (h /\ H), the carrier of (h /\ H)) is set

K20(K20( the carrier of (h /\ H), the carrier of (h /\ H)), the carrier of (h /\ H)) is set

K19(K20(K20( the carrier of (h /\ H), the carrier of (h /\ H)), the carrier of (h /\ H))) is set

the multF of (h /\ H) . (A,B) is Element of the carrier of (h /\ H)

G2 . (A * B) is Element of the carrier of (h ./. F)

G2 . A is Element of the carrier of (h ./. F)

G2 . B is Element of the carrier of (h ./. F)

(G2 . A) * (G2 . B) is Element of the carrier of (h ./. F)

the multF of (h ./. F) is Relation-like K20( the carrier of (h ./. F), the carrier of (h ./. F)) -defined the carrier of (h ./. F) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F)))

K20( the carrier of (h ./. F), the carrier of (h ./. F)) is set

K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F)) is set

K19(K20(K20( the carrier of (h ./. F), the carrier of (h ./. F)), the carrier of (h ./. F))) is set

the multF of (h ./. F) . ((G2 . A),(G2 . B)) is Element of the carrier of (h ./. F)

(carr H) /\ (carr h) is Element of K19( the carrier of G)

((nat_hom F) | the carrier of H) . B is set

(nat_hom F) . B is set

((nat_hom F) | the carrier of H) . (A * B) is set

(nat_hom F) . (A * B) is set

N is Element of the carrier of h

x is Element of the carrier of h

N * x is Element of the carrier of h

the multF of h is Relation-like K20( the carrier of h, the carrier of h) -defined the carrier of h -valued Function-like quasi_total Element of K19(K20(K20( the carrier of h, the carrier of h), the carrier of h))

K20( the carrier of h, the carrier of h) is set

K20(K20( the carrier of h, the carrier of h), the carrier of h) is set

K19(K20(K20( the carrier of h, the carrier of h), the carrier of h)) is set

the multF of h . (N,x) is Element of the carrier of h

((nat_hom F) | the carrier of H) . A is set

(nat_hom F) . A is set

the carrier of H /\ the carrier of h is set

carr (h /\ H) is Element of K19( the carrier of G)

A is Relation-like the carrier of (h /\ H) -defined the carrier of (h ./. F) -valued Function-like quasi_total unity-preserving V103(h /\ H,h ./. F) Element of K19(K20( the carrier of (h /\ H), the carrier of (h ./. F)))

Ker A is non empty strict Group-like associative normal Subgroup of h /\ H

B is non empty Group-like associative Subgroup of G

N is Element of the carrier of G

carr (Ker A) is Element of K19( the carrier of (h /\ H))

K19( the carrier of (h /\ H)) is set

the carrier of (Ker A) is non empty set

(carr H) /\ (carr h) is Element of K19( the carrier of G)

x is Element of the carrier of (h /\ H)

((nat_hom F) | the carrier of H) . x is set

(nat_hom F) . x is set

A . x is Element of the carrier of (h ./. F)

y is Element of the carrier of h

y * F is Element of K19( the carrier of h)

carr F is Element of K19( the carrier of h)

the carrier of F is non empty set

y * (carr F) is Element of K19( the carrier of h)

K107( the carrier of h,y) is non empty Element of K19( the carrier of h)

K107( the carrier of h,y) * (carr F) is Element of K19( the carrier of h)

{ (b

1_ (h ./. F) is Element of the carrier of (h ./. F)

the carrier of F is non empty set

the carrier of H /\ the carrier of F is set

x is non empty strict Group-like associative Subgroup of G

carr x is Element of K19( the carrier of G)

the carrier of x is non empty set

(carr H) /\ (carr x) is Element of K19( the carrier of G)

the carrier of (F /\ H) is non empty set

carr (F /\ H) is Element of K19( the carrier of G)

y is Element of the carrier of (h /\ H)

(carr H) /\ (carr h) is Element of K19( the carrier of G)

((nat_hom F) | the carrier of H) . y is set

(nat_hom F) . y is set

A . y is Element of the carrier of (h ./. F)

a is Element of the carrier of h

a * F is Element of K19( the carrier of h)

carr F is Element of K19( the carrier of h)

a * (carr F) is Element of K19( the carrier of h)

K107( the carrier of h,a) is non empty Element of K19( the carrier of h)

K107( the carrier of h,a) * (carr F) is Element of K19( the carrier of h)

{ (b

1_ (h ./. F) is Element of the carrier of (h ./. F)

z is non empty strict Group-like associative Subgroup of G

B is non empty strict Group-like associative normal Subgroup of z

z ./. B is non empty strict Group-like associative multMagma

Image A is non empty strict Group-like associative Subgroup of h ./. F

N is non empty strict Group-like associative Subgroup of G

x is non empty Group-like associative normal Subgroup of N

N ./. x is non empty strict Group-like associative multMagma

G is non empty strict Group-like associative () multMagma

H is non empty strict Group-like associative Subgroup of G

Subgroups G is non empty set

(Omega). G is non empty strict Group-like associative normal Subgroup of G

the carrier of G is non empty set

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict Group-like associative multMagma

(1). G is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of G

h is Relation-like NAT -defined Subgroups G -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups G

len h is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h . 1 is set

h . (len h) is set

dom h is Element of K19(NAT)

Seg (len h) is V37() V44( len h) Element of K19(NAT)

Subgroups H is non empty set

F is V28() V29() V30() V34() V35() ext-real V107() set

h . F is set

z is non empty strict Group-like associative Subgroup of G

z /\ H is non empty strict Group-like associative Subgroup of G

c

G1 is Element of Subgroups H

F is Relation-like NAT -defined Subgroups H -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups H

dom F is Element of K19(NAT)

z is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

z + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F . z is set

F . (z + 1) is set

h . (z + 1) is set

c

c

h . z is set

G1 is non empty strict Group-like associative Subgroup of G

G1 /\ H is non empty strict Group-like associative Subgroup of G

G2 is non empty strict Group-like associative Subgroup of H

A is non empty strict Group-like associative Subgroup of H

N is non empty strict Group-like associative normal Subgroup of G2

G2 ./. N is non empty strict Group-like associative multMagma

B is non empty strict Group-like associative normal Subgroup of G1

G1 ./. B is non empty strict Group-like associative multMagma

x is non empty Group-like associative Subgroup of G1 ./. B

the carrier of (G2 ./. N) is non empty set

the carrier of x is non empty set

K20( the carrier of (G2 ./. N), the carrier of x) is set

K19(K20( the carrier of (G2 ./. N), the carrier of x)) is set

y is Relation-like the carrier of (G2 ./. N) -defined the carrier of x -valued Function-like quasi_total unity-preserving V103(G2 ./. N,x) Element of K19(K20( the carrier of (G2 ./. N), the carrier of x))

a is Element of the carrier of (G2 ./. N)

y . a is Element of the carrier of x

x1 is Element of the carrier of x

b is Element of the carrier of (G2 ./. N)

y . b is Element of the carrier of x

b1 is Element of the carrier of x

the multF of x is Relation-like K20( the carrier of x, the carrier of x) -defined the carrier of x -valued Function-like quasi_total Element of K19(K20(K20( the carrier of x, the carrier of x), the carrier of x))

K20( the carrier of x, the carrier of x) is set

K20(K20( the carrier of x, the carrier of x), the carrier of x) is set

K19(K20(K20( the carrier of x, the carrier of x), the carrier of x)) is set

x1 * b1 is Element of the carrier of x

the multF of x . (x1,b1) is Element of the carrier of x

b1 * x1 is Element of the carrier of x

the multF of x . (b1,x1) is Element of the carrier of x

the multF of (G2 ./. N) is Relation-like K20( the carrier of (G2 ./. N), the carrier of (G2 ./. N)) -defined the carrier of (G2 ./. N) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (G2 ./. N), the carrier of (G2 ./. N)), the carrier of (G2 ./. N)))

K20( the carrier of (G2 ./. N), the carrier of (G2 ./. N)) is set

K20(K20( the carrier of (G2 ./. N), the carrier of (G2 ./. N)), the carrier of (G2 ./. N)) is set

K19(K20(K20( the carrier of (G2 ./. N), the carrier of (G2 ./. N)), the carrier of (G2 ./. N))) is set

the multF of (G2 ./. N) . (a,b) is Element of the carrier of (G2 ./. N)

y " is Relation-like Function-like set

a * b is Element of the carrier of (G2 ./. N)

y . (a * b) is Element of the carrier of x

(y ") . (y . (a * b)) is set

(y . b) * (y . a) is Element of the carrier of x

the multF of x . ((y . b),(y . a)) is Element of the carrier of x

(y ") . ((y . b) * (y . a)) is set

b * a is Element of the carrier of (G2 ./. N)

the multF of (G2 ./. N) . (b,a) is Element of the carrier of (G2 ./. N)

y . (b * a) is Element of the carrier of x

(y ") . (y . (b * a)) is set

B is non empty strict Group-like associative normal Subgroup of G1

B /\ H is non empty strict Group-like associative Subgroup of G

N is non empty Group-like associative normal Subgroup of G2

G2 ./. N is non empty strict Group-like associative multMagma

len F is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F . 1 is set

(Omega). H is non empty strict Group-like associative normal Subgroup of H

the carrier of H is non empty set

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

multMagma(# the carrier of H, the multF of H #) is strict Group-like associative multMagma

z is non empty strict Group-like associative Subgroup of G

z /\ H is non empty strict Group-like associative Subgroup of G

F . (len F) is set

(1). H is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of H

h . (len F) is set

z is non empty strict Group-like associative Subgroup of G

z /\ H is non empty strict Group-like associative Subgroup of G

c

z is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

z + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F . z is set

G1 is non empty strict Group-like associative Subgroup of H

F . (z + 1) is set

G2 is non empty Group-like associative normal Subgroup of c

c

G is non empty strict Group-like associative multMagma

Subgroups G is non empty set

(Omega). G is non empty strict Group-like associative normal Subgroup of G

the carrier of G is non empty set

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict Group-like associative multMagma

(1). G is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of G

H is Relation-like NAT -defined Subgroups G -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups G

len H is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

H . 1 is set

H . (len H) is set

dom H is Element of K19(NAT)

F is non empty strict Group-like associative Subgroup of G

h is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

H . h is set

z is non empty strict Group-like associative Subgroup of G

H . (h + 1) is set

c

F ./. c

G is non empty strict Group-like associative commutative multMagma

(Omega). G is non empty strict Group-like associative commutative normal Subgroup of G

the carrier of G is non empty set

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict Group-like associative multMagma

Subgroups G is non empty set

(1). G is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of G

<*((Omega). G),((1). G)*> is Relation-like NAT -defined Function-like non empty V37() V44(2) FinSequence-like FinSubsequence-like set

H is Relation-like NAT -defined Subgroups G -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups G

H . 1 is set

len H is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

H . 2 is set

dom H is Element of K19(NAT)

h is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

h + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

H . h is set

H . (h + 1) is set

F is non empty strict Group-like associative commutative Subgroup of G

z is non empty strict Group-like associative commutative Subgroup of G

c

F ./. c

c

F ./. c

F is non empty strict Group-like associative commutative Subgroup of G

z is non empty strict Group-like associative commutative Subgroup of G

c

F ./. c

G is non empty Group-like associative multMagma

the carrier of G is non empty set

H is non empty Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty Group-like associative Subgroup of G

the carrier of F is non empty set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

c

h . c

G1 is Element of the carrier of G

h . G1 is Element of the carrier of H

the multF of H . ((h . c

the multF of G . (c

h . ( the multF of G . (c

(h . c

c

h . (c

z is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total Element of K19(K20( the carrier of F, the carrier of H))

c

z . c

h . c

G1 is Element of the carrier of F

z . G1 is Element of the carrier of H

h . G1 is set

the multF of G . (c

c

the multF of F is Relation-like K20( the carrier of F, the carrier of F) -defined the carrier of F -valued Function-like quasi_total Element of K19(K20(K20( the carrier of F, the carrier of F), the carrier of F))

K20( the carrier of F, the carrier of F) is set

K20(K20( the carrier of F, the carrier of F), the carrier of F) is set

K19(K20(K20( the carrier of F, the carrier of F), the carrier of F)) is set

the multF of F . (c

A is Element of the carrier of G

G2 is Element of the carrier of G

A * G2 is Element of the carrier of G

the multF of G . (A,G2) is Element of the carrier of G

(z . c

the multF of H . ((z . c

h . ( the multF of G . (c

z . (c

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

F is non empty Group-like associative Subgroup of G

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

the carrier of (G,H,h,F) is non empty set

h .: the carrier of F is Element of K19( the carrier of H)

K19( the carrier of H) is set

rng (G,H,h,F) is Element of K19( the carrier of H)

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

Image h is non empty strict Group-like associative Subgroup of H

F is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

h .: the carrier of G is Element of K19( the carrier of H)

K19( the carrier of H) is set

the carrier of (Image h) is non empty set

the carrier of (Image (G,H,h,F)) is non empty set

rng (G,H,h,F) is Element of K19( the carrier of H)

h .: the carrier of F is Element of K19( the carrier of H)

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

Image h is non empty strict Group-like associative Subgroup of H

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

(1). G is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of G

(1). H is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of H

(Omega). G is non empty strict Group-like associative normal Subgroup of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict Group-like associative multMagma

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

(G,H,h,((1). G)) is non empty strict Group-like associative Subgroup of H

(G,H,h,((1). G)) is Relation-like the carrier of ((1). G) -defined the carrier of H -valued Function-like quasi_total unity-preserving V103( (1). G,H) Element of K19(K20( the carrier of ((1). G), the carrier of H))

the carrier of ((1). G) is non empty V12() V37() set

K20( the carrier of ((1). G), the carrier of H) is set

K19(K20( the carrier of ((1). G), the carrier of H)) is set

h | the carrier of ((1). G) is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,((1). G)) is non empty V52() strict Group-like associative Subgroup of H

(G,H,h,((Omega). G)) is non empty strict Group-like associative Subgroup of H

(G,H,h,((Omega). G)) is Relation-like the carrier of ((Omega). G) -defined the carrier of H -valued Function-like quasi_total unity-preserving V103( (Omega). G,H) Element of K19(K20( the carrier of ((Omega). G), the carrier of H))

the carrier of ((Omega). G) is non empty set

K20( the carrier of ((Omega). G), the carrier of H) is set

K19(K20( the carrier of ((Omega). G), the carrier of H)) is set

h | the carrier of ((Omega). G) is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,((Omega). G)) is non empty strict Group-like associative Subgroup of H

Image h is non empty strict Group-like associative Subgroup of H

(Omega). (Image h) is non empty strict Group-like associative normal Subgroup of Image h

the carrier of (Image h) is non empty set

the multF of (Image h) is Relation-like K20( the carrier of (Image h), the carrier of (Image h)) -defined the carrier of (Image h) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (Image h), the carrier of (Image h)), the carrier of (Image h)))

K20( the carrier of (Image h), the carrier of (Image h)) is set

K20(K20( the carrier of (Image h), the carrier of (Image h)), the carrier of (Image h)) is set

K19(K20(K20( the carrier of (Image h), the carrier of (Image h)), the carrier of (Image h))) is set

multMagma(# the carrier of (Image h), the multF of (Image h) #) is strict Group-like associative multMagma

dom h is Element of K19( the carrier of G)

K19( the carrier of G) is set

the carrier of ((1). H) is non empty V12() V37() set

1_ H is Element of the carrier of H

{(1_ H)} is non empty set

1_ G is Element of the carrier of G

{(1_ G)} is non empty set

the carrier of (G,H,h,((1). G)) is non empty set

Im (h,(1_ G)) is set

h .: {(1_ G)} is set

h . (1_ G) is Element of the carrier of H

{(h . (1_ G))} is non empty set

the carrier of (G,H,h,((Omega). G)) is non empty set

h .: the carrier of G is Element of K19( the carrier of H)

K19( the carrier of H) is set

the carrier of ((Omega). (Image h)) is non empty set

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty strict Group-like associative Subgroup of G

z is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,z) is non empty strict Group-like associative Subgroup of H

(G,H,h,z) is Relation-like the carrier of z -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(z,H) Element of K19(K20( the carrier of z, the carrier of H))

the carrier of z is non empty set

K20( the carrier of z, the carrier of H) is set

K19(K20( the carrier of z, the carrier of H)) is set

h | the carrier of z is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,z) is non empty strict Group-like associative Subgroup of H

h .: the carrier of F is Element of K19( the carrier of H)

K19( the carrier of H) is set

h .: the carrier of z is Element of K19( the carrier of H)

the carrier of (G,H,h,z) is non empty set

the carrier of (G,H,h,F) is non empty set

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

z is Element of the carrier of G

h . z is Element of the carrier of H

(h . z) * (G,H,h,F) is Element of K19( the carrier of H)

K19( the carrier of H) is set

carr (G,H,h,F) is Element of K19( the carrier of H)

the carrier of (G,H,h,F) is non empty set

(h . z) * (carr (G,H,h,F)) is Element of K19( the carrier of H)

K107( the carrier of H,(h . z)) is non empty Element of K19( the carrier of H)

K107( the carrier of H,(h . z)) * (carr (G,H,h,F)) is Element of K19( the carrier of H)

{ (b

z * F is Element of K19( the carrier of G)

K19( the carrier of G) is set

carr F is Element of K19( the carrier of G)

z * (carr F) is Element of K19( the carrier of G)

K107( the carrier of G,z) is non empty Element of K19( the carrier of G)

K107( the carrier of G,z) * (carr F) is Element of K19( the carrier of G)

{ (b

h .: (z * F) is Element of K19( the carrier of H)

(G,H,h,F) * (h . z) is Element of K19( the carrier of H)

(carr (G,H,h,F)) * (h . z) is Element of K19( the carrier of H)

(carr (G,H,h,F)) * K107( the carrier of H,(h . z)) is Element of K19( the carrier of H)

{ (b

F * z is Element of K19( the carrier of G)

(carr F) * z is Element of K19( the carrier of G)

(carr F) * K107( the carrier of G,z) is Element of K19( the carrier of G)

{ (b

h .: (F * z) is Element of K19( the carrier of H)

c

G1 is set

h . G1 is set

G2 is Element of the carrier of G

A is Element of the carrier of G

z * A is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

the multF of G . (z,A) is Element of the carrier of G

h . A is Element of the carrier of H

h .: the carrier of F is Element of K19( the carrier of H)

(h . z) * (h . A) is Element of the carrier of H

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of H . ((h . z),(h . A)) is Element of the carrier of H

c

G1 is Element of the carrier of H

(h . z) * G1 is Element of the carrier of H

the multF of H . ((h . z),G1) is Element of the carrier of H

G2 is Element of the carrier of F

(G,H,h,F) . G2 is Element of the carrier of H

A is Element of the carrier of G

h . A is Element of the carrier of H

z * A is Element of the carrier of G

the multF of G . (z,A) is Element of the carrier of G

h . (z * A) is Element of the carrier of H

c

G1 is set

h . G1 is set

G2 is Element of the carrier of G

A is Element of the carrier of G

A * z is Element of the carrier of G

the multF of G . (A,z) is Element of the carrier of G

h . A is Element of the carrier of H

(h . A) * (h . z) is Element of the carrier of H

the multF of H . ((h . A),(h . z)) is Element of the carrier of H

c

G1 is Element of the carrier of H

G1 * (h . z) is Element of the carrier of H

the multF of H . (G1,(h . z)) is Element of the carrier of H

G2 is Element of the carrier of F

(G,H,h,F) . G2 is Element of the carrier of H

A is Element of the carrier of G

h . A is Element of the carrier of H

A * z is Element of the carrier of G

the multF of G . (A,z) is Element of the carrier of G

h . (A * z) is Element of the carrier of H

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

K19( the carrier of G) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is Element of K19( the carrier of G)

h .: F is Element of K19( the carrier of H)

K19( the carrier of H) is set

z is Element of K19( the carrier of G)

h .: z is Element of K19( the carrier of H)

(h .: F) * (h .: z) is Element of K19( the carrier of H)

{ (b

F * z is Element of K19( the carrier of G)

{ (b

h .: (F * z) is Element of K19( the carrier of H)

c

G1 is Element of the carrier of H

G2 is Element of the carrier of H

G1 * G2 is Element of the carrier of H

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of H . (G1,G2) is Element of the carrier of H

A is set

h . A is set

N is set

h . N is set

x is Element of the carrier of G

B is Element of the carrier of G

x * B is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

the multF of G . (x,B) is Element of the carrier of G

h . (x * B) is Element of the carrier of H

c

G1 is set

h . G1 is set

G2 is Element of the carrier of G

A is Element of the carrier of G

B is Element of the carrier of G

A * B is Element of the carrier of G

the multF of G . (A,B) is Element of the carrier of G

h . A is Element of the carrier of H

h . B is Element of the carrier of H

(h . A) * (h . B) is Element of the carrier of H

the multF of H . ((h . A),(h . B)) is Element of the carrier of H

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

F is non empty strict Group-like associative Subgroup of G

z is non empty strict Group-like associative Subgroup of G

(G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,F) is Relation-like the carrier of F -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(F,H) Element of K19(K20( the carrier of F, the carrier of H))

the carrier of F is non empty set

K20( the carrier of F, the carrier of H) is set

K19(K20( the carrier of F, the carrier of H)) is set

h | the carrier of F is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,F) is non empty strict Group-like associative Subgroup of H

(G,H,h,z) is non empty strict Group-like associative Subgroup of H

(G,H,h,z) is Relation-like the carrier of z -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(z,H) Element of K19(K20( the carrier of z, the carrier of H))

the carrier of z is non empty set

K20( the carrier of z, the carrier of H) is set

K19(K20( the carrier of z, the carrier of H)) is set

h | the carrier of z is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,z) is non empty strict Group-like associative Subgroup of H

c

(G,H,h,c

(G,H,h,c

the carrier of c

K20( the carrier of c

K19(K20( the carrier of c

h | the carrier of c

Image (G,H,h,c

the carrier of (G,H,h,z) is non empty set

G1 is non empty strict Group-like associative Subgroup of (G,H,h,z)

G2 is Element of the carrier of (G,H,h,z)

G2 * G1 is Element of K19( the carrier of (G,H,h,z))

K19( the carrier of (G,H,h,z)) is set

carr G1 is Element of K19( the carrier of (G,H,h,z))

the carrier of G1 is non empty set

G2 * (carr G1) is Element of K19( the carrier of (G,H,h,z))

K107( the carrier of (G,H,h,z),G2) is non empty Element of K19( the carrier of (G,H,h,z))

K107( the carrier of (G,H,h,z),G2) * (carr G1) is Element of K19( the carrier of (G,H,h,z))

{ (b

G1 * G2 is Element of K19( the carrier of (G,H,h,z))

(carr G1) * G2 is Element of K19( the carrier of (G,H,h,z))

(carr G1) * K107( the carrier of (G,H,h,z),G2) is Element of K19( the carrier of (G,H,h,z))

{ (b

A is Element of the carrier of z

(G,H,h,z) . A is Element of the carrier of H

B is Element of the carrier of G

h . B is Element of the carrier of H

x is set

y is Element of the carrier of (G,H,h,z)

G2 * y is Element of the carrier of (G,H,h,z)

the multF of (G,H,h,z) is Relation-like K20( the carrier of (G,H,h,z), the carrier of (G,H,h,z)) -defined the carrier of (G,H,h,z) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (G,H,h,z), the carrier of (G,H,h,z)), the carrier of (G,H,h,z)))

K20( the carrier of (G,H,h,z), the carrier of (G,H,h,z)) is set

K20(K20( the carrier of (G,H,h,z), the carrier of (G,H,h,z)), the carrier of (G,H,h,z)) is set

K19(K20(K20( the carrier of (G,H,h,z), the carrier of (G,H,h,z)), the carrier of (G,H,h,z))) is set

the multF of (G,H,h,z) . (G2,y) is Element of the carrier of (G,H,h,z)

a is Element of the carrier of c

(G,H,h,c

b is Element of the carrier of G

h . b is Element of the carrier of H

(h . B) * (h . b) is Element of the carrier of H

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of H . ((h . B),(h . b)) is Element of the carrier of H

B * b is Element of the carrier of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

the multF of G . (B,b) is Element of the carrier of G

h . (B * b) is Element of the carrier of H

B * c

K19( the carrier of G) is set

carr c

B * (carr c

K107( the carrier of G,B) is non empty Element of K19( the carrier of G)

K107( the carrier of G,B) * (carr c

{ (b

c

(carr c

(carr c

{ (b

h .: (c

K19( the carrier of H) is set

(G,H,h,c

carr (G,H,h,c

the carrier of (G,H,h,c

(carr (G,H,h,c

K107( the carrier of H,(h . B)) is non empty Element of K19( the carrier of H)

(carr (G,H,h,c

{ (b

N is Element of the carrier of z

N * c

K19( the carrier of z) is set

carr c

N * (carr c

K107( the carrier of z,N) is non empty Element of K19( the carrier of z)

K107( the carrier of z,N) * (carr c

{ (b

c

(carr c

(carr c

{ (b

G is non empty strict Group-like associative multMagma

the carrier of G is non empty set

H is non empty strict Group-like associative multMagma

the carrier of H is non empty set

K20( the carrier of G, the carrier of H) is set

K19(K20( the carrier of G, the carrier of H)) is set

h is Relation-like the carrier of G -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(G,H) Element of K19(K20( the carrier of G, the carrier of H))

Image h is non empty strict Group-like associative Subgroup of H

Subgroups G is non empty set

(Omega). G is non empty strict Group-like associative normal Subgroup of G

the multF of G is Relation-like K20( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))

K20( the carrier of G, the carrier of G) is set

K20(K20( the carrier of G, the carrier of G), the carrier of G) is set

K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is set

multMagma(# the carrier of G, the multF of G #) is strict Group-like associative multMagma

(1). G is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of G

F is Relation-like NAT -defined Subgroups G -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups G

len F is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

F . 1 is set

F . (len F) is set

dom F is Element of K19(NAT)

Seg (len F) is V37() V44( len F) Element of K19(NAT)

Subgroups (Image h) is non empty set

z is V28() V29() V30() V34() V35() ext-real V107() set

F . z is set

c

(G,H,h,c

(G,H,h,c

the carrier of c

K20( the carrier of c

K19(K20( the carrier of c

h | the carrier of c

Image (G,H,h,c

z is Relation-like NAT -defined Subgroups (Image h) -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of Subgroups (Image h)

dom z is Element of K19(NAT)

len z is V28() V29() V30() V34() V35() ext-real V107() Element of NAT

Seg (len z) is V37() V44( len z) Element of K19(NAT)

c

c

z . c

z . (c

G1 is non empty strict Group-like associative Subgroup of Image h

G2 is non empty strict Group-like associative Subgroup of Image h

F . c

A is non empty strict Group-like associative Subgroup of G

(G,H,h,A) is non empty strict Group-like associative Subgroup of H

(G,H,h,A) is Relation-like the carrier of A -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(A,H) Element of K19(K20( the carrier of A, the carrier of H))

the carrier of A is non empty set

K20( the carrier of A, the carrier of H) is set

K19(K20( the carrier of A, the carrier of H)) is set

h | the carrier of A is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,A) is non empty strict Group-like associative Subgroup of H

F . (c

B is non empty strict Group-like associative Subgroup of G

(G,H,h,B) is non empty strict Group-like associative Subgroup of H

(G,H,h,B) is Relation-like the carrier of B -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(B,H) Element of K19(K20( the carrier of B, the carrier of H))

the carrier of B is non empty set

K20( the carrier of B, the carrier of H) is set

K19(K20( the carrier of B, the carrier of H)) is set

h | the carrier of B is Relation-like the carrier of G -defined the carrier of H -valued Function-like Element of K19(K20( the carrier of G, the carrier of H))

Image (G,H,h,B) is non empty strict Group-like associative Subgroup of H

N is non empty Group-like associative normal Subgroup of G1

G1 ./. N is non empty strict Group-like associative multMagma

the carrier of (G1 ./. N) is non empty set

x is Element of the carrier of (G1 ./. N)

the carrier of G1 is non empty set

a is Element of the carrier of G1

a * N is Element of K19( the carrier of G1)

K19( the carrier of G1) is set

carr N is Element of K19( the carrier of G1)

the carrier of N is non empty set

a * (carr N) is Element of K19( the carrier of G1)

K107( the carrier of G1,a) is non empty Element of K19( the carrier of G1)

K107( the carrier of G1,a) * (carr N) is Element of K19( the carrier of G1)

{ (b

N * a is Element of K19( the carrier of G1)

(carr N) * a is Element of K19( the carrier of G1)

(carr N) * K107( the carrier of G1,a) is Element of K19( the carrier of G1)

{ (b

y is Element of the carrier of (G1 ./. N)

b is Element of the carrier of G1

b * N is Element of K19( the carrier of G1)

b * (carr N) is Element of K19( the carrier of G1)

K107( the carrier of G1,b) is non empty Element of K19( the carrier of G1)

K107( the carrier of G1,b) * (carr N) is Element of K19( the carrier of G1)

{ (b

N * b is Element of K19( the carrier of G1)

(carr N) * b is Element of K19( the carrier of G1)

(carr N) * K107( the carrier of G1,b) is Element of K19( the carrier of G1)

{ (b

Left_Cosets N is non empty Element of K19(K19( the carrier of G1))

K19(K19( the carrier of G1)) is set

b1 is Element of the carrier of A

(G,H,h,A) . b1 is Element of the carrier of H

b1 is Element of the carrier of G

h . b1 is Element of the carrier of H

(h . b1) * (G,H,h,B) is Element of K19( the carrier of H)

K19( the carrier of H) is set

carr (G,H,h,B) is Element of K19( the carrier of H)

the carrier of (G,H,h,B) is non empty set

(h . b1) * (carr (G,H,h,B)) is Element of K19( the carrier of H)

K107( the carrier of H,(h . b1)) is non empty Element of K19( the carrier of H)

K107( the carrier of H,(h . b1)) * (carr (G,H,h,B)) is Element of K19( the carrier of H)

{ (b

b1 * B is Element of K19( the carrier of G)

K19( the carrier of G) is set

carr B is Element of K19( the carrier of G)

b1 * (carr B) is Element of K19( the carrier of G)

K107( the carrier of G,b1) is non empty Element of K19( the carrier of G)

K107( the carrier of G,b1) * (carr B) is Element of K19( the carrier of G)

{ (b

h .: (b1 * B) is Element of K19( the carrier of H)

a1 is Element of the carrier of A

(G,H,h,A) . a1 is Element of the carrier of H

a1 is Element of the carrier of G

h . a1 is Element of the carrier of H

(h . a1) * (G,H,h,B) is Element of K19( the carrier of H)

(h . a1) * (carr (G,H,h,B)) is Element of K19( the carrier of H)

K107( the carrier of H,(h . a1)) is non empty Element of K19( the carrier of H)

K107( the carrier of H,(h . a1)) * (carr (G,H,h,B)) is Element of K19( the carrier of H)

{ (b

a1 * B is Element of K19( the carrier of G)

a1 * (carr B) is Element of K19( the carrier of G)

K107( the carrier of G,a1) is non empty Element of K19( the carrier of G)

K107( the carrier of G,a1) * (carr B) is Element of K19( the carrier of G)

{ (b

h .: (a1 * B) is Element of K19( the carrier of H)

y1 is set

x2 is Element of K19( the carrier of G1)

y2 is Element of K19( the carrier of G1)

x2 * y2 is Element of K19( the carrier of G1)

{ (b

x is Element of the carrier of G1

x is Element of the carrier of G1

x * x is Element of the carrier of G1

the multF of G1 is Relation-like K20( the carrier of G1, the carrier of G1) -defined the carrier of G1 -valued Function-like quasi_total Element of K19(K20(K20( the carrier of G1, the carrier of G1), the carrier of G1))

K20( the carrier of G1, the carrier of G1) is set

K20(K20( the carrier of G1, the carrier of G1), the carrier of G1) is set

K19(K20(K20( the carrier of G1, the carrier of G1), the carrier of G1)) is set

the multF of G1 . (x,x) is Element of the carrier of G1

z2 is Element of the carrier of H

z1 is Element of the carrier of H

z2 * z1 is Element of the carrier of H

the multF of H is Relation-like K20( the carrier of H, the carrier of H) -defined the carrier of H -valued Function-like quasi_total Element of K19(K20(K20( the carrier of H, the carrier of H), the carrier of H))

K20( the carrier of H, the carrier of H) is set

K20(K20( the carrier of H, the carrier of H), the carrier of H) is set

K19(K20(K20( the carrier of H, the carrier of H), the carrier of H)) is set

the multF of H . (z2,z1) is Element of the carrier of H

(h .: (a1 * B)) * (h .: (b1 * B)) is Element of K19( the carrier of H)

{ (b