:: 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₁ where b₁ is Element of the carrier of G : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
{ b₁ where b₁ is Element of the carrier of G : not for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
G is non empty ()
(G) is set
the carrier of G is non empty set
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
(G) is set
{ b₁ where b₁ is Element of the carrier of G : not for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
(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₁ where b₁ is Element of the carrier of G : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
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₁ where b₁ is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G * : ( rng b₁ c= (G) & (G,<* the of G*>,b₁) ) } is 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 set
(G) is set
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
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₁ where b₁ is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G * : ( rng b₁ c= (G) & (G,<* the of G*>,b₁) ) } 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 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*>] where b₁ is Element of G : b₁ = b₁ } is 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
{ [G,<*b₁,G*>] where b₁ is Element of G : b₁ = b₁ } \/ {[G,{}]} is non empty set
X is non empty set
f is Element of X
{ [f,<*b₁,f*>] where b₁ is Element of G : b₁ = b₁ } is set
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₁ where b₁ is Element of the carrier of (G) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G),b₁,b₂) } is set
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₁ where b₁ is Element of the carrier of (G) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G),b₁,b₂) } is set
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₁ where b₁ is Relation-like NAT -defined the carrier of (G) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G) * : ( rng b₁ c= ((G)) & ((G),<* the of (G)*>,b₁) ) } is set
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₁ where b₁ is Element of the carrier of (G,X) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G,X),b₁,b₂) } is set
{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₁ where b₁ is Element of the carrier of (G,X) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G,X),b₁,b₂) } is set
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₁ where b₁ 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 b₁ c= ((G,X)) & ((G,X),<* the of (G,X)*>,b₁) ) } is set
<*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₁ where b₁ is Element of the carrier of (G,X) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G,X),b₁,b₂) } is set
{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₁ where b₁ is Element of the carrier of (G,X) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G,X),b₁,b₂) } is set
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₁ where b₁ 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 b₁ c= ((G,X)) & ((G,X),<* the of (G,X)*>,b₁) ) } is set
{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₁ where b₁ is Element of the carrier of (G) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G),b₁,b₂) } 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) * 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*>] where b₁ is Element of G : b₁ = b₁ } is 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
{ [G,<*b₁,G*>] where b₁ is Element of G : b₁ = b₁ } \/ {[G,{}]} is non empty set
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₁ where b₁ is Element of the carrier of (G) : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds ((G),b₁,b₂) } is set
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₁ where b₁ is Relation-like NAT -defined the carrier of (G) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G) * : ( rng b₁ c= ((G)) & ((G),<* the of (G)*>,b₁) ) } is set
G * is functional non empty FinSequence-membered M8(G)
succ G is non empty set
{G} is non empty trivial finite V40(1) set
G \/ {G} is non empty 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,<*b₁,G*>] where b₁ is Element of G : b₁ = b₁ } is 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
{ [G,<*b₁,G*>] where b₁ is Element of G : b₁ = b₁ } \/ {[G,{}]} is non empty set
x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
x + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
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 y is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
y ^ <* the of (G)*> 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 Function-like finite FinSequence-like FinSubsequence-like set
p is set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like set
x ^ <*p*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
rng <*p*> is non empty trivial finite V40(1) set
{p} is non empty trivial finite V40(1) set
a is Element of G
<*a,G*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set
[G,<*a,G*>] is set
{G,<*a,G*>} is non empty finite set
{{G,<*a,G*>},{G}} is non empty finite V37() set
x is Element of the carrier of (G)
<*x, the of (G)*> 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) *
q is Relation-like NAT -defined the carrier of (G) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G) *
q ^ <* the of (G)*> 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) *
q ^ <*x, the of (G)*> 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 constant non empty trivial finite V40(1) FinSequence-like FinSubsequence-like Element of the carrier of (G) *
<*x*> ^ <* the of (G)*> is Relation-like NAT -defined the carrier of (G) -valued Function-like non empty finite V40(1 + 1) 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
<*> 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 set
y is Relation-like NAT -defined the carrier of (G) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (G) *
rng y is finite Element of bool the carrier of (G)
bool the carrier of (G) is non empty set
x is set
y is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
rng y is finite Element of bool G
bool G is non empty 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) *
x ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ <* the of (G)*> 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) *
len p is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
p ^ <* the of (G)*> 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) *
len x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
(0) is non empty () ()
G is non empty () ()
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 non empty set
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
[0,{}] is set
{0,{}} is functional non empty finite V37() set
{0} is functional non empty trivial finite V37() V40(1) set
{{0,{}},{0}} is non empty finite V37() set
{[0,{}]} is Relation-like Function-like constant non empty trivial finite V40(1) set
{0} is functional non empty trivial finite V37() V40(1) Element of bool NAT
the of G 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 *
(G) is set
{ b₁ where b₁ is Element of the carrier of G : not for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
(G) is set
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
(G) is set
<* 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₁ where b₁ is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of G * : ( rng b₁ c= (G) & (G,<* the of G*>,b₁) ) } is set
X is Element of the carrier of G
G is non empty () ()
(G) is set
the carrier of G is non empty set
{ b₁ where b₁ is Element of the carrier of G : not for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds (G,b₁,b₂) } is set
bool the carrier of G is non empty 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
G is non empty set
X is non empty set
[:G,X:] is Relation-like non empty set
bool [:G,X:] is non empty set
f is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G
x is Relation-like G -defined X -valued Function-like non empty V14(G) V30(G,X) Element of bool [:G,X:]
f * x is Relation-like NAT -defined X -valued Function-like finite set
X * is functional non empty FinSequence-membered M8(X)
rng f is finite Element of bool G
bool G is non empty set
dom f is finite Element of bool NAT
[:(dom f),G:] is Relation-like set
bool [:(dom f),G:] is non empty set
y is Relation-like dom f -defined G -valued Function-like V14( dom f) V30( dom f,G) finite Element of bool [:(dom f),G:]
x * y is Relation-like dom f -defined X -valued Function-like V14( dom f) V30( dom f,X) finite Element of bool [:(dom f),X:]
[:(dom f),X:] is Relation-like set
bool [:(dom f),X:] is non empty set
rng (x * y) is finite Element of bool X
bool X is non empty set
len f is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
Seg (len f) is finite V40( len f) Element of bool NAT
dom (x * y) is finite Element of bool (dom f)
bool (dom f) is non empty finite V37() set
G is non empty set
X is non empty set
[:G,X:] is Relation-like non empty set
bool [:G,X:] is non empty set
G * is functional non empty FinSequence-membered M8(G)
X * is functional non empty FinSequence-membered M8(X)
[:(G *),(X *):] is Relation-like non empty set
bool [:(G *),(X *):] is non empty set
f is Relation-like G -defined X -valued Function-like non empty V14(G) V30(G,X) Element of bool [:G,X:]
x is Relation-like G * -defined X * -valued Function-like non empty V14(G * ) V30(G * ,X * ) Element of bool [:(G *),(X *):]
y is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
x . y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of X *
(G,X,y,f) is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like Element of X *
x is Relation-like G * -defined X * -valued Function-like non empty V14(G * ) V30(G * ,X * ) Element of bool [:(G *),(X *):]
y is Relation-like G * -defined X * -valued Function-like non empty V14(G * ) V30(G * ,X * ) Element of bool [:(G *),(X *):]
x is Relation-like NAT -defined G -valued Function-like finite FinSequence-like FinSubsequence-like Element of G *
x . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of X *
(G,X,x,f) is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like Element of X *
y . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of X *
G is Relation-like set
G [*] is Relation-like set
X is set
f is set
[X,f] is set
{X,f} is non empty finite set
{X} is non empty trivial finite V40(1) set
{{X,f},{X}} is non empty finite V37() set
<*X,f*> is Relation-like NAT -defined Function-like non empty finite V40(2) FinSequence-like FinSubsequence-like set
len <*X,f*> is non empty ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
<*X,f*> . 2 is set
field G is set
dom G is set
rng G is set
(dom G) \/ (rng G) is set
<*X,f*> . 1 is set
x is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() set
1 + 1 is non empty ext-real positive non negative V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
<*X,f*> . x is set
x + 1 is ext-real V21() epsilon-transitive epsilon-connected ordinal natural V29() finite V38() Element of NAT
<*X,f*> . (x + 1) is set
[(<*X,f*> . x),(<*X,f*> . (x + 1))] is set
{(<*X,f*> . x),(<*X,f*> . (x + 1))} is non empty finite set
{(<*X,f*> . x)} is non empty trivial finite V40(1) set
{{(<*X,f*> . x),(<*X,f*> . (x + 1))},{(<*X,f*> . x)}} is non empty finite V37() set
G is non empty set
[:G,G:] is Relation-like non empty set
bool [:G,G:] is non empty set
X is Relation-like G -defined G -valued Element of bool [:G,G:]
X [*] is Relation-like set
f is Relation-like G -defined G -valued Element of bool [:G,G:]
x is set
y is set
[x,y] is set
{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
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
G \/ G is non empty set
G is non empty ()
the carrier of G is non empty set
X is non empty set
[: the carrier of G,X:] is Relation-like non empty set
bool [: the carrier of G,X:] is non empty set
f is Relation-like the carrier of G -defined X -valued Function-like non empty V14( the carrier of G) V30( the carrier of G,X) Element of bool [: the carrier of G,X:]
the of G is Element of the carrier of G
f . the of G is Element of X
the carrier of G * is functional non empty FinSequence-membered M8( the carrier of G)
X * is functional non empty FinSequence-membered M8(X)
f ~ is Relation-like X -defined the carrier of G -valued Element of bool [:X, the carrier of G:]
[:X, the carrier of G:] is Relation-like non empty set
bool [:X, the carrier of G:] is non empty 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
(f ~) * the of G is Relation-like X -defined the carrier of G * -valued Element of bool [:X,( the carrier of G *):]
[:X,( the carrier of G *):] is Relation-like non empty set
bool [:X,( the carrier of G *):] is non empty set
( the carrier of G,X,f) is Relation-like the carrier of G * -defined X * -valued Function-like non empty V14( the carrier of G * ) V30( the carrier of G * ,X * ) Element of bool [:( the carrier of G *),(X *):]
[:( the carrier of G *),(X *):] is Relation-like non empty set
bool [:( the carrier of G *),(X *):] is non empty set
((f ~) * the of G) * ( the carrier of G,X,f) is Relation-like X -defined X * -valued Element of bool [:X,(X *):]
[:X,(X *):] is Relation-like non empty set
bool [:X,(X *):] is non empty set
(X,(f . the of G),(((f ~) * the of G) * ( the carrier of G,X,f))) is () ()