:: GROUPP_1 semantic presentation

REAL is V57() V58() V59() V63() set
NAT is V2() V6() V36() V41() V42() V57() V58() V59() V60() V61() V62() V63() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V57() V63() set
NAT is V2() V6() V36() V41() V42() V57() V58() V59() V60() V61() V62() V63() set
K6(NAT) is V2() V36() set
K6(NAT) is V2() V36() set
RAT is V57() V58() V59() V60() V63() set
INT is V57() V58() V59() V60() V61() V63() set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K304() is non empty strict unital Group-like associative commutative cyclic multMagma
the carrier of K304() is V1() V57() V58() V59() V60() V61() set
0 is V1() V6() V10() V11() V12() V13() ext-real non positive non negative V36() V40() V41() V43( 0 ) V57() V58() V59() V60() V61() V62() V63() set
1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K21(0,1) is V1() V36() V40() V57() V58() V59() V60() V61() V62() set
K458() is set
K6(K458()) is set
K459() is Element of K6(K458())
2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
SetPrimes is V1() V2() V36() V57() V58() V59() V60() V61() V62() Element of K6(NAT)
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is V1() V6() V10() V11() V12() V13() ext-real non positive non negative V35() V36() V40() V41() V43( 0 ) V57() V58() V59() V60() V61() V62() V63() Element of NAT
3 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K38(1) is V11() V12() V13() ext-real non positive set
p is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
G is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |-count p is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |^ H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
H + 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |^ (H + 1) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
(G |^ H) * g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
1 + 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
G * g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(G |^ H) * G is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
((G |^ H) * G) * g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(G |^ (H + 1)) * g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
H is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
NatDivisors (p |^ H) is V57() V58() V59() V60() V61() V62() Element of K6(NAT)
{ (p |^ b₁) where b₁ is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT : b₁ <= H } is set
g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
1_ p is non being_of_order_0 Element of the carrier of p
G is Element of the carrier of p
G " is Element of the carrier of p
H is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
G |^ H is Element of the carrier of p
(G ") |^ H is Element of the carrier of p
(1_ p) " is Element of the carrier of p
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
1_ p is non being_of_order_0 Element of the carrier of p
G is Element of the carrier of p
G " is Element of the carrier of p
H is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
(G ") |^ H is Element of the carrier of p
G |^ H is Element of the carrier of p
(G ") " is Element of the carrier of p
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is Element of the carrier of p
G " is Element of the carrier of p
ord (G ") is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
ord G is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |^ (ord G) is Element of the carrier of p
1_ p is non being_of_order_0 Element of the carrier of p
(G ") |^ (ord G) is Element of the carrier of p
(G ") |^ (ord (G ")) is Element of the carrier of p
G |^ (ord (G ")) is Element of the carrier of p
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is Element of the carrier of p
ord G is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
H is Element of the carrier of p
G |^ H is Element of the carrier of p
ord (G |^ H) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(G |^ H) |^ (ord G) is Element of the carrier of p
G |^ (ord G) is Element of the carrier of p
(G |^ (ord G)) |^ H is Element of the carrier of p
1_ p is non being_of_order_0 Element of the carrier of p
(1_ p) |^ H is Element of the carrier of p
G |^ (ord (G |^ H)) is Element of the carrier of p
(G |^ (ord (G |^ H))) |^ H is Element of the carrier of p
(G |^ H) |^ (ord (G |^ H)) is Element of the carrier of p
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is non empty unital Group-like associative Subgroup of p
g is Element of the carrier of p
H is Element of the carrier of p
H * g is Element of the carrier of p
the multF of p is V15() V18(K7( the carrier of p, the carrier of p)) V19( the carrier of p) V20() V25(K7( the carrier of p, the carrier of p)) quasi_total V191( the carrier of p) Element of K6(K7(K7( the carrier of p, the carrier of p), the carrier of p))
K7( the carrier of p, the carrier of p) is set
K7(K7( the carrier of p, the carrier of p), the carrier of p) is set
K6(K7(K7( the carrier of p, the carrier of p), the carrier of p)) is set
K552( the carrier of p, the multF of p,H,g) is Element of the carrier of p
(H * g) |^ 0 is Element of the carrier of p
1_ p is non being_of_order_0 Element of the carrier of p
H |^ 0 is Element of the carrier of p
(H |^ 0) * (1_ p) is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ 0),(1_ p)) is Element of the carrier of p
(1_ p) * (1_ p) is Element of the carrier of p
K552( the carrier of p, the multF of p,(1_ p),(1_ p)) is Element of the carrier of p
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
(H * g) |^ g1 is Element of the carrier of p
H |^ g1 is Element of the carrier of p
g2 is Element of the carrier of p
(H |^ g1) * g2 is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ g1),g2) is Element of the carrier of p
g1 + 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(H * g) |^ (g1 + 1) is Element of the carrier of p
((H |^ g1) * g2) * (H * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,((H |^ g1) * g2),(H * g)) is Element of the carrier of p
g2 * (H * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,g2,(H * g)) is Element of the carrier of p
(H |^ g1) * (g2 * (H * g)) is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ g1),(g2 * (H * g))) is Element of the carrier of p
g2 * H is Element of the carrier of p
K552( the carrier of p, the multF of p,g2,H) is Element of the carrier of p
(g2 * H) * g is Element of the carrier of p
K552( the carrier of p, the multF of p,(g2 * H),g) is Element of the carrier of p
(H |^ g1) * ((g2 * H) * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ g1),((g2 * H) * g)) is Element of the carrier of p
H * G is Element of K6( the carrier of p)
K6( the carrier of p) is set
G * H is Element of K6( the carrier of p)
h1 is Element of the carrier of p
H * h1 is Element of the carrier of p
K552( the carrier of p, the multF of p,H,h1) is Element of the carrier of p
h1 * g is Element of the carrier of p
K552( the carrier of p, the multF of p,h1,g) is Element of the carrier of p
H * (h1 * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,H,(h1 * g)) is Element of the carrier of p
(H |^ g1) * H is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ g1),H) is Element of the carrier of p
((H |^ g1) * H) * (h1 * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,((H |^ g1) * H),(h1 * g)) is Element of the carrier of p
H |^ (g1 + 1) is Element of the carrier of p
(H |^ (g1 + 1)) * (h1 * g) is Element of the carrier of p
K552( the carrier of p, the multF of p,(H |^ (g1 + 1)),(h1 * g)) is Element of the carrier of p
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
(H * g) |^ g1 is Element of the carrier of p
H |^ g1 is Element of the carrier of p
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is non empty unital Group-like associative normal Subgroup of p
p ./. G is non empty strict unital Group-like associative multMagma
Left_Cosets G is V1() Element of K6(K6( the carrier of p))
K6( the carrier of p) is set
K6(K6( the carrier of p)) is set
CosOp G is V15() V18(K7((Left_Cosets G),(Left_Cosets G))) V19( Left_Cosets G) V20() V25(K7((Left_Cosets G),(Left_Cosets G))) quasi_total Element of K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)))
K7((Left_Cosets G),(Left_Cosets G)) is set
K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)) is set
K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G))) is set
multMagma(# (Left_Cosets G),(CosOp G) #) is strict multMagma
the carrier of (p ./. G) is V1() set
H is Element of the carrier of p
H * G is Element of K6( the carrier of p)
g is Element of the carrier of (p ./. G)
g |^ 0 is Element of the carrier of (p ./. G)
1_ (p ./. G) is non being_of_order_0 Element of the carrier of (p ./. G)
H |^ 0 is Element of the carrier of p
(H |^ 0) * G is Element of K6( the carrier of p)
1_ p is non being_of_order_0 Element of the carrier of p
(1_ p) * G is Element of K6( the carrier of p)
carr G is Element of K6( the carrier of p)
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g |^ g1 is Element of the carrier of (p ./. G)
H |^ g1 is Element of the carrier of p
(H |^ g1) * G is Element of K6( the carrier of p)
g1 + 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g |^ (g1 + 1) is Element of the carrier of (p ./. G)
(g |^ g1) * g is Element of the carrier of (p ./. G)
the multF of (p ./. G) is V15() V18(K7( the carrier of (p ./. G), the carrier of (p ./. G))) V19( the carrier of (p ./. G)) V20() V25(K7( the carrier of (p ./. G), the carrier of (p ./. G))) quasi_total V191( the carrier of (p ./. G)) Element of K6(K7(K7( the carrier of (p ./. G), the carrier of (p ./. G)), the carrier of (p ./. G)))
K7( the carrier of (p ./. G), the carrier of (p ./. G)) is set
K7(K7( the carrier of (p ./. G), the carrier of (p ./. G)), the carrier of (p ./. G)) is set
K6(K7(K7( the carrier of (p ./. G), the carrier of (p ./. G)), the carrier of (p ./. G))) is set
K552( the carrier of (p ./. G), the multF of (p ./. G),(g |^ g1),g) is Element of the carrier of (p ./. G)
@ (g |^ g1) is Element of K6( the carrier of p)
@ g is Element of K6( the carrier of p)
(@ (g |^ g1)) * (@ g) is Element of K6( the carrier of p)
((H |^ g1) * G) * (H * G) is Element of K6( the carrier of p)
(H |^ g1) * H is Element of the carrier of p
the multF of p is V15() V18(K7( the carrier of p, the carrier of p)) V19( the carrier of p) V20() V25(K7( the carrier of p, the carrier of p)) quasi_total V191( the carrier of p) Element of K6(K7(K7( the carrier of p, the carrier of p), the carrier of p))
K7( the carrier of p, the carrier of p) is set
K7(K7( the carrier of p, the carrier of p), the carrier of p) is set
K6(K7(K7( the carrier of p, the carrier of p), the carrier of p)) is set
K552( the carrier of p, the multF of p,(H |^ g1),H) is Element of the carrier of p
((H |^ g1) * H) * G is Element of K6( the carrier of p)
H |^ (g1 + 1) is Element of the carrier of p
(H |^ (g1 + 1)) * G is Element of K6( the carrier of p)
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g |^ g1 is Element of the carrier of (p ./. G)
H |^ g1 is Element of the carrier of p
(H |^ g1) * G is Element of K6( the carrier of p)
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is non empty unital Group-like associative Subgroup of p
H is Element of the carrier of p
H * G is Element of K6( the carrier of p)
K6( the carrier of p) is set
g is Element of the carrier of p
g * G is Element of K6( the carrier of p)
p is non empty finite unital Group-like associative multMagma
center p is non empty finite strict unital Group-like associative Subgroup of p
G is non empty finite unital Group-like associative normal Subgroup of p
p ./. G is non empty strict unital Group-like associative multMagma
Left_Cosets G is V1() V36() V40() Element of K6(K6( the carrier of p))
the carrier of p is V1() V36() set
K6( the carrier of p) is V36() V40() set
K6(K6( the carrier of p)) is V36() V40() set
CosOp G is V15() V18(K7((Left_Cosets G),(Left_Cosets G))) V19( Left_Cosets G) V20() V25(K7((Left_Cosets G),(Left_Cosets G))) quasi_total V36() Element of K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)))
K7((Left_Cosets G),(Left_Cosets G)) is V36() set
K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)) is V36() set
K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G))) is V36() V40() set
multMagma(# (Left_Cosets G),(CosOp G) #) is strict multMagma
H is non empty finite unital Group-like associative multMagma
the carrier of H is V1() V36() set
g is Element of the carrier of H
g1 is Element of the carrier of p
g1 * G is V36() Element of K6( the carrier of p)
G * g1 is V36() Element of K6( the carrier of p)
g2 is Element of the carrier of p
h1 is Element of the carrier of p
g2 * h1 is Element of the carrier of p
the multF of p is V15() V18(K7( the carrier of p, the carrier of p)) V19( the carrier of p) V20() V25(K7( the carrier of p, the carrier of p)) quasi_total V36() V191( the carrier of p) Element of K6(K7(K7( the carrier of p, the carrier of p), the carrier of p))
K7( the carrier of p, the carrier of p) is V36() set
K7(K7( the carrier of p, the carrier of p), the carrier of p) is V36() set
K6(K7(K7( the carrier of p, the carrier of p), the carrier of p)) is V36() V40() set
K552( the carrier of p, the multF of p,g2,h1) is Element of the carrier of p
h1 * g2 is Element of the carrier of p
K552( the carrier of p, the multF of p,h1,g2) is Element of the carrier of p
g2 * G is V36() Element of K6( the carrier of p)
h1 * G is V36() Element of K6( the carrier of p)
h2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g |^ h2 is Element of the carrier of H
g1 |^ h2 is Element of the carrier of p
(g1 |^ h2) * G is V36() Element of K6( the carrier of p)
a is Element of the carrier of p
(g1 |^ h2) * a is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),a) is Element of the carrier of p
b is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g |^ b is Element of the carrier of H
g1 |^ b is Element of the carrier of p
(g1 |^ b) * G is V36() Element of K6( the carrier of p)
b2 is Element of the carrier of p
(g1 |^ b) * b2 is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),b2) is Element of the carrier of p
a * ((g1 |^ b) * b2) is Element of the carrier of p
K552( the carrier of p, the multF of p,a,((g1 |^ b) * b2)) is Element of the carrier of p
(g1 |^ h2) * (a * ((g1 |^ b) * b2)) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),(a * ((g1 |^ b) * b2))) is Element of the carrier of p
((g1 |^ b) * b2) * a is Element of the carrier of p
K552( the carrier of p, the multF of p,((g1 |^ b) * b2),a) is Element of the carrier of p
(g1 |^ h2) * (((g1 |^ b) * b2) * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),(((g1 |^ b) * b2) * a)) is Element of the carrier of p
b2 * a is Element of the carrier of p
K552( the carrier of p, the multF of p,b2,a) is Element of the carrier of p
(g1 |^ b) * (b2 * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),(b2 * a)) is Element of the carrier of p
(g1 |^ h2) * ((g1 |^ b) * (b2 * a)) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),((g1 |^ b) * (b2 * a))) is Element of the carrier of p
(g1 |^ h2) * (g1 |^ b) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),(g1 |^ b)) is Element of the carrier of p
((g1 |^ h2) * (g1 |^ b)) * (b2 * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,((g1 |^ h2) * (g1 |^ b)),(b2 * a)) is Element of the carrier of p
h2 + b is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 |^ (h2 + b) is Element of the carrier of p
(g1 |^ (h2 + b)) * (b2 * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ (h2 + b)),(b2 * a)) is Element of the carrier of p
(g1 |^ b) * (g1 |^ h2) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),(g1 |^ h2)) is Element of the carrier of p
((g1 |^ b) * (g1 |^ h2)) * (b2 * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,((g1 |^ b) * (g1 |^ h2)),(b2 * a)) is Element of the carrier of p
(g1 |^ h2) * (b2 * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),(b2 * a)) is Element of the carrier of p
(g1 |^ b) * ((g1 |^ h2) * (b2 * a)) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),((g1 |^ h2) * (b2 * a))) is Element of the carrier of p
(g1 |^ h2) * b2 is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ h2),b2) is Element of the carrier of p
((g1 |^ h2) * b2) * a is Element of the carrier of p
K552( the carrier of p, the multF of p,((g1 |^ h2) * b2),a) is Element of the carrier of p
(g1 |^ b) * (((g1 |^ h2) * b2) * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),(((g1 |^ h2) * b2) * a)) is Element of the carrier of p
b2 * (g1 |^ h2) is Element of the carrier of p
K552( the carrier of p, the multF of p,b2,(g1 |^ h2)) is Element of the carrier of p
(b2 * (g1 |^ h2)) * a is Element of the carrier of p
K552( the carrier of p, the multF of p,(b2 * (g1 |^ h2)),a) is Element of the carrier of p
(g1 |^ b) * ((b2 * (g1 |^ h2)) * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),((b2 * (g1 |^ h2)) * a)) is Element of the carrier of p
b2 * ((g1 |^ h2) * a) is Element of the carrier of p
K552( the carrier of p, the multF of p,b2,((g1 |^ h2) * a)) is Element of the carrier of p
(g1 |^ b) * (b2 * ((g1 |^ h2) * a)) is Element of the carrier of p
K552( the carrier of p, the multF of p,(g1 |^ b),(b2 * ((g1 |^ h2) * a))) is Element of the carrier of p
p is non empty finite unital Group-like associative multMagma
center p is non empty finite strict unital Group-like associative Subgroup of p
G is non empty finite unital Group-like associative normal Subgroup of p
p ./. G is non empty strict unital Group-like associative multMagma
Left_Cosets G is V1() V36() V40() Element of K6(K6( the carrier of p))
the carrier of p is V1() V36() set
K6( the carrier of p) is V36() V40() set
K6(K6( the carrier of p)) is V36() V40() set
CosOp G is V15() V18(K7((Left_Cosets G),(Left_Cosets G))) V19( Left_Cosets G) V20() V25(K7((Left_Cosets G),(Left_Cosets G))) quasi_total V36() Element of K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)))
K7((Left_Cosets G),(Left_Cosets G)) is V36() set
K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G)) is V36() set
K6(K7(K7((Left_Cosets G),(Left_Cosets G)),(Left_Cosets G))) is V36() V40() set
multMagma(# (Left_Cosets G),(CosOp G) #) is strict multMagma
p is non empty finite unital Group-like associative multMagma
card p is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of p is V1() V36() set
K154( the carrier of p) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative Subgroup of p
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
multMagma(# the carrier of G, the multF of G #) is strict unital Group-like associative multMagma
the multF of p is V15() V18(K7( the carrier of p, the carrier of p)) V19( the carrier of p) V20() V25(K7( the carrier of p, the carrier of p)) quasi_total V36() V191( the carrier of p) Element of K6(K7(K7( the carrier of p, the carrier of p), the carrier of p))
K7( the carrier of p, the carrier of p) is V36() set
K7(K7( the carrier of p, the carrier of p), the carrier of p) is V36() set
K6(K7(K7( the carrier of p, the carrier of p), the carrier of p)) is V36() V40() set
multMagma(# the carrier of p, the multF of p #) is strict unital Group-like associative multMagma
G is non empty unital Group-like associative multMagma
the carrier of G is V1() set
p is non empty unital Group-like associative multMagma
1_ p is non being_of_order_0 Element of the carrier of p
the carrier of p is V1() set
G is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
ord (1_ p) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |^ 0 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
1_ p is non being_of_order_0 Element of the carrier of p
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
the carrier of G is V1() set
H is (p,G) Element of the carrier of G
H " is Element of the carrier of G
ord H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord (H ") is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is non empty unital Group-like associative multMagma
the carrier of p is V1() set
G is Element of the carrier of p
H is Element of the carrier of p
G |^ H is Element of the carrier of p
g is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
ord (G |^ H) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord G is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G is non empty unital Group-like associative multMagma
the carrier of G is V1() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
g is (p,G) Element of the carrier of G
H is Element of the carrier of G
g |^ H is Element of the carrier of G
ord g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord (g |^ H) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative commutative multMagma
the carrier of G is V1() set
H is (p,G) Element of the carrier of G
g is (p,G) Element of the carrier of G
H * g is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K552( the carrier of G, the multF of G,H,g) is Element of the carrier of G
ord H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g1 + g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p |^ (g1 + g2) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
H |^ (p |^ (g1 + g2)) is Element of the carrier of G
(p |^ g1) * (p |^ g2) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
H |^ ((p |^ g1) * (p |^ g2)) is Element of the carrier of G
H |^ (p |^ g1) is Element of the carrier of G
(H |^ (p |^ g1)) |^ (p |^ g2) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) |^ (p |^ g2) is Element of the carrier of G
g |^ (p |^ (g1 + g2)) is Element of the carrier of G
(p |^ g2) * (p |^ g1) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g |^ ((p |^ g2) * (p |^ g1)) is Element of the carrier of G
g |^ (p |^ g2) is Element of the carrier of G
(g |^ (p |^ g2)) |^ (p |^ g1) is Element of the carrier of G
(1_ G) |^ (p |^ g1) is Element of the carrier of G
(H * g) |^ (p |^ (g1 + g2)) is Element of the carrier of G
(1_ G) * (1_ G) is Element of the carrier of G
K552( the carrier of G, the multF of G,(1_ G),(1_ G)) is Element of the carrier of G
ord (H * g) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
h1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ h1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative p -group multMagma
the carrier of G is V1() V36() set
H is Element of the carrier of G
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
the carrier of G is V1() V36() set
H is non empty finite unital Group-like associative Subgroup of G
g is Element of the carrier of G
the carrier of H is V1() V36() set
g1 is Element of the carrier of H
ord g1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative p -group multMagma
H is non empty finite unital Group-like associative Subgroup of G
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of H is V1() V36() set
K154( the carrier of H) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is non empty unital Group-like associative multMagma
(1). p is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of p
G is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
card ((1). p) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
the carrier of ((1). p) is V1() V2() V36() V43(1) set
K154( the carrier of ((1). p)) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
G |^ 0 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card ((1). p) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G is non empty unital Group-like associative multMagma
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
(1). G is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
H is non empty finite unital Group-like associative p -group Subgroup of G
g is non empty finite unital Group-like associative Subgroup of G
H /\ g is non empty finite strict unital Group-like associative Subgroup of G
g1 is non empty finite unital Group-like associative p -group Subgroup of H
g /\ H is non empty finite strict unital Group-like associative p -group Subgroup of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
the carrier of G is V1() V36() set
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
H is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g is Element of the carrier of G
ord g is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative p -group multMagma
H is non empty finite unital Group-like associative normal p -group Subgroup of G
G ./. H is non empty strict unital Group-like associative multMagma
Left_Cosets H is V1() V36() V40() Element of K6(K6( the carrier of G))
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
K6(K6( the carrier of G)) is V36() V40() set
CosOp H is V15() V18(K7((Left_Cosets H),(Left_Cosets H))) V19( Left_Cosets H) V20() V25(K7((Left_Cosets H),(Left_Cosets H))) quasi_total V36() Element of K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)))
K7((Left_Cosets H),(Left_Cosets H)) is V36() set
K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)) is V36() set
K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H))) is V36() V40() set
multMagma(# (Left_Cosets H),(CosOp H) #) is strict multMagma
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of H is V1() V36() set
K154( the carrier of H) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
index H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(card H) * (index H) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
card (G ./. H) is V6() V41() set
the carrier of (G ./. H) is V1() set
K154( the carrier of (G ./. H)) is V1() V6() V41() set
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
g2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
H is non empty finite unital Group-like associative normal Subgroup of G
G ./. H is non empty strict unital Group-like associative multMagma
Left_Cosets H is V1() V36() V40() Element of K6(K6( the carrier of G))
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
K6(K6( the carrier of G)) is V36() V40() set
CosOp H is V15() V18(K7((Left_Cosets H),(Left_Cosets H))) V19( Left_Cosets H) V20() V25(K7((Left_Cosets H),(Left_Cosets H))) quasi_total V36() Element of K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)))
K7((Left_Cosets H),(Left_Cosets H)) is V36() set
K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)) is V36() set
K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H))) is V36() V40() set
multMagma(# (Left_Cosets H),(CosOp H) #) is strict multMagma
card H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of H is V1() V36() set
K154( the carrier of H) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card (G ./. H) is V6() V41() set
the carrier of (G ./. H) is V1() set
K154( the carrier of (G ./. H)) is V1() V6() V41() set
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
index H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
(p |^ g) * (p |^ g1) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
g + g1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p |^ (g + g1) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative commutative multMagma
g is non empty finite unital Group-like associative commutative Subgroup of G
g1 is non empty finite unital Group-like associative commutative Subgroup of G
H is non empty finite unital Group-like associative commutative Subgroup of G
the carrier of H is V1() V36() set
g * g1 is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr g is V36() Element of K6( the carrier of G)
carr g1 is V36() Element of K6( the carrier of G)
(carr g) * (carr g1) is V36() Element of K6( the carrier of G)
g2 is Element of the carrier of H
h1 is Element of the carrier of G
h2 is Element of the carrier of G
h1 * h2 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,h1,h2) is Element of the carrier of G
ord (h1 * h2) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
a is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ a is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
g is non empty finite unital Group-like associative Subgroup of G
H is non empty finite unital Group-like associative Subgroup of G
H * g is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr H is V36() Element of K6( the carrier of G)
carr g is V36() Element of K6( the carrier of G)
(carr H) * (carr g) is V36() Element of K6( the carrier of G)
g * H is V36() Element of K6( the carrier of G)
(carr g) * (carr H) is V36() Element of K6( the carrier of G)
g1 is non empty finite strict unital Group-like associative Subgroup of G
the carrier of g1 is V1() V36() set
g2 is Element of the carrier of g1
h1 is Element of the carrier of G
h2 is Element of the carrier of G
h1 * h2 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,h1,h2) is Element of the carrier of G
ord h1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
a is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ a is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
h1 |^ (p |^ a) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(h1 * h2) |^ (p |^ a) is Element of the carrier of G
b is Element of the carrier of G
(h1 |^ (p |^ a)) * b is Element of the carrier of G
K552( the carrier of G, the multF of G,(h1 |^ (p |^ a)),b) is Element of the carrier of G
ord b is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
b2 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ b2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
b |^ (p |^ b2) is Element of the carrier of G
a + b2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p |^ (a + b2) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g2 |^ (p |^ (a + b2)) is Element of the carrier of g1
(h1 * h2) |^ (p |^ (a + b2)) is Element of the carrier of G
(p |^ a) * (p |^ b2) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(h1 * h2) |^ ((p |^ a) * (p |^ b2)) is Element of the carrier of G
((h1 * h2) |^ (p |^ a)) |^ (p |^ b2) is Element of the carrier of G
c1 is Element of the carrier of G
c1 |^ (p |^ (a + b2)) is Element of the carrier of G
ord c1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
d1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ d1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
H is non empty finite unital Group-like associative normal Subgroup of G
g is non empty finite unital Group-like associative normal Subgroup of G
H * g is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr H is V36() Element of K6( the carrier of G)
carr g is V36() Element of K6( the carrier of G)
(carr H) * (carr g) is V36() Element of K6( the carrier of G)
g1 is non empty finite strict unital Group-like associative Subgroup of G
the carrier of g1 is V1() V36() set
h1 is Element of the carrier of G
g2 is Element of the carrier of G
g2 * h1 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,g2,h1) is Element of the carrier of G
g2 " is Element of the carrier of G
(g2 * h1) * (g2 ") is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h1),(g2 ")) is Element of the carrier of G
h2 is Element of the carrier of G
a is Element of the carrier of G
h2 * a is Element of the carrier of G
K552( the carrier of G, the multF of G,h2,a) is Element of the carrier of G
g2 * h2 is Element of the carrier of G
K552( the carrier of G, the multF of G,g2,h2) is Element of the carrier of G
(g2 * h2) * a is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h2),a) is Element of the carrier of G
((g2 * h2) * a) * (g2 ") is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * a),(g2 ")) is Element of the carrier of G
a * (g2 ") is Element of the carrier of G
K552( the carrier of G, the multF of G,a,(g2 ")) is Element of the carrier of G
(g2 * h2) * (a * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h2),(a * (g2 "))) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(g2 * h2) * (1_ G) is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h2),(1_ G)) is Element of the carrier of G
((g2 * h2) * (1_ G)) * (a * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * (1_ G)),(a * (g2 "))) is Element of the carrier of G
(g2 ") * g2 is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 "),g2) is Element of the carrier of G
(g2 * h2) * ((g2 ") * g2) is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h2),((g2 ") * g2)) is Element of the carrier of G
((g2 * h2) * ((g2 ") * g2)) * (a * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * ((g2 ") * g2)),(a * (g2 "))) is Element of the carrier of G
(g2 * h2) * (g2 ") is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * h2),(g2 ")) is Element of the carrier of G
((g2 * h2) * (g2 ")) * g2 is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * (g2 ")),g2) is Element of the carrier of G
(((g2 * h2) * (g2 ")) * g2) * (a * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,(((g2 * h2) * (g2 ")) * g2),(a * (g2 "))) is Element of the carrier of G
g2 * (a * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,g2,(a * (g2 "))) is Element of the carrier of G
((g2 * h2) * (g2 ")) * (g2 * (a * (g2 "))) is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * (g2 ")),(g2 * (a * (g2 ")))) is Element of the carrier of G
g2 * a is Element of the carrier of G
K552( the carrier of G, the multF of G,g2,a) is Element of the carrier of G
(g2 * a) * (g2 ") is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 * a),(g2 ")) is Element of the carrier of G
((g2 * h2) * (g2 ")) * ((g2 * a) * (g2 ")) is Element of the carrier of G
K552( the carrier of G, the multF of G,((g2 * h2) * (g2 ")),((g2 * a) * (g2 "))) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative p -group multMagma
the carrier of G is V1() V36() set
H is non empty finite unital Group-like associative multMagma
the carrier of H is V1() V36() set
K7( the carrier of G, the carrier of H) is V36() set
K6(K7( the carrier of G, the carrier of H)) is V36() V40() set
g is V1() V15() V18( the carrier of G) V19( the carrier of H) V20() V25( the carrier of G) quasi_total V36() unity-preserving V194(G,H) Element of K6(K7( the carrier of G, the carrier of H))
Image g is non empty finite strict unital Group-like associative Subgroup of H
the carrier of (Image g) is V1() V36() set
g1 is Element of the carrier of (Image g)
g2 is (p,G) Element of the carrier of G
g . g2 is Element of the carrier of H
ord g2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
h1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ h1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g2 |^ (p |^ h1) is (p,G) Element of the carrier of G
g . (g2 |^ (p |^ h1)) is Element of the carrier of H
(g . g2) |^ (p |^ h1) is Element of the carrier of H
g1 |^ (p |^ h1) is Element of the carrier of (Image g)
1_ G is non being_of_order_0 (p,G) Element of the carrier of G
g . (1_ G) is Element of the carrier of H
1_ H is non being_of_order_0 Element of the carrier of H
h2 is Element of the carrier of H
h2 |^ (p |^ h1) is Element of the carrier of H
ord h2 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
a is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ a is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
ord g1 is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty strict unital Group-like associative multMagma
H is non empty strict unital Group-like associative multMagma
card G is V6() V41() set
the carrier of G is V1() set
K154( the carrier of G) is V1() V6() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card H is V6() V41() set
the carrier of H is V1() set
K154( the carrier of H) is V1() V6() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
card G is V6() V41() set
the carrier of G is V1() set
K154( the carrier of G) is V1() V6() V41() set
H is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
H is non empty finite unital Group-like associative Subgroup of G
(p,H) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p |^ (p,G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card H is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of H is V1() V36() set
K154( the carrier of H) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
g is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite strict unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(1). G is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of G
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p |^ 0 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
card ((1). G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of ((1). G) is V1() V2() V36() V43(1) set
K154( the carrier of ((1). G)) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite strict unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p |^ 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is non empty finite unital Group-like associative multMagma
the carrier of p is V1() V36() set
G is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
(G,p) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
G |^ 2 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
H is Element of the carrier of p
ord H is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
card p is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
K154( the carrier of p) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
G is non empty unital Group-like associative multMagma
G is non empty unital Group-like associative multMagma
p is non empty unital Group-like associative multMagma
(1). p is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of p
G is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
the carrier of ((1). p) is V1() V2() V36() V43(1) set
H is Element of the carrier of ((1). p)
g is Element of the carrier of ((1). p)
H * g is Element of the carrier of ((1). p)
the multF of ((1). p) is V15() V18(K7( the carrier of ((1). p), the carrier of ((1). p))) V19( the carrier of ((1). p)) V20() V25(K7( the carrier of ((1). p), the carrier of ((1). p))) quasi_total V36() V191( the carrier of ((1). p)) Element of K6(K7(K7( the carrier of ((1). p), the carrier of ((1). p)), the carrier of ((1). p)))
K7( the carrier of ((1). p), the carrier of ((1). p)) is V36() set
K7(K7( the carrier of ((1). p), the carrier of ((1). p)), the carrier of ((1). p)) is V36() set
K6(K7(K7( the carrier of ((1). p), the carrier of ((1). p)), the carrier of ((1). p))) is V36() V40() set
K552( the carrier of ((1). p), the multF of ((1). p),H,g) is Element of the carrier of ((1). p)
(H * g) |^ G is Element of the carrier of ((1). p)
H |^ G is Element of the carrier of ((1). p)
g |^ G is Element of the carrier of ((1). p)
(H |^ G) * (g |^ G) is Element of the carrier of ((1). p)
K552( the carrier of ((1). p), the multF of ((1). p),(H |^ G),(g |^ G)) is Element of the carrier of ((1). p)
the carrier of p is V1() set
1_ p is non being_of_order_0 Element of the carrier of p
{(1_ p)} is V1() V2() V36() V43(1) Element of K6( the carrier of p)
K6( the carrier of p) is set
H * g is Element of the carrier of ((1). p)
(H * g) |^ G is Element of the carrier of ((1). p)
(H |^ G) * (g |^ G) is Element of the carrier of ((1). p)
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
the non empty unital Group-like associative multMagma is non empty unital Group-like associative multMagma
(1). the non empty unital Group-like associative multMagma is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of the non empty unital Group-like associative multMagma
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative (p) multMagma
H is non empty finite unital Group-like associative Subgroup of G
the carrier of H is V1() V36() set
g is Element of the carrier of H
g1 is Element of the carrier of H
g * g1 is Element of the carrier of H
the multF of H is V15() V18(K7( the carrier of H, the carrier of H)) V19( the carrier of H) V20() V25(K7( the carrier of H, the carrier of H)) quasi_total V36() V191( the carrier of H) Element of K6(K7(K7( the carrier of H, the carrier of H), the carrier of H))
K7( the carrier of H, the carrier of H) is V36() set
K7(K7( the carrier of H, the carrier of H), the carrier of H) is V36() set
K6(K7(K7( the carrier of H, the carrier of H), the carrier of H)) is V36() V40() set
K552( the carrier of H, the multF of H,g,g1) is Element of the carrier of H
(g * g1) |^ p is Element of the carrier of H
g |^ p is Element of the carrier of H
g1 |^ p is Element of the carrier of H
(g |^ p) * (g1 |^ p) is Element of the carrier of H
K552( the carrier of H, the multF of H,(g |^ p),(g1 |^ p)) is Element of the carrier of H
the carrier of G is V1() V36() set
g2 is Element of the carrier of G
h1 is Element of the carrier of G
g2 * h1 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,g2,h1) is Element of the carrier of G
g2 |^ p is Element of the carrier of G
h1 |^ p is Element of the carrier of G
(g2 * h1) |^ p is Element of the carrier of G
(g2 |^ p) * (h1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 |^ p),(h1 |^ p)) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
the carrier of G is V1() set
H is Element of the carrier of G
g is Element of the carrier of G
H * g is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K552( the carrier of G, the multF of G,H,g) is Element of the carrier of G
(H * g) |^ p is Element of the carrier of G
H |^ p is Element of the carrier of G
g |^ p is Element of the carrier of G
(H |^ p) * (g |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ p),(g |^ p)) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite strict unital Group-like associative multMagma
card G is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
the carrier of G is V1() V36() set
K154( the carrier of G) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
p |^ 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
(1). G is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
H is non empty finite unital Group-like associative (p) Subgroup of G
g is non empty finite unital Group-like associative Subgroup of G
H /\ g is non empty finite strict unital Group-like associative Subgroup of G
g1 is non empty finite unital Group-like associative (p) Subgroup of H
g /\ H is non empty finite strict unital Group-like associative (p) Subgroup of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative (p) multMagma
H is non empty finite unital Group-like associative normal (p) Subgroup of G
G ./. H is non empty strict unital Group-like associative multMagma
Left_Cosets H is V1() V36() V40() Element of K6(K6( the carrier of G))
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
K6(K6( the carrier of G)) is V36() V40() set
CosOp H is V15() V18(K7((Left_Cosets H),(Left_Cosets H))) V19( Left_Cosets H) V20() V25(K7((Left_Cosets H),(Left_Cosets H))) quasi_total V36() Element of K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)))
K7((Left_Cosets H),(Left_Cosets H)) is V36() set
K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H)) is V36() set
K6(K7(K7((Left_Cosets H),(Left_Cosets H)),(Left_Cosets H))) is V36() V40() set
multMagma(# (Left_Cosets H),(CosOp H) #) is strict multMagma
the carrier of (G ./. H) is V1() set
g is Element of the carrier of (G ./. H)
g1 is Element of the carrier of (G ./. H)
g * g1 is Element of the carrier of (G ./. H)
the multF of (G ./. H) is V15() V18(K7( the carrier of (G ./. H), the carrier of (G ./. H))) V19( the carrier of (G ./. H)) V20() V25(K7( the carrier of (G ./. H), the carrier of (G ./. H))) quasi_total V191( the carrier of (G ./. H)) Element of K6(K7(K7( the carrier of (G ./. H), the carrier of (G ./. H)), the carrier of (G ./. H)))
K7( the carrier of (G ./. H), the carrier of (G ./. H)) is set
K7(K7( the carrier of (G ./. H), the carrier of (G ./. H)), the carrier of (G ./. H)) is set
K6(K7(K7( the carrier of (G ./. H), the carrier of (G ./. H)), the carrier of (G ./. H))) is set
K552( the carrier of (G ./. H), the multF of (G ./. H),g,g1) is Element of the carrier of (G ./. H)
(g * g1) |^ p is Element of the carrier of (G ./. H)
g |^ p is Element of the carrier of (G ./. H)
g1 |^ p is Element of the carrier of (G ./. H)
(g |^ p) * (g1 |^ p) is Element of the carrier of (G ./. H)
K552( the carrier of (G ./. H), the multF of (G ./. H),(g |^ p),(g1 |^ p)) is Element of the carrier of (G ./. H)
g2 is Element of the carrier of G
g2 * H is V36() Element of K6( the carrier of G)
H * g2 is V36() Element of K6( the carrier of G)
h1 is Element of the carrier of G
h1 * H is V36() Element of K6( the carrier of G)
H * h1 is V36() Element of K6( the carrier of G)
@ g is V36() Element of K6( the carrier of G)
@ g1 is V36() Element of K6( the carrier of G)
(@ g) * (@ g1) is V36() Element of K6( the carrier of G)
g2 * h1 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,g2,h1) is Element of the carrier of G
(g2 * h1) * H is V36() Element of K6( the carrier of G)
(g2 * h1) |^ p is Element of the carrier of G
((g2 * h1) |^ p) * H is V36() Element of K6( the carrier of G)
g2 |^ p is Element of the carrier of G
h1 |^ p is Element of the carrier of G
(g2 |^ p) * (h1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(g2 |^ p),(h1 |^ p)) is Element of the carrier of G
((g2 |^ p) * (h1 |^ p)) * H is V36() Element of K6( the carrier of G)
(g2 |^ p) * H is V36() Element of K6( the carrier of G)
(h1 |^ p) * H is V36() Element of K6( the carrier of G)
((g2 |^ p) * H) * ((h1 |^ p) * H) is V36() Element of K6( the carrier of G)
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
the carrier of G is V1() V36() set
H is Element of the carrier of G
g is Element of the carrier of G
H * g is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,H,g) is Element of the carrier of G
p |^ 0 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
(H * g) |^ (p |^ 0) is Element of the carrier of G
(H * g) |^ 1 is Element of the carrier of G
H |^ (p |^ 0) is Element of the carrier of G
g |^ (p |^ 0) is Element of the carrier of G
(H |^ (p |^ 0)) * (g |^ (p |^ 0)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ (p |^ 0)),(g |^ (p |^ 0))) is Element of the carrier of G
H |^ 1 is Element of the carrier of G
(H |^ 1) * (g |^ (p |^ 0)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ 1),(g |^ (p |^ 0))) is Element of the carrier of G
H * (g |^ (p |^ 0)) is Element of the carrier of G
K552( the carrier of G, the multF of G,H,(g |^ (p |^ 0))) is Element of the carrier of G
g |^ 1 is Element of the carrier of G
H * (g |^ 1) is Element of the carrier of G
K552( the carrier of G, the multF of G,H,(g |^ 1)) is Element of the carrier of G
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
(H * g) |^ (p |^ g1) is Element of the carrier of G
H |^ (p |^ g1) is Element of the carrier of G
g |^ (p |^ g1) is Element of the carrier of G
(H |^ (p |^ g1)) * (g |^ (p |^ g1)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ (p |^ g1)),(g |^ (p |^ g1))) is Element of the carrier of G
g1 + 1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
p |^ (g1 + 1) is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
(H * g) |^ (p |^ (g1 + 1)) is Element of the carrier of G
(p |^ g1) * p is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(H * g) |^ ((p |^ g1) * p) is Element of the carrier of G
((H * g) |^ (p |^ g1)) |^ p is Element of the carrier of G
((H |^ (p |^ g1)) * (g |^ (p |^ g1))) |^ p is Element of the carrier of G
(H |^ (p |^ g1)) |^ p is Element of the carrier of G
(g |^ (p |^ g1)) |^ p is Element of the carrier of G
((H |^ (p |^ g1)) |^ p) * ((g |^ (p |^ g1)) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((H |^ (p |^ g1)) |^ p),((g |^ (p |^ g1)) |^ p)) is Element of the carrier of G
H |^ ((p |^ g1) * p) is Element of the carrier of G
(H |^ ((p |^ g1) * p)) * ((g |^ (p |^ g1)) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ ((p |^ g1) * p)),((g |^ (p |^ g1)) |^ p)) is Element of the carrier of G
g |^ ((p |^ g1) * p) is Element of the carrier of G
(H |^ ((p |^ g1) * p)) * (g |^ ((p |^ g1) * p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ ((p |^ g1) * p)),(g |^ ((p |^ g1) * p))) is Element of the carrier of G
H |^ (p |^ (g1 + 1)) is Element of the carrier of G
(H |^ (p |^ (g1 + 1))) * (g |^ ((p |^ g1) * p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ (p |^ (g1 + 1))),(g |^ ((p |^ g1) * p))) is Element of the carrier of G
g |^ (p |^ (g1 + 1)) is Element of the carrier of G
(H |^ (p |^ (g1 + 1))) * (g |^ (p |^ (g1 + 1))) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ (p |^ (g1 + 1))),(g |^ (p |^ (g1 + 1)))) is Element of the carrier of G
g1 is V6() V10() V11() V12() V13() ext-real non negative V36() V41() set
p |^ g1 is V1() V6() V10() V11() V12() V13() ext-real positive non negative V36() V41() set
(H * g) |^ (p |^ g1) is Element of the carrier of G
H |^ (p |^ g1) is Element of the carrier of G
g |^ (p |^ g1) is Element of the carrier of G
(H |^ (p |^ g1)) * (g |^ (p |^ g1)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(H |^ (p |^ g1)),(g |^ (p |^ g1))) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative commutative multMagma
g is non empty finite unital Group-like associative commutative Subgroup of G
g1 is non empty finite unital Group-like associative commutative Subgroup of G
H is non empty finite unital Group-like associative commutative Subgroup of G
the carrier of H is V1() V36() set
g * g1 is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr g is V36() Element of K6( the carrier of G)
carr g1 is V36() Element of K6( the carrier of G)
(carr g) * (carr g1) is V36() Element of K6( the carrier of G)
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
center G is non empty finite strict unital Group-like associative Subgroup of G
H is non empty finite unital Group-like associative Subgroup of G
g is non empty finite strict unital Group-like associative normal Subgroup of G
H * g is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr H is V36() Element of K6( the carrier of G)
carr g is V36() Element of K6( the carrier of G)
(carr H) * (carr g) is V36() Element of K6( the carrier of G)
g1 is non empty finite strict unital Group-like associative Subgroup of G
the carrier of g1 is V1() V36() set
h1 is Element of the carrier of g1
h2 is Element of the carrier of g1
h1 * h2 is Element of the carrier of g1
the multF of g1 is V15() V18(K7( the carrier of g1, the carrier of g1)) V19( the carrier of g1) V20() V25(K7( the carrier of g1, the carrier of g1)) quasi_total V36() V191( the carrier of g1) Element of K6(K7(K7( the carrier of g1, the carrier of g1), the carrier of g1))
K7( the carrier of g1, the carrier of g1) is V36() set
K7(K7( the carrier of g1, the carrier of g1), the carrier of g1) is V36() set
K6(K7(K7( the carrier of g1, the carrier of g1), the carrier of g1)) is V36() V40() set
K552( the carrier of g1, the multF of g1,h1,h2) is Element of the carrier of g1
(h1 * h2) |^ p is Element of the carrier of g1
h1 |^ p is Element of the carrier of g1
h2 |^ p is Element of the carrier of g1
(h1 |^ p) * (h2 |^ p) is Element of the carrier of g1
K552( the carrier of g1, the multF of g1,(h1 |^ p),(h2 |^ p)) is Element of the carrier of g1
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 is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,a,b) is Element of the carrier of G
b2 is Element of the carrier of G
c1 is Element of the carrier of G
b2 * c1 is Element of the carrier of G
K552( the carrier of G, the multF of G,b2,c1) is Element of the carrier of G
b * c1 is Element of the carrier of G
K552( the carrier of G, the multF of G,b,c1) is Element of the carrier of G
c1 * b is Element of the carrier of G
K552( the carrier of G, the multF of G,c1,b) is Element of the carrier of G
a * b2 is Element of the carrier of G
K552( the carrier of G, the multF of G,a,b2) is Element of the carrier of G
(a * b2) * (c1 * b) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a * b2),(c1 * b)) is Element of the carrier of G
(c1 * b) * (a * b2) is Element of the carrier of G
K552( the carrier of G, the multF of G,(c1 * b),(a * b2)) is Element of the carrier of G
the carrier of H is V1() V36() set
a |^ p is Element of the carrier of G
d1 is Element of the carrier of H
d1 |^ p is Element of the carrier of H
b2 |^ p is Element of the carrier of G
c2 is Element of the carrier of H
c2 |^ p is Element of the carrier of H
d1 * c2 is Element of the carrier of H
the multF of H is V15() V18(K7( the carrier of H, the carrier of H)) V19( the carrier of H) V20() V25(K7( the carrier of H, the carrier of H)) quasi_total V36() V191( the carrier of H) Element of K6(K7(K7( the carrier of H, the carrier of H), the carrier of H))
K7( the carrier of H, the carrier of H) is V36() set
K7(K7( the carrier of H, the carrier of H), the carrier of H) is V36() set
K6(K7(K7( the carrier of H, the carrier of H), the carrier of H)) is V36() V40() set
K552( the carrier of H, the multF of H,d1,c2) is Element of the carrier of H
(a * b2) |^ p is Element of the carrier of G
(d1 * c2) |^ p is Element of the carrier of H
(d1 |^ p) * (c2 |^ p) is Element of the carrier of H
K552( the carrier of H, the multF of H,(d1 |^ p),(c2 |^ p)) is Element of the carrier of H
(a |^ p) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(b2 |^ p)) is Element of the carrier of G
the carrier of g is V1() V36() set
b |^ p is Element of the carrier of G
d2 is Element of the carrier of g
d2 |^ p is Element of the carrier of g
c1 |^ p is Element of the carrier of G
d2 is Element of the carrier of g
d2 |^ p is Element of the carrier of g
d2 * d2 is Element of the carrier of g
the multF of g is V15() V18(K7( the carrier of g, the carrier of g)) V19( the carrier of g) V20() V25(K7( the carrier of g, the carrier of g)) quasi_total V36() V191( the carrier of g) Element of K6(K7(K7( the carrier of g, the carrier of g), the carrier of g))
K7( the carrier of g, the carrier of g) is V36() set
K7(K7( the carrier of g, the carrier of g), the carrier of g) is V36() set
K6(K7(K7( the carrier of g, the carrier of g), the carrier of g)) is V36() V40() set
K552( the carrier of g, the multF of g,d2,d2) is Element of the carrier of g
(c1 * b) |^ p is Element of the carrier of G
(d2 * d2) |^ p is Element of the carrier of g
(d2 |^ p) * (d2 |^ p) is Element of the carrier of g
K552( the carrier of g, the multF of g,(d2 |^ p),(d2 |^ p)) is Element of the carrier of g
(c1 |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(c1 |^ p),(b |^ p)) is Element of the carrier of G
b * a is Element of the carrier of G
K552( the carrier of G, the multF of G,b,a) is Element of the carrier of G
c1 * b2 is Element of the carrier of G
K552( the carrier of G, the multF of G,c1,b2) is Element of the carrier of G
(a * b) * (b2 * c1) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a * b),(b2 * c1)) is Element of the carrier of G
((a * b) * (b2 * c1)) |^ p is Element of the carrier of G
b * (b2 * c1) is Element of the carrier of G
K552( the carrier of G, the multF of G,b,(b2 * c1)) is Element of the carrier of G
a * (b * (b2 * c1)) is Element of the carrier of G
K552( the carrier of G, the multF of G,a,(b * (b2 * c1))) is Element of the carrier of G
(a * (b * (b2 * c1))) |^ p is Element of the carrier of G
(b2 * c1) * b is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 * c1),b) is Element of the carrier of G
a * ((b2 * c1) * b) is Element of the carrier of G
K552( the carrier of G, the multF of G,a,((b2 * c1) * b)) is Element of the carrier of G
(a * ((b2 * c1) * b)) |^ p is Element of the carrier of G
b2 * (c1 * b) is Element of the carrier of G
K552( the carrier of G, the multF of G,b2,(c1 * b)) is Element of the carrier of G
a * (b2 * (c1 * b)) is Element of the carrier of G
K552( the carrier of G, the multF of G,a,(b2 * (c1 * b))) is Element of the carrier of G
(a * (b2 * (c1 * b))) |^ p is Element of the carrier of G
((a * b2) * (c1 * b)) |^ p is Element of the carrier of G
((a * b2) |^ p) * ((c1 * b) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a * b2) |^ p),((c1 * b) |^ p)) is Element of the carrier of G
(b |^ p) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b |^ p),(c1 |^ p)) is Element of the carrier of G
((a |^ p) * (b2 |^ p)) * ((b |^ p) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a |^ p) * (b2 |^ p)),((b |^ p) * (c1 |^ p))) is Element of the carrier of G
(b2 |^ p) * ((b |^ p) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 |^ p),((b |^ p) * (c1 |^ p))) is Element of the carrier of G
(a |^ p) * ((b2 |^ p) * ((b |^ p) * (c1 |^ p))) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),((b2 |^ p) * ((b |^ p) * (c1 |^ p)))) is Element of the carrier of G
(b2 |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 |^ p),(b |^ p)) is Element of the carrier of G
((b2 |^ p) * (b |^ p)) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((b2 |^ p) * (b |^ p)),(c1 |^ p)) is Element of the carrier of G
(a |^ p) * (((b2 |^ p) * (b |^ p)) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(((b2 |^ p) * (b |^ p)) * (c1 |^ p))) is Element of the carrier of G
(b |^ p) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b |^ p),(b2 |^ p)) is Element of the carrier of G
((b |^ p) * (b2 |^ p)) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((b |^ p) * (b2 |^ p)),(c1 |^ p)) is Element of the carrier of G
(a |^ p) * (((b |^ p) * (b2 |^ p)) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(((b |^ p) * (b2 |^ p)) * (c1 |^ p))) is Element of the carrier of G
(a |^ p) * ((b |^ p) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),((b |^ p) * (b2 |^ p))) is Element of the carrier of G
((a |^ p) * ((b |^ p) * (b2 |^ p))) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a |^ p) * ((b |^ p) * (b2 |^ p))),(c1 |^ p)) is Element of the carrier of G
(a |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(b |^ p)) is Element of the carrier of G
((a |^ p) * (b |^ p)) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a |^ p) * (b |^ p)),(b2 |^ p)) is Element of the carrier of G
(((a |^ p) * (b |^ p)) * (b2 |^ p)) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(((a |^ p) * (b |^ p)) * (b2 |^ p)),(c1 |^ p)) is Element of the carrier of G
(b2 |^ p) * (c1 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 |^ p),(c1 |^ p)) is Element of the carrier of G
((a |^ p) * (b |^ p)) * ((b2 |^ p) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a |^ p) * (b |^ p)),((b2 |^ p) * (c1 |^ p))) is Element of the carrier of G
(a * b) |^ p is Element of the carrier of G
((a * b) |^ p) * ((b2 |^ p) * (c1 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a * b) |^ p),((b2 |^ p) * (c1 |^ p))) is Element of the carrier of G
(b2 * c1) |^ p is Element of the carrier of G
((a * b) |^ p) * ((b2 * c1) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a * b) |^ p),((b2 * c1) |^ p)) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative multMagma
center G is non empty finite strict unital Group-like associative Subgroup of G
g is non empty finite unital Group-like associative normal Subgroup of G
H is non empty finite unital Group-like associative normal Subgroup of G
H * g is V36() Element of K6( the carrier of G)
the carrier of G is V1() V36() set
K6( the carrier of G) is V36() V40() set
carr H is V36() Element of K6( the carrier of G)
carr g is V36() Element of K6( the carrier of G)
(carr H) * (carr g) is V36() Element of K6( the carrier of G)
g1 is non empty finite strict unital Group-like associative normal Subgroup of G
the carrier of g1 is V1() V36() set
g2 is Element of the carrier of g1
h1 is Element of the carrier of g1
g2 * h1 is Element of the carrier of g1
the multF of g1 is V15() V18(K7( the carrier of g1, the carrier of g1)) V19( the carrier of g1) V20() V25(K7( the carrier of g1, the carrier of g1)) quasi_total V36() V191( the carrier of g1) Element of K6(K7(K7( the carrier of g1, the carrier of g1), the carrier of g1))
K7( the carrier of g1, the carrier of g1) is V36() set
K7(K7( the carrier of g1, the carrier of g1), the carrier of g1) is V36() set
K6(K7(K7( the carrier of g1, the carrier of g1), the carrier of g1)) is V36() V40() set
K552( the carrier of g1, the multF of g1,g2,h1) is Element of the carrier of g1
(g2 * h1) |^ p is Element of the carrier of g1
g2 |^ p is Element of the carrier of g1
h1 |^ p is Element of the carrier of g1
(g2 |^ p) * (h1 |^ p) is Element of the carrier of g1
K552( the carrier of g1, the multF of g1,(g2 |^ p),(h1 |^ p)) is Element of the carrier of g1
h2 is Element of the carrier of G
a is Element of the carrier of G
h2 * a is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,h2,a) is Element of the carrier of G
b is Element of the carrier of G
b2 is Element of the carrier of G
b * b2 is Element of the carrier of G
K552( the carrier of G, the multF of G,b,b2) is Element of the carrier of G
a * b2 is Element of the carrier of G
K552( the carrier of G, the multF of G,a,b2) is Element of the carrier of G
b2 * a is Element of the carrier of G
K552( the carrier of G, the multF of G,b2,a) is Element of the carrier of G
h2 * b is Element of the carrier of G
K552( the carrier of G, the multF of G,h2,b) is Element of the carrier of G
(h2 * b) * (b2 * a) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 * b),(b2 * a)) is Element of the carrier of G
(b2 * a) * (h2 * b) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 * a),(h2 * b)) is Element of the carrier of G
the carrier of H is V1() V36() set
h2 |^ p is Element of the carrier of G
c1 is Element of the carrier of H
c1 |^ p is Element of the carrier of H
b |^ p is Element of the carrier of G
d1 is Element of the carrier of H
d1 |^ p is Element of the carrier of H
c1 * d1 is Element of the carrier of H
the multF of H is V15() V18(K7( the carrier of H, the carrier of H)) V19( the carrier of H) V20() V25(K7( the carrier of H, the carrier of H)) quasi_total V36() V191( the carrier of H) Element of K6(K7(K7( the carrier of H, the carrier of H), the carrier of H))
K7( the carrier of H, the carrier of H) is V36() set
K7(K7( the carrier of H, the carrier of H), the carrier of H) is V36() set
K6(K7(K7( the carrier of H, the carrier of H), the carrier of H)) is V36() V40() set
K552( the carrier of H, the multF of H,c1,d1) is Element of the carrier of H
(h2 * b) |^ p is Element of the carrier of G
(c1 * d1) |^ p is Element of the carrier of H
(c1 |^ p) * (d1 |^ p) is Element of the carrier of H
K552( the carrier of H, the multF of H,(c1 |^ p),(d1 |^ p)) is Element of the carrier of H
(h2 |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),(b |^ p)) is Element of the carrier of G
the carrier of g is V1() V36() set
a |^ p is Element of the carrier of G
c2 is Element of the carrier of g
c2 |^ p is Element of the carrier of g
b2 |^ p is Element of the carrier of G
d2 is Element of the carrier of g
d2 |^ p is Element of the carrier of g
d2 * c2 is Element of the carrier of g
the multF of g is V15() V18(K7( the carrier of g, the carrier of g)) V19( the carrier of g) V20() V25(K7( the carrier of g, the carrier of g)) quasi_total V36() V191( the carrier of g) Element of K6(K7(K7( the carrier of g, the carrier of g), the carrier of g))
K7( the carrier of g, the carrier of g) is V36() set
K7(K7( the carrier of g, the carrier of g), the carrier of g) is V36() set
K6(K7(K7( the carrier of g, the carrier of g), the carrier of g)) is V36() V40() set
K552( the carrier of g, the multF of g,d2,c2) is Element of the carrier of g
(b2 * a) |^ p is Element of the carrier of G
(d2 * c2) |^ p is Element of the carrier of g
(d2 |^ p) * (c2 |^ p) is Element of the carrier of g
K552( the carrier of g, the multF of g,(d2 |^ p),(c2 |^ p)) is Element of the carrier of g
(b2 |^ p) * (a |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b2 |^ p),(a |^ p)) is Element of the carrier of G
a * h2 is Element of the carrier of G
K552( the carrier of G, the multF of G,a,h2) is Element of the carrier of G
b2 * b is Element of the carrier of G
K552( the carrier of G, the multF of G,b2,b) is Element of the carrier of G
(h2 * a) * (b * b2) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 * a),(b * b2)) is Element of the carrier of G
((h2 * a) * (b * b2)) |^ p is Element of the carrier of G
a * (b * b2) is Element of the carrier of G
K552( the carrier of G, the multF of G,a,(b * b2)) is Element of the carrier of G
h2 * (a * (b * b2)) is Element of the carrier of G
K552( the carrier of G, the multF of G,h2,(a * (b * b2))) is Element of the carrier of G
(h2 * (a * (b * b2))) |^ p is Element of the carrier of G
(b * b2) * a is Element of the carrier of G
K552( the carrier of G, the multF of G,(b * b2),a) is Element of the carrier of G
h2 * ((b * b2) * a) is Element of the carrier of G
K552( the carrier of G, the multF of G,h2,((b * b2) * a)) is Element of the carrier of G
(h2 * ((b * b2) * a)) |^ p is Element of the carrier of G
b * (b2 * a) is Element of the carrier of G
K552( the carrier of G, the multF of G,b,(b2 * a)) is Element of the carrier of G
h2 * (b * (b2 * a)) is Element of the carrier of G
K552( the carrier of G, the multF of G,h2,(b * (b2 * a))) is Element of the carrier of G
(h2 * (b * (b2 * a))) |^ p is Element of the carrier of G
((h2 * b) * (b2 * a)) |^ p is Element of the carrier of G
((h2 * b) |^ p) * ((b2 * a) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 * b) |^ p),((b2 * a) |^ p)) is Element of the carrier of G
(a |^ p) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(b2 |^ p)) is Element of the carrier of G
((h2 |^ p) * (b |^ p)) * ((a |^ p) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 |^ p) * (b |^ p)),((a |^ p) * (b2 |^ p))) is Element of the carrier of G
(b |^ p) * ((a |^ p) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b |^ p),((a |^ p) * (b2 |^ p))) is Element of the carrier of G
(h2 |^ p) * ((b |^ p) * ((a |^ p) * (b2 |^ p))) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),((b |^ p) * ((a |^ p) * (b2 |^ p)))) is Element of the carrier of G
(b |^ p) * (a |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b |^ p),(a |^ p)) is Element of the carrier of G
((b |^ p) * (a |^ p)) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((b |^ p) * (a |^ p)),(b2 |^ p)) is Element of the carrier of G
(h2 |^ p) * (((b |^ p) * (a |^ p)) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),(((b |^ p) * (a |^ p)) * (b2 |^ p))) is Element of the carrier of G
(a |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(b |^ p)) is Element of the carrier of G
((a |^ p) * (b |^ p)) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((a |^ p) * (b |^ p)),(b2 |^ p)) is Element of the carrier of G
(h2 |^ p) * (((a |^ p) * (b |^ p)) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),(((a |^ p) * (b |^ p)) * (b2 |^ p))) is Element of the carrier of G
(h2 |^ p) * ((a |^ p) * (b |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),((a |^ p) * (b |^ p))) is Element of the carrier of G
((h2 |^ p) * ((a |^ p) * (b |^ p))) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 |^ p) * ((a |^ p) * (b |^ p))),(b2 |^ p)) is Element of the carrier of G
(h2 |^ p) * (a |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h2 |^ p),(a |^ p)) is Element of the carrier of G
((h2 |^ p) * (a |^ p)) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 |^ p) * (a |^ p)),(b |^ p)) is Element of the carrier of G
(((h2 |^ p) * (a |^ p)) * (b |^ p)) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(((h2 |^ p) * (a |^ p)) * (b |^ p)),(b2 |^ p)) is Element of the carrier of G
(b |^ p) * (b2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(b |^ p),(b2 |^ p)) is Element of the carrier of G
((h2 |^ p) * (a |^ p)) * ((b |^ p) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 |^ p) * (a |^ p)),((b |^ p) * (b2 |^ p))) is Element of the carrier of G
(h2 * a) |^ p is Element of the carrier of G
((h2 * a) |^ p) * ((b |^ p) * (b2 |^ p)) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 * a) |^ p),((b |^ p) * (b2 |^ p))) is Element of the carrier of G
(b * b2) |^ p is Element of the carrier of G
((h2 * a) |^ p) * ((b * b2) |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,((h2 * a) |^ p),((b * b2) |^ p)) is Element of the carrier of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty unital Group-like associative multMagma
H is non empty unital Group-like associative multMagma
the carrier of H is V1() set
g is Element of the carrier of H
g1 is Element of the carrier of H
g * g1 is Element of the carrier of H
the multF of H is V15() V18(K7( the carrier of H, the carrier of H)) V19( the carrier of H) V20() V25(K7( the carrier of H, the carrier of H)) quasi_total V191( the carrier of H) Element of K6(K7(K7( the carrier of H, the carrier of H), the carrier of H))
K7( the carrier of H, the carrier of H) is set
K7(K7( the carrier of H, the carrier of H), the carrier of H) is set
K6(K7(K7( the carrier of H, the carrier of H), the carrier of H)) is set
K552( the carrier of H, the multF of H,g,g1) is Element of the carrier of H
(g * g1) |^ p is Element of the carrier of H
g |^ p is Element of the carrier of H
g1 |^ p is Element of the carrier of H
(g |^ p) * (g1 |^ p) is Element of the carrier of H
K552( the carrier of H, the multF of H,(g |^ p),(g1 |^ p)) is Element of the carrier of H
the carrier of G is V1() set
K7( the carrier of G, the carrier of H) is set
K6(K7( the carrier of G, the carrier of H)) is set
g2 is V1() V15() V18( the carrier of G) V19( the carrier of H) V20() V25( the carrier of G) quasi_total unity-preserving V194(G,H) Element of K6(K7( the carrier of G, the carrier of H))
h1 is Element of the carrier of G
g2 . h1 is Element of the carrier of H
h2 is Element of the carrier of G
g2 . h2 is Element of the carrier of H
h1 * h2 is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K552( the carrier of G, the multF of G,h1,h2) is Element of the carrier of G
g2 . (h1 * h2) is Element of the carrier of H
(h1 * h2) |^ p is Element of the carrier of G
g2 . ((h1 * h2) |^ p) is Element of the carrier of H
h1 |^ p is Element of the carrier of G
h2 |^ p is Element of the carrier of G
(h1 |^ p) * (h2 |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(h1 |^ p),(h2 |^ p)) is Element of the carrier of G
g2 . ((h1 |^ p) * (h2 |^ p)) is Element of the carrier of H
g2 . (h1 |^ p) is Element of the carrier of H
g2 . (h2 |^ p) is Element of the carrier of H
(g2 . (h1 |^ p)) * (g2 . (h2 |^ p)) is Element of the carrier of H
K552( the carrier of H, the multF of H,(g2 . (h1 |^ p)),(g2 . (h2 |^ p))) is Element of the carrier of H
(g2 . h1) |^ p is Element of the carrier of H
((g2 . h1) |^ p) * (g2 . (h2 |^ p)) is Element of the carrier of H
K552( the carrier of H, the multF of H,((g2 . h1) |^ p),(g2 . (h2 |^ p))) is Element of the carrier of H
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty strict unital Group-like associative multMagma
H is non empty strict unital Group-like associative multMagma
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite unital Group-like associative (p) multMagma
the carrier of G is V1() V36() set
H is non empty finite unital Group-like associative multMagma
the carrier of H is V1() V36() set
K7( the carrier of G, the carrier of H) is V36() set
K6(K7( the carrier of G, the carrier of H)) is V36() V40() set
g is V1() V15() V18( the carrier of G) V19( the carrier of H) V20() V25( the carrier of G) quasi_total V36() unity-preserving V194(G,H) Element of K6(K7( the carrier of G, the carrier of H))
Image g is non empty finite strict unital Group-like associative Subgroup of H
the carrier of (Image g) is V1() V36() set
g1 is Element of the carrier of (Image g)
g2 is Element of the carrier of (Image g)
g1 * g2 is Element of the carrier of (Image g)
the multF of (Image g) is V15() V18(K7( the carrier of (Image g), the carrier of (Image g))) V19( the carrier of (Image g)) V20() V25(K7( the carrier of (Image g), the carrier of (Image g))) quasi_total V36() V191( the carrier of (Image g)) Element of K6(K7(K7( the carrier of (Image g), the carrier of (Image g)), the carrier of (Image g)))
K7( the carrier of (Image g), the carrier of (Image g)) is V36() set
K7(K7( the carrier of (Image g), the carrier of (Image g)), the carrier of (Image g)) is V36() set
K6(K7(K7( the carrier of (Image g), the carrier of (Image g)), the carrier of (Image g))) is V36() V40() set
K552( the carrier of (Image g), the multF of (Image g),g1,g2) is Element of the carrier of (Image g)
(g1 * g2) |^ p is Element of the carrier of (Image g)
g1 |^ p is Element of the carrier of (Image g)
g2 |^ p is Element of the carrier of (Image g)
(g1 |^ p) * (g2 |^ p) is Element of the carrier of (Image g)
K552( the carrier of (Image g), the multF of (Image g),(g1 |^ p),(g2 |^ p)) is Element of the carrier of (Image g)
a is Element of the carrier of G
g . a is Element of the carrier of H
b is Element of the carrier of G
g . b is Element of the carrier of H
h1 is Element of the carrier of H
h2 is Element of the carrier of H
h1 * h2 is Element of the carrier of H
the multF of H is V15() V18(K7( the carrier of H, the carrier of H)) V19( the carrier of H) V20() V25(K7( the carrier of H, the carrier of H)) quasi_total V36() V191( the carrier of H) Element of K6(K7(K7( the carrier of H, the carrier of H), the carrier of H))
K7( the carrier of H, the carrier of H) is V36() set
K7(K7( the carrier of H, the carrier of H), the carrier of H) is V36() set
K6(K7(K7( the carrier of H, the carrier of H), the carrier of H)) is V36() V40() set
K552( the carrier of H, the multF of H,h1,h2) is Element of the carrier of H
a * b is Element of the carrier of G
the multF of G is V15() V18(K7( the carrier of G, the carrier of G)) V19( the carrier of G) V20() V25(K7( the carrier of G, the carrier of G)) quasi_total V36() V191( the carrier of G) Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is V36() set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is V36() set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is V36() V40() set
K552( the carrier of G, the multF of G,a,b) is Element of the carrier of G
g . (a * b) is Element of the carrier of H
(g . (a * b)) |^ p is Element of the carrier of H
(a * b) |^ p is Element of the carrier of G
g . ((a * b) |^ p) is Element of the carrier of H
a |^ p is Element of the carrier of G
b |^ p is Element of the carrier of G
(a |^ p) * (b |^ p) is Element of the carrier of G
K552( the carrier of G, the multF of G,(a |^ p),(b |^ p)) is Element of the carrier of G
g . ((a |^ p) * (b |^ p)) is Element of the carrier of H
g . (a |^ p) is Element of the carrier of H
g . (b |^ p) is Element of the carrier of H
(g . (a |^ p)) * (g . (b |^ p)) is Element of the carrier of H
K552( the carrier of H, the multF of H,(g . (a |^ p)),(g . (b |^ p))) is Element of the carrier of H
(g . a) |^ p is Element of the carrier of H
((g . a) |^ p) * (g . (b |^ p)) is Element of the carrier of H
K552( the carrier of H, the multF of H,((g . a) |^ p),(g . (b |^ p))) is Element of the carrier of H
h1 |^ p is Element of the carrier of H
h2 |^ p is Element of the carrier of H
(h1 |^ p) * (h2 |^ p) is Element of the carrier of H
K552( the carrier of H, the multF of H,(h1 |^ p),(h2 |^ p)) is Element of the carrier of H
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite strict unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT
(1). G is non empty V74() finite 1 -element strict unital Group-like associative commutative cyclic normal Subgroup of G
p is V1() V6() V10() V11() V12() V13() prime ext-real positive non negative V36() V41() set
G is non empty finite strict unital Group-like associative multMagma
(p,G) is V6() V10() V11() V12() V13() ext-real non negative V35() V36() V41() V57() V58() V59() V60() V61() V62() Element of NAT