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

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