:: GROUP_10 semantic presentation

REAL is set

bool REAL is non empty set

RAT is set
INT is set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite 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 non empty finite V39() set
K463() is set
bool K463() is non empty set
K464() is Element of bool K463()

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

the carrier of INT.Group is non empty V86() set
SetPrimes is non empty non trivial non finite Element of bool NAT

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

[: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 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)}:]

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

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

dom P9 is set
rng P9 is set

dom P9 is set
rng P9 is set
G is non empty multMagma
the carrier of G is non empty set

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

dom P9 is set
rng P9 is set
(P *) . P9 is set
rng (P *) is Element of bool the carrier of G

dom P9 is set
rng P9 is set
dom (E *) is Element of bool the carrier of G

dom P9 is set
rng P9 is set

dom P9 is set
rng P9 is set
P9 is set
(P *) . P9 is 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

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

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

p is non empty 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

dom P is set
rng P is set
P .: G is finite set

G is non empty finite 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

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

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

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

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

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

P9 is set
[H9,P9] is set
{H9,P9} is non empty finite set
{{H9,P9},{H9}} is non empty finite V39() set

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

P9 is 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

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

[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

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

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

T is Element of G
G9 is Element of {E,P}
G9 is Element of {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

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

rng H9 is set
P9 is set

P9 " {E} is finite Element of bool G

[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

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

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

(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

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

dom K is set
rng K is set
rng ((E,G,P9,P) | G9) is Element of bool G

K is Element of bool G

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

(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)

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)

dom T9 is set
rng T9 is set
dom (G,p,E,P9,P) is Element of bool (G,p)

dom T9 is set
rng T9 is set

dom T9 is set
rng T9 is set
G9 is set
(G,p,E,H9,P) . G9 is 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

(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) .: P9 is Element of bool G

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

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

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

dom T is set
rng T is set
(G,P9,p) . P9 is 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:]

dom T is set
rng T is 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:]

dom P9 is set
rng P9 is set
P is Relation-like the