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
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
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
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
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)
{ (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
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)))
c6 is Relation-like Function-like set
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 ((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)
{ (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)
((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)
{ (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
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)))
c6 is Relation-like Function-like set
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 ((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)
{ (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)
((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)
{ (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
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
c6 is non empty strict Group-like associative Subgroup of H
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
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)
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
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
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
c6 is non empty Group-like associative normal Subgroup of F
F ./. c6 is non empty strict Group-like associative multMagma
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
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
F is non empty strict Group-like associative commutative Subgroup of G
z is non empty strict Group-like associative commutative Subgroup of G
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
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)
{ (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
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)
{ (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
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
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
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
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
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)
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 * B) & b2 in h .: (b1 * B) ) } is set
(a1 * B) * (b1 * B) is Element of K19( the carrier of G)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in a1 * B & b2 in b1 * B ) } is set
(b1 * B) * (a1 * B) is Element of K19( the carrier of G)
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in b1 * B & b2 in a1 * B ) } is set
y1 is non empty Group-like associative normal Subgroup of A
x is Element of the carrier of A
x * y1 is Element of K19( the carrier of A)
K19( the carrier of A) is set
carr y1 is Element of K19( the carrier of A)
the carrier of y1 is non empty set
x * (carr y1) is Element of K19( the carrier of A)
K107( the carrier of A,x) is non empty Element of K19( the carrier of A)
K107( the carrier of A,x) * (carr y1) is Element of K19( the carrier of A)
{ (b1 * b2) where b1, b2 is Element of the carrier of A : ( b1 in K107( the carrier of A,x) & b2 in carr y1 ) } is set
x is Element of the carrier of A
x * y1 is Element of K19( the carrier of A)
x * (carr y1) is Element of K19( the carrier of A)
K107( the carrier of A,x) is non empty Element of K19( the carrier of A)
K107( the carrier of A,x) * (carr y1) is Element of K19( the carrier of A)
{ (b1 * b2) where b1, b2 is Element of the carrier of A : ( b1 in K107( the carrier of A,x) & b2 in carr y1 ) } is set
Left_Cosets y1 is non empty Element of K19(K19( the carrier of A))
K19(K19( the carrier of A)) is set
A ./. y1 is non empty strict Group-like associative multMagma
the carrier of (A ./. y1) is non empty set
z22 is Element of Left_Cosets y1
z11 is Element of Left_Cosets y1
x is set
z1 is Element of the carrier of G
z2 is Element of the carrier of G
z1 * z2 is Element of the carrier of G
the multF of G . (z1,z2) is Element of the carrier of G
z1 is Element of K19( the carrier of A)
z2 is Element of K19( the carrier of A)
z11 is Element of the carrier of A
z22 is Element of the carrier of A
z11 * z22 is Element of the carrier of A
the multF of A is Relation-like K20( the carrier of A, the carrier of A) -defined the carrier of A -valued Function-like quasi_total Element of K19(K20(K20( the carrier of A, the carrier of A), the carrier of A))
K20( the carrier of A, the carrier of A) is set
K20(K20( the carrier of A, the carrier of A), the carrier of A) is set
K19(K20(K20( the carrier of A, the carrier of A), the carrier of A)) is set
the multF of A . (z11,z22) is Element of the carrier of A
z1 * z2 is Element of K19( the carrier of A)
{ (b1 * b2) where b1, b2 is Element of the carrier of A : ( b1 in z1 & b2 in z2 ) } is set
x is set
z1 is Element of the carrier of G
z2 is Element of the carrier of G
z1 * z2 is Element of the carrier of G
the multF of G . (z1,z2) is Element of the carrier of G
z11 is Element of the carrier of A
z22 is Element of the carrier of A
z11 * z22 is Element of the carrier of A
the multF of A . (z11,z22) is Element of the carrier of A
z2 * z1 is Element of K19( the carrier of A)
{ (b1 * b2) where b1, b2 is Element of the carrier of A : ( b1 in z2 & b2 in z1 ) } is set
x is set
z1 is Element of the carrier of A
z2 is Element of the carrier of A
z1 * z2 is Element of the carrier of A
the multF of A . (z1,z2) is Element of the carrier of A
z11 is Element of the carrier of G
z22 is Element of the carrier of G
z11 * z22 is Element of the carrier of G
the multF of G . (z11,z22) is Element of the carrier of G
the multF of (A ./. y1) is Relation-like K20( the carrier of (A ./. y1), the carrier of (A ./. y1)) -defined the carrier of (A ./. y1) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (A ./. y1), the carrier of (A ./. y1)), the carrier of (A ./. y1)))
K20( the carrier of (A ./. y1), the carrier of (A ./. y1)) is set
K20(K20( the carrier of (A ./. y1), the carrier of (A ./. y1)), the carrier of (A ./. y1)) is set
K19(K20(K20( the carrier of (A ./. y1), the carrier of (A ./. y1)), the carrier of (A ./. y1))) is set
x is Element of the carrier of (A ./. y1)
z1 is Element of the carrier of (A ./. y1)
the multF of (A ./. y1) . (x,z1) is Element of the carrier of (A ./. y1)
the multF of (A ./. y1) . (z1,x) is Element of the carrier of (A ./. y1)
CosOp y1 is Relation-like K20((Left_Cosets y1),(Left_Cosets y1)) -defined Left_Cosets y1 -valued Function-like quasi_total Element of K19(K20(K20((Left_Cosets y1),(Left_Cosets y1)),(Left_Cosets y1)))
K20((Left_Cosets y1),(Left_Cosets y1)) is set
K20(K20((Left_Cosets y1),(Left_Cosets y1)),(Left_Cosets y1)) is set
K19(K20(K20((Left_Cosets y1),(Left_Cosets y1)),(Left_Cosets y1))) is set
a11 is Element of the carrier of (A ./. y1)
b11 is Element of the carrier of (A ./. y1)
(CosOp y1) . (a11,b11) is set
the multF of (A ./. y1) . (z22,z11) is set
the multF of (A ./. y1) . (b11,a11) is Element of the carrier of (A ./. y1)
(CosOp y1) . (z11,z22) is Element of Left_Cosets y1
x is set
z1 is Element of the carrier of A
z2 is Element of the carrier of A
z1 * z2 is Element of the carrier of A
the multF of A . (z1,z2) is Element of the carrier of A
z11 is Element of the carrier of G
z22 is Element of the carrier of G
z11 * z22 is Element of the carrier of G
the multF of G . (z11,z22) is Element of the carrier of G
y1 is set
y2 * x2 is Element of K19( the carrier of G1)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in y2 & b2 in x2 ) } 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 . (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 . (z2,z1) is Element of the carrier of H
(h .: (b1 * B)) * (h .: (a1 * B)) is Element of K19( the carrier of H)
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in h .: (b1 * B) & b2 in h .: (a1 * B) ) } is set
h .: ((b1 * B) * (a1 * B)) is Element of K19( the carrier of H)
y1 is set
x is set
h . x is set
x is Element of the carrier of G
z1 is Element of the carrier of G
z2 is Element of the carrier of G
z1 * z2 is Element of the carrier of G
the multF of G . (z1,z2) is Element of the carrier of G
h . z2 is Element of the carrier of H
h . z1 is Element of the carrier of H
(h . z1) * (h . z2) is Element of the carrier of H
the multF of H . ((h . z1),(h . z2)) is Element of the carrier of H
z11 is Element of the carrier of G1
z22 is Element of the carrier of G1
z11 * z22 is Element of the carrier of G1
the multF of G1 . (z11,z22) is Element of the carrier of G1
h .: ((a1 * B) * (b1 * B)) is Element of K19( the carrier of H)
y1 is set
x is set
h . x is set
x is Element of the carrier of G
z1 is Element of the carrier of G
z2 is Element of the carrier of G
z1 * z2 is Element of the carrier of G
the multF of G . (z1,z2) is Element of the carrier of G
h . z2 is Element of the carrier of H
h . z1 is Element of the carrier of H
(h . z1) * (h . z2) is Element of the carrier of H
the multF of H . ((h . z1),(h . z2)) is Element of the carrier of H
z11 is Element of the carrier of G1
z22 is Element of the carrier of G1
z11 * z22 is Element of the carrier of G1
the multF of G1 . (z11,z22) is Element of the carrier of G1
x * y is Element of the carrier of (G1 ./. N)
the multF of (G1 ./. N) is Relation-like K20( the carrier of (G1 ./. N), the carrier of (G1 ./. N)) -defined the carrier of (G1 ./. N) -valued Function-like quasi_total Element of K19(K20(K20( the carrier of (G1 ./. N), the carrier of (G1 ./. N)), the carrier of (G1 ./. N)))
K20( the carrier of (G1 ./. N), the carrier of (G1 ./. N)) is set
K20(K20( the carrier of (G1 ./. N), the carrier of (G1 ./. N)), the carrier of (G1 ./. N)) is set
K19(K20(K20( the carrier of (G1 ./. N), the carrier of (G1 ./. N)), the carrier of (G1 ./. N))) is set
the multF of (G1 ./. N) . (x,y) is Element of the carrier of (G1 ./. N)
CosOp N is Relation-like K20((Left_Cosets N),(Left_Cosets N)) -defined Left_Cosets N -valued Function-like quasi_total Element of K19(K20(K20((Left_Cosets N),(Left_Cosets N)),(Left_Cosets N)))
K20((Left_Cosets N),(Left_Cosets N)) is set
K20(K20((Left_Cosets N),(Left_Cosets N)),(Left_Cosets N)) is set
K19(K20(K20((Left_Cosets N),(Left_Cosets N)),(Left_Cosets N))) is set
(CosOp N) . (x,y) is set
y1 is Element of K19( the carrier of G1)
x1 is Element of K19( the carrier of G1)
y1 * x1 is Element of K19( the carrier of G1)
{ (b1 * b2) where b1, b2 is Element of the carrier of G1 : ( b1 in y1 & b2 in x1 ) } is set
(CosOp N) . (y,x) is set
y * x is Element of the carrier of (G1 ./. N)
the multF of (G1 ./. N) . (y,x) is Element of the carrier of (G1 ./. N)
N is non empty Group-like associative normal Subgroup of G1
G1 ./. N is non empty strict Group-like associative multMagma
z . 1 is set
(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
z . (len z) is set
(1). (Image h) is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of Image h
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
z . (len F) is set
(1). H is non empty V51() V52() 1 -element strict Group-like associative commutative normal cyclic Subgroup of H
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
G1 is non empty strict Group-like associative Subgroup of Image h
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
G2 is non empty strict Group-like associative Subgroup of Image h
z . (c6 + 1) is set
A is non empty Group-like associative normal Subgroup of G1
G1 ./. A is non empty strict Group-like associative multMagma