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