:: GROUP_10 semantic presentation

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

F

the carrier of F

F

[:F

bool [:F

1_ F

F

id F

Funcs (F

[: the carrier of F

bool [: the carrier of F

{ [b

p is set

E is Element of the carrier of F

F

[E,F

[: the carrier of F

{E,F

{E} is non empty trivial finite 1 -element set

{{E,F

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 F

F

[P9,F

{P9,F

{P9} is non empty trivial finite 1 -element set

{{P9,F

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 F

F

[P9,F

{P9,F

{P9} is non empty trivial finite 1 -element set

{{P9,F

E is set

P is Element of the carrier of F

F

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 F

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 F

F

[P9,F

{P9,F

{P9} is non empty trivial finite 1 -element set

{{P9,F

dom p is Element of bool the carrier of F

bool the carrier of F

P is Element of the carrier of F

E is Relation-like the carrier of F

dom E is Element of bool the carrier of F

E . P is Relation-like Function-like Element of Funcs (F

[P,(E . P)] is Element of [: the carrier of F

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

F

[P9,F

{P9,F

{P9} is non empty trivial finite 1 -element set

{{P9,F

P9 is Element of the carrier of F

E . P9 is Relation-like Function-like Element of Funcs (F

[P9,(E . P9)] is Element of [: the carrier of F

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

F

[H9,F

{H9,F

{H9} is non empty trivial finite 1 -element set

{{H9,F

P * P9 is Element of the carrier of F

E . (P * P9) is Relation-like Function-like Element of Funcs (F

[(P * P9),(E . (P * P9))] is Element of [: the carrier of F

{(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 F

F

[P9,F

{P9,F

{P9} is non empty trivial finite 1 -element set

{{P9,F

(F

F

(F

(F

(F

E . (1_ F

[(1_ F

{(1_ F

{(1_ F

{{(1_ F

P is Element of the carrier of F

F

[P,F

{P,F

{P} is non empty trivial finite 1 -element set

{{P,F

P9 is Relation-like the carrier of F

P9 is Element of the carrier of F

P9 . P9 is Relation-like Function-like Element of Funcs (F

F

[P9,(P9 . P9)] is Element of [: the carrier of F

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

F

[H9,F

{H9,F

{H9} is non empty trivial finite 1 -element set

{{H9,F

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

H

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

{ b

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

{ b

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

{ b

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

{ b

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

{ [b

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

{ b

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

{ [b

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

{ b

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

H

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

{ [b

( b

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

H

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