:: LANG1 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V38() V39() Element of bool REAL

bool REAL is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V38() V39() set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

COMPLEX is set

RAT is set

INT is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

2 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

3 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

Seg 1 is non empty trivial finite V40(1) Element of bool NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

the non empty set is non empty set

the non empty set * is functional non empty FinSequence-membered M8( 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 *):] is non empty set

the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):] is Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]

( the non empty set , the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]) is () ()

the carrier of ( the non empty set , the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]) is set

the non empty set is non empty set

the non empty set * is functional non empty FinSequence-membered M8( 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 *):] is non empty set

the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):] is Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]

the Element of the non empty set is Element of the non empty set

( the non empty set , the Element of the non empty set , the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]) is () ()

the carrier of ( the non empty set , the Element of the non empty set , the Relation-like the non empty set -defined the non empty set * -valued Element of bool [: the non empty set ,( the non empty set *):]) is set

G is non empty ()

the carrier of G is non empty set

G is non empty ()

the carrier of G is non empty set

{ b

{ b

G is non empty ()

(G) is set

the carrier of G is non empty set

{ b

(G) is set

{ b

(G) \/ (G) is set

X is set

f is Element of the carrier of G

x is Element of the carrier of G

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X is set

f is Element of the carrier of G

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Element of the carrier of G

<*X*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ <*X*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(x ^ <*X*>) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(x ^ f) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Element of the carrier of G

<*X*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

<*> the carrier of G is Relation-like non-empty empty-yielding NAT -defined the carrier of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of G *

x is Relation-like non-empty empty-yielding NAT -defined the carrier of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of G *

y is Relation-like non-empty empty-yielding NAT -defined the carrier of G -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(x ^ x) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ <*X*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite V40({} + 1) FinSequence-like FinSubsequence-like Element of the carrier of G *

{} + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(x ^ <*X*>) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Element of the carrier of G

<*X*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

p is Element of the carrier of G

<*p*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ <*p*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(x ^ <*p*>) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(x ^ x) ^ y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

len <*p*> is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

len (x ^ <*p*>) is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

len x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len x) + (len <*p*>) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

len <*X*> is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

len y is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len (x ^ <*p*>)) + (len y) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

1 + 0 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len x) + (len y) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

1 + ((len x) + (len y)) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

{} ^ x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*X*> . 1 is set

<*p*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

{} ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V40({} + 1) FinSequence-like FinSubsequence-like set

{} + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

X ^ f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

f ^ X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

X ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

q is Element of the carrier of G

<*q*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

y ^ <*q*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(y ^ <*q*>) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

p is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

y ^ p is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(y ^ p) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

X ^ y is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(X ^ y) ^ p is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

((X ^ y) ^ p) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(X ^ y) ^ <*q*> is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

((X ^ y) ^ <*q*>) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

X ^ (y ^ <*q*>) is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(X ^ (y ^ <*q*>)) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

X ^ (y ^ p) is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(X ^ (y ^ p)) ^ x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x ^ X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(y ^ p) ^ (x ^ X) is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(y ^ <*q*>) ^ (x ^ X) is Relation-like NAT -defined the carrier of G -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of G *

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

( the carrier of G *) * is functional non empty FinSequence-membered M8( the carrier of G * )

<*X*> is Relation-like NAT -defined the carrier of G * -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of ( the carrier of G *) *

f is Relation-like NAT -defined the carrier of G * -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of ( the carrier of G *) *

len f is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

f . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f . (len f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

f . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

f . (x + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

( the carrier of G *) * is functional non empty FinSequence-membered M8( the carrier of G * )

<*X,f*> is Relation-like NAT -defined the carrier of G * -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of ( the carrier of G *) *

x is Relation-like NAT -defined the carrier of G * -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of ( the carrier of G *) *

len x is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x . (len x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

y is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x . y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

y + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x . (y + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

p is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

1 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

x is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len y is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

y . 1 is set

y . (len y) is set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x . 1 is set

x . (len x) is set

p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

q is set

<*q*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set

p ^ <*q*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

p ^ y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len a is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

a . 1 is set

a . (len a) is set

len p is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

1 + (len p) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len p) + (len y) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

0 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

dom p is finite Element of bool NAT

p . 1 is set

dom y is finite Element of bool NAT

x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

a . x is set

x + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

a . (x + 1) is set

len <*q*> is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len p) + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x . x is set

x . (x + 1) is set

q is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

l is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

dom p is finite Element of bool NAT

p . x is set

a is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

b is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

q is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() set

(len x) + q is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

l is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

1 + l is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

(len p) + (1 + l) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

y . (1 + l) is set

(1 + l) + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

y . ((1 + l) + 1) is set

a is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

b is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

(len p) + ((1 + l) + 1) is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

a is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

b is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

1 + x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

dom p is finite Element of bool NAT

p . (x + 1) is set

x . x is set

x . (x + 1) is set

q is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

l is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

p . x is set

a is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

b is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

q is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

l is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

(G) is set

{ b

the of G is Element of the carrier of G

<* the of G*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

{ b

G is non empty ()

the carrier of G is non empty set

the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)

(G) is set

(G) is set

{ b

the of G is Element of the carrier of G

<* the of G*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of G *

{ b

X is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

rng X is finite Element of bool the carrier of G

bool the carrier of G is non empty set

f is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G *

rng f is finite Element of bool the carrier of G

G is non empty set

X is non empty set

[:G,X:] is Relation-like non empty set

f is Element of [:G,X:]

{f} is non empty trivial finite V40(1) set

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

{f} is Relation-like G -defined X -valued non empty trivial finite V40(1) Element of bool [:G,X:]

x is Element of [:G,X:]

{f,x} is non empty finite set

{f,x} is Relation-like G -defined X -valued non empty finite Element of bool [:G,X:]

G is set

{G} is non empty trivial finite V40(1) set

[G,{}] is set

{G,{}} is non empty finite set

{{G,{}},{G}} is non empty finite V37() set

{[G,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set

X is Element of {G}

{G} * is functional non empty FinSequence-membered M8({G})

<*> {G} is Relation-like non-empty empty-yielding NAT -defined {G} -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of {G} *

[X,(<*> {G})] is Element of [:{G},({G} *):]

[:{G},({G} *):] is Relation-like non empty set

{X,(<*> {G})} is non empty finite set

{X} is non empty trivial finite V40(1) set

{{X,(<*> {G})},{X}} is non empty finite V37() set

({G},({G} *),[X,(<*> {G})]) is Relation-like {G} -defined {G} * -valued Function-like constant non empty trivial finite V40(1) Element of bool [:{G},({G} *):]

bool [:{G},({G} *):] is non empty set

({G},X,({G},({G} *),[X,(<*> {G})])) is () ()

the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) is set

the of ({G},X,({G},({G} *),[X,(<*> {G})])) is Relation-like the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) -defined the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) * -valued Element of bool [: the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])),( the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) *):]

the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) * is functional non empty FinSequence-membered M8( the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])))

[: the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])),( the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) *):] is Relation-like set

bool [: the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])),( the carrier of ({G},X,({G},({G} *),[X,(<*> {G})])) *):] is non empty set

X is () ()

the carrier of X is set

the of X is Relation-like the carrier of X -defined the carrier of X * -valued Element of bool [: the carrier of X,( the carrier of X *):]

the carrier of X * is functional non empty FinSequence-membered M8( the carrier of X)

[: the carrier of X,( the carrier of X *):] is Relation-like set

bool [: the carrier of X,( the carrier of X *):] is non empty set

f is () ()

the carrier of f is set

the of f is Relation-like the carrier of f -defined the carrier of f * -valued Element of bool [: the carrier of f,( the carrier of f *):]

the carrier of f * is functional non empty FinSequence-membered M8( the carrier of f)

[: the carrier of f,( the carrier of f *):] is Relation-like set

bool [: the carrier of f,( the carrier of f *):] is non empty set

the of X is Element of the carrier of X

X is set

{G,X} is non empty finite set

<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set

[G,<*X*>] is set

{G,<*X*>} is non empty finite set

{{G,<*X*>},{G}} is non empty finite V37() set

{[G,<*X*>]} is Relation-like Function-like constant non empty trivial finite V40(1) set

f is Element of {G,X}

{G,X} * is functional non empty FinSequence-membered M8({G,X})

x is Element of {G,X}

<*x*> is Relation-like NAT -defined {G,X} -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of {G,X} *

[f,<*x*>] is Element of [:{G,X},({G,X} *):]

[:{G,X},({G,X} *):] is Relation-like non empty set

{f,<*x*>} is non empty finite set

{f} is non empty trivial finite V40(1) set

{{f,<*x*>},{f}} is non empty finite V37() set

({G,X},({G,X} *),[f,<*x*>]) is Relation-like {G,X} -defined {G,X} * -valued Function-like constant non empty trivial finite V40(1) Element of bool [:{G,X},({G,X} *):]

bool [:{G,X},({G,X} *):] is non empty set

({G,X},f,({G,X},({G,X} *),[f,<*x*>])) is () ()

the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) is set

the of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) is Element of the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>]))

the of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) is Relation-like the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) -defined the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) * -valued Element of bool [: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) *):]

the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) * is functional non empty FinSequence-membered M8( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])))

[: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) *):] is Relation-like set

bool [: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x*>])) *):] is non empty set

f is () ()

the carrier of f is set

the of f is Element of the carrier of f

the of f is Relation-like the carrier of f -defined the carrier of f * -valued Element of bool [: the carrier of f,( the carrier of f *):]

the carrier of f * is functional non empty FinSequence-membered M8( the carrier of f)

[: the carrier of f,( the carrier of f *):] is Relation-like set

bool [: the carrier of f,( the carrier of f *):] is non empty set

x is () ()

the carrier of x is set

the of x is Element of the carrier of x

the of x is Relation-like the carrier of x -defined the carrier of x * -valued Element of bool [: the carrier of x,( the carrier of x *):]

the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)

[: the carrier of x,( the carrier of x *):] is Relation-like set

bool [: the carrier of x,( the carrier of x *):] is non empty set

<*X,G*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set

[G,<*X,G*>] is set

{G,<*X,G*>} is non empty finite set

{{G,<*X,G*>},{G}} is non empty finite V37() set

{[G,<*X,G*>],[G,{}]} is Relation-like non empty finite set

f is Element of {G,X}

{G,X} * is functional non empty FinSequence-membered M8({G,X})

x is Element of {G,X}

<*x,f*> is Relation-like NAT -defined {G,X} -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of {G,X} *

[f,<*x,f*>] is Element of [:{G,X},({G,X} *):]

[:{G,X},({G,X} *):] is Relation-like non empty set

{f,<*x,f*>} is non empty finite set

{f} is non empty trivial finite V40(1) set

{{f,<*x,f*>},{f}} is non empty finite V37() set

<*> {G,X} is Relation-like non-empty empty-yielding NAT -defined {G,X} -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of {G,X} *

[f,(<*> {G,X})] is Element of [:{G,X},({G,X} *):]

{f,(<*> {G,X})} is non empty finite set

{{f,(<*> {G,X})},{f}} is non empty finite V37() set

({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})]) is Relation-like {G,X} -defined {G,X} * -valued non empty finite Element of bool [:{G,X},({G,X} *):]

bool [:{G,X},({G,X} *):] is non empty set

({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) is () ()

the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) is set

the of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) is Element of the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})]))

the of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) is Relation-like the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) -defined the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) * -valued Element of bool [: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) *):]

the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) * is functional non empty FinSequence-membered M8( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])))

[: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) *):] is Relation-like set

bool [: the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])),( the carrier of ({G,X},f,({G,X},({G,X} *),[f,<*x,f*>],[f,(<*> {G,X})])) *):] is non empty set

f is () ()

the carrier of f is set

the of f is Element of the carrier of f

the of f is Relation-like the carrier of f -defined the carrier of f * -valued Element of bool [: the carrier of f,( the carrier of f *):]

the carrier of f * is functional non empty FinSequence-membered M8( the carrier of f)

[: the carrier of f,( the carrier of f *):] is Relation-like set

bool [: the carrier of f,( the carrier of f *):] is non empty set

x is () ()

the carrier of x is set

the of x is Element of the carrier of x

the of x is Relation-like the carrier of x -defined the carrier of x * -valued Element of bool [: the carrier of x,( the carrier of x *):]

the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)

[: the carrier of x,( the carrier of x *):] is Relation-like set

bool [: the carrier of x,( the carrier of x *):] is non empty set

G is set

(G) is () ()

the carrier of (G) is set

{G} is non empty trivial finite V40(1) set

X is set

(G,X) is () ()

the carrier of (G,X) is set

{G,X} is non empty finite set

(G,X) is () ()

the carrier of (G,X) is set

{G,X} is non empty finite set

G is non empty set

succ G is non empty set

{G} is non empty trivial finite V40(1) set

G \/ {G} is non empty set

{ [G,<*b

[G,{}] is set

{G,{}} is non empty finite set

{{G,{}},{G}} is non empty finite V37() set

{[G,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set

{ [G,<*b

X is non empty set

f is Element of X

{ [f,<*b

X * is functional non empty FinSequence-membered M8(X)

[:X,(X *):] is Relation-like non empty set

y is set

x is Element of G

<*x,f*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set

[f,<*x,f*>] is set

{f,<*x,f*>} is non empty finite set

{f} is non empty trivial finite V40(1) set

{{f,<*x,f*>},{f}} is non empty finite V37() set

p is Element of X

<*p,f*> is Relation-like NAT -defined X -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of X *

[f,<*p,f*>] is Element of [:X,(X *):]

{f,<*p,f*>} is non empty finite set

{{f,<*p,f*>},{f}} is non empty finite V37() set

bool [:X,(X *):] is non empty set

y is Relation-like X -defined X * -valued Element of bool [:X,(X *):]

<*> X is Relation-like non-empty empty-yielding NAT -defined X -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of X *

[f,(<*> X)] is Element of [:X,(X *):]

{f,(<*> X)} is non empty finite set

{f} is non empty trivial finite V40(1) set

{{f,(<*> X)},{f}} is non empty finite V37() set

(X,(X *),[f,(<*> X)]) is Relation-like X -defined X * -valued Function-like constant non empty trivial finite V40(1) Element of bool [:X,(X *):]

y \/ (X,(X *),[f,(<*> X)]) is Relation-like X -defined X * -valued non empty Element of bool [:X,(X *):]

(X,f,(y \/ (X,(X *),[f,(<*> X)]))) is () ()

the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) is set

the of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) is Element of the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)])))

the of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) is Relation-like the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) -defined the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) * -valued Element of bool [: the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))),( the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) *):]

the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) * is functional non empty FinSequence-membered M8( the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))))

[: the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))),( the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) *):] is Relation-like set

bool [: the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))),( the carrier of (X,f,(y \/ (X,(X *),[f,(<*> X)]))) *):] is non empty set

X is () ()

the carrier of X is set

the of X is Element of the carrier of X

the of X is Relation-like the carrier of X -defined the carrier of X * -valued Element of bool [: the carrier of X,( the carrier of X *):]

the carrier of X * is functional non empty FinSequence-membered M8( the carrier of X)

[: the carrier of X,( the carrier of X *):] is Relation-like set

bool [: the carrier of X,( the carrier of X *):] is non empty set

f is () ()

the carrier of f is set

the of f is Element of the carrier of f

the of f is Relation-like the carrier of f -defined the carrier of f * -valued Element of bool [: the carrier of f,( the carrier of f *):]

the carrier of f * is functional non empty FinSequence-membered M8( the carrier of f)

[: the carrier of f,( the carrier of f *):] is Relation-like set

bool [: the carrier of f,( the carrier of f *):] is non empty set

G is non empty set

(G) is () ()

the carrier of (G) is set

succ G is non empty set

{G} is non empty trivial finite V40(1) set

G \/ {G} is non empty set

G is set

(G) is non empty () ()

((G)) is set

the carrier of (G) is non empty set

{ b

the Element of ((G)) is Element of ((G))

the of (G) is Relation-like the carrier of (G) -defined the carrier of (G) * -valued Element of bool [: the carrier of (G),( the carrier of (G) *):]

the carrier of (G) * is functional non empty FinSequence-membered M8( 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

[G,{}] is set

{G,{}} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,{}},{G}} is non empty finite V37() set

{[G,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set

x is Element of the carrier of (G)

<*> the carrier of (G) is Relation-like non-empty empty-yielding NAT -defined the carrier of (G) -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of (G) *

{{}} is functional non empty trivial finite V37() V40(1) set

G is set

(G) is non empty () ()

((G)) is set

the carrier of (G) is non empty set

the carrier of (G) * is functional non empty FinSequence-membered M8( the carrier of (G))

((G)) is set

{ b

the of (G) is Element of the carrier of (G)

<* the of (G)*> is Relation-like NAT -defined the carrier of (G) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G) *

{ b

f is set

x is Relation-like NAT -defined the carrier of (G) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G) *

rng x is finite Element of bool the carrier of (G)

bool the carrier of (G) is non empty set

f is set

the of (G) is Relation-like the carrier of (G) -defined the carrier of (G) * -valued 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

[G,{}] is set

{G,{}} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,{}},{G}} is non empty finite V37() set

{[G,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set

<*> the carrier of (G) is Relation-like non-empty empty-yielding NAT -defined the carrier of (G) -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of (G) *

rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

G is set

X is set

(G,X) is non empty () ()

((G,X)) is set

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

{ b

{X} is non empty trivial finite V40(1) set

the of (G,X) is Relation-like the carrier of (G,X) -defined the carrier of (G,X) * -valued Element of bool [: the carrier of (G,X),( the carrier of (G,X) *):]

the carrier of (G,X) * is functional non empty FinSequence-membered M8( the carrier of (G,X))

[: the carrier of (G,X),( the carrier of (G,X) *):] is Relation-like non empty set

bool [: the carrier of (G,X),( the carrier of (G,X) *):] is non empty set

<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set

[G,<*X*>] is set

{G,<*X*>} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,<*X*>},{G}} is non empty finite V37() set

{[G,<*X*>]} is Relation-like Function-like constant non empty trivial finite V40(1) set

{G,X} is non empty finite set

y is Element of the carrier of (G,X)

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

[y,x] is set

{y,x} is non empty finite set

{y} is non empty trivial finite V40(1) set

{{y,x},{y}} is non empty finite V37() set

x is Element of the carrier of (G,X)

<*y*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

[x,<*y*>] is Element of [: the carrier of (G,X),( the carrier of (G,X) *):]

{x,<*y*>} is non empty finite set

{x} is non empty trivial finite V40(1) set

{{x,<*y*>},{x}} is non empty finite V37() set

x is set

p is Element of the carrier of (G,X)

x is set

G is set

X is set

(G,X) is non empty () ()

((G,X)) is set

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

the carrier of (G,X) * is functional non empty FinSequence-membered M8( the carrier of (G,X))

((G,X)) is set

{ b

the of (G,X) is Element of the carrier of (G,X)

<* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

{ b

<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set

{<*X*>} is functional non empty trivial finite V37() V40(1) set

{G,X} is non empty finite set

the of (G,X) is Relation-like the carrier of (G,X) -defined the carrier of (G,X) * -valued Element of bool [: the carrier of (G,X),( the carrier of (G,X) *):]

[: the carrier of (G,X),( the carrier of (G,X) *):] is Relation-like non empty set

bool [: the carrier of (G,X),( the carrier of (G,X) *):] is non empty set

[G,<*X*>] is set

{G,<*X*>} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,<*X*>},{G}} is non empty finite V37() set

{[G,<*X*>]} is Relation-like Function-like constant non empty trivial finite V40(1) set

y is Element of the carrier of (G,X)

<*y*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

{X} is non empty trivial finite V40(1) set

x is set

p is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

rng p is finite Element of bool the carrier of (G,X)

bool the carrier of (G,X) is non empty set

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len q is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

q . 1 is set

q . (len q) is set

x is Element of the carrier of (G,X)

<*x*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

{x} is non empty trivial finite V40(1) Element of bool the carrier of (G,X)

1 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

q . (1 + 1) is set

a is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

x is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

[x,x] is Element of [: the carrier of (G,X),( the carrier of (G,X) *):]

{x,x} is non empty finite set

{x} is non empty trivial finite V40(1) set

{{x,x},{x}} is non empty finite V37() set

q . 2 is set

2 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

q . (2 + 1) is set

q is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

l is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

[y,l] is Element of [: the carrier of (G,X),( the carrier of (G,X) *):]

{y,l} is non empty finite set

{y} is non empty trivial finite V40(1) set

{{y,l},{y}} is non empty finite V37() set

x is set

rng <*X*> is non empty trivial finite V40(1) set

G is set

X is set

(G,X) is non empty () ()

((G,X)) is set

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

{ b

{X} is non empty trivial finite V40(1) set

{G,X} is non empty finite set

the of (G,X) is Relation-like the carrier of (G,X) -defined the carrier of (G,X) * -valued Element of bool [: the carrier of (G,X),( the carrier of (G,X) *):]

the carrier of (G,X) * is functional non empty FinSequence-membered M8( the carrier of (G,X))

[: the carrier of (G,X),( the carrier of (G,X) *):] is Relation-like non empty set

bool [: the carrier of (G,X),( the carrier of (G,X) *):] is non empty set

<*X,G*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set

[G,<*X,G*>] is set

{G,<*X,G*>} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,<*X,G*>},{G}} is non empty finite V37() set

[G,{}] is set

{G,{}} is non empty finite set

{{G,{}},{G}} is non empty finite V37() set

{[G,<*X,G*>],[G,{}]} is Relation-like non empty finite set

x is set

p is Element of the carrier of (G,X)

x is Element of the carrier of (G,X)

y is Element of the carrier of (G,X)

<*y,x*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

x is set

y is Element of the carrier of (G,X)

p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

[X,p] is set

{X,p} is non empty finite set

{{X,p},{X}} is non empty finite V37() set

G is set

X is set

(G,X) is non empty () ()

((G,X)) is set

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

the carrier of (G,X) * is functional non empty FinSequence-membered M8( the carrier of (G,X))

((G,X)) is set

{ b

the of (G,X) is Element of the carrier of (G,X)

<* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

{ b

{X} is non empty trivial finite V40(1) set

{X} * is functional non empty FinSequence-membered M8({X})

{G,X} is non empty finite set

y is set

x is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

rng x is finite Element of bool the carrier of (G,X)

bool the carrier of (G,X) is non empty set

the of (G,X) is Relation-like the carrier of (G,X) -defined the carrier of (G,X) * -valued Element of bool [: the carrier of (G,X),( the carrier of (G,X) *):]

[: the carrier of (G,X),( the carrier of (G,X) *):] is Relation-like non empty set

bool [: the carrier of (G,X),( the carrier of (G,X) *):] is non empty set

<*X,G*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set

[G,<*X,G*>] is set

{G,<*X,G*>} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,<*X,G*>},{G}} is non empty finite V37() set

[G,{}] is set

{G,{}} is non empty finite set

{{G,{}},{G}} is non empty finite V37() set

{[G,<*X,G*>],[G,{}]} is Relation-like non empty finite set

<*> the carrier of (G,X) is Relation-like non-empty empty-yielding NAT -defined the carrier of (G,X) -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of (G,X) *

y is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

y + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

len x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

x ^ <* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

q is set

<*q*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set

p ^ <*q*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

len p is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

rng <*q*> is non empty trivial finite V40(1) set

{q} is non empty trivial finite V40(1) set

a is Element of {X}

x is Element of the carrier of (G,X)

<*x, the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

q is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

q ^ <* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

q ^ <*x, the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

<*x*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

<*x*> ^ <* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite V40(1 + 1) FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

1 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

y is set

x is Relation-like NAT -defined {X} -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of {X}

rng x is trivial finite Element of bool {X}

bool {X} is non empty finite V37() set

p is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

p ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

p ^ <* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

q is Relation-like NAT -defined the carrier of (G,X) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

len q is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

q ^ <* the of (G,X)*> is Relation-like NAT -defined the carrier of (G,X) -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of (G,X) *

len p is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT

G is non empty set

(G) is non empty () ()

((G)) is set

the carrier of (G) is non empty set

{ b

the of (G) is Relation-like the carrier of (G) -defined the carrier of (G) * -valued Element of bool [: the carrier of (G),( the carrier of (G) *):]

the carrier of (G) * is functional non empty FinSequence-membered M8( 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

{ [G,<*b

[G,{}] is set

{G,{}} is non empty finite set

{G} is non empty trivial finite V40(1) set

{{G,{}},{G}} is non empty finite V37() set

{[G,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set

{ [G,<*b

succ G is non empty set

G \/ {G} is non empty set

x is set

y is Element of the carrier of (G)

f is Element of the carrier of (G)

<*> the carrier of (G) is Relation-like non-empty empty-yielding NAT -defined the carrier of (G) -valued Function-like one-to-one constant functional empty ext-real non positive non negative V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() finite finite-yielding V37() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of the carrier of (G) *

f is set

x is Element of G

y is Element of the carrier of (G)

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

[x,x] is set

{x,x} is non empty finite set

{x} is non empty trivial finite V40(1) set

{{x,x},{x}} is non empty finite V37() set

p is Element of G

<*p,G*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set

[G,<*p,G*>] is set

{G,<*p,G*>} is non empty finite set

{{G,<*p,G*>},{G}} is non empty finite V37() set

G is non empty set

(G) is non empty () ()

((G)) is set

the carrier of (G) is non empty set

the carrier of (G) * is functional non empty FinSequence-membered M8( the carrier of (G))

((G)) is set

{ b

the of (G) is Element of the carrier of (G)

<* the of (G)*> is Relation-like NAT -defined the carrier of (G) -valued Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the