REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K268() is set
1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real V18() Function-like functional finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative set
{{},1} is non empty finite V39() set
K463() is set
bool K463() is non empty set
K464() is Element of bool K463()
2 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
[:2,2:] is non empty finite set
[:[:2,2:],2:] is non empty finite set
bool [:[:2,2:],2:] is non empty finite V39() set
INT.Group is non empty strict unital Group-like associative commutative cyclic multMagma
the carrier of INT.Group is non empty V86() set
SetPrimes is non empty non trivial non finite Element of bool NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real V18() Function-like functional finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative Element of NAT
card {} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real V18() Function-like functional finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative set
<*> REAL is Relation-like NAT -defined REAL -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real V18() Function-like one-to-one constant functional finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V72() V73() V74() V75() FinSequence of REAL
Sum (<*> REAL) is complex real ext-real Element of REAL
G is non empty 1-sorted
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
G is non empty 1-sorted
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total Element of bool [: the carrier of G,(Funcs (p,p)):]
P is Element of the carrier of G
E . P is Relation-like Function-like set
[:p,p:] is set
bool [:p,p:] is non empty set
E . P is Relation-like Function-like Element of Funcs (p,p)
G is non empty unital multMagma
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
G is non empty unital multMagma
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
[:p,p:] is set
bool [:p,p:] is non empty set
id p is Relation-like p -defined p -valued Function-like one-to-one total quasi_total Element of bool [:p,p:]
{(id p)} is non empty trivial functional finite 1 -element Element of bool (bool [:p,p:])
bool (bool [:p,p:]) is non empty set
[: the carrier of G,{(id p)}:] is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total Element of bool [: the carrier of G,(Funcs (p,p)):]
bool [: the carrier of G,{(id p)}:] is non empty set
P9 is set
H9 is set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
dom E is Element of bool the carrier of G
bool the carrier of G is non empty set
P is Element of the carrier of G
E . P is Relation-like Function-like Element of Funcs (p,p)
rng E is functional Element of bool (Funcs (p,p))
bool (Funcs (p,p)) is non empty set
P9 is Relation-like the carrier of G -defined {(id p)} -valued Element of bool [: the carrier of G,{(id p)}:]
rng P9 is trivial functional finite Element of bool {(id p)}
bool {(id p)} is non empty finite V39() set
1_ G is Element of the carrier of G
(G,p,E,(1_ G)) is Relation-like p -defined p -valued Function-like total quasi_total Element of bool [:p,p:]
P is Element of the carrier of G
P9 is Element of the carrier of G
P * P9 is Element of the carrier of G
(G,p,E,(P * P9)) is Relation-like p -defined p -valued Function-like total quasi_total Element of bool [:p,p:]
(G,p,E,P9) is Relation-like p -defined p -valued Function-like total quasi_total Element of bool [:p,p:]
(G,p,E,P) is Relation-like p -defined p -valued Function-like total quasi_total Element of bool [:p,p:]
(G,p,E,P) * (G,p,E,P9) is Relation-like p -defined p -valued Function-like total quasi_total Element of bool [:p,p:]
F2() is non empty unital Group-like multMagma
the carrier of F2() is non empty set
F1() is set
[:F1(),F1():] is set
bool [:F1(),F1():] is non empty set
1_ F2() is Element of the carrier of F2()
F3((1_ F2())) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
id F1() is Relation-like F1() -defined F1() -valued Function-like one-to-one total quasi_total Element of bool [:F1(),F1():]
Funcs (F1(),F1()) is non empty functional set
[: the carrier of F2(),(Funcs (F1(),F1())):] is non empty set
bool [: the carrier of F2(),(Funcs (F1(),F1())):] is non empty set
{ [b1,F3(b1)] where b1 is Element of the carrier of F2() : verum } is set
p is set
E is Element of the carrier of F2()
F3(E) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[E,F3(E)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
[: the carrier of F2(),(bool [:F1(),F1():]):] is non empty set
{E,F3(E)} is non empty finite set
{E} is non empty trivial finite 1 -element set
{{E,F3(E)},{E}} is non empty finite V39() set
p is set
E is set
[p,E] is set
{p,E} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,E},{p}} is non empty finite V39() set
P9 is Element of the carrier of F2()
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,F3(P9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P9,F3(P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,F3(P9)},{P9}} is non empty finite V39() set
P is set
[p,P] is set
{p,P} is non empty finite set
{{p,P},{p}} is non empty finite V39() set
P9 is Element of the carrier of F2()
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,F3(P9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P9,F3(P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,F3(P9)},{P9}} is non empty finite V39() set
E is set
P is Element of the carrier of F2()
F3(P) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
P9 is set
P9 is set
[E,P9] is set
{E,P9} is non empty finite set
{E} is non empty trivial finite 1 -element set
{{E,P9},{E}} is non empty finite V39() set
p is Relation-like the carrier of F2() -defined Funcs (F1(),F1()) -valued Function-like Element of bool [: the carrier of F2(),(Funcs (F1(),F1())):]
P is set
[E,P] is set
{E,P} is non empty finite set
{{E,P},{E}} is non empty finite V39() set
P9 is Element of the carrier of F2()
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,F3(P9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P9,F3(P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,F3(P9)},{P9}} is non empty finite V39() set
dom p is Element of bool the carrier of F2()
bool the carrier of F2() is non empty set
P is Element of the carrier of F2()
E is Relation-like the carrier of F2() -defined Funcs (F1(),F1()) -valued non empty Function-like total quasi_total Element of bool [: the carrier of F2(),(Funcs (F1(),F1())):]
dom E is Element of bool the carrier of F2()
E . P is Relation-like Function-like Element of Funcs (F1(),F1())
[P,(E . P)] is Element of [: the carrier of F2(),(Funcs (F1(),F1())):]
{P,(E . P)} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,(E . P)},{P}} is non empty finite V39() set
P9 is Element of the carrier of F2()
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,F3(P9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P9,F3(P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,F3(P9)},{P9}} is non empty finite V39() set
P9 is Element of the carrier of F2()
E . P9 is Relation-like Function-like Element of Funcs (F1(),F1())
[P9,(E . P9)] is Element of [: the carrier of F2(),(Funcs (F1(),F1())):]
{P9,(E . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(E . P9)},{P9}} is non empty finite V39() set
H9 is Element of the carrier of F2()
F3(H9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[H9,F3(H9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{H9,F3(H9)} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,F3(H9)},{H9}} is non empty finite V39() set
P * P9 is Element of the carrier of F2()
E . (P * P9) is Relation-like Function-like Element of Funcs (F1(),F1())
[(P * P9),(E . (P * P9))] is Element of [: the carrier of F2(),(Funcs (F1(),F1())):]
{(P * P9),(E . (P * P9))} is non empty finite set
{(P * P9)} is non empty trivial finite 1 -element set
{{(P * P9),(E . (P * P9))},{(P * P9)}} is non empty finite V39() set
P9 is Element of the carrier of F2()
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,F3(P9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P9,F3(P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,F3(P9)},{P9}} is non empty finite V39() set
(F2(),F1(),E,(P * P9)) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
F3((P * P9)) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
(F2(),F1(),E,P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
(F2(),F1(),E,P) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
(F2(),F1(),E,P) * (F2(),F1(),E,P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
E . (1_ F2()) is Relation-like Function-like Element of Funcs (F1(),F1())
[(1_ F2()),(E . (1_ F2()))] is Element of [: the carrier of F2(),(Funcs (F1(),F1())):]
{(1_ F2()),(E . (1_ F2()))} is non empty finite set
{(1_ F2())} is non empty trivial finite 1 -element set
{{(1_ F2()),(E . (1_ F2()))},{(1_ F2())}} is non empty finite V39() set
P is Element of the carrier of F2()
F3(P) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P,F3(P)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{P,F3(P)} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,F3(P)},{P}} is non empty finite V39() set
P9 is Relation-like the carrier of F2() -defined Funcs (F1(),F1()) -valued non empty Function-like total quasi_total (F2(),F1()) Element of bool [: the carrier of F2(),(Funcs (F1(),F1())):]
P9 is Element of the carrier of F2()
P9 . P9 is Relation-like Function-like Element of Funcs (F1(),F1())
F3(P9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[P9,(P9 . P9)] is Element of [: the carrier of F2(),(Funcs (F1(),F1())):]
{P9,(P9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(P9 . P9)},{P9}} is non empty finite V39() set
H9 is Element of the carrier of F2()
F3(H9) is Relation-like F1() -defined F1() -valued Function-like total quasi_total Element of bool [:F1(),F1():]
[H9,F3(H9)] is Element of [: the carrier of F2(),(bool [:F1(),F1():]):]
{H9,F3(H9)} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,F3(H9)},{H9}} is non empty finite V39() set
p is non empty unital Group-like multMagma
the carrier of p is non empty set
G is non empty set
Funcs (G,G) is non empty functional set
[: the carrier of p,(Funcs (G,G)):] is non empty set
bool [: the carrier of p,(Funcs (G,G)):] is non empty set
[:G,G:] is non empty set
bool [:G,G:] is non empty set
P is Relation-like the carrier of p -defined Funcs (G,G) -valued non empty Function-like total quasi_total (p,G) Element of bool [: the carrier of p,(Funcs (G,G)):]
E is Element of the carrier of p
(p,G,P,E) is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
P9 is Element of the carrier of p
P9 is Element of the carrier of p
E * P9 is Element of the carrier of p
P9 * E is Element of the carrier of p
(p,G,P,P9) is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
Funcs (G,G) is non empty functional FUNCTION_DOMAIN of G,G
id G is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
1_ p is Element of the carrier of p
(p,G,P,(1_ p)) is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
(p,G,P,(P9 * E)) is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
(p,G,P,P9) * (p,G,P,E) is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
H9 is Relation-like G -defined G -valued non empty Function-like total quasi_total Element of bool [:G,G:]
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
G is non empty multMagma
the carrier of G is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is non empty functional set
[: the carrier of G,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
bool [: the carrier of G,(Funcs ( the carrier of G, the carrier of G)):] is non empty set
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
E is Element of the carrier of G
P is Element of the carrier of G
E * P is Element of the carrier of G
(E * P) * is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
P * is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
E * is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
H1(E) * H1(P) is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
Funcs ( the carrier of G, the carrier of G) is non empty functional FUNCTION_DOMAIN of the carrier of G, the carrier of G
P9 is set
dom ((E * P) *) is Element of bool the carrier of G
bool the carrier of G is non empty set
dom (P *) is Element of bool the carrier of G
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
(P *) . P9 is set
rng (P *) is Element of bool the carrier of G
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
dom (E *) is Element of bool the carrier of G
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P9 is set
(P *) . P9 is set
T is Relation-like Function-like set
dom T is set
rng T is set
((E * P) *) . P9 is set
P9 is Element of the carrier of G
(E * P) * P9 is Element of the carrier of G
P * P9 is Element of the carrier of G
E * (P * P9) is Element of the carrier of G
T is Element of the carrier of G
E * T is Element of the carrier of G
(E *) . ((P *) . P9) is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like one-to-one total quasi_total Element of bool [: the carrier of G, the carrier of G:]
P is set
P9 is Element of the carrier of G
((1_ G) *) . P9 is Element of the carrier of G
(1_ G) * P9 is Element of the carrier of G
((1_ G) *) . P is set
Funcs ( the carrier of G, the carrier of G) is non empty functional FUNCTION_DOMAIN of the carrier of G, the carrier of G
P is Relation-like Function-like set
dom P is set
rng P is set
E is Relation-like the carrier of G -defined Funcs ( the carrier of G, the carrier of G) -valued non empty Function-like total quasi_total (G, the carrier of G) Element of bool [: the carrier of G,(Funcs ( the carrier of G, the carrier of G)):]
p is Relation-like the carrier of G -defined Funcs ( the carrier of G, the carrier of G) -valued non empty Function-like total quasi_total (G, the carrier of G) Element of bool [: the carrier of G,(Funcs ( the carrier of G, the carrier of G)):]
E is Relation-like the carrier of G -defined Funcs ( the carrier of G, the carrier of G) -valued non empty Function-like total quasi_total (G, the carrier of G) Element of bool [: the carrier of G,(Funcs ( the carrier of G, the carrier of G)):]
P is Element of the carrier of G
p . P is Relation-like Function-like set
E . P is Relation-like Function-like set
p . P is Relation-like Function-like Element of Funcs ( the carrier of G, the carrier of G)
P * is Relation-like the carrier of G -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty set
bool [: the carrier of G, the carrier of G:] is non empty set
E . P is Relation-like Function-like Element of Funcs ( the carrier of G, the carrier of G)
G is set
bool G is non empty set
p is set
{ b1 where b1 is Element of bool G : card b1 = p } is set
bool (bool G) is non empty set
P is set
P9 is Element of bool G
card P9 is epsilon-transitive epsilon-connected ordinal cardinal set
G is finite set
p is set
(G,p) is finite V39() Element of bool (bool G)
bool G is non empty finite V39() set
bool (bool G) is non empty finite V39() set
{ b1 where b1 is Element of bool G : card b1 = p } is set
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p is non empty set
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(p,G) is Element of bool (bool p)
bool p is non empty set
bool (bool p) is non empty set
{ b1 where b1 is Element of bool p : card b1 = G } is set
P is Relation-like Function-like set
dom P is set
rng P is set
P .: G is finite set
card (P .: G) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is non empty finite set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(G,p) is finite V39() Element of bool (bool G)
bool G is non empty finite V39() set
bool (bool G) is non empty finite V39() set
{ b1 where b1 is Element of bool G : card b1 = p } is set
card (G,p) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is set
P is set
Choose (G,p,E,P) is functional Element of bool (Funcs (G,{E,P}))
{E,P} is non empty finite set
Funcs (G,{E,P}) is non empty functional FUNCTION_DOMAIN of G,{E,P}
bool (Funcs (G,{E,P})) is non empty set
card (Choose (G,p,E,P)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:G,{E,P}:] is non empty finite set
bool [:G,{E,P}:] is non empty finite V39() set
{E} is non empty trivial finite 1 -element set
{ [b1,b2] where b1 is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:], b2 is finite Element of bool G : ( card (b1 " {E}) = p & b1 " {E} = b2 ) } is set
P9 is set
H9 is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
P9 is finite Element of bool G
[H9,P9] is Element of [:(bool [:G,{E,P}:]),(bool G):]
[:(bool [:G,{E,P}:]),(bool G):] is non empty finite set
{H9,P9} is non empty finite V39() set
{H9} is non empty trivial functional finite V39() 1 -element set
{{H9,P9},{H9}} is non empty finite V39() set
H9 " {E} is finite Element of bool G
card (H9 " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is set
T is set
G9 is set
T9 is set
[G9,T9] is set
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
H9 is set
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,P9},{H9}} is non empty finite V39() set
P9 is Relation-like set
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
G9 is finite Element of bool G
[T,G9] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T,G9} is non empty finite V39() set
{T} is non empty trivial functional finite V39() 1 -element set
{{T,G9},{T}} is non empty finite V39() set
T " {E} is finite Element of bool G
card (T " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{{H9,P9},{H9}} is non empty finite V39() set
T9 is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
K is finite Element of bool G
[T9,K] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T9,K} is non empty finite V39() set
{T9} is non empty trivial functional finite V39() 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
T9 " {E} is finite Element of bool G
card (T9 " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is set
H9 is Relation-like Function-like set
dom H9 is set
P9 is set
H9 . P9 is set
H9 . P9 is set
[P9,(H9 . P9)] is set
{P9,(H9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(H9 . P9)},{P9}} is non empty finite V39() set
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
G9 is finite Element of bool G
[T,G9] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T,G9} is non empty finite V39() set
{T} is non empty trivial functional finite V39() 1 -element set
{{T,G9},{T}} is non empty finite V39() set
T " {E} is finite Element of bool G
card (T " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
[P9,(H9 . P9)] is set
{P9,(H9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(H9 . P9)},{P9}} is non empty finite V39() set
T9 is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
K is finite Element of bool G
[T9,K] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T9,K} is non empty finite V39() set
{T9} is non empty trivial functional finite V39() 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
T9 " {E} is finite Element of bool G
card (T9 " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom T9 is finite Element of bool G
dom T is finite Element of bool G
P is set
T9 . P is set
T . P is set
P is set
T9 . P is set
T . P is set
[P,(T9 . P)] is set
{P,(T9 . P)} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,(T9 . P)},{P}} is non empty finite V39() set
T is set
[P,T] is set
{P,T} is non empty finite set
{{P,T},{P}} is non empty finite V39() set
[P,(T . P)] is set
{P,(T . P)} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,(T . P)},{P}} is non empty finite V39() set
T is set
[P,T] is set
{P,T} is non empty finite set
{{P,T},{P}} is non empty finite V39() set
P9 is set
P9 is finite Element of bool G
card P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is Element of G
G9 is Element of {E,P}
G9 is Element of {E,P}
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
G9 is set
K is set
P is Element of G
T . P is Element of {E,P}
dom T is finite Element of bool G
T . K is set
[K,(T . K)] is set
{K,(T . K)} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,(T . K)},{K}} is non empty finite V39() set
T " {E} is finite Element of bool G
P is set
[K,P] is set
{K,P} is non empty finite set
{{K,P},{K}} is non empty finite V39() set
T is Element of G
T . T is Element of {E,P}
T9 is set
[T9,P9] is set
{T9,P9} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,P9},{T9}} is non empty finite V39() set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
G9 is finite Element of bool G
[T,G9] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T,G9} is non empty finite V39() set
{T} is non empty trivial functional finite V39() 1 -element set
{{T,G9},{T}} is non empty finite V39() set
T " {E} is finite Element of bool G
card (T " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
rng H9 is set
P9 is set
P9 is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
P9 " {E} is finite Element of bool G
card (P9 " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
[P9,(P9 " {E})] is set
{P9,(P9 " {E})} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(P9 " {E})},{P9}} is non empty finite V39() set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
T is Relation-like G -defined {E,P} -valued non empty Function-like total quasi_total finite Element of bool [:G,{E,P}:]
G9 is finite Element of bool G
[T,G9] is Element of [:(bool [:G,{E,P}:]),(bool G):]
{T,G9} is non empty finite V39() set
{T} is non empty trivial functional finite V39() 1 -element set
{{T,G9},{T}} is non empty finite V39() set
T " {E} is finite Element of bool G
card (T " {E}) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is non empty unital Group-like multMagma
the carrier of E is non empty set
G is non empty set
Funcs (G,G) is non empty functional set
[: the carrier of E,(Funcs (G,G)):] is non empty set
bool [: the carrier of E,(Funcs (G,G)):] is non empty set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card G is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(G,p) is Element of bool (bool G)
bool G is non empty set
bool (bool G) is non empty set
{ b1 where b1 is Element of bool G : card b1 = p } is set
[:(G,p),(G,p):] is set
bool [:(G,p),(G,p):] is non empty set
P9 is Relation-like the carrier of E -defined Funcs (G,G) -valued non empty Function-like total quasi_total (E,G) Element of bool [: the carrier of E,(Funcs (G,G)):]
P is Element of the carrier of E
(E,G,P9,P) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
[:G,G:] is non empty set
bool [:G,G:] is non empty set
{ [b1,((E,G,P9,P) .: b1)] where b1 is Element of (G,p) : verum } is set
P9 is set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
G9 is Element of (G,p)
(E,G,P9,P) .: G9 is Element of bool G
[G9,((E,G,P9,P) .: G9)] is set
{G9,((E,G,P9,P) .: G9)} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,((E,G,P9,P) .: G9)},{G9}} is non empty finite V39() set
T is set
[P9,T] is set
{P9,T} is non empty finite set
{{P9,T},{P9}} is non empty finite V39() set
T9 is Element of (G,p)
(E,G,P9,P) .: T9 is Element of bool G
[T9,((E,G,P9,P) .: T9)] is set
{T9,((E,G,P9,P) .: T9)} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,((E,G,P9,P) .: T9)},{T9}} is non empty finite V39() set
P9 is set
P9 is Element of (G,p)
(E,G,P9,P) .: P9 is Element of bool G
[P9,((E,G,P9,P) .: P9)] is set
{P9,((E,G,P9,P) .: P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,((E,G,P9,P) .: P9)},{P9}} is non empty finite V39() set
T is set
G9 is set
T9 is set
K is set
[T9,K] is set
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
P9 is set
T is Element of (G,p)
(E,G,P9,P) .: T is Element of bool G
G9 is set
T9 is set
[P9,T9] is set
{P9,T9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T9},{P9}} is non empty finite V39() set
P9 is Relation-like Function-like set
T is set
[P9,T] is set
{P9,T} is non empty finite set
{{P9,T},{P9}} is non empty finite V39() set
G9 is Element of (G,p)
(E,G,P9,P) .: G9 is Element of bool G
[G9,((E,G,P9,P) .: G9)] is set
{G9,((E,G,P9,P) .: G9)} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,((E,G,P9,P) .: G9)},{G9}} is non empty finite V39() set
dom P9 is set
P9 is set
rng P9 is set
T is set
[T,P9] is set
{T,P9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,P9},{T}} is non empty finite V39() set
G9 is Element of (G,p)
(E,G,P9,P) .: G9 is Element of bool G
[G9,((E,G,P9,P) .: G9)] is set
{G9,((E,G,P9,P) .: G9)} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,((E,G,P9,P) .: G9)},{G9}} is non empty finite V39() set
(E,G,P9,P) | G9 is Relation-like G -defined G -valued Function-like Element of bool [:G,G:]
Funcs (G,G) is non empty functional FUNCTION_DOMAIN of G,G
dom ((E,G,P9,P) | G9) is Element of bool G
K is Relation-like Function-like set
dom K is set
rng K is set
rng ((E,G,P9,P) | G9) is Element of bool G
card P9 is epsilon-transitive epsilon-connected ordinal cardinal set
K is Element of bool G
card K is epsilon-transitive epsilon-connected ordinal cardinal set
P9 is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
T is Element of (G,p)
P9 . T is set
(E,G,P9,P) .: T is Element of bool G
[T,(P9 . T)] is set
{T,(P9 . T)} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,(P9 . T)},{T}} is non empty finite V39() set
G9 is Element of (G,p)
(E,G,P9,P) .: G9 is Element of bool G
[G9,((E,G,P9,P) .: G9)] is set
{G9,((E,G,P9,P) .: G9)} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,((E,G,P9,P) .: G9)},{G9}} is non empty finite V39() set
H9 is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
P9 is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
P9 is Element of (G,p)
H9 . P9 is set
P9 . P9 is set
(E,G,P9,P) .: P9 is Element of bool G
E is non empty unital Group-like multMagma
the carrier of E is non empty set
G is non empty set
Funcs (G,G) is non empty functional set
[: the carrier of E,(Funcs (G,G)):] is non empty set
bool [: the carrier of E,(Funcs (G,G)):] is non empty set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card G is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(G,p) is Element of bool (bool G)
bool G is non empty set
bool (bool G) is non empty set
{ b1 where b1 is Element of bool G : card b1 = p } is set
Funcs ((G,p),(G,p)) is non empty functional set
[: the carrier of E,(Funcs ((G,p),(G,p))):] is non empty set
bool [: the carrier of E,(Funcs ((G,p),(G,p))):] is non empty set
P is Relation-like the carrier of E -defined Funcs (G,G) -valued non empty Function-like total quasi_total (E,G) Element of bool [: the carrier of E,(Funcs (G,G)):]
[:(G,p),(G,p):] is set
bool [:(G,p),(G,p):] is non empty set
P9 is Element of the carrier of E
H9 is Element of the carrier of E
P9 * H9 is Element of the carrier of E
(G,p,E,(P9 * H9),P) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
(G,p,E,H9,P) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
(G,p,E,P9,P) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
H1(P9) * H1(H9) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
G9 is set
dom (G,p,E,(P9 * H9),P) is Element of bool (G,p)
bool (G,p) is non empty set
dom (G,p,E,H9,P) is Element of bool (G,p)
T9 is Relation-like Function-like set
dom T9 is set
rng T9 is set
(G,p,E,H9,P) . G9 is set
rng (G,p,E,H9,P) is Element of bool (G,p)
T9 is Relation-like Function-like set
dom T9 is set
rng T9 is set
dom (G,p,E,P9,P) is Element of bool (G,p)
T9 is Relation-like Function-like set
dom T9 is set
rng T9 is set
T9 is Relation-like Function-like set
dom T9 is set
rng T9 is set
G9 is set
(G,p,E,H9,P) . G9 is set
K is Relation-like Function-like set
dom K is set
rng K is set
(G,p,E,(P9 * H9),P) . G9 is set
(E,G,P,(P9 * H9)) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
[:G,G:] is non empty set
bool [:G,G:] is non empty set
T9 is Element of (G,p)
(E,G,P,(P9 * H9)) .: T9 is Element of bool G
(E,G,P,H9) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
(E,G,P,P9) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
(E,G,P,P9) * (E,G,P,H9) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
((E,G,P,P9) * (E,G,P,H9)) .: T9 is Element of bool G
(E,G,P,H9) .: T9 is Element of bool G
(E,G,P,P9) .: ((E,G,P,H9) .: T9) is Element of bool G
K is Element of (G,p)
(E,G,P,P9) .: K is Element of bool G
(G,p,E,P9,P) . ((G,p,E,H9,P) . G9) is set
1_ E is Element of the carrier of E
(G,p,E,(1_ E),P) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
id (G,p) is Relation-like (G,p) -defined (G,p) -valued Function-like one-to-one total quasi_total Element of bool [:(G,p),(G,p):]
H9 is set
P9 is Element of (G,p)
P9 is Element of bool G
card P9 is epsilon-transitive epsilon-connected ordinal cardinal set
(G,p,E,(1_ E),P) . P9 is set
(E,G,P,(1_ E)) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
[:G,G:] is non empty set
bool [:G,G:] is non empty set
(E,G,P,(1_ E)) .: P9 is Element of bool G
(G,p,E,(1_ E),P) . H9 is set
id G is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total Element of bool [:G,G:]
(id G) .: P9 is Element of bool G
H9 is Relation-like Function-like set
dom H9 is set
rng H9 is set
P9 is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
P9 is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
P9 is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
H9 is Element of the carrier of E
P9 . H9 is Relation-like Function-like set
P9 . H9 is Relation-like Function-like set
P9 . H9 is Relation-like Function-like Element of Funcs ((G,p),(G,p))
(G,p,E,H9,P) is Relation-like (G,p) -defined (G,p) -valued Function-like total quasi_total Element of bool [:(G,p),(G,p):]
[:(G,p),(G,p):] is set
bool [:(G,p),(G,p):] is non empty set
P9 . H9 is Relation-like Function-like Element of Funcs ((G,p),(G,p))
G is non empty multMagma
the carrier of G is non empty set
E is non empty set
[: the carrier of G,E:] is non empty set
[:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
bool [:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
p is Element of the carrier of G
{ [b1,b2] where b1, b2 is Element of [: the carrier of G,E:] : ex b3, b4 being Element of the carrier of G ex b5 being Element of E st
( b4 = p * b3 & b1 = [b3,b5] & b2 = [b4,b5] ) } is set
P9 is set
H9 is set
[P9,H9] is set
{P9,H9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,H9},{P9}} is non empty finite V39() set
P9 is Element of [: the carrier of G,E:]
T is Element of [: the carrier of G,E:]
[P9,T] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
T9 is Element of the carrier of G
G9 is Element of the carrier of G
p * G9 is Element of the carrier of G
K is Element of E
[G9,K] is Element of [: the carrier of G,E:]
{G9,K} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,K},{G9}} is non empty finite V39() set
[T9,K] is Element of [: the carrier of G,E:]
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
T9 is Element of the carrier of G
G9 is Element of the carrier of G
p * G9 is Element of the carrier of G
K is Element of E
[G9,K] is Element of [: the carrier of G,E:]
{G9,K} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,K},{G9}} is non empty finite V39() set
[T9,K] is Element of [: the carrier of G,E:]
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{{P9,P9},{P9}} is non empty finite V39() set
P is Element of [: the carrier of G,E:]
T is Element of [: the carrier of G,E:]
[P,T] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{P,T} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,T},{P}} is non empty finite V39() set
Q is Element of the carrier of G
K is Element of the carrier of G
p * K is Element of the carrier of G
H99 is Element of E
[K,H99] is Element of [: the carrier of G,E:]
{K,H99} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,H99},{K}} is non empty finite V39() set
[Q,H99] is Element of [: the carrier of G,E:]
{Q,H99} is non empty finite set
{Q} is non empty trivial finite 1 -element set
{{Q,H99},{Q}} is non empty finite V39() set
Q is Element of the carrier of G
K is Element of the carrier of G
p * K is Element of the carrier of G
H99 is Element of E
[K,H99] is Element of [: the carrier of G,E:]
{K,H99} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,H99},{K}} is non empty finite V39() set
[Q,H99] is Element of [: the carrier of G,E:]
{Q,H99} is non empty finite set
{Q} is non empty trivial finite 1 -element set
{{Q,H99},{Q}} is non empty finite V39() set
P9 is set
H9 is Element of [: the carrier of G,E:]
P9 is Element of [: the carrier of G,E:]
[H9,P9] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{H9,P9} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,P9},{H9}} is non empty finite V39() set
P9 is set
T is set
G9 is set
T9 is set
[G9,T9] is set
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
H9 is set
P9 is set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
G9 is Element of the carrier of G
p * G9 is Element of the carrier of G
T is Element of E
[(p * G9),T] is Element of [: the carrier of G,E:]
{(p * G9),T} is non empty finite set
{(p * G9)} is non empty trivial finite 1 -element set
{{(p * G9),T},{(p * G9)}} is non empty finite V39() set
K is set
[G9,T] is Element of [: the carrier of G,E:]
{G9,T} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T},{G9}} is non empty finite V39() set
P is set
[H9,P] is set
{H9,P} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,P},{H9}} is non empty finite V39() set
P9 is Relation-like Function-like set
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{{H9,P9},{H9}} is non empty finite V39() set
P9 is Element of [: the carrier of G,E:]
T is Element of [: the carrier of G,E:]
[P9,T] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
dom P9 is set
H9 is set
rng P9 is set
P9 is set
[P9,H9] is set
{P9,H9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,H9},{P9}} is non empty finite V39() set
P9 is Element of [: the carrier of G,E:]
T is Element of [: the carrier of G,E:]
[P9,T] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
H9 is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
P9 is Element of [: the carrier of G,E:]
H9 . P9 is Element of [: the carrier of G,E:]
[P9,(H9 . P9)] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{P9,(H9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(H9 . P9)},{P9}} is non empty finite V39() set
T is Element of [: the carrier of G,E:]
G9 is Element of [: the carrier of G,E:]
[T,G9] is Element of [:[: the carrier of G,E:],[: the carrier of G,E:]:]
{T,G9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,G9},{T}} is non empty finite V39() set
K is Element of the carrier of G
T9 is Element of the carrier of G
p * T9 is Element of the carrier of G
P is Element of E
[T9,P] is Element of [: the carrier of G,E:]
{T9,P} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,P},{T9}} is non empty finite V39() set
[K,P] is Element of [: the carrier of G,E:]
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
K is Element of the carrier of G
T9 is Element of the carrier of G
p * T9 is Element of the carrier of G
P is Element of E
[T9,P] is Element of [: the carrier of G,E:]
{T9,P} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,P},{T9}} is non empty finite V39() set
[K,P] is Element of [: the carrier of G,E:]
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
P is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
P9 is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
P9 is Element of [: the carrier of G,E:]
P . P9 is set
P9 . P9 is set
P . P9 is Element of [: the carrier of G,E:]
H9 is Element of [: the carrier of G,E:]
P9 is Element of the carrier of G
P9 is Element of the carrier of G
p * P9 is Element of the carrier of G
T is Element of E
[P9,T] is Element of [: the carrier of G,E:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
[P9,T] is Element of [: the carrier of G,E:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
P9 . P9 is Element of [: the carrier of G,E:]
G9 is Element of [: the carrier of G,E:]
K is Element of the carrier of G
T9 is Element of the carrier of G
p * T9 is Element of the carrier of G
P is Element of E
[T9,P] is Element of [: the carrier of G,E:]
{T9,P} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,P},{T9}} is non empty finite V39() set
[K,P] is Element of [: the carrier of G,E:]
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
[: the carrier of G,p:] is non empty set
Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) is non empty functional set
[: the carrier of G,(Funcs ([: the carrier of G,p:],[: the carrier of G,p:])):] is non empty set
bool [: the carrier of G,(Funcs ([: the carrier of G,p:],[: the carrier of G,p:])):] is non empty set
[:[: the carrier of G,p:],[: the carrier of G,p:]:] is non empty set
bool [:[: the carrier of G,p:],[: the carrier of G,p:]:] is non empty set
P is Element of the carrier of G
P9 is Element of the carrier of G
P * P9 is Element of the carrier of G
(G,(P * P9),p) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
(G,P9,p) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
(G,P,p) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
H1(P) * H1(P9) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) is non empty functional FUNCTION_DOMAIN of [: the carrier of G,p:],[: the carrier of G,p:]
P9 is set
dom (G,(P * P9),p) is Relation-like the carrier of G -defined p -valued Element of bool [: the carrier of G,p:]
bool [: the carrier of G,p:] is non empty set
T is Element of [: the carrier of G,p:]
(G,P9,p) . T is Element of [: the carrier of G,p:]
T9 is Element of [: the carrier of G,p:]
P is Element of the carrier of G
K is Element of the carrier of G
P9 * K is Element of the carrier of G
T is Element of p
[K,T] is Element of [: the carrier of G,p:]
{K,T} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,T},{K}} is non empty finite V39() set
[P,T] is Element of [: the carrier of G,p:]
{P,T} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,T},{P}} is non empty finite V39() set
(G,P9,p) . P9 is set
rng (G,P9,p) is Relation-like the carrier of G -defined p -valued Element of bool [: the carrier of G,p:]
K is Relation-like Function-like set
dom K is set
rng K is set
K is Element of [: the carrier of G,p:]
(G,P,p) . K is Element of [: the carrier of G,p:]
Q is Element of [: the carrier of G,p:]
Q9 is Element of the carrier of G
H99 is Element of the carrier of G
P * H99 is Element of the carrier of G
N is Element of p
[H99,N] is Element of [: the carrier of G,p:]
{H99,N} is non empty finite set
{H99} is non empty trivial finite 1 -element set
{{H99,N},{H99}} is non empty finite V39() set
[Q9,N] is Element of [: the carrier of G,p:]
{Q9,N} is non empty finite set
{Q9} is non empty trivial finite 1 -element set
{{Q9,N},{Q9}} is non empty finite V39() set
G9 is Element of [: the carrier of G,p:]
(G,(P * P9),p) . G9 is Element of [: the carrier of G,p:]
N is Element of [: the carrier of G,p:]
P99 is Element of the carrier of G
Q99 is Element of the carrier of G
(P * P9) * Q99 is Element of the carrier of G
n is Element of p
[Q99,n] is Element of [: the carrier of G,p:]
{Q99,n} is non empty finite set
{Q99} is non empty trivial finite 1 -element set
{{Q99,n},{Q99}} is non empty finite V39() set
[P99,n] is Element of [: the carrier of G,p:]
{P99,n} is non empty finite set
{P99} is non empty trivial finite 1 -element set
{{P99,n},{P99}} is non empty finite V39() set
(P * P9) * K is Element of the carrier of G
P * (P9 * K) is Element of the carrier of G
(G,(P * P9),p) . P9 is set
(G,P,p) . ((G,P9,p) . P9) is set
P9 is set
dom (G,P9,p) is Relation-like the carrier of G -defined p -valued Element of bool [: the carrier of G,p:]
T is Relation-like Function-like set
dom T is set
rng T is set
(G,P9,p) . P9 is set
T is Relation-like Function-like set
dom T is set
rng T is set
dom (G,P,p) is Relation-like the carrier of G -defined p -valued Element of bool [: the carrier of G,p:]
T is Relation-like Function-like set
dom T is set
rng T is set
T is Relation-like Function-like set
dom T is set
rng T is set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G),p) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
id [: the carrier of G,p:] is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like one-to-one total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
P9 is set
P9 is Element of [: the carrier of G,p:]
(G,(1_ G),p) . P9 is Element of [: the carrier of G,p:]
(G,(1_ G),p) . P9 is set
H9 is Element of [: the carrier of G,p:]
P9 is Element of the carrier of G
P9 is Element of the carrier of G
(1_ G) * P9 is Element of the carrier of G
T is Element of p
[P9,T] is Element of [: the carrier of G,p:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
[P9,T] is Element of [: the carrier of G,p:]
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) is non empty functional FUNCTION_DOMAIN of [: the carrier of G,p:],[: the carrier of G,p:]
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P is Relation-like the carrier of G -defined Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) -valued non empty Function-like total quasi_total (G,[: the carrier of G,p:]) Element of bool [: the carrier of G,(Funcs ([: the carrier of G,p:],[: the carrier of G,p:])):]
E is Relation-like the carrier of G -defined Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) -valued non empty Function-like total quasi_total (G,[: the carrier of G,p:]) Element of bool [: the carrier of G,(Funcs ([: the carrier of G,p:],[: the carrier of G,p:])):]
P is Relation-like the carrier of G -defined Funcs ([: the carrier of G,p:],[: the carrier of G,p:]) -valued non empty Function-like total quasi_total (G,[: the carrier of G,p:]) Element of bool [: the carrier of G,(Funcs ([: the carrier of G,p:],[: the carrier of G,p:])):]
P9 is Element of the carrier of G
E . P9 is Relation-like Function-like set
P . P9 is Relation-like Function-like set
E . P9 is Relation-like Function-like Element of Funcs ([: the carrier of G,p:],[: the carrier of G,p:])
(G,P9,p) is Relation-like [: the carrier of G,p:] -defined [: the carrier of G,p:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,p:],[: the carrier of G,p:]:]
[:[: the carrier of G,p:],[: the carrier of G,p:]:] is non empty set
bool [:[: the carrier of G,p:],[: the carrier of G,p:]:] is non empty set
P . P9 is Relation-like Function-like Element of Funcs ([: the carrier of G,p:],[: the carrier of G,p:])
G is non empty unital Group-like associative multMagma
p is non empty unital Group-like associative Subgroup of G
the carrier of p is non empty set
E is non empty unital Group-like associative Subgroup of G
Left_Cosets E is Element of bool (bool the carrier of G)
the carrier of G is non empty set
bool the carrier of G is non empty set
bool (bool the carrier of G) is non empty set
[:(Left_Cosets E),(Left_Cosets E):] is set
bool [:(Left_Cosets E),(Left_Cosets E):] is non empty set
P is Element of the carrier of p
{ [b1,b2] where b1, b2 is Element of Left_Cosets E : ex b3, b4 being Element of bool the carrier of G ex b5 being Element of the carrier of G st
( b4 = b5 * b3 & b3 = b1 & b4 = b2 & b5 = P ) } is set
P9 is set
H9 is set
[P9,H9] is set
{P9,H9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,H9},{P9}} is non empty finite V39() set
P9 is Element of Left_Cosets E
T is Element of Left_Cosets E
[P9,T] is set
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{{P9,P9},{P9}} is non empty finite V39() set
G9 is Element of Left_Cosets E
T9 is Element of Left_Cosets E
[G9,T9] is set
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
P is Element of bool the carrier of G
T is Element of the carrier of G
K is Element of bool the carrier of G
T * K is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in K ) } is set
Q is Element of bool the carrier of G
H99 is Element of the carrier of G
K is Element of bool the carrier of G
H99 * K is Element of bool the carrier of G
{H99} is non empty trivial finite 1 -element Element of bool the carrier of G
{H99} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H99} & b2 in K ) } is set
P9 is set
H9 is Element of Left_Cosets E
P9 is Element of Left_Cosets E
[H9,P9] is set
{H9,P9} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,P9},{H9}} is non empty finite V39() set
P9 is set
T is set
G9 is set
T9 is set
[G9,T9] is set
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
H9 is set
P9 is Element of the carrier of G
P9 * E is Element of bool the carrier of G
carr E is Element of bool the carrier of G
the carrier of E is non empty set
P9 * (carr E) is Element of bool the carrier of G
{P9} is non empty trivial finite 1 -element Element of bool the carrier of G
{P9} * (carr E) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {P9} & b2 in carr E ) } is set
P9 is Element of the carrier of G
P9 * (P9 * E) is Element of bool the carrier of G
{P9} is non empty trivial finite 1 -element Element of bool the carrier of G
{P9} * (P9 * E) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {P9} & b2 in P9 * E ) } is set
G9 is set
P9 * P9 is Element of the carrier of G
(P9 * P9) * E is Element of bool the carrier of G
(P9 * P9) * (carr E) is Element of bool the carrier of G
{(P9 * P9)} is non empty trivial finite 1 -element Element of bool the carrier of G
{(P9 * P9)} * (carr E) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {(P9 * P9)} & b2 in carr E ) } is set
T9 is set
T is Element of Left_Cosets E
K is Element of Left_Cosets E
[H9,T9] is set
{H9,T9} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,T9},{H9}} is non empty finite V39() set
P9 is Relation-like Function-like set
T is Element of bool the carrier of G
P is Element of bool the carrier of G
P9 * P is Element of bool the carrier of G
{P9} * P is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {P9} & b2 in P ) } is set
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{{H9,P9},{H9}} is non empty finite V39() set
P9 is Element of Left_Cosets E
T is Element of Left_Cosets E
[P9,T] is set
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
dom P9 is set
H9 is set
rng P9 is set
P9 is set
P9 . P9 is set
[P9,H9] is set
{P9,H9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,H9},{P9}} is non empty finite V39() set
P9 is Element of Left_Cosets E
T is Element of Left_Cosets E
[P9,T] is set
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
H9 is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
P9 is Element of Left_Cosets E
H9 . P9 is set
[P9,(H9 . P9)] is set
{P9,(H9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(H9 . P9)},{P9}} is non empty finite V39() set
T is Element of Left_Cosets E
G9 is Element of Left_Cosets E
[T,G9] is set
{T,G9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,G9},{T}} is non empty finite V39() set
P is Element of bool the carrier of G
T is Element of the carrier of G
K is Element of bool the carrier of G
T * K is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in K ) } is set
P is Element of bool the carrier of G
T is Element of the carrier of G
K is Element of bool the carrier of G
T * K is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in K ) } is set
T9 is Element of Left_Cosets E
Q is Element of bool the carrier of G
H99 is Element of the carrier of G
K is Element of bool the carrier of G
H99 * K is Element of bool the carrier of G
{H99} is non empty trivial finite 1 -element Element of bool the carrier of G
{H99} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H99} & b2 in K ) } is set
P9 is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
P9 is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
H9 is Element of Left_Cosets E
P9 . H9 is set
P9 . H9 is set
P9 is Element of Left_Cosets E
T is Element of bool the carrier of G
G9 is Element of the carrier of G
P9 is Element of bool the carrier of G
G9 * P9 is Element of bool the carrier of G
{G9} is non empty trivial finite 1 -element Element of bool the carrier of G
{G9} * P9 is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {G9} & b2 in P9 ) } is set
T9 is Element of Left_Cosets E
P is Element of bool the carrier of G
T is Element of the carrier of G
K is Element of bool the carrier of G
T * K is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in K ) } is set
G is non empty unital Group-like associative multMagma
p is non empty unital Group-like associative Subgroup of G
the carrier of p is non empty set
E is non empty unital Group-like associative Subgroup of G
Left_Cosets E is Element of bool (bool the carrier of G)
the carrier of G is non empty set
bool the carrier of G is non empty set
bool (bool the carrier of G) is non empty set
Funcs ((Left_Cosets E),(Left_Cosets E)) is non empty functional set
[: the carrier of p,(Funcs ((Left_Cosets E),(Left_Cosets E))):] is non empty set
bool [: the carrier of p,(Funcs ((Left_Cosets E),(Left_Cosets E))):] is non empty set
[:(Left_Cosets E),(Left_Cosets E):] is set
bool [:(Left_Cosets E),(Left_Cosets E):] is non empty set
P is Element of the carrier of p
P9 is Element of the carrier of p
P * P9 is Element of the carrier of p
(G,p,E,(P * P9)) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
(G,p,E,P9) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
(G,p,E,P) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
H1(P) * H1(P9) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
P9 is set
dom (G,p,E,(P * P9)) is Element of bool (Left_Cosets E)
bool (Left_Cosets E) is non empty set
(G,p,E,P9) . P9 is set
rng (G,p,E,P9) is Element of bool (Left_Cosets E)
G9 is Relation-like Function-like set
dom G9 is set
rng G9 is set
G9 is Element of Left_Cosets E
(G,p,E,P) . G9 is set
T9 is Element of Left_Cosets E
P is Element of bool the carrier of G
T is Element of the carrier of G
K is Element of bool the carrier of G
T * K is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * K is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in K ) } is set
T is Element of Left_Cosets E
(G,p,E,P9) . T is set
Q is Element of Left_Cosets E
Q9 is Element of bool the carrier of G
N is Element of the carrier of G
H99 is Element of bool the carrier of G
N * H99 is Element of bool the carrier of G
{N} is non empty trivial finite 1 -element Element of bool the carrier of G
{N} * H99 is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {N} & b2 in H99 ) } is set
K is Element of Left_Cosets E
(G,p,E,(P * P9)) . K is set
N is Element of Left_Cosets E
P99 is Element of bool the carrier of G
n is Element of the carrier of G
Q99 is Element of bool the carrier of G
n * Q99 is Element of bool the carrier of G
{n} is non empty trivial finite 1 -element Element of bool the carrier of G
{n} * Q99 is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {n} & b2 in Q99 ) } is set
T * N is Element of the carrier of G
(G,p,E,(P * P9)) . P9 is set
(G,p,E,P) . ((G,p,E,P9) . P9) is set
P9 is set
dom (G,p,E,P9) is Element of bool (Left_Cosets E)
T is Relation-like Function-like set
dom T is set
rng T is set
(G,p,E,P9) . P9 is set
T is Relation-like Function-like set
dom T is set
rng T is set
dom (G,p,E,P) is Element of bool (Left_Cosets E)
T is Relation-like Function-like set
dom T is set
rng T is set
T is Relation-like Function-like set
dom T is set
rng T is set
1_ p is non being_of_order_0 Element of the carrier of p
(G,p,E,(1_ p)) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
id (Left_Cosets E) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like one-to-one total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
P9 is set
P9 is Element of Left_Cosets E
(G,p,E,(1_ p)) . P9 is set
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,E,(1_ p)) . P9 is set
H9 is Element of Left_Cosets E
P9 is Element of bool the carrier of G
T is Element of the carrier of G
P9 is Element of bool the carrier of G
T * P9 is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * P9 is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in P9 ) } is set
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P is Relation-like the carrier of p -defined Funcs ((Left_Cosets E),(Left_Cosets E)) -valued non empty Function-like total quasi_total (p, Left_Cosets E) Element of bool [: the carrier of p,(Funcs ((Left_Cosets E),(Left_Cosets E))):]
P is Relation-like the carrier of p -defined Funcs ((Left_Cosets E),(Left_Cosets E)) -valued non empty Function-like total quasi_total (p, Left_Cosets E) Element of bool [: the carrier of p,(Funcs ((Left_Cosets E),(Left_Cosets E))):]
P9 is Relation-like the carrier of p -defined Funcs ((Left_Cosets E),(Left_Cosets E)) -valued non empty Function-like total quasi_total (p, Left_Cosets E) Element of bool [: the carrier of p,(Funcs ((Left_Cosets E),(Left_Cosets E))):]
P9 is Element of the carrier of p
P . P9 is Relation-like Function-like set
P9 . P9 is Relation-like Function-like set
P . P9 is Relation-like Function-like Element of Funcs ((Left_Cosets E),(Left_Cosets E))
(G,p,E,P9) is Relation-like Left_Cosets E -defined Left_Cosets E -valued Function-like total quasi_total Element of bool [:(Left_Cosets E),(Left_Cosets E):]
[:(Left_Cosets E),(Left_Cosets E):] is set
bool [:(Left_Cosets E),(Left_Cosets E):] is non empty set
P9 . P9 is Relation-like Function-like Element of Funcs ((Left_Cosets E),(Left_Cosets E))
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
bool p is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
P is Element of bool p
{ b1 where b1 is Element of the carrier of G : (G,p,E,b1) .: P = P } is set
P9 is set
H9 is Element of the carrier of G
(G,p,E,H9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,E,H9) .: P is Element of bool p
bool the carrier of G is non empty set
P9 is Element of bool the carrier of G
H9 is Element of the carrier of G
P9 is Element of the carrier of G
H9 * P9 is Element of the carrier of G
(G,p,E,(H9 * P9)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,E,(H9 * P9)) .: P is Element of bool p
(G,p,E,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,H9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,H9) * (G,p,E,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,E,H9) * (G,p,E,P9)) .: P is Element of bool p
P9 is Element of the carrier of G
(G,p,E,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,P9) .: P is Element of bool p
T is Element of the carrier of G
(G,p,E,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,T) .: P is Element of bool p
id p is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(id p) .: P is Element of bool p
H9 is Element of the carrier of G
H9 " is Element of the carrier of G
(G,p,E,(H9 ")) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,(H9 ")) .: P is Element of bool p
(G,p,E,H9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,(H9 ")) * (G,p,E,H9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,E,(H9 ")) * (G,p,E,H9)) .: P is Element of bool p
(H9 ") * H9 is Element of the carrier of G
(G,p,E,((H9 ") * H9)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,((H9 ") * H9)) .: P is Element of bool p
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,E,(1_ G)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,(1_ G)) .: P is Element of bool p
P9 is Element of the carrier of G
(G,p,E,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,P9) .: P is Element of bool p
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,E,(1_ G)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,E,(1_ G)) .: P is Element of bool p
P9 is non empty strict unital Group-like associative Subgroup of G
the carrier of P9 is non empty set
P9 is non empty strict unital Group-like associative Subgroup of G
the carrier of P9 is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
P is Element of p
{P} is non empty trivial finite 1 -element Element of bool p
bool p is non empty set
(G,p,E,{P}) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital multMagma
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
G is non empty unital multMagma
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
{ b1 where b1 is Element of p : (G,p,E,b1) } is set
bool p is non empty set
{} p is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real V18() Function-like functional finite V39() cardinal {} -element FinSequence-membered ext-real non positive non negative Element of bool p
P9 is Element of bool p
P9 is set
H9 is Element of p
H9 is Element of p
P9 is Element of p
H9 is Element of p
G is non empty unital multMagma
the carrier of G is non empty set
p is set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
G is non empty unital multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
P is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
id p is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(id p) . E is Element of p
1_ G is Element of the carrier of G
(G,p,P,(1_ G)) is Relation-like p -defined p -valued non empty Function-like total quasi_total Element of bool [:p,p:]
(G,p,P,(1_ G)) . E is Element of p
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
P is Element of p
P9 is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
P9 is Element of the carrier of G
(G,p,P9,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P9,P9) . E is Element of p
dom (G,p,P9,P9) is Element of bool p
bool p is non empty set
P9 " is Element of the carrier of G
(G,p,P9,(P9 ")) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P9,(P9 ")) . P is Element of p
(G,p,P9,(P9 ")) * (G,p,P9,P9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,P9,(P9 ")) * (G,p,P9,P9)) . E is Element of p
(P9 ") * P9 is Element of the carrier of G
(G,p,P9,((P9 ") * P9)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P9,((P9 ") * P9)) . E is Element of p
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,P9,(1_ G)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P9,(1_ G)) . E is Element of p
id p is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(id p) . E is Element of p
G is non empty unital multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
P is Element of p
P9 is Element of p
P9 is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
H9 is Element of the carrier of G
(G,p,P9,H9) is Relation-like p -defined p -valued non empty Function-like total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P9,H9) . E is Element of p
P9 is Element of the carrier of G
(G,p,P9,P9) is Relation-like p -defined p -valued non empty Function-like total quasi_total Element of bool [:p,p:]
(G,p,P9,P9) . P is Element of p
dom (G,p,P9,H9) is Element of bool p
bool p is non empty set
(G,p,P9,P9) * (G,p,P9,H9) is Relation-like p -defined p -valued non empty Function-like total quasi_total Element of bool [:p,p:]
((G,p,P9,P9) * (G,p,P9,H9)) . E is Element of p
P9 * H9 is Element of the carrier of G
(G,p,P9,(P9 * H9)) is Relation-like p -defined p -valued non empty Function-like total quasi_total Element of bool [:p,p:]
(G,p,P9,(P9 * H9)) . E is Element of p
G is non empty unital multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
P is Element of p
{ b1 where b1 is Element of p : (G,p,E,P,b1) } is set
bool p is non empty set
P9 is Element of bool p
H9 is set
P9 is Element of p
P9 is Element of p
P9 is Element of p
P9 is Element of p
p is non empty set
G is non empty unital multMagma
the carrier of G is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
P is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
E is Element of p
(G,p,P,E) is Element of bool p
bool p is non empty set
{ b1 where b1 is Element of p : (G,p,P,E,b1) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
P is Element of p
P9 is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
(G,p,P9,E) is non empty Element of bool p
bool p is non empty set
{ b1 where b1 is Element of p : (G,p,P9,E,b1) } is set
(G,p,P9,P) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,P9,P,b1) } is set
(G,p,P9,E) /\ (G,p,P9,P) is Element of bool p
P9 is set
H9 is Element of p
P9 is Element of p
P9 is set
T is Element of p
T is Element of p
G is non empty unital multMagma
the carrier of G is non empty set
p is non empty finite set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
{E} is non empty trivial finite 1 -element Element of bool p
bool p is non empty finite V39() set
P is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
(G,p,P,E) is non empty finite Element of bool p
{ b1 where b1 is Element of p : (G,p,P,E,b1) } is set
P9 is set
H9 is set
P9 is set
P9 is set
H9 is Element of p
P9 is Element of the carrier of G
(G,p,P,P9) is Relation-like p -defined p -valued non empty Function-like total quasi_total finite Element of bool [:p,p:]
[:p,p:] is non empty finite set
bool [:p,p:] is non empty finite V39() set
(G,p,P,P9) . E is Element of p
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is Element of p
P is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
(G,p,P,E) is non empty Element of bool p
bool p is non empty set
{ b1 where b1 is Element of p : (G,p,P,E,b1) } is set
card (G,p,P,E) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(G,p,P,E) is non empty strict unital Group-like associative Subgroup of G
{E} is non empty trivial finite 1 -element Element of bool p
(G,p,P,{E}) is non empty strict unital Group-like associative Subgroup of G
Index (G,p,P,E) is epsilon-transitive epsilon-connected ordinal cardinal set
Left_Cosets (G,p,P,E) is Element of bool (bool the carrier of G)
bool the carrier of G is non empty set
bool (bool the carrier of G) is non empty set
card (Left_Cosets (G,p,P,E)) is epsilon-transitive epsilon-connected ordinal cardinal set
{ [b1,b2] where b1 is Element of p, b2 is Element of bool the carrier of G : ex b3 being Element of the carrier of G st
( b1 = (G,p,P,b3) . E & b2 = b3 * (G,p,P,E) ) } is set
P9 is set
P9 is Element of p
T is Element of bool the carrier of G
[P9,T] is Element of [:p,(bool the carrier of G):]
[:p,(bool the carrier of G):] is non empty set
{P9,T} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,T},{P9}} is non empty finite V39() set
G9 is set
T9 is set
K is set
P is set
[K,P] is set
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
P9 is set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
G9 is Element of p
T9 is Element of bool the carrier of G
[G9,T9] is Element of [:p,(bool the carrier of G):]
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
T is set
[P9,T] is set
{P9,T} is non empty finite set
{{P9,T},{P9}} is non empty finite V39() set
K is Element of p
P is Element of bool the carrier of G
[K,P] is Element of [:p,(bool the carrier of G):]
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
T is Element of the carrier of G
(G,p,P,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P,T) . E is Element of p
T * (G,p,P,E) is Element of bool the carrier of G
carr (G,p,P,E) is Element of bool the carrier of G
the carrier of (G,p,P,E) is non empty set
T * (carr (G,p,P,E)) is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in carr (G,p,P,E) ) } is set
T is Element of the carrier of G
(G,p,P,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P,T) . E is Element of p
T * (G,p,P,E) is Element of bool the carrier of G
carr (G,p,P,E) is Element of bool the carrier of G
the carrier of (G,p,P,E) is non empty set
T * (carr (G,p,P,E)) is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in carr (G,p,P,E) ) } is set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
dom (G,p,P,T) is Element of bool p
dom (G,p,P,K) is Element of bool p
Im ((G,p,P,T),E) is set
{E} is non empty trivial finite 1 -element set
(G,p,P,T) .: {E} is finite set
{((G,p,P,K) . E)} is non empty trivial finite 1 -element Element of bool p
Im ((G,p,P,K),E) is set
(G,p,P,K) .: {E} is finite set
K " is Element of the carrier of G
(K ") * T is Element of the carrier of G
H9 is Element of bool p
(G,p,P,H9) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,p,P,H9) is non empty set
{ b1 where b1 is Element of the carrier of G : (G,p,P,b1) .: H9 = H9 } is set
H99 is Element of the carrier of G
(G,p,P,H99) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,H99) .: H9 is Element of bool p
(G,p,P,(K ")) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,(K ")) * (G,p,P,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,P,(K ")) * (G,p,P,T)) .: H9 is Element of bool p
(G,p,P,T) .: H9 is Element of bool p
(G,p,P,(K ")) .: ((G,p,P,T) .: H9) is Element of bool p
(G,p,P,(K ")) * (G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,P,(K ")) * (G,p,P,K)) .: H9 is Element of bool p
(K ") * K is Element of the carrier of G
(G,p,P,((K ") * K)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,((K ") * K)) .: H9 is Element of bool p
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,P,(1_ G)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,(1_ G)) .: H9 is Element of bool p
id p is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(id p) .: H9 is Element of bool p
P9 is Relation-like Function-like set
P9 is set
T is Element of bool the carrier of G
G9 is Element of the carrier of G
G9 * (G,p,P,E) is Element of bool the carrier of G
G9 * (carr (G,p,P,E)) is Element of bool the carrier of G
{G9} is non empty trivial finite 1 -element Element of bool the carrier of G
{G9} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {G9} & b2 in carr (G,p,P,E) ) } is set
(G,p,P,G9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,G9) . E is Element of p
T9 is set
K is set
[K,P9] is set
{K,P9} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P9},{K}} is non empty finite V39() set
T is set
[T,P9] is set
{T,P9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,P9},{T}} is non empty finite V39() set
G9 is Element of p
T9 is Element of bool the carrier of G
[G9,T9] is Element of [:p,(bool the carrier of G):]
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
rng P9 is set
P9 is set
dom P9 is set
P9 . P9 is set
[P9,(P9 . P9)] is set
{P9,(P9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(P9 . P9)},{P9}} is non empty finite V39() set
G9 is Element of p
T9 is Element of bool the carrier of G
[G9,T9] is Element of [:p,(bool the carrier of G):]
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
T is set
P9 . T is set
[T,(P9 . T)] is set
{T,(P9 . T)} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,(P9 . T)},{T}} is non empty finite V39() set
K is Element of p
P is Element of bool the carrier of G
[K,P] is Element of [:p,(bool the carrier of G):]
{K,P} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,P},{K}} is non empty finite V39() set
T is Element of the carrier of G
(G,p,P,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,T) . E is Element of p
T * (G,p,P,E) is Element of bool the carrier of G
T * (carr (G,p,P,E)) is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in carr (G,p,P,E) ) } is set
T is Element of the carrier of G
(G,p,P,T) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,T) . E is Element of p
T * (G,p,P,E) is Element of bool the carrier of G
T * (carr (G,p,P,E)) is Element of bool the carrier of G
{T} is non empty trivial finite 1 -element Element of bool the carrier of G
{T} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {T} & b2 in carr (G,p,P,E) ) } is set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
T " is Element of the carrier of G
(T ") * K is Element of the carrier of G
(G,p,P,K) .: H9 is Element of bool p
(id p) .: ((G,p,P,K) .: H9) is Element of bool p
(G,p,P,(1_ G)) .: ((G,p,P,K) .: H9) is Element of bool p
T * (T ") is Element of the carrier of G
(G,p,P,(T * (T "))) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,(T * (T "))) .: ((G,p,P,K) .: H9) is Element of bool p
(G,p,P,(T * (T "))) * (G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,P,(T * (T "))) * (G,p,P,K)) .: H9 is Element of bool p
(T * (T ")) * K is Element of the carrier of G
(G,p,P,((T * (T ")) * K)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,((T * (T ")) * K)) .: H9 is Element of bool p
T * ((T ") * K) is Element of the carrier of G
(G,p,P,(T * ((T ") * K))) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,(T * ((T ") * K))) .: H9 is Element of bool p
(G,p,P,((T ") * K)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,T) * (G,p,P,((T ") * K)) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
((G,p,P,T) * (G,p,P,((T ") * K))) .: H9 is Element of bool p
(G,p,P,T) .: H9 is Element of bool p
H99 is Element of the carrier of G
(G,p,P,H99) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,H99) .: H9 is Element of bool p
dom (G,p,P,T) is Element of bool p
Im ((G,p,P,K),E) is set
(G,p,P,K) .: {E} is finite set
Im ((G,p,P,T),E) is set
(G,p,P,T) .: {E} is finite set
dom (G,p,P,K) is Element of bool p
{((G,p,P,T) . E)} is non empty trivial finite 1 -element Element of bool p
{((G,p,P,K) . E)} is non empty trivial finite 1 -element Element of bool p
P9 is set
T is Element of p
G9 is Element of the carrier of G
(G,p,P,G9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,G9) . E is Element of p
G9 * (G,p,P,E) is Element of bool the carrier of G
G9 * (carr (G,p,P,E)) is Element of bool the carrier of G
{G9} is non empty trivial finite 1 -element Element of bool the carrier of G
{G9} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {G9} & b2 in carr (G,p,P,E) ) } is set
T9 is set
K is set
[P9,K] is set
{P9,K} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,K},{P9}} is non empty finite V39() set
T is set
[P9,T] is set
{P9,T} is non empty finite set
{{P9,T},{P9}} is non empty finite V39() set
G9 is Element of p
T9 is Element of bool the carrier of G
[G9,T9] is Element of [:p,(bool the carrier of G):]
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
K is Element of the carrier of G
(G,p,P,K) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
(G,p,P,K) . E is Element of p
K * (G,p,P,E) is Element of bool the carrier of G
K * (carr (G,p,P,E)) is Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr (G,p,P,E)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr (G,p,P,E) ) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
bool p is non empty set
E is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
{ b1 where b1 is Element of bool p : ex b2 being Element of p st b1 = (G,p,E,b2) } is set
P9 is set
P9 is Element of bool p
H9 is Element of p
(G,p,E,H9) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,E,H9,b1) } is set
bool (bool p) is non empty set
P9 is Element of bool (bool p)
P9 is set
H9 is Element of p
(G,p,E,H9) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,E,H9,b1) } is set
P9 is set
P9 is set
H9 is set
union P9 is Element of bool p
P9 is Element of bool p
H9 is Element of bool p
P9 is Element of p
(G,p,E,P9) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,E,P9,b1) } is set
H9 is Element of bool p
P9 is Element of bool p
P9 is Element of p
(G,p,E,P9) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,E,P9,b1) } is set
T is Element of bool p
G9 is Element of p
(G,p,E,G9) is non empty Element of bool p
{ b1 where b1 is Element of p : (G,p,E,G9,b1) } is set
G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
INT.Group G is non empty finite strict unital Group-like associative commutative cyclic multMagma
card (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of (INT.Group G) is non empty finite set
card the carrier of (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
Segm G is non empty V87() Element of bool NAT
addint G is Relation-like [:(Segm G),(Segm G):] -defined Segm G -valued non empty Function-like total quasi_total V72() V73() V74() V75() Element of bool [:[:(Segm G),(Segm G):],(Segm G):]
[:(Segm G),(Segm G):] is non empty V75() set
[:[:(Segm G),(Segm G):],(Segm G):] is non empty V75() set
bool [:[:(Segm G),(Segm G):],(Segm G):] is non empty set
multMagma(# (Segm G),(addint G) #) is strict multMagma
G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
INT.Group G is non empty finite strict unital Group-like associative commutative cyclic multMagma
card (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
the carrier of (INT.Group G) is non empty finite set
card the carrier of (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
G |^ 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
INT.Group G is non empty finite strict unital Group-like associative commutative cyclic (G) multMagma
G is non empty finite set
Funcs (G,G) is non empty functional set
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
p is non empty finite unital Group-like associative multMagma
the carrier of p is non empty finite set
[: the carrier of p,(Funcs (G,G)):] is non empty set
bool [: the carrier of p,(Funcs (G,G)):] is non empty set
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
(card G) mod E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P is Relation-like the carrier of p -defined Funcs (G,G) -valued non empty Function-like total quasi_total finite (p,G) Element of bool [: the carrier of p,(Funcs (G,G)):]
(p,G,P) is finite Element of bool G
bool G is non empty finite V39() set
card (p,G,P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card (p,G,P)) mod E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
{ b1 where b1 is finite Element of bool G : ( card b1 = 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } is set
{ b1 where b1 is finite Element of bool G : ( not card b1 <= 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } is set
{ b1 where b1 is finite Element of bool G : ( card b1 = 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } \/ { b1 where b1 is finite Element of bool G : ( not card b1 <= 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } is set
P9 is set
T is Element of G
(p,G,P,T) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T,b1) } is set
G9 is set
P is Element of G
T is set
(p,G,P,P) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,P,b1) } is set
{ b1 where b1 is Element of G : (p,G,P,b1) } is set
K is Element of G
T9 is Element of G
K is set
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
P9 is Relation-like Function-like set
dom P9 is set
T is set
G9 is finite Element of bool G
card G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
K is set
{K} is non empty trivial finite 1 -element set
card {K} is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
P is set
{P} is non empty trivial finite 1 -element set
K is Element of the carrier of p
(p,G,P,K) is Relation-like G -defined G -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:G,G:]
[:G,G:] is non empty finite set
bool [:G,G:] is non empty finite V39() set
(p,G,P,K) . T9 is Element of G
T is set
{ b1 where b1 is Element of G : (p,G,P,b1) } is set
P9 . T is set
[T,T] is set
{T,T} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,T},{T}} is non empty finite V39() set
K is Element of G
Q is finite Element of bool G
(p,G,P,K) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,K,b1) } is set
G9 is set
[G9,T] is set
{G9,T} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T},{G9}} is non empty finite V39() set
P9 . G9 is set
T9 is Element of G
K is finite Element of bool G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
{T9} is non empty trivial finite 1 -element Element of bool G
card K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
rng P9 is set
T is set
P9 . T is set
T9 is Element of G
K is finite Element of bool G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
G9 is set
P9 . G9 is set
P is Element of G
T is finite Element of bool G
(p,G,P,P) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,P,b1) } is set
{T9} is non empty trivial finite 1 -element Element of bool G
{P} is non empty trivial finite 1 -element Element of bool G
T is set
(p,G,P) is finite V39() a_partition of G
{ b1 where b1 is Element of bool G : ex b2 being Element of G st b1 = (p,G,P,b2) } is set
G9 is finite Element of bool G
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
card G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card G9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
G9 is finite Element of bool G
card G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
G9 is finite Element of bool G
card G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T9 is Element of G
(p,G,P,T9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,T9,b1) } is set
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng T is finite set
G9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng G9 is finite set
T ^ G9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (T ^ G9) is finite set
K is finite V39() a_partition of G
{ b1 where b1 is finite Element of bool G : ( card b1 = 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } /\ { b1 where b1 is finite Element of bool G : ( not card b1 <= 1 & ex b2 being Element of G st b1 = (p,G,P,b2) ) } is set
P is set
T is finite Element of bool G
card T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
K is Element of G
(p,G,P,K) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,K,b1) } is set
Q is finite Element of bool G
card Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H99 is Element of G
(p,G,P,H99) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,H99,b1) } is set
len T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom T is finite Element of bool NAT
rng T is finite set
K is set
Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
T . Q is set
dom T is finite Element of bool NAT
T . Q is set
card (T . Q) is epsilon-transitive epsilon-connected ordinal cardinal set
H99 is finite Element of bool G
card H99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q9 is Element of G
(p,G,P,Q9) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,Q9,b1) } is set
len G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom Q is finite Element of bool NAT
rng Q is finite set
H99 is set
Q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
Q . Q9 is set
dom G9 is finite Element of bool NAT
G9 . Q9 is set
card (G9 . Q9) is epsilon-transitive epsilon-connected ordinal cardinal set
N is finite Element of bool G
card N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N is Element of G
(p,G,P,N) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,N,b1) } is set
K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
H99 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
K ^ H99 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
N is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
dom N is finite Element of bool NAT
P is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of K
N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N . N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P . N is set
card (P . N) is epsilon-transitive epsilon-connected ordinal cardinal set
dom K is finite Element of bool NAT
dom T is finite Element of bool NAT
K . N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
T . N is set
card (T . N) is epsilon-transitive epsilon-connected ordinal cardinal set
dom H99 is finite Element of bool NAT
len K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(len K) + Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(len K) + Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom G9 is finite Element of bool NAT
H99 . Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G9 . Q99 is set
card (G9 . Q99) is epsilon-transitive epsilon-connected ordinal cardinal set
dom K is finite Element of bool NAT
dom H99 is finite Element of bool NAT
len K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom H99 is finite Element of bool NAT
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H99 /. N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E |^ P99 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
dom G9 is finite Element of bool NAT
G9 . N is set
n9 is finite Element of bool G
card n9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
y is Element of G
(p,G,P,y) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,y,b1) } is set
y is Element of G
(p,G,P,y) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,y,b1) } is set
(p,G,P,y) is non empty finite strict unital Group-like associative Subgroup of p
{y} is non empty trivial finite 1 -element Element of bool G
(p,G,P,{y}) is non empty finite strict unital Group-like associative Subgroup of p
H99 . N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card (G9 . N) is epsilon-transitive epsilon-connected ordinal cardinal set
Index (p,G,P,y) is epsilon-transitive epsilon-connected ordinal cardinal set
Left_Cosets (p,G,P,y) is finite V39() Element of bool (bool the carrier of p)
bool the carrier of p is non empty finite V39() set
bool (bool the carrier of p) is non empty finite V39() set
card (Left_Cosets (p,G,P,y)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
index (p,G,P,y) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (p,G,P,y) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of (p,G,P,y) is non empty finite set
card the carrier of (p,G,P,y) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card (p,G,P,y)) * (H99 /. N) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 |^ n is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (p,G,P,y) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(card p) * (index (p,G,P,y)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
((card p) * (index (p,G,P,y))) / (card p) is complex real ext-real non negative set
(card p) / (card p) is complex real ext-real non negative set
((card p) / (card p)) * (index (p,G,P,y)) is complex real ext-real non negative set
1 * (index (p,G,P,y)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E * q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Sum H99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(Sum H99) mod E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E * N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
len N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(len T) + (len G9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
len P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Sum N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Sum K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(Sum K) + (Sum H99) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(Sum K) + ((Sum H99) mod E) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
((Sum K) + ((Sum H99) mod E)) mod E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(Sum K) mod E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom K is finite Element of bool NAT
N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
K . N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
dom T is finite Element of bool NAT
T . N is set
Q99 is finite Element of bool G
card Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P99 is Element of G
(p,G,P,P99) is non empty finite Element of bool G
{ b1 where b1 is Element of G : (p,G,P,P99,b1) } is set
rng K is finite V82() V83() V84() V87() Element of bool REAL
{1} is non empty trivial finite V39() 1 -element Element of bool NAT
N is set
Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
K . Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
len K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N is set
Seg (len K) is finite len K -element Element of bool NAT
K . (len K) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(dom K) --> 1 is Relation-like dom K -defined NAT -valued INT -valued Function-like total quasi_total finite V72() V73() V74() V75() Element of bool [:(dom K),NAT:]
[:(dom K),NAT:] is set
bool [:(dom K),NAT:] is non empty set
Seg (len K) is finite len K -element Element of bool NAT
(Seg (len K)) --> 1 is Relation-like Seg (len K) -defined NAT -valued INT -valued Function-like total quasi_total finite V72() V73() V74() V75() Element of bool [:(Seg (len K)),NAT:]
[:(Seg (len K)),NAT:] is set
bool [:(Seg (len K)),NAT:] is non empty set
(len K) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() Element of (len K) -tuples_on NAT
(len K) -tuples_on NAT is FinSequenceSet of NAT
(len K) * 1 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (rng T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p is non empty unital Group-like associative multMagma
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
p |-count G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p |^ (p |-count G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(p |^ (p |-count G)) * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(p |-count G) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
p |^ ((p |-count G) + 1) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(p |^ (p |-count G)) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((p |^ (p |-count G)) * p) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(p |^ ((p |-count G) + 1)) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p is non empty set
G is non empty set
{ [:G,{b1}:] where b1 is Element of p : verum } is set
card { [:G,{b1}:] where b1 is Element of p : verum } is epsilon-transitive epsilon-connected ordinal cardinal set
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
P is Relation-like Function-like set
dom P is set
P is Relation-like Function-like set
dom P is set
P9 is set
P9 is Element of p
{P9} is non empty trivial finite 1 -element Element of bool p
bool p is non empty set
[:G,{P9}:] is non empty set
H9 is set
P9 is set
P . P9 is set
P9 is set
P . P9 is set
{P9} is non empty trivial finite 1 -element set
[:G,{P9}:] is non empty set
rng P is set
P9 is set
P9 is set
P . P9 is set
P . P9 is set
{P9} is non empty trivial finite 1 -element set
[:G,{P9}:] is non empty set
{P9} is non empty trivial finite 1 -element set
[:G,{P9}:] is non empty set
G is non empty finite unital Group-like associative multMagma
the carrier of G is non empty finite set
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is non empty set
Funcs (p,p) is non empty functional set
[: the carrier of G,(Funcs (p,p)):] is non empty set
bool [: the carrier of G,(Funcs (p,p)):] is non empty set
E is non empty set
[: the carrier of G,E:] is non empty set
Funcs ([: the carrier of G,E:],[: the carrier of G,E:]) is non empty functional set
(G,E) is Relation-like the carrier of G -defined Funcs ([: the carrier of G,E:],[: the carrier of G,E:]) -valued non empty Function-like total quasi_total finite (G,[: the carrier of G,E:]) Element of bool [: the carrier of G,(Funcs ([: the carrier of G,E:],[: the carrier of G,E:])):]
[: the carrier of G,(Funcs ([: the carrier of G,E:],[: the carrier of G,E:])):] is non empty set
bool [: the carrier of G,(Funcs ([: the carrier of G,E:],[: the carrier of G,E:])):] is non empty set
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
{ [: the carrier of G,{b1}:] where b1 is Element of E : verum } is set
P is Relation-like the carrier of G -defined Funcs (p,p) -valued non empty Function-like total quasi_total finite (G,p) Element of bool [: the carrier of G,(Funcs (p,p)):]
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p,P9) is Element of bool (bool p)
bool p is non empty set
bool (bool p) is non empty set
{ b1 where b1 is Element of bool p : card b1 = P9 } is set
(p,P9,G,P) is Relation-like the carrier of G -defined Funcs ((p,P9),(p,P9)) -valued non empty Function-like total quasi_total finite (G,(p,P9)) Element of bool [: the carrier of G,(Funcs ((p,P9),(p,P9))):]
Funcs ((p,P9),(p,P9)) is non empty functional set
[: the carrier of G,(Funcs ((p,P9),(p,P9))):] is non empty set
bool [: the carrier of G,(Funcs ((p,P9),(p,P9))):] is non empty set
(G,(p,P9),(p,P9,G,P)) is Element of bool (p,P9)
bool (p,P9) is non empty set
P9 is set
{ b1 where b1 is Element of (p,P9) : (G,(p,P9),(p,P9,G,P),b1) } is set
P9 is Element of (p,P9)
T is Element of bool p
card T is epsilon-transitive epsilon-connected ordinal cardinal set
G9 is Element of the carrier of G
(G,G9,E) is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
[:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
bool [:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
(G,G9,E) .: P9 is Relation-like the carrier of G -defined E -valued Element of bool [: the carrier of G,E:]
bool [: the carrier of G,E:] is non empty set
(p,P9,G,P) . G9 is Relation-like Function-like Element of Funcs ((p,P9),(p,P9))
(p,P9,G,G9,P) is Relation-like (p,P9) -defined (p,P9) -valued Function-like total quasi_total Element of bool [:(p,P9),(p,P9):]
[:(p,P9),(p,P9):] is set
bool [:(p,P9),(p,P9):] is non empty set
(G,(p,P9),(p,P9,G,P),G9) is Relation-like (p,P9) -defined (p,P9) -valued Function-like total quasi_total Element of bool [:(p,P9),(p,P9):]
(G,(p,P9),(p,P9,G,P),G9) . P9 is set
(G,p,P,G9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P,G9) .: P9 is Element of bool p
G9 is set
T9 is set
K is set
[T9,K] is set
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
P is Element of E
{P} is non empty trivial finite 1 -element Element of bool E
bool E is non empty set
[: the carrier of G,{P}:] is non empty finite set
Q is set
H99 is set
Q9 is set
[H99,Q9] is set
{H99,Q9} is non empty finite set
{H99} is non empty trivial finite 1 -element set
{{H99,Q9},{H99}} is non empty finite V39() set
N is Element of the carrier of G
T is Element of the carrier of G
T " is Element of the carrier of G
N * (T ") is Element of the carrier of G
(G,(N * (T ")),E) is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
[:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
bool [:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
K is Element of [: the carrier of G,E:]
(G,(N * (T ")),E) . K is Element of [: the carrier of G,E:]
Q99 is Element of [: the carrier of G,E:]
n is Element of the carrier of G
P99 is Element of the carrier of G
(N * (T ")) * P99 is Element of the carrier of G
n9 is Element of E
[P99,n9] is Element of [: the carrier of G,E:]
{P99,n9} is non empty finite set
{P99} is non empty trivial finite 1 -element set
{{P99,n9},{P99}} is non empty finite V39() set
[n,n9] is Element of [: the carrier of G,E:]
{n,n9} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,n9},{n}} is non empty finite V39() set
dom (G,(N * (T ")),E) is Relation-like the carrier of G -defined E -valued Element of bool [: the carrier of G,E:]
bool [: the carrier of G,E:] is non empty set
(G,(N * (T ")),E) . G9 is set
(G,(N * (T ")),E) .: P9 is Relation-like the carrier of G -defined E -valued Element of bool [: the carrier of G,E:]
(N * (T ")) * T is Element of the carrier of G
(T ") * T is Element of the carrier of G
N * ((T ") * T) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
N * (1_ G) is Element of the carrier of G
G9 is Element of E
{G9} is non empty trivial finite 1 -element Element of bool E
bool E is non empty set
[: the carrier of G,{G9}:] is non empty finite set
G9 is Element of E
{G9} is non empty trivial finite 1 -element Element of bool E
bool E is non empty set
[: the carrier of G,{G9}:] is non empty finite set
T9 is Relation-like Function-like set
dom T9 is set
rng T9 is set
card [: the carrier of G,{G9}:] is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
K is finite set
P9 is Element of E
{P9} is non empty trivial finite 1 -element Element of bool E
[: the carrier of G,{P9}:] is non empty finite set
T is set
G9 is set
T9 is set
[G9,T9] is set
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
T is Element of bool p
card T is epsilon-transitive epsilon-connected ordinal cardinal set
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
G9 is Element of (p,P9)
T9 is Element of the carrier of G
(G,p,P,T9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P,T9) .: G9 is Element of bool p
(G,T9,E) is Relation-like [: the carrier of G,E:] -defined [: the carrier of G,E:] -valued non empty Function-like total quasi_total Element of bool [:[: the carrier of G,E:],[: the carrier of G,E:]:]
[:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
bool [:[: the carrier of G,E:],[: the carrier of G,E:]:] is non empty set
K is set
P is set
T is set
[P,T] is set
{P,T} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,T},{P}} is non empty finite V39() set
T9 " is Element of the carrier of G
K is Element of the carrier of G
(T9 ") * K is Element of the carrier of G
[((T9 ") * K),T] is set
{((T9 ") * K),T} is non empty finite set
{((T9 ") * K)} is non empty trivial finite 1 -element set
{{((T9 ") * K),T},{((T9 ") * K)}} is non empty finite V39() set
Q is set
dom (G,p,P,T9) is Element of bool p
H99 is set
Q9 is Element of [: the carrier of G,E:]
(G,p,P,T9) . Q9 is set
N is Element of [: the carrier of G,E:]
Q99 is Element of the carrier of G
N is Element of the carrier of G
T9 * N is Element of the carrier of G
P99 is Element of E
[N,P99] is Element of [: the carrier of G,E:]
{N,P99} is non empty finite set
{N} is non empty trivial finite 1 -element set
{{N,P99},{N}} is non empty finite V39() set
[Q99,P99] is Element of [: the carrier of G,E:]
{Q99,P99} is non empty finite set
{Q99} is non empty trivial finite 1 -element set
{{Q99,P99},{Q99}} is non empty finite V39() set
T9 * ((T9 ") * K) is Element of the carrier of G
T9 * (T9 ") is Element of the carrier of G
(T9 * (T9 ")) * K is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * K is Element of the carrier of G
(G,p,P,T9) . H99 is set
P is set
(G,p,P,T9) . P is set
T is Element of [: the carrier of G,E:]
(G,p,P,T9) . T is set
K is Element of [: the carrier of G,E:]
H99 is Element of the carrier of G
Q is Element of the carrier of G
T9 * Q is Element of the carrier of G
Q9 is Element of E
[Q,Q9] is Element of [: the carrier of G,E:]
{Q,Q9} is non empty finite set
{Q} is non empty trivial finite 1 -element set
{{Q,Q9},{Q}} is non empty finite V39() set
[H99,Q9] is Element of [: the carrier of G,E:]
{H99,Q9} is non empty finite set
{H99} is non empty trivial finite 1 -element set
{{H99,Q9},{H99}} is non empty finite V39() set
{Q9} is non empty trivial finite 1 -element Element of bool E
N is set
N is set
[N,N] is set
{N,N} is non empty finite set
{N} is non empty trivial finite 1 -element set
{{N,N},{N}} is non empty finite V39() set
T9 is Element of the carrier of G
(G,(p,P9),(p,P9,G,P),T9) is Relation-like (p,P9) -defined (p,P9) -valued Function-like total quasi_total Element of bool [:(p,P9),(p,P9):]
[:(p,P9),(p,P9):] is set
bool [:(p,P9),(p,P9):] is non empty set
(G,(p,P9),(p,P9,G,P),T9) . G9 is set
(p,P9,G,P) . T9 is Relation-like Function-like Element of Funcs ((p,P9),(p,P9))
(p,P9,G,T9,P) is Relation-like (p,P9) -defined (p,P9) -valued Function-like total quasi_total Element of bool [:(p,P9),(p,P9):]
(G,p,P,T9) is Relation-like p -defined p -valued non empty Function-like one-to-one total quasi_total Element of bool [:p,p:]
[:p,p:] is non empty set
bool [:p,p:] is non empty set
(G,p,P,T9) .: G9 is Element of bool p
[G9,((G,(p,P9),(p,P9,G,P),T9) . G9)] is set
{G9,((G,(p,P9),(p,P9,G,P),T9) . G9)} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,((G,(p,P9),(p,P9,G,P),T9) . G9)},{G9}} is non empty finite V39() set
K is Element of (p,P9)
(G,p,P,T9) .: K is Element of bool p
[K,((G,p,P,T9) .: K)] is set
{K,((G,p,P,T9) .: K)} is non empty finite set
{K} is non empty trivial finite 1 -element set
{{K,((G,p,P,T9) .: K)},{K}} is non empty finite V39() set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
P9 |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(P9 |^ P9) * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E choose (P9 |^ P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E choose (P9 |^ P9)) mod P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
P9 |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
INT.Group T is non empty finite strict unital Group-like associative commutative cyclic (T) multMagma
the carrier of (INT.Group T) is non empty finite set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Segm P9 is V87() Element of bool NAT
card (Segm P9) is epsilon-transitive epsilon-connected ordinal cardinal set
P is non empty finite set
[: the carrier of (INT.Group T),P:] is non empty finite set
K is non empty finite set
(K,T) is finite V39() Element of bool (bool K)
bool K is non empty finite V39() set
bool (bool K) is non empty finite V39() set
{ b1 where b1 is Element of bool K : card b1 = T } is set
Segm T is non empty V87() Element of bool NAT
addint T is Relation-like [:(Segm T),(Segm T):] -defined Segm T -valued non empty Function-like total quasi_total V72() V73() V74() V75() Element of bool [:[:(Segm T),(Segm T):],(Segm T):]
[:(Segm T),(Segm T):] is non empty V75() set
[:[:(Segm T),(Segm T):],(Segm T):] is non empty V75() set
bool [:[:(Segm T),(Segm T):],(Segm T):] is non empty set
multMagma(# (Segm T),(addint T) #) is strict multMagma
card the carrier of (INT.Group T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card [: the carrier of (INT.Group T),P:] is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
E * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
H9 is complex real ext-real set
H9 / H9 is complex real ext-real set
H9 * P is complex real ext-real set
(H9 * P) / H9 is complex real ext-real set
(H9 / H9) * P is complex real ext-real set
1 * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card (card [: the carrier of (INT.Group T),P:]) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
G is set
p is set
Choose ([: the carrier of (INT.Group T),P:],T,G,p) is functional Element of bool (Funcs ([: the carrier of (INT.Group T),P:],{G,p}))
{G,p} is non empty finite set
Funcs ([: the carrier of (INT.Group T),P:],{G,p}) is non empty functional FUNCTION_DOMAIN of [: the carrier of (INT.Group T),P:],{G,p}
bool (Funcs ([: the carrier of (INT.Group T),P:],{G,p})) is non empty set
card (Choose ([: the carrier of (INT.Group T),P:],T,G,p)) is epsilon-transitive epsilon-connected ordinal cardinal set
H99 is non empty finite set
card H99 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
E choose T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
((INT.Group T),P) is Relation-like the carrier of (INT.Group T) -defined Funcs ([: the carrier of (INT.Group T),P:],[: the carrier of (INT.Group T),P:]) -valued non empty Function-like total quasi_total finite ( INT.Group T,[: the carrier of (INT.Group T),P:]) Element of bool [: the carrier of (INT.Group T),(Funcs ([: the carrier of (INT.Group T),P:],[: the carrier of (INT.Group T),P:])):]
Funcs ([: the carrier of (INT.Group T),P:],[: the carrier of (INT.Group T),P:]) is non empty functional set
[: the carrier of (INT.Group T),(Funcs ([: the carrier of (INT.Group T),P:],[: the carrier of (INT.Group T),P:])):] is non empty set
bool [: the carrier of (INT.Group T),(Funcs ([: the carrier of (INT.Group T),P:],[: the carrier of (INT.Group T),P:])):] is non empty set
([: the carrier of (INT.Group T),P:],T,(INT.Group T),((INT.Group T),P)) is Relation-like the carrier of (INT.Group T) -defined Funcs (([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T)) -valued non empty Function-like total quasi_total finite ( INT.Group T,([: the carrier of (INT.Group T),P:],T)) Element of bool [: the carrier of (INT.Group T),(Funcs (([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T))):]
([: the carrier of (INT.Group T),P:],T) is finite V39() Element of bool (bool [: the carrier of (INT.Group T),P:])
bool [: the carrier of (INT.Group T),P:] is non empty finite V39() set
bool (bool [: the carrier of (INT.Group T),P:]) is non empty finite V39() set
{ b1 where b1 is Element of bool [: the carrier of (INT.Group T),P:] : card b1 = T } is set
Funcs (([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T)) is non empty functional set
[: the carrier of (INT.Group T),(Funcs (([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T))):] is non empty set
bool [: the carrier of (INT.Group T),(Funcs (([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T))):] is non empty set
P mod P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P div P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 * (P div P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(P9 * (P div P9)) + 0 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (INT.Group T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of (INT.Group T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
((INT.Group T),([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T,(INT.Group T),((INT.Group T),P))) is finite V39() Element of bool ([: the carrier of (INT.Group T),P:],T)
bool ([: the carrier of (INT.Group T),P:],T) is non empty finite V39() set
card ((INT.Group T),([: the carrier of (INT.Group T),P:],T),([: the carrier of (INT.Group T),P:],T,(INT.Group T),((INT.Group T),P))) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
{ [: the carrier of (INT.Group T),{b1}:] where b1 is Element of P : verum } is set
card { [: the carrier of (INT.Group T),{b1}:] where b1 is Element of P : verum } is epsilon-transitive epsilon-connected ordinal cardinal set
card P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
P9 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(P9 |^ (G + 1)) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 |^ G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(P9 |^ G) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((P9 |^ G) * P9) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 |^ G) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((P9 |^ G) * p) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
H9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 * H9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
((P9 |^ G) * p) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H9 * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(H9 * P) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 |^ G) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((P9 |^ G) * P9) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 |^ (G + 1)) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
P9 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 |^ (G + 1)) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p * E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
P |^ 0 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(P |^ 0) * G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 |^ G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 |^ G) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E * P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
p is non empty Element of bool the carrier of G
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
E is Element of the carrier of G
p * E is Element of bool the carrier of G
{E} is non empty trivial finite 1 -element Element of bool the carrier of G
p * {E} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in p & b2 in {E} ) } is set
card (p * E) is epsilon-transitive epsilon-connected ordinal cardinal set
the Element of p is Element of p
the Element of p * E is Element of the carrier of G
[:p, the carrier of G:] is non empty set
bool [:p, the carrier of G:] is non empty set
P9 is Relation-like p -defined the carrier of G -valued non empty Function-like total quasi_total Element of bool [:p, the carrier of G:]
P9 is non empty Element of bool the carrier of G
rng P9 is Element of bool the carrier of G
H9 is set
P9 is Element of the carrier of G
P9 * E is Element of the carrier of G
dom P9 is Element of bool p
bool p is non empty set
P9 . P9 is set
P9 is set
P9 . P9 is set
dom P9 is Element of bool p
bool p is non empty set
H9 is set
P9 is set
P9 . P9 is set
P9 is Element of p
P9 * E is Element of the carrier of G
[:p,P9:] is non empty set
bool [:p,P9:] is non empty set
H9 is Relation-like p -defined P9 -valued non empty Function-like total quasi_total Element of bool [:p,P9:]
P9 is Element of p
H9 . P9 is Element of P9
P9 is Element of p
H9 . P9 is Element of P9
P9 * E is Element of the carrier of G
P9 * E is Element of the carrier of G
dom H9 is set
rng H9 is set
E is non empty finite unital Group-like associative multMagma
P is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
card E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of E is non empty finite set
card the carrier of E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(E) is Relation-like the carrier of E -defined Funcs ( the carrier of E, the carrier of E) -valued non empty Function-like total quasi_total finite (E, the carrier of E) Element of bool [: the carrier of E,(Funcs ( the carrier of E, the carrier of E)):]
Funcs ( the carrier of E, the carrier of E) is non empty functional set
[: the carrier of E,(Funcs ( the carrier of E, the carrier of E)):] is non empty set
bool [: the carrier of E,(Funcs ( the carrier of E, the carrier of E)):] is non empty set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P |^ P9) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
P9 |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
( the carrier of E,T) is finite V39() Element of bool (bool the carrier of E)
bool the carrier of E is non empty finite V39() set
bool (bool the carrier of E) is non empty finite V39() set
{ b1 where b1 is Element of bool the carrier of E : card b1 = T } is set
card ( the carrier of E,T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is set
p is set
Choose ( the carrier of E,T,G,p) is functional Element of bool (Funcs ( the carrier of E,{G,p}))
{G,p} is non empty finite set
Funcs ( the carrier of E,{G,p}) is non empty functional FUNCTION_DOMAIN of the carrier of E,{G,p}
bool (Funcs ( the carrier of E,{G,p})) is non empty set
card (Choose ( the carrier of E,T,G,p)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card E) choose T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card ( the carrier of E,T)) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
( the carrier of E,T,E,(E)) is Relation-like the carrier of E -defined Funcs (( the carrier of E,T),( the carrier of E,T)) -valued non empty Function-like total quasi_total finite (E,( the carrier of E,T)) Element of bool [: the carrier of E,(Funcs (( the carrier of E,T),( the carrier of E,T))):]
Funcs (( the carrier of E,T),( the carrier of E,T)) is non empty functional set
[: the carrier of E,(Funcs (( the carrier of E,T),( the carrier of E,T))):] is non empty set
bool [: the carrier of E,(Funcs (( the carrier of E,T),( the carrier of E,T))):] is non empty set
T9 is non empty finite set
Funcs (T9,T9) is non empty functional set
[: the carrier of E,(Funcs (T9,T9)):] is non empty set
bool [: the carrier of E,(Funcs (T9,T9)):] is non empty set
P is Relation-like the carrier of E -defined Funcs (T9,T9) -valued non empty Function-like total quasi_total finite (E,T9) Element of bool [: the carrier of E,(Funcs (T9,T9)):]
(E,T9,P) is finite V39() a_partition of T9
bool T9 is non empty finite V39() set
{ b1 where b1 is Element of bool T9 : ex b2 being Element of T9 st b1 = (E,T9,P,b2) } is set
T is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng T is finite set
K is Relation-like NAT -defined (E,T9,P) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (E,T9,P)
len K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom Q is finite Element of bool NAT
rng Q is finite set
H99 is set
Q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
Q . Q9 is set
dom K is finite Element of bool NAT
K . Q9 is set
N is finite Element of bool T9
card N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H99 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len H99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom Q9 is finite Element of bool NAT
rng Q9 is finite set
N is set
Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
Q9 . Q99 is set
P99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom K is finite Element of bool NAT
K . P99 is set
n is finite Element of bool T9
H99 . P99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card n is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(H99 . P99) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
n9 is Element of T9
(E,T9,P,n9) is non empty finite Element of bool T9
{ b1 where b1 is Element of T9 : (E,T9,P,n9,b1) } is set
(H99 . P99) div P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 * ((H99 . P99) div P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(H99 . P99) mod P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(P9 * ((H99 . P99) div P9)) + ((H99 . P99) mod P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P * y is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
N is complex real ext-real set
N * y is complex real ext-real set
(N * y) / N is complex real ext-real set
N / N is complex real ext-real set
(N / N) * y is complex real ext-real set
1 * y is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
dom H99 is finite Element of bool NAT
N is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() V75() FinSequence of NAT
len N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Seg (len N) is finite len N -element Element of bool NAT
dom N is finite Element of bool NAT
P9 * N is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V72() V73() V74() FinSequence of REAL
dom (P9 * N) is finite Element of bool NAT
Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
H99 . Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P9 * N) . Q99 is complex real ext-real set
N . Q99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P * (N . Q99) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(H99 . Q99) / P9 is complex real ext-real non negative set
P * ((H99 . Q99) / P9) is complex real ext-real non negative set
N is complex real ext-real set
N * (H99 . Q99) is complex real ext-real set
(N * (H99 . Q99)) / N is complex real ext-real set
N / N is complex real ext-real set
(N / N) * (H99 . Q99) is complex real ext-real set
1 * (H99 . Q99) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q . N is set
K . N is set
card (K . N) is epsilon-transitive epsilon-connected ordinal cardinal set
card T9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
Sum H99 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card T9) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Sum N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 * (Sum N) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(P9 * (Sum N)) mod P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is Element of T9
(E,T9,P,T) is non empty finite Element of bool T9
bool T9 is non empty finite V39() set
{ b1 where b1 is Element of T9 : (E,T9,P,T,b1) } is set
card (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(card (E,T9,P,T)) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is Element of T9
(E,T9,P,T) is non empty finite Element of bool T9
bool T9 is non empty finite V39() set
{ b1 where b1 is Element of T9 : (E,T9,P,T,b1) } is set
card (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(card (E,T9,P,T)) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E,T9,P,T) is non empty finite strict unital Group-like associative Subgroup of E
{T} is non empty trivial finite 1 -element Element of bool T9
(E,T9,P,{T}) is non empty finite strict unital Group-like associative Subgroup of E
Index (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal cardinal set
Left_Cosets (E,T9,P,T) is finite V39() Element of bool (bool the carrier of E)
card (Left_Cosets (E,T9,P,T)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
index (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(index (E,T9,P,T)) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P * Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
{ b1 where b1 is finite Element of bool the carrier of E : card b1 = T } is set
the carrier of (E,T9,P,T) is non empty finite set
{ b1 where b1 is Element of the carrier of E : (E,T9,P,b1) .: {T} = {T} } is set
Q9 is finite Element of bool the carrier of E
card Q9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H99 is non empty finite Element of bool the carrier of E
the Element of H99 is Element of H99
card T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card the carrier of E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
Q99 is set
Q is non empty finite unital Group-like associative multMagma
the carrier of Q is non empty finite set
{H99} is non empty trivial finite V39() 1 -element Element of bool (bool the carrier of E)
P99 is Element of the carrier of E
(E,T9,P,P99) is Relation-like T9 -defined T9 -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:T9,T9:]
[:T9,T9:] is non empty finite set
bool [:T9,T9:] is non empty finite V39() set
(E,T9,P,P99) .: {H99} is finite Element of bool T9
dom (E,T9,P,P99) is finite Element of bool T9
Im ((E,T9,P,P99),H99) is set
{H99} is non empty trivial finite V39() 1 -element set
(E,T9,P,P99) .: {H99} is finite set
(E,T9,P,P99) . H99 is set
{((E,T9,P,P99) . H99)} is non empty trivial finite 1 -element set
N is Element of the carrier of E
P99 * N is Element of the carrier of E
P . P99 is Relation-like Function-like Element of Funcs (T9,T9)
( the carrier of E,T,E,P99,(E)) is Relation-like ( the carrier of E,T) -defined ( the carrier of E,T) -valued Function-like total quasi_total finite Element of bool [:( the carrier of E,T),( the carrier of E,T):]
[:( the carrier of E,T),( the carrier of E,T):] is finite set
bool [:( the carrier of E,T),( the carrier of E,T):] is non empty finite V39() set
N is Element of T9
(E,T9,P,P99) . N is Element of T9
(E, the carrier of E,(E),P99) is Relation-like the carrier of E -defined the carrier of E -valued non empty Function-like one-to-one total quasi_total finite Element of bool [: the carrier of E, the carrier of E:]
[: the carrier of E, the carrier of E:] is non empty finite set
bool [: the carrier of E, the carrier of E:] is non empty finite V39() set
(E, the carrier of E,(E),P99) .: N is finite Element of bool the carrier of E
n9 is Relation-like the carrier of E -defined Funcs ( the carrier of E, the carrier of E) -valued non empty Function-like total quasi_total finite (E, the carrier of E) Element of bool [: the carrier of E,(Funcs ( the carrier of E, the carrier of E)):]
(E, the carrier of E,n9,P99) is Relation-like the carrier of E -defined the carrier of E -valued non empty Function-like one-to-one total quasi_total finite Element of bool [: the carrier of E, the carrier of E:]
P99 * is Relation-like the carrier of E -defined the carrier of E -valued non empty Function-like total quasi_total finite Element of bool [: the carrier of E, the carrier of E:]
dom (E, the carrier of E,n9,P99) is finite Element of bool the carrier of E
y is set
(E, the carrier of E,n9,P99) . y is set
(E, the carrier of E,n9,P99) .: H99 is finite Element of bool the carrier of E
y is set
(E, the carrier of E,n9,P99) . y is set
N " is Element of the carrier of E
(P99 * N) * (N ") is Element of the carrier of E
N * (N ") is Element of the carrier of E
P99 * (N * (N ")) is Element of the carrier of E
1_ E is non being_of_order_0 Element of the carrier of E
P99 * (1_ E) is Element of the carrier of E
H99 * (N ") is finite Element of bool the carrier of E
{(N ")} is non empty trivial finite 1 -element Element of bool the carrier of E
H99 * {(N ")} is finite Element of bool the carrier of E
{ (b1 * b2) where b1, b2 is Element of the carrier of E : ( b1 in H99 & b2 in {(N ")} ) } is set
card the carrier of Q is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card (H99 * (N ")) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card Q is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of Q is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
N is finite Element of bool the carrier of E
card N is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of (E,T9,P,T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card (E,T9,P,T)) * (index (E,T9,P,T)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(index (E,T9,P,T)) * (card (E,T9,P,T)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
1 / (card (E,T9,P,T)) is complex real ext-real non negative set
((index (E,T9,P,T)) * (card (E,T9,P,T))) * (1 / (card (E,T9,P,T))) is complex real ext-real non negative set
((P |^ P9) * P9) * (1 / (card (E,T9,P,T))) is complex real ext-real non negative set
(P9 |^ P9) * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
1 / (P9 |^ P9) is complex real ext-real non negative set
((P9 |^ P9) * P9) * (1 / (P9 |^ P9)) is complex real ext-real non negative set
(P9 |^ P9) * (1 / (P9 |^ P9)) is complex real ext-real non negative set
P9 * ((P9 |^ P9) * (1 / (P9 |^ P9))) is complex real ext-real non negative set
(P9 |^ P9) / (P9 |^ P9) is complex real ext-real non negative set
P9 * ((P9 |^ P9) / (P9 |^ P9)) is complex real ext-real non negative set
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
E |^ p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E * P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is non empty finite unital Group-like associative multMagma
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of G is non empty finite set
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
P is non empty finite strict unital Group-like associative Subgroup of G
P9 is non empty finite unital Group-like associative multMagma
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of P9 is non empty finite set
card the carrier of P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
1 * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
1 - 1 is complex real V18() ext-real set
P9 - 1 is complex real V18() ext-real set
H9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E |^ H9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(E |^ H9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
p |^ H9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
1 * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p |^ H9) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(Omega). P9 is non empty finite strict unital Group-like associative Subgroup of P9
the multF of P9 is Relation-like [: the carrier of P9, the carrier of P9:] -defined the carrier of P9 -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of P9, the carrier of P9:], the carrier of P9:]
[: the carrier of P9, the carrier of P9:] is non empty finite set
[:[: the carrier of P9, the carrier of P9:], the carrier of P9:] is non empty finite set
bool [:[: the carrier of P9, the carrier of P9:], the carrier of P9:] is non empty finite V39() set
multMagma(# the carrier of P9, the multF of P9 #) is strict unital Group-like associative multMagma
card ((Omega). P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of ((Omega). P9) is non empty finite set
card the carrier of ((Omega). P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card ((Omega). P9)) * 1 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
p |^ (H9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
1_ ((Omega). P9) is non being_of_order_0 Element of the carrier of ((Omega). P9)
P9 is Element of the carrier of ((Omega). P9)
{P9} is non empty trivial finite 1 -element Element of bool the carrier of ((Omega). P9)
bool the carrier of ((Omega). P9) is non empty finite V39() set
gr {P9} is non empty finite strict unital Group-like associative Subgroup of (Omega). P9
T is non empty strict unital Group-like associative multMagma
G9 is non empty finite strict unital Group-like associative multMagma
card G9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of G9 is non empty finite set
card the carrier of G9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
ord P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
K is non empty finite strict unital Group-like associative Subgroup of G9
card K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of K is non empty finite set
card the carrier of K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P is Element of the carrier of K
ord P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is non empty finite strict unital Group-like associative Subgroup of G
the carrier of T is non empty finite set
K is Element of the carrier of T
Q is Element of the carrier of G
ord Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is non empty finite unital Group-like associative multMagma
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
the carrier of G is non empty finite set
P is non empty finite unital Group-like associative Subgroup of G
P9 is non empty finite unital Group-like associative Subgroup of G
carr P is finite Element of bool the carrier of G
bool the carrier of G is non empty finite V39() set
the carrier of P is non empty finite set
Left_Cosets P9 is finite V39() Element of bool (bool the carrier of G)
bool (bool the carrier of G) is non empty finite V39() set
(G,P,P9) is Relation-like the carrier of P -defined Funcs ((Left_Cosets P9),(Left_Cosets P9)) -valued non empty Function-like total quasi_total finite (P, Left_Cosets P9) Element of bool [: the carrier of P,(Funcs ((Left_Cosets P9),(Left_Cosets P9))):]
Funcs ((Left_Cosets P9),(Left_Cosets P9)) is non empty functional set
[: the carrier of P,(Funcs ((Left_Cosets P9),(Left_Cosets P9))):] is non empty set
bool [: the carrier of P,(Funcs ((Left_Cosets P9),(Left_Cosets P9))):] is non empty set
P9 is non empty finite set
Funcs (P9,P9) is non empty functional set
[: the carrier of P,(Funcs (P9,P9)):] is non empty set
bool [: the carrier of P,(Funcs (P9,P9)):] is non empty set
T is Relation-like the carrier of P -defined Funcs (P9,P9) -valued non empty Function-like total quasi_total finite (P,P9) Element of bool [: the carrier of P,(Funcs (P9,P9)):]
(P,P9,T) is finite Element of bool P9
bool P9 is non empty finite V39() set
card (P,P9,T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card (P,P9,T)) mod p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(card P9) mod p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
index P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p * G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(p * G9) + 0 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G9 is set
{ b1 where b1 is Element of P9 : (P,P9,T,b1) } is set
T9 is Element of P9
K is Element of the carrier of G
K * P9 is finite Element of bool the carrier of G
carr P9 is finite Element of bool the carrier of G
the carrier of P9 is non empty finite set
K * (carr P9) is finite Element of bool the carrier of G
{K} is non empty trivial finite 1 -element Element of bool the carrier of G
{K} * (carr P9) is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {K} & b2 in carr P9 ) } is set
K " is Element of the carrier of G
P9 |^ (K ") is non empty finite strict unital Group-like associative Subgroup of G
carr (P9 |^ (K ")) is finite Element of bool the carrier of G
the carrier of (P9 |^ (K ")) is non empty finite set
K is set
Q is Element of the carrier of P
H99 is Element of the carrier of P
(G,P,P9,H99) is Relation-like Left_Cosets P9 -defined Left_Cosets P9 -valued Function-like total quasi_total finite Element of bool [:(Left_Cosets P9),(Left_Cosets P9):]
[:(Left_Cosets P9),(Left_Cosets P9):] is finite set
bool [:(Left_Cosets P9),(Left_Cosets P9):] is non empty finite V39() set
T is finite Element of Left_Cosets P9
(G,P,P9,H99) . T is set
Q9 is finite Element of Left_Cosets P9
N is finite Element of bool the carrier of G
Q99 is Element of the carrier of G
N is finite Element of bool the carrier of G
Q99 * N is finite Element of bool the carrier of G
{Q99} is non empty trivial finite 1 -element Element of bool the carrier of G
{Q99} * N is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {Q99} & b2 in N ) } is set
(G,P,P9) . H99 is Relation-like Function-like Element of Funcs ((Left_Cosets P9),(Left_Cosets P9))
(K * P9) * (K ") is finite Element of bool the carrier of G
{(K ")} is non empty trivial finite 1 -element Element of bool the carrier of G
(K * P9) * {(K ")} is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K * P9 & b2 in {(K ")} ) } is set
Q99 * (K * P9) is finite Element of bool the carrier of G
{Q99} * (K * P9) is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {Q99} & b2 in K * P9 ) } is set
(Q99 * (K * P9)) * (K ") is finite Element of bool the carrier of G
(Q99 * (K * P9)) * {(K ")} is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in Q99 * (K * P9) & b2 in {(K ")} ) } is set
Q99 * ((K * P9) * (K ")) is finite Element of bool the carrier of G
{Q99} * ((K * P9) * (K ")) is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {Q99} & b2 in (K * P9) * (K ") ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
K * (1_ G) is Element of the carrier of G
K * (K ") is Element of the carrier of G
Q99 * (1_ G) is Element of the carrier of G
(K ") " is Element of the carrier of G
((K ") ") * P9 is finite Element of bool the carrier of G
((K ") ") * (carr P9) is finite Element of bool the carrier of G
{((K ") ")} is non empty trivial finite 1 -element Element of bool the carrier of G
{((K ") ")} * (carr P9) is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {((K ") ")} & b2 in carr P9 ) } is set
(((K ") ") * P9) * (K ") is finite Element of bool the carrier of G
(((K ") ") * P9) * {(K ")} is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in ((K ") ") * P9 & b2 in {(K ")} ) } is set
P is non empty finite unital Group-like associative Subgroup of G
P9 is non empty finite strict unital Group-like associative Subgroup of G
carr P is finite Element of bool the carrier of G
bool the carrier of G is non empty finite V39() set
the carrier of P is non empty finite set
P9 is Element of the carrier of G
P9 |^ P9 is non empty finite strict unital Group-like associative Subgroup of G
carr (P9 |^ P9) is finite Element of bool the carrier of G
the carrier of (P9 |^ P9) is non empty finite set
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of P9 is non empty finite set
card the carrier of P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card (P9 |^ P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of (P9 |^ P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
T is non empty finite unital Group-like associative multMagma
card T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of T is non empty finite set
card the carrier of T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P9 is non empty finite unital Group-like associative multMagma
G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p |^ G9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
index (P9 |^ P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card (P9 |^ P9)) * (index (P9 |^ P9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card (P9 |^ P9)) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P is non empty finite unital Group-like associative Subgroup of G
P9 is non empty finite unital Group-like associative Subgroup of G
P9 is non empty finite unital Group-like associative multMagma
index P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of P9 is non empty finite set
card the carrier of P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
H9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p |^ H9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is non empty finite unital Group-like associative multMagma
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of P9 is non empty finite set
card the carrier of P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of P9 is non empty finite set
card the carrier of P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card P9) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p |^ H9) * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p |^ P9) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H9 -' P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H9 - P9 is complex real V18() ext-real set
P9 - P9 is complex real V18() ext-real set
G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
P9 + (H9 -' P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
E |^ H9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
E |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
E |^ (H9 -' P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(E |^ P9) * (E |^ (H9 -' P9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ (H9 -' P9)) * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ P9) * ((E |^ (H9 -' P9)) * (index P)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ P9) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p |^ G9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(p |^ G9) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((p |^ G9) * p) * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p |^ G9) * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p * ((p |^ G9) * (index P)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 -' H9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 - H9 is complex real V18() ext-real set
H9 - H9 is complex real V18() ext-real set
G9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
H9 + (P9 -' H9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative Element of NAT
E |^ P9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
E |^ H9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
E |^ (P9 -' H9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(E |^ H9) * (E |^ (P9 -' H9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ (P9 -' H9)) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ H9) * ((E |^ (P9 -' H9)) * (index P9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(E |^ H9) * (index P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p |^ G9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(p |^ G9) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
((p |^ G9) * p) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(p |^ G9) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p * ((p |^ G9) * (index P9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
carr P is finite Element of bool the carrier of G
bool the carrier of G is non empty finite V39() set
the carrier of P is non empty finite set
card (carr P) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
carr P9 is finite Element of bool the carrier of G
card (carr P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
T is Element of the carrier of G
P9 |^ T is non empty finite strict unital Group-like associative Subgroup of G
carr (P9 |^ T) is finite Element of bool the carrier of G
the carrier of (P9 |^ T) is non empty finite set
card (P9 |^ T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of (P9 |^ T) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card (carr (P9 |^ T)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
the multF of P is Relation-like [: the carrier of P, the carrier of P:] -defined the carrier of P -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of P, the carrier of P:], the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty finite set
[:[: the carrier of P, the carrier of P:], the carrier of P:] is non empty finite set
bool [:[: the carrier of P, the carrier of P:], the carrier of P:] is non empty finite V39() set
multMagma(# the carrier of P, the multF of P #) is strict unital Group-like associative multMagma
the multF of (P9 |^ T) is Relation-like [: the carrier of (P9 |^ T), the carrier of (P9 |^ T):] -defined the carrier of (P9 |^ T) -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of (P9 |^ T), the carrier of (P9 |^ T):], the carrier of (P9 |^ T):]
[: the carrier of (P9 |^ T), the carrier of (P9 |^ T):] is non empty finite set
[:[: the carrier of (P9 |^ T), the carrier of (P9 |^ T):], the carrier of (P9 |^ T):] is non empty finite set
bool [:[: the carrier of (P9 |^ T), the carrier of (P9 |^ T):], the carrier of (P9 |^ T):] is non empty finite V39() set
multMagma(# the carrier of (P9 |^ T), the multF of (P9 |^ T) #) is strict unital Group-like associative multMagma
G is non empty unital Group-like associative multMagma
Subgroups G is non empty set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
{ b1 where b1 is Element of Subgroups G : ex b2 being non empty strict unital Group-like associative Subgroup of G st
( b2 = b1 & (p,G,b2) ) } is set
bool (Subgroups G) is non empty set
P is set
P9 is Element of Subgroups G
P9 is non empty strict unital Group-like associative Subgroup of G
G is non empty finite unital Group-like associative multMagma
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
(G,p) is Element of bool (Subgroups G)
Subgroups G is non empty set
bool (Subgroups G) is non empty set
{ b1 where b1 is Element of Subgroups G : ex b2 being non empty strict unital Group-like associative Subgroup of G st
( b2 = b1 & (p,G,b2) ) } is set
E is non empty finite strict unital Group-like associative Subgroup of G
(Omega). E is non empty finite strict unital Group-like associative Subgroup of E
the carrier of E is non empty finite set
the multF of E is Relation-like [: the carrier of E, the carrier of E:] -defined the carrier of E -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of E, the carrier of E:], the carrier of E:]
[: the carrier of E, the carrier of E:] is non empty finite set
[:[: the carrier of E, the carrier of E:], the carrier of E:] is non empty finite set
bool [:[: the carrier of E, the carrier of E:], the carrier of E:] is non empty finite V39() set
multMagma(# the carrier of E, the multF of E #) is strict unital Group-like associative multMagma
P is Element of Subgroups G
G is non empty finite unital Group-like associative multMagma
E is non empty finite unital Group-like associative Subgroup of G
the carrier of E is non empty finite set
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
(G,p) is non empty finite Element of bool (Subgroups G)
Subgroups G is non empty set
bool (Subgroups G) is non empty set
{ b1 where b1 is Element of Subgroups G : ex b2 being non empty strict unital Group-like associative Subgroup of G st
( b2 = b1 & (p,G,b2) ) } is set
[:(G,p),(G,p):] is non empty finite set
bool [:(G,p),(G,p):] is non empty finite V39() set
the carrier of G is non empty finite set
P is Element of the carrier of E
P " is Element of the carrier of E
{ [b1,b2] where b1, b2 is Element of (G,p) : ex b3, b4 being non empty finite strict unital Group-like associative Subgroup of G ex b5 being Element of the carrier of G st
( b1 = b3 & b2 = b4 & P " = b5 & b4 = b3 |^ b5 ) } is set
H9 is set
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{H9} is non empty trivial finite 1 -element set
{{H9,P9},{H9}} is non empty finite V39() set
T is Element of (G,p)
G9 is Element of (G,p)
[T,G9] is Element of [:(G,p),(G,p):]
{T,G9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,G9},{T}} is non empty finite V39() set
P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{{H9,P9},{H9}} is non empty finite V39() set
T9 is Element of (G,p)
K is Element of (G,p)
[T9,K] is Element of [:(G,p),(G,p):]
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
P is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
K is Element of the carrier of G
P |^ K is non empty finite strict unital Group-like associative Subgroup of G
Q is non empty finite strict unital Group-like associative Subgroup of G
H99 is non empty finite strict unital Group-like associative Subgroup of G
Q9 is Element of the carrier of G
Q |^ Q9 is non empty finite strict unital Group-like associative Subgroup of G
H9 is set
P9 is Element of (G,p)
P9 is Element of (G,p)
[P9,P9] is Element of [:(G,p),(G,p):]
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
T is set
G9 is set
T9 is set
K is set
[T9,K] is set
{T9,K} is non empty finite set
{T9} is non empty trivial finite 1 -element set
{{T9,K},{T9}} is non empty finite V39() set
P9 is set
H9 is Relation-like Function-like set
rng H9 is set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,P9},{P9}} is non empty finite V39() set
T is Element of (G,p)
G9 is Element of (G,p)
[T,G9] is Element of [:(G,p),(G,p):]
{T,G9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,G9},{T}} is non empty finite V39() set
P9 is set
T is Element of (G,p)
G9 is Element of Subgroups G
K is non empty finite strict unital Group-like associative Subgroup of G
T9 is non empty finite strict unital Group-like associative Subgroup of G
K is non empty finite strict unital Group-like associative Subgroup of G
K is non empty finite unital Group-like associative multMagma
P9 is Element of the carrier of G
T9 |^ P9 is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
card K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of K is non empty finite set
card the carrier of K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
K is non empty finite unital Group-like associative multMagma
card K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of K is non empty finite set
card the carrier of K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
p |^ Q is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card T9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of T9 is non empty finite set
card the carrier of T9 is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of T is non empty finite set
card the carrier of T is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index T9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card T9) * (index T9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index T is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card T9) * (index T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
H99 is non empty finite strict unital Group-like associative Subgroup of G
Q is Element of Subgroups G
H99 is Element of (G,p)
Q9 is set
N is set
[P9,N] is set
{P9,N} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,N},{P9}} is non empty finite V39() set
P9 is set
[P9,P9] is set
{P9,P9} is non empty finite set
{{P9,P9},{P9}} is non empty finite V39() set
T is Element of (G,p)
G9 is Element of (G,p)
[T,G9] is Element of [:(G,p),(G,p):]
{T,G9} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,G9},{T}} is non empty finite V39() set
dom H9 is set
P9 is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
P9 is Element of (G,p)
P9 . P9 is Element of (G,p)
[P9,(P9 . P9)] is Element of [:(G,p),(G,p):]
{P9,(P9 . P9)} is non empty finite set
{P9} is non empty trivial finite 1 -element set
{{P9,(P9 . P9)},{P9}} is non empty finite V39() set
G9 is Element of (G,p)
T9 is Element of (G,p)
[G9,T9] is Element of [:(G,p),(G,p):]
{G9,T9} is non empty finite set
{G9} is non empty trivial finite 1 -element set
{{G9,T9},{G9}} is non empty finite V39() set
P is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
K is Element of the carrier of G
P |^ K is non empty finite strict unital Group-like associative Subgroup of G
P is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
K is Element of the carrier of G
P |^ K is non empty finite strict unital Group-like associative Subgroup of G
K is Element of (G,p)
Q is non empty finite strict unital Group-like associative Subgroup of G
H99 is non empty finite strict unital Group-like associative Subgroup of G
Q9 is Element of the carrier of G
Q |^ Q9 is non empty finite strict unital Group-like associative Subgroup of G
P9 is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
P9 is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
H9 is Element of (G,p)
P9 . H9 is set
P9 . H9 is set
P9 . H9 is Element of (G,p)
P9 . H9 is Element of (G,p)
P9 is Element of (G,p)
P9 is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
G9 is Element of the carrier of G
P9 |^ G9 is non empty finite strict unital Group-like associative Subgroup of G
T9 is Element of (G,p)
K is non empty finite strict unital Group-like associative Subgroup of G
P is non empty finite strict unital Group-like associative Subgroup of G
T is Element of the carrier of G
K |^ T is non empty finite strict unital Group-like associative Subgroup of G
G is non empty finite unital Group-like associative multMagma
E is non empty finite unital Group-like associative Subgroup of G
the carrier of E is non empty finite set
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
(G,p) is non empty finite Element of bool (Subgroups G)
Subgroups G is non empty set
bool (Subgroups G) is non empty set
{ b1 where b1 is Element of Subgroups G : ex b2 being non empty strict unital Group-like associative Subgroup of G st
( b2 = b1 & (p,G,b2) ) } is set
Funcs ((G,p),(G,p)) is non empty functional set
[: the carrier of E,(Funcs ((G,p),(G,p))):] is non empty set
bool [: the carrier of E,(Funcs ((G,p),(G,p))):] is non empty set
[:(G,p),(G,p):] is non empty finite set
bool [:(G,p),(G,p):] is non empty finite V39() set
P9 is Element of the carrier of E
P9 is Element of the carrier of E
P9 * P9 is Element of the carrier of E
(G,p,E,(P9 * P9)) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
(G,p,E,P9) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
(G,p,E,P9) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
H1(P9) * H1(P9) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
Funcs ((G,p),(G,p)) is non empty functional FUNCTION_DOMAIN of (G,p),(G,p)
T is set
dom (G,p,E,(P9 * P9)) is finite Element of bool (G,p)
bool (G,p) is non empty finite V39() set
the carrier of G is non empty finite set
G9 is Element of (G,p)
(G,p,E,P9) . G9 is Element of (G,p)
P9 " is Element of the carrier of E
K is Element of (G,p)
P is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
K is Element of the carrier of G
P |^ K is non empty finite strict unital Group-like associative Subgroup of G
(G,p,E,P9) . T is set
rng (G,p,E,P9) is finite Element of bool (G,p)
Q is Relation-like Function-like set
dom Q is set
rng Q is set
Q is Element of (G,p)
(G,p,E,P9) . Q is Element of (G,p)
P9 " is Element of the carrier of E
H99 is Element of (G,p)
Q9 is non empty finite strict unital Group-like associative Subgroup of G
N is non empty finite strict unital Group-like associative Subgroup of G
N is Element of the carrier of G
Q9 |^ N is non empty finite strict unital Group-like associative Subgroup of G
T9 is Element of (G,p)
(G,p,E,(P9 * P9)) . T9 is Element of (G,p)
(P9 * P9) " is Element of the carrier of E
Q99 is Element of (G,p)
P99 is non empty finite strict unital Group-like associative Subgroup of G
n is non empty finite strict unital Group-like associative Subgroup of G
n9 is Element of the carrier of G
P99 |^ n9 is non empty finite strict unital Group-like associative Subgroup of G
(P9 ") * (P9 ") is Element of the carrier of E
K * N is Element of the carrier of G
P99 |^ (K * N) is non empty finite strict unital Group-like associative Subgroup of G
(G,p,E,(P9 * P9)) . T is set
(G,p,E,P9) . ((G,p,E,P9) . T) is set
T is set
dom (G,p,E,P9) is finite Element of bool (G,p)
G9 is Relation-like Function-like set
dom G9 is set
rng G9 is set
(G,p,E,P9) . T is set
G9 is Relation-like Function-like set
dom G9 is set
rng G9 is set
dom (G,p,E,P9) is finite Element of bool (G,p)
G9 is Relation-like Function-like set
dom G9 is set
rng G9 is set
G9 is Relation-like Function-like set
dom G9 is set
rng G9 is set
1_ E is non being_of_order_0 Element of the carrier of E
(G,p,E,(1_ E)) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
id (G,p) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:(G,p),(G,p):]
P9 is set
the carrier of G is non empty finite set
H9 is Element of (G,p)
(G,p,E,(1_ E)) . H9 is Element of (G,p)
(1_ E) " is Element of the carrier of E
P9 is Element of (G,p)
P9 is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
G9 is Element of the carrier of G
P9 |^ G9 is non empty finite strict unital Group-like associative Subgroup of G
1_ G is non being_of_order_0 Element of the carrier of G
(G,p,E,(1_ E)) . P9 is set
Funcs ((G,p),(G,p)) is non empty functional FUNCTION_DOMAIN of (G,p),(G,p)
P9 is Relation-like Function-like set
dom P9 is set
rng P9 is set
P9 is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
P is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
P9 is Relation-like the carrier of E -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite (E,(G,p)) Element of bool [: the carrier of E,(Funcs ((G,p),(G,p))):]
P9 is Element of the carrier of E
P . P9 is Relation-like Function-like set
P9 . P9 is Relation-like Function-like set
P . P9 is Relation-like Function-like Element of Funcs ((G,p),(G,p))
(G,p,E,P9) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
[:(G,p),(G,p):] is non empty finite set
bool [:(G,p),(G,p):] is non empty finite V39() set
P9 . P9 is Relation-like Function-like Element of Funcs ((G,p),(G,p))
G is non empty finite unital Group-like associative multMagma
p is non empty finite unital Group-like associative multMagma
E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
P is non empty finite unital Group-like associative Subgroup of G
P9 is non empty finite unital Group-like associative Subgroup of p
index P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
index P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P9 is non empty finite unital Group-like associative Subgroup of G
index P9 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(index P9) * (index P9) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is non empty finite unital Group-like associative multMagma
card G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of G is non empty finite set
card the carrier of G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
(G,p) is non empty finite Element of bool (Subgroups G)
Subgroups G is non empty set
bool (Subgroups G) is non empty set
{ b1 where b1 is Element of Subgroups G : ex b2 being non empty strict unital Group-like associative Subgroup of G st
( b2 = b1 & (p,G,b2) ) } is set
card (G,p) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
(card (G,p)) mod p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
P is non empty finite strict unital Group-like associative Subgroup of G
(Omega). P is non empty finite strict unital Group-like associative Subgroup of P
the carrier of P is non empty finite set
the multF of P is Relation-like [: the carrier of P, the carrier of P:] -defined the carrier of P -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of P, the carrier of P:], the carrier of P:]
[: the carrier of P, the carrier of P:] is non empty finite set
[:[: the carrier of P, the carrier of P:], the carrier of P:] is non empty finite set
bool [:[: the carrier of P, the carrier of P:], the carrier of P:] is non empty finite V39() set
multMagma(# the carrier of P, the multF of P #) is strict unital Group-like associative multMagma
P9 is non empty finite strict unital Group-like associative Subgroup of G
H9 is Element of Subgroups G
P9 is non empty finite strict unital Group-like associative Subgroup of G
(G,p,P) is Relation-like the carrier of P -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite (P,(G,p)) Element of bool [: the carrier of P,(Funcs ((G,p),(G,p))):]
Funcs ((G,p),(G,p)) is non empty functional set
[: the carrier of P,(Funcs ((G,p),(G,p))):] is non empty set
bool [: the carrier of P,(Funcs ((G,p),(G,p))):] is non empty set
(Omega). G is non empty finite strict unital Group-like associative Subgroup of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is non empty finite set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty finite set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty finite V39() set
multMagma(# the carrier of G, the multF of G #) is strict unital Group-like associative multMagma
(G,p,((Omega). G)) is Relation-like the carrier of ((Omega). G) -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite ( (Omega). G,(G,p)) Element of bool [: the carrier of ((Omega). G),(Funcs ((G,p),(G,p))):]
the carrier of ((Omega). G) is non empty finite set
[: the carrier of ((Omega). G),(Funcs ((G,p),(G,p))):] is non empty set
bool [: the carrier of ((Omega). G),(Funcs ((G,p),(G,p))):] is non empty set
P9 is Element of (G,p)
(((Omega). G),(G,p),(G,p,((Omega). G)),P9) is non empty finite strict unital Group-like associative Subgroup of (Omega). G
{P9} is non empty trivial finite 1 -element Element of bool (G,p)
bool (G,p) is non empty finite V39() set
(((Omega). G),(G,p),(G,p,((Omega). G)),{P9}) is non empty finite strict unital Group-like associative Subgroup of (Omega). G
K is set
(((Omega). G),(G,p),(G,p,((Omega). G)),P9) is non empty finite Element of bool (G,p)
{ b1 where b1 is Element of (G,p) : ( (Omega). G,(G,p),(G,p,((Omega). G)),P9,b1) } is set
Q is Element of Subgroups G
H99 is non empty finite strict unital Group-like associative Subgroup of G
H99 is non empty finite strict unital Group-like associative Subgroup of G
T is non empty finite strict unital Group-like associative Subgroup of G
Q9 is Element of the carrier of G
T |^ Q9 is non empty finite strict unital Group-like associative Subgroup of G
Q9 " is Element of the carrier of G
N is Element of the carrier of ((Omega). G)
N " is Element of the carrier of ((Omega). G)
(Q9 ") " is Element of the carrier of G
(G,p,((Omega). G),N) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
[:(G,p),(G,p):] is non empty finite set
bool [:(G,p),(G,p):] is non empty finite V39() set
P is Element of (G,p)
(G,p,((Omega). G),N) . P is Element of (G,p)
(((Omega). G),(G,p),(G,p,((Omega). G)),N) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:(G,p),(G,p):]
(((Omega). G),(G,p),(G,p,((Omega). G)),N) . P9 is Element of (G,p)
Q99 is Element of (G,p)
P99 is non empty finite strict unital Group-like associative Subgroup of G
n is non empty finite strict unital Group-like associative Subgroup of G
n9 is Element of the carrier of G
P99 |^ n9 is non empty finite strict unital Group-like associative Subgroup of G
N is Element of (G,p)
P is non empty finite unital Group-like associative Subgroup of G
the carrier of P is non empty finite set
[: the carrier of P,(Funcs ((G,p),(G,p))):] is non empty set
bool [: the carrier of P,(Funcs ((G,p),(G,p))):] is non empty set
T is Relation-like the carrier of P -defined Funcs ((G,p),(G,p)) -valued non empty Function-like total quasi_total finite (P,(G,p)) Element of bool [: the carrier of P,(Funcs ((G,p),(G,p))):]
(P,(G,p),T) is finite Element of bool (G,p)
K is set
H99 is Element of the carrier of P
(P,(G,p),T,H99) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:(G,p),(G,p):]
(P,(G,p),T,H99) . P9 is Element of (G,p)
(G,p,P,H99) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
Q is Element of (G,p)
(G,p,P,H99) . Q is Element of (G,p)
H99 " is Element of the carrier of P
Q9 is Element of (G,p)
N is non empty finite strict unital Group-like associative Subgroup of G
N is non empty finite strict unital Group-like associative Subgroup of G
Q99 is Element of the carrier of G
N |^ Q99 is non empty finite strict unital Group-like associative Subgroup of G
P99 is set
carr N is finite Element of bool the carrier of G
bool the carrier of G is non empty finite V39() set
the carrier of N is non empty finite set
n is Element of the carrier of G
Q99 " is Element of the carrier of G
(Q99 ") * N is finite Element of bool the carrier of G
(Q99 ") * (carr N) is finite Element of bool the carrier of G
{(Q99 ")} is non empty trivial finite 1 -element Element of bool the carrier of G
{(Q99 ")} * (carr N) is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {(Q99 ")} & b2 in carr N ) } is set
n * (Q99 ") is Element of the carrier of G
(n * (Q99 ")) * Q99 is Element of the carrier of G
(Q99 ") * Q99 is Element of the carrier of G
n * ((Q99 ") * Q99) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
n * (1_ G) is Element of the carrier of G
Q99 * (n * (Q99 ")) is Element of the carrier of G
(Q99 ") * (Q99 * (n * (Q99 "))) is Element of the carrier of G
((Q99 ") * Q99) * (n * (Q99 ")) is Element of the carrier of G
(1_ G) * (n * (Q99 ")) is Element of the carrier of G
y is Element of the carrier of G
(Q99 ") * y is Element of the carrier of G
((Q99 ") * N) * Q99 is finite Element of bool the carrier of G
{Q99} is non empty trivial finite 1 -element Element of bool the carrier of G
((Q99 ") * N) * {Q99} is finite Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (Q99 ") * N & b2 in {Q99} ) } is set
n9 is Element of the carrier of G
n9 * Q99 is Element of the carrier of G
carr (N |^ Q99) is finite Element of bool the carrier of G
the carrier of (N |^ Q99) is non empty finite set
card (carr N) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card N is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of N is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card (N |^ Q99) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of (N |^ Q99) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
card (carr (N |^ Q99)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
{ b1 where b1 is Element of (G,p) : (P,(G,p),T,b1) } is set
Q is Element of (G,p)
H99 is Element of Subgroups G
Q9 is non empty finite strict unital Group-like associative Subgroup of G
Q9 is non empty finite strict unital Group-like associative Subgroup of G
Normalizer Q9 is non empty finite strict unital Group-like associative Subgroup of G
N is set
P99 is Element of the carrier of G
Q9 |^ P99 is non empty finite strict unital Group-like associative Subgroup of G
n is Element of the carrier of P
(P,(G,p),T,n) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like one-to-one total quasi_total finite Element of bool [:(G,p),(G,p):]
dom (P,(G,p),T,n) is finite Element of bool (G,p)
(G,p,P,n) is Relation-like (G,p) -defined (G,p) -valued non empty Function-like total quasi_total finite Element of bool [:(G,p),(G,p):]
n9 is Element of (G,p)
(G,p,P,n) . n9 is Element of (G,p)
n " is Element of the carrier of P
(P,(G,p),T,n) . Q9 is set
T . n is Relation-like Function-like Element of Funcs ((G,p),(G,p))
P99 " is Element of the carrier of G
Q9 |^ (P99 ") is non empty finite strict unital Group-like associative Subgroup of G
y is Element of (G,p)
q99 is non empty finite strict unital Group-like associative Subgroup of G
q9 is non empty finite strict unital Group-like associative Subgroup of G
c29 is Element of the carrier of G
q99 |^ c29 is non empty finite strict unital Group-like associative Subgroup of G
(P99 ") * P99 is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
Q9 |^ ((P99 ") * P99) is non empty finite strict unital Group-like associative Subgroup of G
Q99 is Element of the carrier of G
Q9 |^ Q99 is non empty finite strict unital Group-like associative Subgroup of G
the carrier of (Normalizer Q9) is non empty finite set
N is set
the carrier of Q9 is non empty finite set
P99 is Element of the carrier of G
Q9 |^ P99 is non empty finite strict unital Group-like associative Subgroup of G
n is Element of the carrier of G
P99 * n is Element of the carrier of G
P99 " is Element of the carrier of G
(P99 * n) * (P99 ") is Element of the carrier of G
((P99 * n) * (P99 ")) |^ P99 is Element of the carrier of G
(P99 ") * ((P99 * n) * (P99 ")) is Element of the carrier of G
((P99 ") * ((P99 * n) * (P99 "))) * P99 is Element of the carrier of G
n * (P99 ") is Element of the carrier of G
P99 * (n * (P99 ")) is Element of the carrier of G
(P99 ") * (P99 * (n * (P99 "))) is Element of the carrier of G
((P99 ") * (P99 * (n * (P99 ")))) * P99 is Element of the carrier of G
(P99 ") * P99 is Element of the carrier of G
((P99 ") * P99) * (n * (P99 ")) is Element of the carrier of G
(((P99 ") * P99) * (n * (P99 "))) * P99 is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * (n * (P99 ")) is Element of the carrier of G
((1_ G) * (n * (P99 "))) * P99 is Element of the carrier of G
(n * (P99 ")) * P99 is Element of the carrier of G
n * ((P99 ") * P99) is Element of the carrier of G
n * (1_ G) is Element of the carrier of G
n9 is Element of the carrier of G
n9 |^ P99 is Element of the carrier of G
n9 is Element of the carrier of G
n9 |^ P99 is Element of the carrier of G
P99 " is Element of the carrier of G
(P99 ") * n9 is Element of the carrier of G
((P99 ") * n9) * P99 is Element of the carrier of G
Q99 is Element of the carrier of G
Q9 |^ Q99 is non empty finite strict unital Group-like associative Subgroup of G
N is non empty finite unital Group-like associative multMagma
Q99 is non empty finite strict unital Group-like associative Subgroup of N
P99 is non empty finite strict unital Group-like associative Subgroup of N
the carrier of N is non empty finite set
n is Element of the carrier of N
Q99 |^ n is non empty finite strict unital Group-like associative Subgroup of N
the carrier of (Q99 |^ n) is non empty finite set
the multF of G || the carrier of (Q99 |^ n) is Relation-like Function-like set
[: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):] is non empty finite set
the multF of G | [: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):] is Relation-like Function-like finite set
the multF of G || the carrier of N is Relation-like Function-like set
[: the carrier of N, the carrier of N:] is non empty finite set
the multF of G | [: the carrier of N, the carrier of N:] is Relation-like Function-like finite set
( the multF of G || the carrier of N) || the carrier of (Q99 |^ n) is Relation-like Function-like set
( the multF of G || the carrier of N) | [: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):] is Relation-like Function-like finite set
the multF of N is Relation-like [: the carrier of N, the carrier of N:] -defined the carrier of N -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty finite set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is non empty finite V39() set
the multF of N || the carrier of (Q99 |^ n) is Relation-like Function-like set
the multF of N | [: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):] is Relation-like Function-like finite set
n9 is Element of the carrier of G
Q9 |^ n9 is non empty finite strict unital Group-like associative Subgroup of G
y is set
the carrier of (Q9 |^ n9) is non empty finite set
carr Q9 is finite Element of bool the carrier of G
bool the carrier of G is non empty finite V39() set
(carr Q9) |^ n9 is finite Element of bool the carrier of G
q99 is Element of the carrier of G
q99 |^ n9 is Element of the carrier of G
n9 " is Element of the carrier of G
n " is Element of the carrier of N
(n9 ") * q99 is Element of the carrier of G
q9 is Element of the carrier of N
(n ") * q9 is Element of the carrier of N
((n9 ") * q99) * n9 is Element of the carrier of G
((n ") * q9) * n is Element of the carrier of N
q9 |^ n is Element of the carrier of N
carr Q99 is finite Element of bool the carrier of N
bool the carrier of N is non empty finite V39() set
the carrier of Q99 is non empty finite set
(carr Q99) |^ n is finite Element of bool the carrier of N
q99 is Element of the carrier of N
q99 |^ n is Element of the carrier of N
q9 is Element of the carrier of G
(n9 ") * q9 is Element of the carrier of G
(n ") * q99 is Element of the carrier of N
((n9 ") * q9) * n9 is Element of the carrier of G
((n ") * q99) * n is Element of the carrier of N
q9 |^ n9 is Element of the carrier of G
the multF of (Q9 |^ n9) is Relation-like [: the carrier of (Q9 |^ n9), the carrier of (Q9 |^ n9):] -defined the carrier of (Q9 |^ n9) -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of (Q9 |^ n9), the carrier of (Q9 |^ n9):], the carrier of (Q9 |^ n9):]
[: the carrier of (Q9 |^ n9), the carrier of (Q9 |^ n9):] is non empty finite set
[:[: the carrier of (Q9 |^ n9), the carrier of (Q9 |^ n9):], the carrier of (Q9 |^ n9):] is non empty finite set
bool [:[: the carrier of (Q9 |^ n9), the carrier of (Q9 |^ n9):], the carrier of (Q9 |^ n9):] is non empty finite V39() set
the multF of (Q99 |^ n) is Relation-like [: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):] -defined the carrier of (Q99 |^ n) -valued non empty Function-like total quasi_total finite Element of bool [:[: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):], the carrier of (Q99 |^ n):]
[:[: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):], the carrier of (Q99 |^ n):] is non empty finite set
bool [:[: the carrier of (Q99 |^ n), the carrier of (Q99 |^ n):], the carrier of (Q99 |^ n):] is non empty finite V39() set
card (P,(G,p),T) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card (P,(G,p),T)) mod p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
1 mod p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
card (((Omega). G),(G,p),(G,p,((Omega). G)),P9) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
Index (((Omega). G),(G,p),(G,p,((Omega). G)),P9) is epsilon-transitive epsilon-connected ordinal cardinal set
Left_Cosets (((Omega). G),(G,p),(G,p,((Omega). G)),P9) is finite V39() Element of bool (bool the carrier of ((Omega). G))
bool the carrier of ((Omega). G) is non empty finite V39() set
bool (bool the carrier of ((Omega). G)) is non empty finite V39() set
card (Left_Cosets (((Omega). G),(G,p),(G,p,((Omega). G)),P9)) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
card ((Omega). G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
card the carrier of ((Omega). G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
(card ((Omega). G)) * 1 is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
K is non empty finite unital Group-like associative Subgroup of (Omega). G
card K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of K is non empty finite set
card the carrier of K is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
index K is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(card K) * (index K) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
Left_Cosets K is finite V39() Element of bool (bool the carrier of ((Omega). G))
Q is finite set
card Q is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
p is non empty set
G is non empty set
{ [:G,{b1}:] where b1 is Element of p : verum } is set
card { [:G,{b1}:] where b1 is Element of p : verum } is epsilon-transitive epsilon-connected ordinal cardinal set
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
G is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() prime finite cardinal ext-real positive non negative set
E is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
P |^ E is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
(P |^ E) * p is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative set
G choose (P |^ E) is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
(G choose (P |^ E)) mod P is epsilon-transitive epsilon-connected ordinal natural complex real V18() finite cardinal ext-real non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
INT.Group G is non empty finite strict unital Group-like associative commutative cyclic (G) multMagma
card (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative Element of NAT
the carrier of (INT.Group G) is non empty finite set
card the carrier of (INT.Group G) is epsilon-transitive epsilon-connected ordinal natural non empty complex real V18() finite cardinal ext-real positive non negative set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
p is non empty Element of bool the carrier of G
card p is epsilon-transitive epsilon-connected ordinal non empty cardinal set
E is Element of the carrier of G
p * E is Element of bool the carrier of G
{E} is non empty trivial finite 1 -element Element of bool the carrier of G
p * {E} is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in p & b2 in {E} ) } is set
card (p * E) is epsilon-transitive epsilon-connected ordinal cardinal set