:: GROUP_9 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V207() V210() V211() V213() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V208() V210() Element of bool REAL

bool REAL is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite complex-membered V207() set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V208() V210() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V207() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V207() set

[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V191() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V191() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:REAL,REAL:] is Relation-like non empty non trivial non finite V191() V192() V193() set

bool [:REAL,REAL:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V191() V192() V193() set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V191() V192() V193() set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V191() V192() V193() set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() V194() set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() V194() set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

K284() is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

[:2,2:] is Relation-like RAT -valued INT -valued non empty finite V191() V192() V193() V194() set

[:[:2,2:],2:] is Relation-like RAT -valued INT -valued non empty finite V191() V192() V193() V194() set

bool [:[:2,2:],2:] is non empty finite V39() set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT

{ b

{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set

Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT

{ b

{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() Element of NAT

idseq 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*1,2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set

<*1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

[1,1] is set

{1,1} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() set

{{1,1},{1}} is non empty finite V39() set

{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element set

<*2*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

[1,2] is set

{{1,2},{1}} is non empty finite V39() set

{[1,2]} is Relation-like Function-like constant non empty trivial finite 1 -element set

<*1*> ^ <*2*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

Sgm {} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V191() V192() V193() V194() FinSequence of NAT

len {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() set

Permutations 2 is non empty permutational set

<*2,1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set

<*2*> ^ <*1*> is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set

{<*1,2*>,<*2,1*>} is functional non empty finite V39() set

<*> INT is Relation-like non-empty empty-yielding NAT -defined INT -valued Function-like one-to-one constant functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() integer finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V191() V192() V193() V194() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V207() V210() V211() V212() V213() FinSequence of INT

[:NAT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V191() V192() V193() set

O is set

G is set

Funcs (G,G) is functional non empty set

[:O,(Funcs (G,G)):] is Relation-like set

bool [:O,(Funcs (G,G)):] is non empty set

O is set

G is set

Funcs (G,G) is functional non empty set

[:O,(Funcs (G,G)):] is Relation-like set

bool [:O,(Funcs (G,G)):] is non empty set

[#] G is non proper Element of bool G

bool G is non empty set

s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]

[:G,G:] is Relation-like set

bool [:G,G:] is non empty set

s2 is Element of O

s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s1 . s2 is Relation-like Function-like set

s19 .: ([#] G) is Element of bool G

O is set

G is set

Funcs (G,G) is functional non empty set

[:O,(Funcs (G,G)):] is Relation-like set

bool [:O,(Funcs (G,G)):] is non empty set

bool G is non empty set

s2 is Element of bool G

s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]

bool G is non empty Element of bool (bool G)

bool (bool G) is non empty set

s19 is set

meet s19 is set

[#] G is non proper Element of bool G

p is set

p is Element of bool G

f1 is set

i is set

s199 is Element of bool G

[:G,G:] is Relation-like set

bool [:G,G:] is non empty set

f1 is Element of O

i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s1 . f1 is Relation-like Function-like set

s199 is set

i .: p is Element of bool G

s199 is set

i .: s199 is Element of bool G

f2 is Element of bool G

f1 is Element of bool G

f1 is Element of bool G

s19 is Element of bool G

s29 is Element of bool G

O is set

G is set

Funcs (G,G) is functional non empty set

[:O,(Funcs (G,G)):] is Relation-like set

bool [:O,(Funcs (G,G)):] is non empty set

s2 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O

len s2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

[:G,G:] is Relation-like set

bool [:G,G:] is non empty set

id G is Relation-like G -defined G -valued Function-like one-to-one total quasi_total Element of bool [:G,G:]

s1 is Relation-like O -defined Funcs (G,G) -valued Function-like total quasi_total Element of bool [:O,(Funcs (G,G)):]

s2 . 1 is set

s1 . (s2 . 1) is Relation-like Function-like set

s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s19 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

s29 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O

len s29 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s29 . 1 is set

s1 . (s29 . 1) is Relation-like Function-like set

Seg s19 is finite s19 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

{ b

s29 | (Seg s19) is Relation-like NAT -defined Seg s19 -defined NAT -defined O -valued Function-like finite FinSubsequence-like Element of bool [:NAT,O:]

[:NAT,O:] is Relation-like set

bool [:NAT,O:] is non empty set

p is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O

len p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

Seg (len s29) is finite len s29 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

{ b

dom s29 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

rng s29 is finite Element of bool O

bool O is non empty set

dom s1 is Element of bool O

rng s1 is functional Element of bool (Funcs (G,G))

bool (Funcs (G,G)) is non empty set

the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 is Relation-like Function-like Element of Funcs (G,G)

<*s199*> is Relation-like NAT -defined Funcs (G,G) -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on (Funcs (G,G))

1 -tuples_on (Funcs (G,G)) is FinSequenceSet of Funcs (G,G)

[1,s199] is set

{1,s199} is non empty finite set

{{1,s199},{1}} is non empty finite V39() set

{[1,s199]} is Relation-like Function-like constant non empty trivial finite 1 -element set

p is Relation-like Function-like set

dom p is set

rng p is set

len <*s199*> is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

<*s199*> . (len <*s199*>) is Relation-like Function-like set

<*s199*> . 1 is Relation-like Function-like set

f2 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set

<*s199*> . p is Relation-like Function-like set

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

s29 . (p + 1) is set

s1 . (s29 . (p + 1)) is Relation-like Function-like set

<*s199*> . (p + 1) is Relation-like Function-like set

the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] * the Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:] is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s29 . (s19 + 1) is set

s1 . (s29 . (s19 + 1)) is Relation-like Function-like set

0 + s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

Seg (s19 + 1) is non empty finite s19 + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of bool NAT

{ b

(Seg (s19 + 1)) /\ (Seg s19) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

dom s29 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

(dom s29) /\ (Seg s19) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

Seg (len s29) is finite len s29 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

{ b

rng s29 is finite Element of bool O

bool O is non empty set

dom s1 is Element of bool O

rng s1 is functional Element of bool (Funcs (G,G))

bool (Funcs (G,G)) is non empty set

s199 is Relation-like Function-like set

dom s199 is set

rng s199 is set

p . 1 is set

s1 . (p . 1) is Relation-like Function-like set

s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

len s199 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s199 . (len s199) is Relation-like Function-like set

s199 . 1 is Relation-like Function-like set

s199 . s19 is Relation-like Function-like set

Seg (len s199) is finite len s199 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

{ b

dom s199 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of bool NAT

H1 is Relation-like Function-like set

dom H1 is set

rng H1 is set

i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p * i is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

<*(p * i)*> is Relation-like NAT -defined bool [:G,G:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on (bool [:G,G:])

1 -tuples_on (bool [:G,G:]) is FinSequenceSet of bool [:G,G:]

[1,(p * i)] is set

{1,(p * i)} is non empty finite set

{{1,(p * i)},{1}} is non empty finite V39() set

{[1,(p * i)]} is Relation-like Function-like constant non empty trivial finite 1 -element set

s199 ^ <*(p * i)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

j is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

len j is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

j . (len j) is Relation-like Function-like set

j . 1 is Relation-like Function-like set

len <*(p * i)*> is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

(len p) + (len <*(p * i)*>) is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

(len s199) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

H2 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set

j . H2 is Relation-like Function-like set

H2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

s29 . (H2 + 1) is set

s1 . (s29 . (H2 + 1)) is Relation-like Function-like set

j . (H2 + 1) is Relation-like Function-like set

H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

H1 * s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 . H2 is Relation-like Function-like set

p . (H2 + 1) is set

s1 . (p . (H2 + 1)) is Relation-like Function-like set

s199 . (H2 + 1) is Relation-like Function-like set

s299 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s299 * H1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

1 + s19 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

s19 is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of O

len s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s19 . 1 is set

s1 . (s19 . 1) is Relation-like Function-like set

s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s19 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

len s19 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s19 . (len s19) is Relation-like Function-like set

s19 . 1 is Relation-like Function-like set

s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

p . (len s2) is Relation-like Function-like set

len p is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

p . 1 is Relation-like Function-like set

s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

f1 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

f1 . (len s2) is Relation-like Function-like set

len f1 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

f1 . 1 is Relation-like Function-like set

i is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal ext-real non negative set

p . i is Relation-like Function-like set

f1 . i is Relation-like Function-like set

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

p . (i + 1) is Relation-like Function-like set

f1 . (i + 1) is Relation-like Function-like set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V208() V209() V210() V211() V212() Element of NAT

s2 . (i + 1) is set

s1 . (s2 . (i + 1)) is Relation-like Function-like set

s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 * s199 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

f2 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

f2 * p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p . 0 is Relation-like Function-like set

f1 . 0 is Relation-like Function-like set

s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s29 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

p is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

i is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

i . (len s2) is Relation-like Function-like set

len i is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

i . 1 is Relation-like Function-like set

f1 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s199 is Relation-like NAT -defined Funcs (G,G) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (G,G)

s199 . (len s2) is Relation-like Function-like set

len s199 is epsilon-transitive epsilon-connected ordinal natural V31() V32() integer finite cardinal V46() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V210() V211() V212() Element of NAT

s199 . 1 is Relation-like Function-like set

O is 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 functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

O is set

the non empty set is non empty set

[: the non empty set , the non empty set :] is Relation-like non empty set

[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set

bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set

the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

Funcs ( the non empty set , the non empty set ) is functional non empty set

[:O,(Funcs ( the non empty set , the non empty set )):] is Relation-like set

bool [:O,(Funcs ( the non empty set , the non empty set )):] is non empty set

the Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):] is Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):]

(O, the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like O -defined Funcs ( the non empty set , the non empty set ) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the non empty set , the non empty set )):]) is (O) (O)

O is set

O is set

G is set

id G is Relation-like G -defined G -valued Function-like one-to-one total quasi_total Element of bool [:G,G:]

[:G,G:] is Relation-like set

bool [:G,G:] is non empty set

{(id G)} is functional non empty trivial finite 1 -element set

[:O,{(id G)}:] is Relation-like set

Funcs (G,G) is functional non empty set

[:O,(Funcs (G,G)):] is Relation-like set

bool [:O,(Funcs (G,G)):] is non empty set

s2 is set

s19 is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]

s2 is Relation-like O -defined Funcs (G,G) -valued Element of bool [:O,(Funcs (G,G)):]

dom s2 is Element of bool O

bool O is non empty set

s19 is set

s29 is set

p is set

[s19,p] is set

{s19,p} is non empty finite set

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

{{s19,p},{s19}} is non empty finite V39() set

s19 is set

s29 is set

[s19,s29] is set

{s19,s29} is non empty finite set

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

{{s19,s29},{s19}} is non empty finite V39() set

p is set

[s19,p] is set

{s19,p} is non empty finite set

{{s19,p},{s19}} is non empty finite V39() set

f1 is set

i is set

[f1,i] is set

{f1,i} is non empty finite set

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

{{f1,i},{f1}} is non empty finite V39() set

s199 is set

s199 is set

[s199,s199] is set

{s199,s199} is non empty finite set

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

{{s199,s199},{s199}} is non empty finite V39() set

s19 is Relation-like O -defined Funcs (G,G) -valued Function-like Element of bool [:O,(Funcs (G,G)):]

O is set

G is non empty strict unital Group-like associative multMagma

the carrier of G is non empty set

Funcs ( the carrier of G, the carrier of G) is functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier of G, the carrier of G:] is non empty set

{(id the carrier of G)} is functional non empty trivial finite 1 -element set

[:O,{(id the carrier of G)}:] is Relation-like set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

s1 is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]

(O, the carrier of G, the multF of G,s1) is (O) (O)

p is non empty (O)

1_ G is non being_of_order_0 Element of the carrier of G

f1 is non empty multMagma

the carrier of f1 is non empty set

s199 is Element of the carrier of f1

f2 is Element of the carrier of f1

p is Element of the carrier of G

p " is Element of the carrier of G

s199 is Element of the carrier of f1

f2 * s199 is Element of the carrier of f1

the multF of f1 is Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]

[: the carrier of f1, the carrier of f1:] is Relation-like non empty set

[:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is Relation-like non empty set

bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is non empty set

the multF of f1 . (f2,s199) is Element of the carrier of f1

p * (1_ G) is Element of the carrier of G

the multF of G . (p,(1_ G)) is Element of the carrier of G

s199 * f2 is Element of the carrier of f1

the multF of f1 . (s199,f2) is Element of the carrier of f1

(1_ G) * p is Element of the carrier of G

the multF of G . ((1_ G),p) is Element of the carrier of G

j is Element of the carrier of f1

j is Element of the carrier of f1

f2 * j is Element of the carrier of f1

the multF of f1 . (f2,j) is Element of the carrier of f1

p * (p ") is Element of the carrier of G

the multF of G . (p,(p ")) is Element of the carrier of G

j * f2 is Element of the carrier of f1

the multF of f1 . (j,f2) is Element of the carrier of f1

(p ") * p is Element of the carrier of G

the multF of G . ((p "),p) is Element of the carrier of G

the carrier of p is non empty set

the multF of p is Relation-like [: the carrier of p, the carrier of p:] -defined the carrier of p -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of p, the carrier of p:], the carrier of p:]

[: the carrier of p, the carrier of p:] is Relation-like non empty set

[:[: the carrier of p, the carrier of p:], the carrier of p:] is Relation-like non empty set

bool [:[: the carrier of p, the carrier of p:], the carrier of p:] is non empty set

multMagma(# the carrier of p, the multF of p #) is non empty strict multMagma

i is non empty unital Group-like associative multMagma

the carrier of i is non empty set

Funcs ( the carrier of i, the carrier of i) is functional non empty set

[:O,(Funcs ( the carrier of i, the carrier of i)):] is Relation-like set

bool [:O,(Funcs ( the carrier of i, the carrier of i)):] is non empty set

Funcs ( the carrier of p, the carrier of p) is functional non empty set

s199 is Relation-like O -defined Funcs ( the carrier of i, the carrier of i) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of i, the carrier of i)):]

the of p is Relation-like O -defined Funcs ( the carrier of p, the carrier of p) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of p, the carrier of p)):]

[:O,(Funcs ( the carrier of p, the carrier of p)):] is Relation-like set

bool [:O,(Funcs ( the carrier of p, the carrier of p)):] is non empty set

the multF of i is Relation-like [: the carrier of i, the carrier of i:] -defined the carrier of i -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]

[: the carrier of i, the carrier of i:] is Relation-like non empty set

[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like non empty set

bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is non empty set

multMagma(# the carrier of i, the multF of i #) is non empty strict multMagma

s199 is Element of O

dom s1 is Element of bool O

bool O is non empty set

s1 . s199 is Relation-like Function-like set

[s199,(s1 . s199)] is set

{s199,(s1 . s199)} is non empty finite set

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

{{s199,(s1 . s199)},{s199}} is non empty finite V39() set

id the carrier of i is Relation-like the carrier of i -defined the carrier of i -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of i, the carrier of i:]

bool [: the carrier of i, the carrier of i:] is non empty set

{(id the carrier of i)} is functional non empty trivial finite 1 -element set

[:O,{(id the carrier of i)}:] is Relation-like set

f2 is set

p is set

[f2,p] is set

{f2,p} is non empty finite set

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

{{f2,p},{f2}} is non empty finite V39() set

s199 . s199 is Relation-like Function-like set

i is Element of the carrier of f1

s199 is Element of the carrier of f1

s199 is Element of the carrier of f1

i * s199 is Element of the carrier of f1

the multF of f1 . (i,s199) is Element of the carrier of f1

(i * s199) * s199 is Element of the carrier of f1

the multF of f1 . ((i * s199),s199) is Element of the carrier of f1

f2 is Element of the carrier of G

p is Element of the carrier of G

f2 * p is Element of the carrier of G

the multF of G . (f2,p) is Element of the carrier of G

H1 is Element of the carrier of G

(f2 * p) * H1 is Element of the carrier of G

the multF of G . ((f2 * p),H1) is Element of the carrier of G

p * H1 is Element of the carrier of G

the multF of G . (p,H1) is Element of the carrier of G

f2 * (p * H1) is Element of the carrier of G

the multF of G . (f2,(p * H1)) is Element of the carrier of G

s199 * s199 is Element of the carrier of f1

the multF of f1 . (s199,s199) is Element of the carrier of f1

i * (s199 * s199) is Element of the carrier of f1

the multF of f1 . (i,(s199 * s199)) is Element of the carrier of f1

i is Element of the carrier of f1

O is set

the non empty strict unital Group-like associative multMagma is non empty strict unital Group-like associative multMagma

s1 is non empty (O)

the carrier of s1 is non empty set

the multF of s1 is Relation-like [: the carrier of s1, the carrier of s1:] -defined the carrier of s1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:]

[: the carrier of s1, the carrier of s1:] is Relation-like non empty set

[:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is Relation-like non empty set

bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is non empty set

multMagma(# the carrier of s1, the multF of s1 #) is non empty strict multMagma

O is set

s1 is Element of O

G is non empty unital Group-like associative (O) (O)

the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]

the carrier of G is non empty set

Funcs ( the carrier of G, the carrier of G) is functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

the of G . s1 is Relation-like Function-like set

[: the carrier of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier of G, the carrier of G:] is non empty set

id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

multMagma(# the carrier of G, the multF of G #) is non empty strict multMagma

s2 is non empty unital Group-like associative multMagma

the carrier of s2 is non empty set

the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]

[: the carrier of s2, the carrier of s2:] is Relation-like non empty set

[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set

bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set

multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma

Funcs ( the carrier of s2, the carrier of s2) is functional non empty set

[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set

s19 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]

bool [: the carrier of s2, the carrier of s2:] is non empty set

s19 . s1 is Relation-like Function-like set

s29 is Relation-like the carrier of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s2, the carrier of s2:]

f1 is Element of the carrier of G

i is Element of the carrier of G

p is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier of G, the carrier of G:]

f1 * i is Element of the carrier of G

the multF of G . (f1,i) is Element of the carrier of G

p . (f1 * i) is Element of the carrier of G

s199 is Element of the carrier of s2

s199 is Element of the carrier of s2

s199 * s199 is Element of the carrier of s2

the multF of s2 . (s199,s199) is Element of the carrier of s2

s29 . (s199 * s199) is Element of the carrier of s2

s29 . s199 is Element of the carrier of s2

s29 . s199 is Element of the carrier of s2

(s29 . s199) * (s29 . s199) is Element of the carrier of s2

the multF of s2 . ((s29 . s199),(s29 . s199)) is Element of the carrier of s2

p . f1 is Element of the carrier of G

p . i is Element of the carrier of G

the multF of G . ((p . f1),(p . i)) is Element of the carrier of G

(p . f1) * (p . i) is Element of the carrier of G

O is set

G is non empty unital Group-like associative (O) (O)

the carrier of G is non empty set

s2 is Element of O

(O,G,s2) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier of G, the carrier of G:] is non empty set

(O,G,s2) | the carrier of G is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]

O is set

G is non empty unital Group-like associative (O) (O)

the carrier of G is non empty set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]

Funcs ( the carrier of G, the carrier of G) is functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

(O, the carrier of G, the multF of G, the of G) is (O) (O)

1_ G is non being_of_order_0 Element of the carrier of G

s1 is non empty multMagma

the carrier of s1 is non empty set

s19 is Element of the carrier of s1

p is Element of the carrier of s1

f1 is Element of the carrier of G

f1 " is Element of the carrier of G

s29 is Element of the carrier of s1

p * s29 is Element of the carrier of s1

the multF of s1 is Relation-like [: the carrier of s1, the carrier of s1:] -defined the carrier of s1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:]

[: the carrier of s1, the carrier of s1:] is Relation-like non empty set

[:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is Relation-like non empty set

bool [:[: the carrier of s1, the carrier of s1:], the carrier of s1:] is non empty set

the multF of s1 . (p,s29) is Element of the carrier of s1

f1 * (1_ G) is Element of the carrier of G

the multF of G . (f1,(1_ G)) is Element of the carrier of G

s29 * p is Element of the carrier of s1

the multF of s1 . (s29,p) is Element of the carrier of s1

(1_ G) * f1 is Element of the carrier of G

the multF of G . ((1_ G),f1) is Element of the carrier of G

s199 is Element of the carrier of s1

s199 is Element of the carrier of s1

p * s199 is Element of the carrier of s1

the multF of s1 . (p,s199) is Element of the carrier of s1

f1 * (f1 ") is Element of the carrier of G

the multF of G . (f1,(f1 ")) is Element of the carrier of G

s199 * p is Element of the carrier of s1

the multF of s1 . (s199,p) is Element of the carrier of s1

(f1 ") * f1 is Element of the carrier of G

the multF of G . ((f1 "),f1) is Element of the carrier of G

s2 is Element of the carrier of s1

s19 is Element of the carrier of s1

s29 is Element of the carrier of s1

s2 * s19 is Element of the carrier of s1

the multF of s1 . (s2,s19) is Element of the carrier of s1

(s2 * s19) * s29 is Element of the carrier of s1

the multF of s1 . ((s2 * s19),s29) is Element of the carrier of s1

p is Element of the carrier of G

f1 is Element of the carrier of G

p * f1 is Element of the carrier of G

the multF of G . (p,f1) is Element of the carrier of G

i is Element of the carrier of G

(p * f1) * i is Element of the carrier of G

the multF of G . ((p * f1),i) is Element of the carrier of G

f1 * i is Element of the carrier of G

the multF of G . (f1,i) is Element of the carrier of G

p * (f1 * i) is Element of the carrier of G

the multF of G . (p,(f1 * i)) is Element of the carrier of G

s19 * s29 is Element of the carrier of s1

the multF of s1 . (s19,s29) is Element of the carrier of s1

s2 * (s19 * s29) is Element of the carrier of s1

the multF of s1 . (s2,(s19 * s29)) is Element of the carrier of s1

s19 is Element of the carrier of s1

s2 is non empty unital Group-like associative (O) (O)

the carrier of s2 is non empty set

Funcs ( the carrier of s2, the carrier of s2) is functional non empty set

the of s2 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]

[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set

the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]

[: the carrier of s2, the carrier of s2:] is Relation-like non empty set

[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set

bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set

multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma

s19 is non empty unital Group-like associative multMagma

the carrier of s19 is non empty set

Funcs ( the carrier of s19, the carrier of s19) is functional non empty set

[:O,(Funcs ( the carrier of s19, the carrier of s19)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):] is non empty set

s29 is Relation-like O -defined Funcs ( the carrier of s19, the carrier of s19) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):]

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma

s29 is Element of O

s19 is non empty unital Group-like associative (O) (O)

(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]

the carrier of s19 is non empty set

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

bool [: the carrier of s19, the carrier of s19:] is non empty set

the of s19 is Relation-like O -defined Funcs ( the carrier of s19, the carrier of s19) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):]

Funcs ( the carrier of s19, the carrier of s19) is functional non empty set

[:O,(Funcs ( the carrier of s19, the carrier of s19)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s19, the carrier of s19)):] is non empty set

the of s19 . s29 is Relation-like Function-like set

(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

bool [: the carrier of G, the carrier of G:] is non empty set

s29 is Element of O

s19 is non empty unital Group-like associative (O) (O)

the carrier of s19 is non empty set

(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

bool [: the carrier of s19, the carrier of s19:] is non empty set

id the carrier of s19 is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of s19, the carrier of s19:]

(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

bool [: the carrier of G, the carrier of G:] is non empty set

s29 is Element of O

s19 is non empty unital Group-like associative (O) (O)

the carrier of s19 is non empty set

(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

bool [: the carrier of s19, the carrier of s19:] is non empty set

(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

bool [: the carrier of G, the carrier of G:] is non empty set

s19 is non empty unital Group-like associative (O) (O)

the carrier of s19 is non empty set

s29 is Element of O

(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

bool [: the carrier of s19, the carrier of s19:] is non empty set

(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

bool [: the carrier of G, the carrier of G:] is non empty set

dom (O,s19,s29) is non empty Element of bool the carrier of s19

bool the carrier of s19 is non empty set

(O,G,s29) | the carrier of s19 is Relation-like the carrier of G -defined the carrier of s19 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]

dom the multF of G is Relation-like the carrier of G -defined the carrier of G -valued non empty Element of bool [: the carrier of G, the carrier of G:]

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

the multF of G || the carrier of s19 is set

the multF of G | [: the carrier of s19, the carrier of s19:] is Relation-like [: the carrier of s19, the carrier of s19:] -defined [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like set

O is set

G is non empty unital Group-like associative (O) (O)

the carrier of G is non empty set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]

Funcs ( the carrier of G, the carrier of G) is functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

(O, the carrier of G, the multF of G, the of G) is (O) (O)

s1 is non empty unital Group-like associative (O) (O,G)

O is set

G is non empty unital Group-like associative (O) (O)

s1 is non empty unital Group-like associative (O) (O) (O,G)

the carrier of s1 is non empty set

s2 is non empty unital Group-like associative (O) (O) (O,G)

the carrier of s2 is non empty set

the of s2 is Relation-like O -defined Funcs ( the carrier of s2, the carrier of s2) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):]

Funcs ( the carrier of s2, the carrier of s2) is functional non empty set

[:O,(Funcs ( the carrier of s2, the carrier of s2)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s2, the carrier of s2)):] is non empty set

dom the of s2 is Element of bool O

bool O is non empty set

the of s1 is Relation-like O -defined Funcs ( the carrier of s1, the carrier of s1) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of s1, the carrier of s1)):]

Funcs ( the carrier of s1, the carrier of s1) is functional non empty set

[:O,(Funcs ( the carrier of s1, the carrier of s1)):] is Relation-like set

bool [:O,(Funcs ( the carrier of s1, the carrier of s1)):] is non empty set

dom the of s1 is Element of bool O

p is set

f1 is Element of O

(O,s1,f1) is Relation-like the carrier of s1 -defined the carrier of s1 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s1, the carrier of s1:]

[: the carrier of s1, the carrier of s1:] is Relation-like non empty set

bool [: the carrier of s1, the carrier of s1:] is non empty set

the of s1 . f1 is Relation-like Function-like set

the carrier of G is non empty set

(O,G,f1) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

bool [: the carrier of G, the carrier of G:] is non empty set

(O,G,f1) | the carrier of s2 is Relation-like the carrier of s2 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]

(O,s2,f1) is Relation-like the carrier of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s2, the carrier of s2:]

[: the carrier of s2, the carrier of s2:] is Relation-like non empty set

bool [: the carrier of s2, the carrier of s2:] is non empty set

the of s1 . p is Relation-like Function-like set

the of s2 . p is Relation-like Function-like set

s19 is non empty unital Group-like associative Subgroup of G

the carrier of s19 is non empty set

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma

s29 is non empty unital Group-like associative Subgroup of G

the carrier of s29 is non empty set

the multF of s29 is Relation-like [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:]

[: the carrier of s29, the carrier of s29:] is Relation-like non empty set

[:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is Relation-like non empty set

bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is non empty set

multMagma(# the carrier of s29, the multF of s29 #) is non empty strict multMagma

O is set

G is non empty unital Group-like associative (O) (O)

1_ G is non being_of_order_0 Element of the carrier of G

the carrier of G is non empty set

{(1_ G)} is non empty trivial finite 1 -element set

(1). G is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of G

s2 is non empty (O)

the carrier of s2 is non empty set

the multF of s2 is Relation-like [: the carrier of s2, the carrier of s2:] -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:]

[: the carrier of s2, the carrier of s2:] is Relation-like non empty set

[:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is Relation-like non empty set

bool [:[: the carrier of s2, the carrier of s2:], the carrier of s2:] is non empty set

multMagma(# the carrier of s2, the multF of s2 #) is non empty strict multMagma

s19 is non empty unital Group-like associative (O) (O) (O)

the carrier of s19 is non empty set

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G || the carrier of s19 is set

the multF of G | [: the carrier of s19, the carrier of s19:] is Relation-like [: the carrier of s19, the carrier of s19:] -defined [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like set

s29 is Element of O

(O,s19,s29) is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of s19, the carrier of s19:]

bool [: the carrier of s19, the carrier of s19:] is non empty set

(O,G,s29) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total quasi_total unity-preserving multiplicative Element of bool [: the carrier of G, the carrier of G:]

bool [: the carrier of G, the carrier of G:] is non empty set

(O,G,s29) | the carrier of s19 is Relation-like the carrier of G -defined the carrier of s19 -defined the carrier of G -defined the carrier of G -valued Function-like Element of bool [: the carrier of G, the carrier of G:]

f1 is Relation-like Function-like set

dom f1 is set

id the carrier of s19 is Relation-like the carrier of s19 -defined the carrier of s19 -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of s19, the carrier of s19:]

(O,G,s29) * (id the carrier of s19) is Relation-like the carrier of s19 -defined the carrier of G -valued Function-like Element of bool [: the carrier of s19, the carrier of G:]

[: the carrier of s19, the carrier of G:] is Relation-like non empty set

bool [: the carrier of s19, the carrier of G:] is non empty set

dom ((O,G,s29) * (id the carrier of s19)) is Element of bool the carrier of s19

bool the carrier of s19 is non empty set

dom (O,G,s29) is non empty Element of bool the carrier of G

bool the carrier of G is non empty set

(dom (O,G,s29)) /\ the carrier of s19 is Element of bool the carrier of G

the carrier of G /\ the carrier of s19 is set

the carrier of ((1). G) is non empty trivial finite 1 -element set

i is set

dom (id the carrier of s19) is non empty Element of bool the carrier of s19

1_ s19 is non being_of_order_0 Element of the carrier of s19

p is Relation-like Function-like set

p . i is set

f1 . i is set

((O,G,s29) * (id the carrier of s19)) . i is set

(id the carrier of s19) . i is set

(O,G,s29) . ((id the carrier of s19) . i) is set

(O,G,s29) . i is set

dom p is set

s29 is non empty unital Group-like associative (O) (O) (O,G)

the carrier of s29 is non empty set

s1 is non empty unital Group-like associative (O) (O) (O,G)

the carrier of s1 is non empty set

s2 is non empty unital Group-like associative (O) (O) (O,G)

the carrier of s2 is non empty set

O is set

G is non empty unital Group-like associative (O) (O)

the carrier of G is non empty set

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is Relation-like non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the of G is Relation-like O -defined Funcs ( the carrier of G, the carrier of G) -valued Function-like total quasi_total Element of bool [:O,(Funcs ( the carrier of G, the carrier of G)):]

Funcs ( the carrier of G, the carrier of G) is functional non empty set

[:O,(Funcs ( the carrier of G, the carrier of G)):] is Relation-like set

bool [:O,(Funcs ( the carrier of G, the carrier of G)):] is non empty set

(O, the carrier of G, the multF of G, the of G) is (O) (O)

O is set

G is non empty unital Group-like associative (O) (O)

O is set

G is non empty unital Group-like associative (O) (O)

(O,G) is non empty unital Group-like associative (O) (O) (O,G)

p is non empty strict unital Group-like associative Subgroup of G

s19 is non empty unital Group-like associative (O) (O,G)

the carrier of s19 is non empty set

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma

s29 is non empty unital Group-like associative multMagma

(1). s29 is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of s29

the multF of ((1). s29) is Relation-like [: the carrier of ((1). s29), the carrier of ((1). s29):] -defined the carrier of ((1). s29) -valued Function-like non empty total quasi_total associative finite Element of bool [:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):]

the carrier of ((1). s29) is non empty trivial finite 1 -element set

[: the carrier of ((1). s29), the carrier of ((1). s29):] is Relation-like non empty finite set

[:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):] is Relation-like non empty finite set

bool [:[: the carrier of ((1). s29), the carrier of ((1). s29):], the carrier of ((1). s29):] is non empty finite V39() set

the multF of s29 is Relation-like [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:]

the carrier of s29 is non empty set

[: the carrier of s29, the carrier of s29:] is Relation-like non empty set

[:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is Relation-like non empty set

bool [:[: the carrier of s29, the carrier of s29:], the carrier of s29:] is non empty set

the multF of s29 || the carrier of ((1). s29) is set

the multF of s29 | [: the carrier of ((1). s29), the carrier of ((1). s29):] is Relation-like [: the carrier of ((1). s29), the carrier of ((1). s29):] -defined [: the carrier of s29, the carrier of s29:] -defined the carrier of s29 -valued Function-like finite set

1_ s29 is non being_of_order_0 Element of the carrier of s29

{(1_ s29)} is non empty trivial finite 1 -element set

the carrier of (O,G) is non empty set

O is set

G is non empty unital Group-like associative (O) (O)

s1 is non empty unital Group-like associative (O) (O,G)

(O,s1) is non empty unital Group-like associative (O) (O) (O,s1)

s2 is non empty unital Group-like associative (O) (O)

s19 is non empty unital Group-like associative (O) (O,s1)

the carrier of s19 is non empty set

the multF of s19 is Relation-like [: the carrier of s19, the carrier of s19:] -defined the carrier of s19 -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:]

[: the carrier of s19, the carrier of s19:] is Relation-like non empty set

[:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is Relation-like non empty set

bool [:[: the carrier of s19, the carrier of s19:], the carrier of s19:] is non empty set

multMagma(# the carrier of s19, the multF of s19 #) is non empty strict multMagma

s29 is non empty strict unital Group-like associative Subgroup of s1

the carrier of s29 is non empty set

p is non empty unital Group-like associative multMagma

1_ p is non being_of_order_0 Element of the carrier of p

the carrier of p is non empty set

{(1_ p)} is non empty trivial finite 1 -element set

(1). p is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of p

O is set

G is non empty unital Group-like associative (O) (O)

(O,G) is non empty unital Group-like associative (O) (O) (O,G)

s1 is non empty unital Group-like associative multMagma

s2 is non empty strict unital Group-like associative Subgroup of G

the carrier of (O,G) is non empty set

the multF of (O,G) is Relation-like [: the carrier of (O,G), the carrier of (O,G):] -defined the carrier of (O,G) -valued Function-like non empty total quasi_total associative Element of bool [:[: the carrier of (O,G), the