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

RAT is set
INT is set
K20(REAL,REAL) is set
K19(K20(REAL,REAL)) is set

the carrier of K354() is non empty V126() 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

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

rng <*H*> is set
Subgroups H is non empty set
h is set
{H} is non empty set

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

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

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
c6 is non empty V52() Group-like associative commutative Subgroup of H
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
c6 is non empty V52() strict Group-like associative commutative Subgroup of H
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

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
c6 is non empty Group-like associative normal Subgroup of F
z is non empty Group-like associative Subgroup of F
c6 /\ z is non empty strict Group-like associative normal Subgroup of z

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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,F) & b2 in carr h ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,z) & b2 in carr h ) } is set
(F * h) * (z * h) is Element of K19( the carrier of H)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in F * h & b2 in z * h ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,(F * z)) & b2 in carr h ) } is set

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
() . F is Element of the carrier of (H ./. h)
() . z is Element of the carrier of (H ./. h)
@ (() . F) is Element of K19( the carrier of H)
@ (() . z) is Element of K19( the carrier of H)
() . (F * z) is Element of the carrier of (H ./. h)
(() . F) * (() . 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) . ((() . F),(() . z)) is Element of the carrier of (H ./. h)

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

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

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 c6 is set
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 (() | the carrier of H) is Element of K19( the carrier of (h ./. F))
K19( the carrier of (h ./. F)) is set
rng () 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)
(() | the carrier of H) . B is set
() . B is set
(() | the carrier of H) . (A * B) is set
() . (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
(() | the carrier of H) . A is set
() . 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)
(() | the carrier of H) . x is set
() . 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)
{ (b1 * b2) where b1, b2 is Element of the carrier of h : ( b1 in K107( the carrier of h,y) & b2 in carr F ) } is set
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)
(() | the carrier of H) . y is set
() . 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)
{ (b1 * b2) where b1, b2 is Element of the carrier of h : ( b1 in K107( the carrier of h,a) & b2 in carr F ) } is set
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

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

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

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

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 c6 is set
the carrier of h /\ the carrier of H is set
the carrier of (h /\ H) is non empty set
rng (() | the carrier of H) is Element of K19( the carrier of (h ./. F))
K19( the carrier of (h ./. F)) is set
rng () 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)
(() | the carrier of H) . B is set
() . B is set
(() | the carrier of H) . (A * B) is set
() . (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
(() | the carrier of H) . A is set
() . 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)
(() | the carrier of H) . x is set
() . 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)
{ (b1 * b2) where b1, b2 is Element of the carrier of h : ( b1 in K107( the carrier of h,y) & b2 in carr F ) } is set
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)
(() | the carrier of H) . y is set
() . 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)
{ (b1 * b2) where b1, b2 is Element of the carrier of h : ( b1 in K107( the carrier of h,a) & b2 in carr F ) } is set
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

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

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

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

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
c6 is non empty strict Group-like associative Subgroup of H
G1 is Element 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
c6 is non empty strict Group-like associative Subgroup of G
c6 /\ H is non empty strict Group-like associative Subgroup of G
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)

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

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

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
c6 is non empty strict Group-like associative Subgroup of H
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 c6
c6 ./. G2 is non empty strict Group-like associative multMagma

Subgroups G is non empty set

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

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
c6 is non empty Group-like associative normal Subgroup of F
F ./. c6 is non empty strict Group-like associative multMagma

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

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

c6 is non empty Group-like associative commutative normal Subgroup of F
F ./. c6 is non empty strict Group-like associative multMagma
c6 is non empty Group-like associative commutative normal Subgroup of F
F ./. c6 is non empty strict Group-like associative multMagma

c6 is non empty Group-like associative commutative normal Subgroup of F
F ./. c6 is non empty strict Group-like associative multMagma
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
c6 is Element of the carrier of G
h . c6 is Element of the carrier of H
G1 is Element of the carrier of G
h . G1 is Element of the carrier of H
the multF of H . ((h . c6),(h . G1)) is Element of the carrier of H
the multF of G . (c6,G1) is Element of the carrier of G
h . ( the multF of G . (c6,G1)) is Element of the carrier of H
(h . c6) * (h . G1) is Element of the carrier of H
c6 * G1 is Element of the carrier of G
h . (c6 * G1) is Element of the carrier of H
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))
c6 is Element of the carrier of F
z . c6 is Element of the carrier of H
h . c6 is set
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 . (c6,G1) is set
c6 * G1 is Element of the carrier of F
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 . (c6,G1) is Element of the carrier of F
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 . c6) * (z . G1) is Element of the carrier of H
the multF of H . ((z . c6),(z . G1)) is Element of the carrier of H
h . ( the multF of G . (c6,G1)) is set
z . (c6 * G1) is Element of the carrier of H

the carrier of G is non empty set

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

the carrier of G is non empty set

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)

the carrier of G is non empty set

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

the carrier of G is non empty set

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

the carrier of G is non empty set

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

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,()) is non empty strict Group-like associative Subgroup of H
(G,H,h,()) is Relation-like the carrier of () -defined the carrier of H -valued Function-like quasi_total unity-preserving V103( (Omega). G,H) Element of K19(K20( the carrier of (), the carrier of H))
the carrier of () is non empty set
K20( the carrier of (), the carrier of H) is set
K19(K20( the carrier of (), the carrier of H)) is set
h | the carrier of () 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,()) is non empty strict Group-like associative Subgroup of H
Image h is non empty strict Group-like associative Subgroup of H

the carrier of () is non empty set
the multF of () is Relation-like K20( the carrier of (), the carrier of ()) -defined the carrier of () -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ()))
K20( the carrier of (), the carrier of ()) is set
K20(K20( the carrier of (), the carrier of ()), the carrier of ()) is set
K19(K20(K20( the carrier of (), the carrier of ()), the carrier of ())) is set
multMagma(# the carrier of (), the multF of () #) 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,()) 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). ()) is non empty set

the carrier of G is non empty set

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

the carrier of G is non empty set

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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,(h . z)) & b2 in carr (G,H,h,F) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K107( the carrier of G,z) & b2 in carr F ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in carr (G,H,h,F) & b2 in K107( the carrier of H,(h . z)) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr F & b2 in K107( the carrier of G,z) ) } is set
h .: (F * z) is Element of K19( the carrier of H)
c6 is set
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
c6 is set
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
c6 is set
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
c6 is set
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

the carrier of G is non empty set

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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in h .: F & b2 in h .: z ) } is set
F * z is Element of K19( the carrier of G)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in F & b2 in z ) } is set
h .: (F * z) is Element of K19( the carrier of H)
c6 is set
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
c6 is set
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

the carrier of G is non empty set

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
c6 is non empty strict Group-like associative normal Subgroup of z
(G,H,h,c6) is non empty strict Group-like associative Subgroup of H
(G,H,h,c6) is Relation-like the carrier of c6 -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(c6,H) Element of K19(K20( the carrier of c6, the carrier of H))
the carrier of c6 is non empty set
K20( the carrier of c6, the carrier of H) is set
K19(K20( the carrier of c6, the carrier of H)) is set
h | the carrier of c6 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,c6) is non empty strict Group-like associative Subgroup of H
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))
{ (b1 * b2) where b1, b2 is Element of the carrier of (G,H,h,z) : ( b1 in K107( the carrier of (G,H,h,z),G2) & b2 in carr G1 ) } is set
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))
{ (b1 * b2) where b1, b2 is Element of the carrier of (G,H,h,z) : ( b1 in carr G1 & b2 in K107( the carrier of (G,H,h,z),G2) ) } is set
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 c6
(G,H,h,c6) . 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
(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 * c6 is Element of K19( the carrier of G)
K19( the carrier of G) is set
carr c6 is Element of K19( the carrier of G)
B * (carr c6) is Element of K19( the carrier of G)
K107( the carrier of G,B) is non empty Element of K19( the carrier of G)
K107( the carrier of G,B) * (carr c6) is Element of K19( the carrier of G)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K107( the carrier of G,B) & b2 in carr c6 ) } is set
c6 * B is Element of K19( the carrier of G)
(carr c6) * B is Element of K19( the carrier of G)
(carr c6) * K107( the carrier of G,B) is Element of K19( the carrier of G)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr c6 & b2 in K107( the carrier of G,B) ) } is set
h .: (c6 * B) is Element of K19( the carrier of H)
K19( the carrier of H) is set
(G,H,h,c6) * (h . B) is Element of K19( the carrier of H)
carr (G,H,h,c6) is Element of K19( the carrier of H)
the carrier of (G,H,h,c6) is non empty set
(carr (G,H,h,c6)) * (h . B) is Element of K19( the carrier of H)
K107( the carrier of H,(h . B)) is non empty Element of K19( the carrier of H)
(carr (G,H,h,c6)) * K107( the carrier of H,(h . B)) is Element of K19( the carrier of H)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in carr (G,H,h,c6) & b2 in K107( the carrier of H,(h . B)) ) } is set
N is Element of the carrier of z
N * c6 is Element of K19( the carrier of z)
K19( the carrier of z) is set
carr c6 is Element of K19( the carrier of z)
N * (carr c6) is Element of K19( the carrier of z)
K107( the carrier of z,N) is non empty Element of K19( the carrier of z)
K107( the carrier of z,N) * (carr c6) is Element of K19( the carrier of z)
{ (b1 * b2) where b1, b2 is Element of the carrier of z : ( b1 in K107( the carrier of z,N) & b2 in carr c6 ) } is set
c6 * N is Element of K19( the carrier of z)
(carr c6) * N is Element of K19( the carrier of z)
(carr c6) * K107( the carrier of z,N) is Element of K19( the carrier of z)
{ (b1 * b2) where b1, b2 is Element of the carrier of z : ( b1 in carr c6 & b2 in K107( the carrier of z,N) ) } is set

the carrier of G is non empty set

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

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

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 () is non empty set
z is V28() V29() V30() V34() V35() ext-real V107() set
F . z is set
c6 is non empty strict Group-like associative Subgroup of G
(G,H,h,c6) is non empty strict Group-like associative Subgroup of H
(G,H,h,c6) is Relation-like the carrier of c6 -defined the carrier of H -valued Function-like quasi_total unity-preserving V103(c6,H) Element of K19(K20( the carrier of c6, the carrier of H))
the carrier of c6 is non empty set
K20( the carrier of c6, the carrier of H) is set
K19(K20( the carrier of c6, the carrier of H)) is set
h | the carrier of c6 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,c6) is non empty strict Group-like associative Subgroup of 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)
c6 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT
c6 + 1 is V28() V29() V30() V34() V35() ext-real V107() Element of NAT
z . c6 is set
z . (c6 + 1) is set
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 . c6 is set
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 . (c6 + 1) is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in K107( the carrier of G1,a) & b2 in carr N ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in carr N & b2 in K107( the carrier of G1,a) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in K107( the carrier of G1,b) & b2 in carr N ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in carr N & b2 in K107( the carrier of G1,b) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,(h . b1)) & b2 in carr (G,H,h,B) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K107( the carrier of G,b1) & b2 in carr B ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in K107( the carrier of H,(h . a1)) & b2 in carr (G,H,h,B) ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K107( the carrier of G,a1) & b2 in carr B ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in x2 & b2 in y2 ) } is set
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)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in h .: (a1 *