:: FINTOPO6 semantic presentation

REAL is V68() V69() V70() V74() set
NAT is V68() V69() V70() V71() V72() V73() V74() Element of K32(REAL)
K32(REAL) is set
NAT is V68() V69() V70() V71() V72() V73() V74() set
K32(NAT) is set
K32(NAT) is set
COMPLEX is V68() V74() set
RAT is V68() V69() V70() V71() V74() set
INT is V68() V69() V70() V71() V72() V74() set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() set
the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() set
1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
{{},1} is non empty set
2 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
3 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Seg 1 is non empty V40() V47(1) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V39() V40() FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() ext-real non positive non negative V56() V57() V68() V69() V70() V71() V72() V73() V74() Element of NAT
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
(g \/ A) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g \/ A } is set
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(g ^b) \/ (A ^b) is Element of K32( the carrier of FT)
x1 is set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
FT is non empty RelStr
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
the carrier of FT is non empty set
K32( the carrier of FT) is set
({} FT) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses {} FT } is set
g is set
A is Element of the carrier of FT
U_FT A is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,A) is Element of K32( the carrier of FT)
FT is non empty RelStr
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
the carrier of FT is non empty set
K32( the carrier of FT) is set
({} FT) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses {} FT } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
x1 is set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
B0 is set
i is Element of the carrier of FT
U_FT i is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,i) is Element of K32( the carrier of FT)
(g ^b) /\ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
FT is RelStr
the carrier of FT is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
g is Element of the carrier of FT
U_FT g is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,g) is Element of K32( the carrier of FT)
Im ( the InternalRel of FT,g) is set
(Im ( the InternalRel of FT,g)) /\ the carrier of FT is set
FT is RelStr
the carrier of FT is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
RelStr(# the carrier of FT, the InternalRel of FT #) is strict RelStr
the carrier of RelStr(# the carrier of FT, the InternalRel of FT #) is set
A is Element of the carrier of RelStr(# the carrier of FT, the InternalRel of FT #)
U_FT A is Element of K32( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #))
K32( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #)) is set
the InternalRel of RelStr(# the carrier of FT, the InternalRel of FT #) is Relation-like Element of K32(K33( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #), the carrier of RelStr(# the carrier of FT, the InternalRel of FT #)))
K33( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #), the carrier of RelStr(# the carrier of FT, the InternalRel of FT #)) is Relation-like set
K32(K33( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #), the carrier of RelStr(# the carrier of FT, the InternalRel of FT #))) is set
K123( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #), the carrier of RelStr(# the carrier of FT, the InternalRel of FT #), the InternalRel of RelStr(# the carrier of FT, the InternalRel of FT #),A) is Element of K32( the carrier of RelStr(# the carrier of FT, the InternalRel of FT #))
Im ( the InternalRel of FT,A) is set
(Im ( the InternalRel of FT,A)) /\ the carrier of FT is set
FT is RelStr
the carrier of FT is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
RelStr(# the carrier of FT, the InternalRel of FT #) is strict RelStr
FT is non empty RelStr
the carrier of FT is non empty set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
RelStr(# the carrier of FT, the InternalRel of FT #) is strict RelStr
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
A is Element of the carrier of FT
Im ( the InternalRel of FT,A) is set
(Im ( the InternalRel of FT,A)) /\ g is Element of K32( the carrier of FT)
K33(g,g) is Relation-like set
K32(K33(g,g)) is set
A is Relation-like Element of K32(K33(g,g))
RelStr(# g,A #) is strict RelStr
the carrier of RelStr(# g,A #) is set
x2 is Element of the carrier of RelStr(# g,A #)
U_FT x2 is Element of K32( the carrier of RelStr(# g,A #))
K32( the carrier of RelStr(# g,A #)) is set
the InternalRel of RelStr(# g,A #) is Relation-like Element of K32(K33( the carrier of RelStr(# g,A #), the carrier of RelStr(# g,A #)))
K33( the carrier of RelStr(# g,A #), the carrier of RelStr(# g,A #)) is Relation-like set
K32(K33( the carrier of RelStr(# g,A #), the carrier of RelStr(# g,A #))) is set
K123( the carrier of RelStr(# g,A #), the carrier of RelStr(# g,A #), the InternalRel of RelStr(# g,A #),x2) is Element of K32( the carrier of RelStr(# g,A #))
Im ( the InternalRel of FT,x2) is set
(Im ( the InternalRel of FT,x2)) /\ the carrier of RelStr(# g,A #) is set
[#] RelStr(# g,A #) is non proper Element of K32( the carrier of RelStr(# g,A #))
K32( the carrier of RelStr(# g,A #)) is set
A is non empty strict (FT)
[#] A is non empty non proper Element of K32( the carrier of A)
the carrier of A is non empty set
K32( the carrier of A) is set
x1 is non empty strict (FT)
[#] x1 is non empty non proper Element of K32( the carrier of x1)
the carrier of x1 is non empty set
K32( the carrier of x1) is set
K33(g,g) is Relation-like set
K32(K33(g,g)) is set
the InternalRel of A is Relation-like Element of K32(K33( the carrier of A, the carrier of A))
K33( the carrier of A, the carrier of A) is Relation-like set
K32(K33( the carrier of A, the carrier of A)) is set
the InternalRel of x1 is Relation-like Element of K32(K33( the carrier of x1, the carrier of x1))
K33( the carrier of x1, the carrier of x1) is Relation-like set
K32(K33( the carrier of x1, the carrier of x1)) is set
x2 is Relation-like Element of K32(K33(g,g))
B0 is Relation-like Element of K32(K33(g,g))
i is set
Im (x2,i) is set
Im (B0,i) is set
y0 is Element of the carrier of A
U_FT y0 is Element of K32( the carrier of A)
K123( the carrier of A, the carrier of A, the InternalRel of A,y0) is Element of K32( the carrier of A)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
Im ( the InternalRel of FT,y0) is set
(Im ( the InternalRel of FT,y0)) /\ the carrier of A is set
x is Element of the carrier of x1
U_FT x is Element of K32( the carrier of x1)
K123( the carrier of x1, the carrier of x1, the InternalRel of x1,x) is Element of K32( the carrier of x1)
FT is non empty RelStr
g is non empty (FT)
the carrier of g is non empty set
A is Element of the carrier of g
U_FT A is Element of K32( the carrier of g)
K32( the carrier of g) is set
the InternalRel of g is Relation-like Element of K32(K33( the carrier of g, the carrier of g))
K33( the carrier of g, the carrier of g) is Relation-like set
K32(K33( the carrier of g, the carrier of g)) is set
K123( the carrier of g, the carrier of g, the InternalRel of g,A) is Element of K32( the carrier of g)
the carrier of FT is non empty set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
[#] g is non empty non proper Element of K32( the carrier of g)
(U_FT x1) /\ ([#] g) is Element of K32( the carrier of g)
FT is non empty reflexive RelStr
g is non empty (FT)
FT is non empty RelStr
g is non empty (FT)
the carrier of g is non empty set
x1 is Element of the carrier of g
A is Element of the carrier of g
U_FT A is Element of K32( the carrier of g)
K32( the carrier of g) is set
the InternalRel of g is Relation-like Element of K32(K33( the carrier of g, the carrier of g))
K33( the carrier of g, the carrier of g) is Relation-like set
K32(K33( the carrier of g, the carrier of g)) is set
K123( the carrier of g, the carrier of g, the InternalRel of g,A) is Element of K32( the carrier of g)
U_FT x1 is Element of K32( the carrier of g)
K123( the carrier of g, the carrier of g, the InternalRel of g,x1) is Element of K32( the carrier of g)
the carrier of FT is non empty set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
[#] g is non empty non proper Element of K32( the carrier of g)
(U_FT x2) /\ ([#] g) is Element of K32( the carrier of g)
B0 is Element of the carrier of FT
U_FT B0 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,B0) is Element of K32( the carrier of FT)
(U_FT B0) /\ ([#] g) is Element of K32( the carrier of g)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is (FT)
the carrier of g is set
K32( the carrier of g) is set
A is Element of K32( the carrier of g)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
(g `) ` is Element of K32( the carrier of FT)
the carrier of FT \ (g `) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^i is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : U_FT b₁ c= g } is set
A is Element of the carrier of FT
U_FT A is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,A) is Element of K32( the carrier of FT)
A is Element of the carrier of FT
U_FT A is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,A) is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
A is Element of the carrier of FT
U_FT A is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,A) is Element of K32( the carrier of FT)
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty (FT)
the carrier of g is non empty set
K32( the carrier of g) is set
[#] g is non empty non proper Element of K32( the carrier of g)
A is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(A ^b) /\ ([#] g) is Element of K32( the carrier of g)
x1 is Element of K32( the carrier of g)
x1 ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses x1 } is set
x2 is set
B0 is Element of the carrier of FT
U_FT B0 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,B0) is Element of K32( the carrier of FT)
y0 is set
i is Element of the carrier of g
U_FT i is Element of K32( the carrier of g)
the InternalRel of g is Relation-like Element of K32(K33( the carrier of g, the carrier of g))
K33( the carrier of g, the carrier of g) is Relation-like set
K32(K33( the carrier of g, the carrier of g)) is set
K123( the carrier of g, the carrier of g, the InternalRel of g,i) is Element of K32( the carrier of g)
(U_FT B0) /\ ([#] g) is Element of K32( the carrier of g)
B0 is set
x2 is non empty RelStr
the carrier of x2 is non empty set
i is Element of the carrier of x2
U_FT i is Element of K32( the carrier of x2)
K32( the carrier of x2) is set
the InternalRel of x2 is Relation-like Element of K32(K33( the carrier of x2, the carrier of x2))
K33( the carrier of x2, the carrier of x2) is Relation-like set
K32(K33( the carrier of x2, the carrier of x2)) is set
K123( the carrier of x2, the carrier of x2, the InternalRel of x2,i) is Element of K32( the carrier of x2)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
Im ( the InternalRel of FT,i) is set
(Im ( the InternalRel of FT,i)) /\ the carrier of g is set
y0 is Element of the carrier of FT
U_FT y0 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,y0) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty (FT)
the carrier of g is non empty set
K32( the carrier of g) is set
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of g)
B0 is Element of K32( the carrier of g)
x2 ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses x2 } is set
(x2 ^b) /\ B0 is Element of K32( the carrier of g)
B0 ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses B0 } is set
x2 /\ (B0 ^b) is Element of K32( the carrier of g)
[#] g is non empty non proper Element of K32( the carrier of g)
y0 is Element of K32( the carrier of FT)
y0 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses y0 } is set
([#] g) /\ (y0 ^b) is Element of K32( the carrier of FT)
x2 /\ (([#] g) /\ (y0 ^b)) is Element of K32( the carrier of FT)
x2 /\ ([#] g) is Element of K32( the carrier of g)
(x2 /\ ([#] g)) /\ (y0 ^b) is Element of K32( the carrier of FT)
i is Element of K32( the carrier of FT)
i /\ (y0 ^b) is Element of K32( the carrier of FT)
i ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses i } is set
(i ^b) /\ ([#] g) is Element of K32( the carrier of g)
((i ^b) /\ ([#] g)) /\ B0 is Element of K32( the carrier of g)
B0 /\ ([#] g) is Element of K32( the carrier of g)
(i ^b) /\ (B0 /\ ([#] g)) is Element of K32( the carrier of g)
(i ^b) /\ y0 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty (FT)
the carrier of g is non empty set
K32( the carrier of g) is set
[#] g is non empty non proper Element of K32( the carrier of g)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of g)
B0 is Element of K32( the carrier of g)
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
A /\ (x1 ^b) is Element of K32( the carrier of FT)
i is Element of K32( the carrier of g)
y0 is Element of K32( the carrier of g)
y0 ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses y0 } is set
i /\ (y0 ^b) is Element of K32( the carrier of g)
([#] g) /\ (x1 ^b) is Element of K32( the carrier of FT)
i /\ (([#] g) /\ (x1 ^b)) is Element of K32( the carrier of FT)
i /\ ([#] g) is Element of K32( the carrier of g)
(i /\ ([#] g)) /\ (x1 ^b) is Element of K32( the carrier of FT)
i ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses i } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(A ^b) /\ ([#] g) is Element of K32( the carrier of g)
(i ^b) /\ y0 is Element of K32( the carrier of g)
y0 /\ ([#] g) is Element of K32( the carrier of g)
(A ^b) /\ (y0 /\ ([#] g)) is Element of K32( the carrier of g)
(A ^b) /\ x1 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty Element of K32( the carrier of FT)
(FT,g) is non empty strict (FT)
[#] (FT,g) is non empty non proper Element of K32( the carrier of (FT,g))
the carrier of (FT,g) is non empty set
K32( the carrier of (FT,g)) is set
A is Element of K32( the carrier of (FT,g))
x1 is Element of K32( the carrier of (FT,g))
A \/ x1 is Element of K32( the carrier of (FT,g))
A ^b is Element of K32( the carrier of (FT,g))
{ b₁ where b₁ is Element of the carrier of (FT,g) : not U_FT b₁ misses A } is set
([#] (FT,g)) /\ x1 is Element of K32( the carrier of (FT,g))
x2 is Element of K32( the carrier of FT)
x2 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x2 } is set
B0 is Element of K32( the carrier of FT)
(A ^b) /\ x1 is Element of K32( the carrier of (FT,g))
(x2 ^b) /\ ([#] (FT,g)) is Element of K32( the carrier of (FT,g))
((x2 ^b) /\ ([#] (FT,g))) /\ x1 is Element of K32( the carrier of (FT,g))
(x2 ^b) /\ B0 is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
B0 is Element of K32( the carrier of (FT,g))
([#] (FT,g)) /\ B0 is Element of K32( the carrier of (FT,g))
x2 is Element of K32( the carrier of (FT,g))
x2 ^b is Element of K32( the carrier of (FT,g))
{ b₁ where b₁ is Element of the carrier of (FT,g) : not U_FT b₁ misses x2 } is set
(A ^b) /\ ([#] (FT,g)) is Element of K32( the carrier of (FT,g))
(A ^b) /\ x1 is Element of K32( the carrier of FT)
(x2 ^b) /\ B0 is Element of K32( the carrier of (FT,g))
FT is non empty reflexive RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is non empty Element of K32( the carrier of FT)
(FT,g) is non empty strict reflexive (FT)
[#] (FT,g) is non empty non proper Element of K32( the carrier of (FT,g))
the carrier of (FT,g) is non empty set
K32( the carrier of (FT,g)) is set
A is Element of K32( the carrier of (FT,g))
x1 is Element of K32( the carrier of (FT,g))
A \/ x1 is Element of K32( the carrier of (FT,g))
A ^b is Element of K32( the carrier of (FT,g))
{ b₁ where b₁ is Element of the carrier of (FT,g) : not U_FT b₁ misses A } is set
x2 is Element of K32( the carrier of FT)
B0 is Element of K32( the carrier of FT)
i is Element of K32( the carrier of FT)
y0 is Element of K32( the carrier of FT)
i \/ y0 is Element of K32( the carrier of FT)
i ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses i } is set
(i ^b) /\ ([#] (FT,g)) is Element of K32( the carrier of (FT,g))
([#] (FT,g)) /\ y0 is Element of K32( the carrier of FT)
(i ^b) /\ y0 is Element of K32( the carrier of FT)
((i ^b) /\ ([#] (FT,g))) /\ x1 is Element of K32( the carrier of (FT,g))
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of FT)
B0 is Element of K32( the carrier of FT)
x2 \/ B0 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^delta is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : ( not U_FT b<sub>1</sub> misses g & not U_FT b<sub>1</sub> misses g ` ) } is set
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
(g `) ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g ` } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g \/ (g `) is Element of K32( the carrier of FT)
[#] FT is non empty non proper Element of K32( the carrier of FT)
A is Element of the carrier of FT
U_FT A is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,A) is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^deltai is Element of K32( the carrier of FT)
g ^delta is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : ( not U_FT b₁ misses g & not U_FT b₁ misses g ` ) } is set
g /\ (g ^delta) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
x2 is set
B0 is Element of the carrier of FT
U_FT B0 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,B0) is Element of K32( the carrier of FT)
(g `) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g ` } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g \/ (g `) is Element of K32( the carrier of FT)
[#] FT is non empty non proper Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^deltao is Element of K32( the carrier of FT)
g ^delta is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : ( not U_FT b<sub>1</sub> misses g & not U_FT b<sub>1</sub> misses g ` ) } is set
(g `) /\ (g ^delta) is Element of K32( the carrier of FT)
(g `) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g ` } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
x2 is set
B0 is Element of the carrier of FT
U_FT B0 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,B0) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g } is set
A is set
x1 is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g \/ (g `) is Element of K32( the carrier of FT)
[#] FT is non empty non proper Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^deltai is Element of K32( the carrier of FT)
g ^delta is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : ( not U_FT b<sub>1</sub> misses g & not U_FT b<sub>1</sub> misses g ` ) } is set
g /\ (g ^delta) is Element of K32( the carrier of FT)
g ^deltao is Element of K32( the carrier of FT)
(g `) /\ (g ^delta) is Element of K32( the carrier of FT)
g /\ (g `) is Element of K32( the carrier of FT)
(g ^deltai) /\ (g ^deltao) is Element of K32( the carrier of FT)
(g ^delta) /\ (g `) is Element of K32( the carrier of FT)
g /\ ((g ^delta) /\ (g `)) is Element of K32( the carrier of FT)
(g /\ ((g ^delta) /\ (g `))) /\ (g ^delta) is Element of K32( the carrier of FT)
(g /\ (g `)) /\ (g ^delta) is Element of K32( the carrier of FT)
((g /\ (g `)) /\ (g ^delta)) /\ (g ^delta) is Element of K32( the carrier of FT)
FT is non empty reflexive RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^deltao is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^delta is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : ( not U_FT b₁ misses g & not U_FT b₁ misses g ` ) } is set
(g `) /\ (g ^delta) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
(g ^b) \ g is Element of K32( the carrier of FT)
(g `) ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g ` } is set
(g `) /\ ((g `) ^b) is Element of K32( the carrier of FT)
(g ^b) /\ ((g `) ^b) is Element of K32( the carrier of FT)
(g `) /\ ((g ^b) /\ ((g `) ^b)) is Element of K32( the carrier of FT)
(g ^b) /\ ((g `) /\ ((g `) ^b)) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g ^deltao is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^delta is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : ( not U_FT b₁ misses g & not U_FT b₁ misses g ` ) } is set
(g `) /\ (g ^delta) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
(g ^deltao) /\ A is Element of K32( the carrier of FT)
(g ^delta) /\ A is Element of K32( the carrier of FT)
(g `) /\ ((g ^delta) /\ A) is Element of K32( the carrier of FT)
(g `) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g ` } is set
(g ^b) /\ ((g `) ^b) is Element of K32( the carrier of FT)
((g ^b) /\ ((g `) ^b)) /\ A is Element of K32( the carrier of FT)
(g `) /\ (((g ^b) /\ ((g `) ^b)) /\ A) is Element of K32( the carrier of FT)
(g ^b) /\ A is Element of K32( the carrier of FT)
((g `) ^b) /\ ((g ^b) /\ A) is Element of K32( the carrier of FT)
(g `) /\ (((g `) ^b) /\ ((g ^b) /\ A)) is Element of K32( the carrier of FT)
((g `) ^b) /\ {} is Relation-like V68() V69() V70() V71() V72() V73() Element of K32( the carrier of FT)
(g `) /\ (((g `) ^b) /\ {}) is Relation-like V68() V69() V70() V71() V72() V73() Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g ^deltao is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
g ^delta is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : ( not U_FT b₁ misses g & not U_FT b₁ misses g ` ) } is set
(g `) /\ (g ^delta) is Element of K32( the carrier of FT)
A ^deltao is Element of K32( the carrier of FT)
A ` is Element of K32( the carrier of FT)
the carrier of FT \ A is set
A ^delta is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : ( not U_FT b<sub>1</sub> misses A & not U_FT b<sub>1</sub> misses A ` ) } is set
(A `) /\ (A ^delta) is Element of K32( the carrier of FT)
g /\ A is Element of K32( the carrier of FT)
(g ^deltao) /\ A is Element of K32( the carrier of FT)
(A ^deltao) /\ g is Element of K32( the carrier of FT)
(A ^delta) /\ g is Element of K32( the carrier of FT)
(A `) /\ ((A ^delta) /\ g) is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(A `) ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses A ` } is set
(A ^b) /\ ((A `) ^b) is Element of K32( the carrier of FT)
((A ^b) /\ ((A `) ^b)) /\ g is Element of K32( the carrier of FT)
(A `) /\ (((A ^b) /\ ((A `) ^b)) /\ g) is Element of K32( the carrier of FT)
(A ^b) /\ g is Element of K32( the carrier of FT)
((A `) ^b) /\ ((A ^b) /\ g) is Element of K32( the carrier of FT)
(A `) /\ (((A `) ^b) /\ ((A ^b) /\ g)) is Element of K32( the carrier of FT)
(A `) /\ ((A `) ^b) is Element of K32( the carrier of FT)
((A `) /\ ((A `) ^b)) /\ ((A ^b) /\ g) is Element of K32( the carrier of FT)
((A ^b) /\ g) /\ g is Element of K32( the carrier of FT)
A /\ g is Element of K32( the carrier of FT)
g /\ g is Element of K32( the carrier of FT)
(A ^b) /\ (g /\ g) is Element of K32( the carrier of FT)
(g ^delta) /\ A is Element of K32( the carrier of FT)
(g `) /\ ((g ^delta) /\ A) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
(g `) ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g ` } is set
(g ^b) /\ ((g `) ^b) is Element of K32( the carrier of FT)
((g ^b) /\ ((g `) ^b)) /\ A is Element of K32( the carrier of FT)
(g `) /\ (((g ^b) /\ ((g `) ^b)) /\ A) is Element of K32( the carrier of FT)
(g ^b) /\ A is Element of K32( the carrier of FT)
((g `) ^b) /\ ((g ^b) /\ A) is Element of K32( the carrier of FT)
(g `) /\ (((g `) ^b) /\ ((g ^b) /\ A)) is Element of K32( the carrier of FT)
(g `) /\ ((g `) ^b) is Element of K32( the carrier of FT)
((g `) /\ ((g `) ^b)) /\ ((g ^b) /\ A) is Element of K32( the carrier of FT)
((g ^b) /\ A) /\ A is Element of K32( the carrier of FT)
A /\ A is Element of K32( the carrier of FT)
(g ^b) /\ (A /\ A) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
g is Element of the carrier of FT
{g} is non empty Element of K32( the carrier of FT)
K32( the carrier of FT) is set
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses A } is set
x1 ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses x1 } is set
A /\ x1 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of the carrier of FT
{g} is non empty Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
the Element of the carrier of FT is Element of the carrier of FT
{ the Element of the carrier of FT} is non empty connected Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g /\ A is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses A } is set
g /\ (A ^b) is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g } is set
(g ^b) /\ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses A } is set
g ^b is Element of K32( the carrier of FT)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FT : not U_FT b<sub>1</sub> misses g } is set
A ` is Element of K32( the carrier of FT)
the carrier of FT \ A is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
g /\ (A ^b) is Element of K32( the carrier of FT)
x2 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x2 } is set
x1 /\ (x2 ^b) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
(g ^b) /\ A is Element of K32( the carrier of FT)
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
(x1 ^b) /\ x2 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
(g ^b) /\ A is Element of K32( the carrier of FT)
(g ^b) /\ (A \/ x1) is Element of K32( the carrier of FT)
(g ^b) /\ x1 is Element of K32( the carrier of FT)
((g ^b) /\ A) \/ ((g ^b) /\ x1) is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
g /\ (A ^b) is Element of K32( the carrier of FT)
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
(A \/ x1) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A \/ x1 } is set
g /\ ((A \/ x1) ^b) is Element of K32( the carrier of FT)
(A ^b) \/ (x1 ^b) is Element of K32( the carrier of FT)
g /\ ((A ^b) \/ (x1 ^b)) is Element of K32( the carrier of FT)
g /\ (x1 ^b) is Element of K32( the carrier of FT)
(g /\ (A ^b)) \/ (g /\ (x1 ^b)) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
g /\ A is Element of K32( the carrier of FT)
g /\ x1 is Element of K32( the carrier of FT)
(g /\ A) \/ (g /\ x1) is Element of K32( the carrier of FT)
g /\ (A \/ x1) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of FT)
x1 \/ x2 is Element of K32( the carrier of FT)
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
g /\ x1 is Element of K32( the carrier of FT)
g /\ x2 is Element of K32( the carrier of FT)
x2 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x2 } is set
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(g /\ x1) \/ (g /\ x2) is Element of K32( the carrier of FT)
g /\ (x1 \/ x2) is Element of K32( the carrier of FT)
A /\ x2 is Element of K32( the carrier of FT)
A /\ x1 is Element of K32( the carrier of FT)
(A /\ x2) \/ (A /\ x1) is Element of K32( the carrier of FT)
x2 \/ x1 is Element of K32( the carrier of FT)
A /\ (x2 \/ x1) is Element of K32( the carrier of FT)
(A /\ x1) \/ (A /\ x2) is Element of K32( the carrier of FT)
A /\ (x1 \/ x2) is Element of K32( the carrier of FT)
(A /\ x1) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A /\ x1 } is set
(g /\ x1) \/ (A /\ x1) is Element of K32( the carrier of FT)
(g \/ A) /\ x1 is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
(g /\ x2) \/ (g /\ x1) is Element of K32( the carrier of FT)
g /\ (x2 \/ x1) is Element of K32( the carrier of FT)
(A /\ x2) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A /\ x2 } is set
(g /\ x2) \/ (A /\ x2) is Element of K32( the carrier of FT)
(g \/ A) /\ x2 is Element of K32( the carrier of FT)
(g /\ x1) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g /\ x1 } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
A is Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of FT)
x1 \/ x2 is Element of K32( the carrier of FT)
x1 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 } is set
the Element of x2 is Element of x2
x2 \/ x1 is Element of K32( the carrier of FT)
i is Element of the carrier of FT
U_FT i is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,i) is Element of K32( the carrier of FT)
(U_FT i) /\ A is Element of K32( the carrier of FT)
the Element of (U_FT i) /\ A is Element of (U_FT i) /\ A
x is Element of the carrier of FT
U_FT x is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x) is Element of K32( the carrier of FT)
(U_FT x) /\ x2 is Element of K32( the carrier of FT)
x1 /\ A is Element of K32( the carrier of FT)
x2 /\ A is Element of K32( the carrier of FT)
g /\ A is Element of K32( the carrier of FT)
(x1 /\ A) \/ (x2 /\ A) is Element of K32( the carrier of FT)
the Element of x1 is Element of x1
h3 is Element of the carrier of FT
U_FT h3 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h3) is Element of K32( the carrier of FT)
(U_FT h3) /\ A is Element of K32( the carrier of FT)
the Element of (U_FT h3) /\ A is Element of (U_FT h3) /\ A
i is Element of the carrier of FT
U_FT i is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,i) is Element of K32( the carrier of FT)
(U_FT i) /\ x1 is Element of K32( the carrier of FT)
z2 is Element of the carrier of FT
U_FT z2 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,z2) is Element of K32( the carrier of FT)
i is set
z2 is Element of the carrier of FT
U_FT z2 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,z2) is Element of K32( the carrier of FT)
(x1 ^b) /\ x2 is Element of K32( the carrier of FT)
(x1 /\ A) ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x1 /\ A } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
([#] FT) \ g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
x2 is Element of K32( the carrier of FT)
B0 is Element of K32( the carrier of FT)
x2 \/ B0 is Element of K32( the carrier of FT)
g \/ (A \/ x1) is Element of K32( the carrier of FT)
(x2 \/ B0) \/ x1 is Element of K32( the carrier of FT)
B0 \/ x1 is Element of K32( the carrier of FT)
x2 \/ (B0 \/ x1) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
x2 \/ x1 is Element of K32( the carrier of FT)
B0 \/ (x2 \/ x1) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is non empty (FT)
the carrier of g is non empty set
K32( the carrier of g) is set
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of g)
y0 is Element of K32( the carrier of FT)
x is Element of K32( the carrier of FT)
y0 \/ x is Element of K32( the carrier of FT)
y0 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses y0 } is set
i is non empty RelStr
the carrier of i is non empty set
K32( the carrier of i) is set
x3 is Element of K32( the carrier of i)
h is Element of K32( the carrier of i)
h ^b is Element of K32( the carrier of i)
{ b₁ where b₁ is Element of the carrier of i : not U_FT b₁ misses h } is set
[#] i is non empty non proper Element of K32( the carrier of i)
(y0 ^b) /\ ([#] i) is Element of K32( the carrier of i)
(h ^b) /\ x3 is Element of K32( the carrier of i)
([#] i) /\ x is Element of K32( the carrier of FT)
(y0 ^b) /\ (([#] i) /\ x) is Element of K32( the carrier of FT)
(y0 ^b) /\ x is Element of K32( the carrier of FT)
B0 is non empty Element of K32( the carrier of g)
y0 is Element of K32( the carrier of g)
x is Element of K32( the carrier of g)
y0 \/ x is Element of K32( the carrier of g)
y0 ^b is Element of K32( the carrier of g)
{ b₁ where b₁ is Element of the carrier of g : not U_FT b₁ misses y0 } is set
h is Element of K32( the carrier of FT)
h ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses h } is set
(h ^b) /\ ([#] i) is Element of K32( the carrier of i)
x3 is Element of K32( the carrier of FT)
(h ^b) /\ x3 is Element of K32( the carrier of FT)
([#] i) /\ x is Element of K32( the carrier of g)
(h ^b) /\ (([#] i) /\ x) is Element of K32( the carrier of g)
(y0 ^b) /\ x is Element of K32( the carrier of g)
x2 is non empty Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
g ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses g } is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
g \/ A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
[#] FT is non empty non proper Element of K32( the carrier of FT)
g is Element of K32( the carrier of FT)
([#] FT) \ g is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
([#] FT) \ A is Element of K32( the carrier of FT)
x1 is non empty Element of K32( the carrier of FT)
(FT,x1) is non empty strict (FT)
the carrier of (FT,x1) is non empty set
K32( the carrier of (FT,x1)) is set
x2 is Element of K32( the carrier of (FT,x1))
[#] (FT,x1) is non empty non proper Element of K32( the carrier of (FT,x1))
(([#] FT) \ g) ` is Element of K32( the carrier of FT)
the carrier of FT \ (([#] FT) \ g) is set
B0 is Element of K32( the carrier of FT)
B0 ` is Element of K32( the carrier of FT)
the carrier of FT \ B0 is set
([#] FT) \ B0 is Element of K32( the carrier of FT)
g /\ x2 is Element of K32( the carrier of (FT,x1))
i is Element of K32( the carrier of FT)
y0 is Element of K32( the carrier of FT)
i \/ y0 is Element of K32( the carrier of FT)
y0 ` is Element of K32( the carrier of FT)
the carrier of FT \ y0 is set
g /\ i is Element of K32( the carrier of FT)
y0 /\ (y0 `) is Element of K32( the carrier of FT)
A \/ i is Element of K32( the carrier of FT)
(A \/ i) /\ g is Element of K32( the carrier of FT)
g /\ A is Element of K32( the carrier of FT)
(g /\ A) \/ (g /\ i) is Element of K32( the carrier of FT)
g ` is Element of K32( the carrier of FT)
the carrier of FT \ g is set
x is Element of K32( the carrier of (FT,x1))
x2 \/ i is set
A ` is Element of K32( the carrier of FT)
the carrier of FT \ A is set
A /\ (([#] FT) \ A) is Element of K32( the carrier of FT)
{} FT is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() connected Element of K32( the carrier of FT)
i ` is Element of K32( the carrier of FT)
the carrier of FT \ i is set
g /\ y0 is Element of K32( the carrier of FT)
i /\ (i `) is Element of K32( the carrier of FT)
A \/ y0 is Element of K32( the carrier of FT)
(A \/ y0) /\ g is Element of K32( the carrier of FT)
(g /\ A) \/ (g /\ y0) is Element of K32( the carrier of FT)
x is Element of K32( the carrier of (FT,x1))
x2 \/ y0 is set
FT is non empty RelStr
the carrier of FT is non empty set
FT is non empty RelStr
the carrier of FT is non empty set
g is Element of the carrier of FT
<*g*> is non empty Relation-like NAT -defined the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
[1,g] is set
{1,g} is non empty set
{1} is non empty V68() V69() V70() V71() V72() V73() set
{{1,g},{1}} is non empty set
{[1,g]} is non empty Relation-like Function-like set
len <*g*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is V35() V39() V51() V52() ext-real non negative set
x1 is Element of the carrier of FT
<*g*> . A is set
A + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
<*g*> . (A + 1) is set
U_FT x1 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
g is Element of the carrier of FT
<*g*> is non empty Relation-like NAT -defined the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
[1,g] is set
{1,g} is non empty set
{1} is non empty V68() V69() V70() V71() V72() V73() set
{{1,g},{1}} is non empty set
{[1,g]} is non empty Relation-like Function-like set
A is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
FT is non empty RelStr
the carrier of FT is non empty set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (len g) is set
x1 is Element of the carrier of FT
A is Element of the carrier of FT
U_FT x1 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x1) is Element of K32( the carrier of FT)
<*A*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is non empty Relation-like Function-like set
g ^ <*A*> is non empty Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
Seg (len g) is V40() V47( len g) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= len g ) } is set
len <*A*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len x2 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 is V35() V39() V51() V52() ext-real non negative set
x2 . B0 is set
B0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 . (B0 + 1) is set
i is Element of the carrier of FT
U_FT i is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,i) is Element of K32( the carrier of FT)
dom x2 is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
x2 /. (B0 + 1) is Element of the carrier of FT
g . (B0 + 1) is set
g . B0 is set
y0 is Element of the carrier of FT
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 is Element of the carrier of FT
y0 is Element of the carrier of FT
y0 is Element of the carrier of FT
len (g ^ <*A*>) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) + (len <*A*>) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
FT is non empty RelStr
the carrier of FT is non empty set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
A is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
A . 1 is set
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g /. (len g) is Element of the carrier of FT
U_FT (g /. (len g)) is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. (len g))) is Element of K32( the carrier of FT)
g ^ A is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g ^ A) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len A is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) + (len A) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x1 is V35() V39() V51() V52() ext-real non negative set
(g ^ A) . x1 is set
x1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g ^ A) . (x1 + 1) is set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
Seg (len g) is V40() V47( len g) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= len g ) } is set
dom (g ^ A) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(g ^ A) /. (x1 + 1) is Element of the carrier of FT
g . (x1 + 1) is set
g . x1 is set
g . (len g) is set
i is Element of the carrier of FT
(x1 + 1) - (len g) is V51() V52() ext-real set
A . ((x1 + 1) - (len g)) is set
x1 -' (len g) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x1 - (len g) is V51() V52() ext-real set
(x1 -' (len g)) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(x1 + 1) - (len g) is V51() V52() ext-real set
i is Element of the carrier of FT
A . ((x1 -' (len g)) + 1) is set
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A . (x1 -' (len g)) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of the carrier of FT
x1 is Element of the carrier of FT
FT is non empty RelStr
the carrier of FT is non empty set
g is Element of the carrier of FT
{g} is non empty connected Element of K32( the carrier of FT)
K32( the carrier of FT) is set
<*g*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,g] is set
{1,g} is non empty set
{{1,g},{1}} is non empty set
{[1,g]} is non empty Relation-like Function-like set
rng <*g*> is non empty Element of K32( the carrier of FT)
<*g*> . 1 is set
len <*g*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
<*g*> . (len <*g*>) is set
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of the carrier of FT
{g} is non empty connected Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of the carrier of FT
x1 is Element of the carrier of FT
{ b₁ where b₁ is Element of the carrier of FT : ( b₁ in g & ex b₂ being Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT st
( b₂ is (FT) & rng b₂ c= g & b₂ . 1 = A & b₂ . (len b₂) = b₁ ) ) } is set
x2 is set
B0 is Element of the carrier of FT
i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng i is Element of K32( the carrier of FT)
i . 1 is set
len i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i . (len i) is set
x2 is Element of K32( the carrier of FT)
g \ x2 is Element of K32( the carrier of FT)
x2 ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses x2 } is set
B0 is set
i is Element of the carrier of FT
U_FT i is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,i) is Element of K32( the carrier of FT)
y0 is set
x is Element of the carrier of FT
x3 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x3 is Element of K32( the carrier of FT)
x3 . 1 is set
len x3 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x3 . (len x3) is set
x3 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x3 is Element of K32( the carrier of FT)
x3 . 1 is set
len x3 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x3 . (len x3) is set
<*i*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is non empty Relation-like Function-like set
x3 ^ <*i*> is non empty Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
h is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng h is Element of K32( the carrier of FT)
rng <*i*> is non empty Element of K32( the carrier of FT)
(rng x3) \/ (rng <*i*>) is non empty Element of K32( the carrier of FT)
{i} is non empty connected (FT) Element of K32( the carrier of FT)
(rng x3) \/ {i} is non empty Element of K32( the carrier of FT)
dom x3 is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len x3) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
h . ((len x3) + 1) is set
h . 1 is set
U_FT x is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x) is Element of K32( the carrier of FT)
len h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len <*i*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len x3) + (len <*i*>) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
{A} is non empty connected (FT) Element of K32( the carrier of FT)
<*A*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is non empty Relation-like Function-like set
rng <*A*> is non empty Element of K32( the carrier of FT)
<*A*> . 1 is set
len <*A*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
<*A*> . (len <*A*>) is set
B0 is Element of the carrier of FT
i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng i is Element of K32( the carrier of FT)
i . 1 is set
len i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i . (len i) is set
x2 \/ (g \ x2) is Element of K32( the carrier of FT)
A is Element of K32( the carrier of FT)
x1 is Element of K32( the carrier of FT)
A \/ x1 is Element of K32( the carrier of FT)
A ^b is Element of K32( the carrier of FT)
{ b₁ where b₁ is Element of the carrier of FT : not U_FT b₁ misses A } is set
the Element of x1 is Element of x1
the Element of A is Element of A
y0 is Element of the carrier of FT
B0 is Element of the carrier of FT
x is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x is Element of K32( the carrier of FT)
x . 1 is set
len x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x . (len x) is set
x3 is V35() V39() V51() V52() ext-real non negative set
x . x3 is set
x3 is V35() V39() V51() V52() ext-real non negative set
x . x3 is set
x3 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom x is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
x . (x3 + 1) is set
s is Element of the carrier of FT
h is Element of the carrier of FT
U_FT h is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h) is Element of K32( the carrier of FT)
U_FT s is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,s) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
A is V35() V39() V51() V52() ext-real non negative set
g | A is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg A is V40() V47(A) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
g | (Seg A) is Relation-like NAT -defined Seg A -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g | A) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x1 is V35() V39() V51() V52() ext-real non negative set
(g | A) . x1 is set
x1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g | A) . (x1 + 1) is set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
g . x1 is set
g . (x1 + 1) is set
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
FT is non empty RelStr
the carrier of FT is non empty set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g /^ A is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(len g) - A is V51() V52() ext-real set
(len g) -' A is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g /^ A) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x1 is V35() V39() V51() V52() ext-real non negative set
(g /^ A) . x1 is set
x1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g /^ A) . (x1 + 1) is set
x2 is Element of the carrier of FT
U_FT x2 is Element of K32( the carrier of FT)
K32( the carrier of FT) is set
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,x2) is Element of K32( the carrier of FT)
1 + x1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ A) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
x1 + A is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (x1 + A) is set
(x1 + 1) + A is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(x1 + A) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((x1 + 1) + A) is set
((len g) - A) + A is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of the carrier of FT
<*A*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is non empty Relation-like Function-like set
rng <*A*> is non empty Element of K32( the carrier of FT)
<*A*> . 1 is set
len <*A*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
<*A*> . (len <*A*>) is set
{A} is non empty connected (FT) Element of K32( the carrier of FT)
x1 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x1 is Element of K32( the carrier of FT)
x1 . 1 is set
len x1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x1 . (len x1) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng g is Element of K32( the carrier of FT)
g . 1 is set
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (len g) is set
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng i is Element of K32( the carrier of FT)
i . 1 is set
len i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i . (len i) is set
B0 is V35() V39() V51() V52() ext-real non negative set
B0 is V35() V39() V51() V52() ext-real non negative set
i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng i is Element of K32( the carrier of FT)
i . 1 is set
len i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i . (len i) is set
i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng i is Element of K32( the carrier of FT)
i . 1 is set
len i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i . (len i) is set
y0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng y0 is Element of K32( the carrier of FT)
y0 . 1 is set
len y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 . (len y0) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of the carrier of FT
x1 is Element of the carrier of FT
x2 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x2 is Element of K32( the carrier of FT)
x2 . 1 is set
len x2 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 . (len x2) is set
x2 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x2 is Element of K32( the carrier of FT)
x2 . 1 is set
len x2 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 . (len x2) is set
A is Element of the carrier of FT
x1 is Element of the carrier of FT
x2 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
x2 . 1 is set
len x2 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 . (len x2) is set
rng x2 is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Element of K32( the carrier of FT)
A is Element of the carrier of FT
x1 is Element of the carrier of FT
x2 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng x2 is Element of K32( the carrier of FT)
x2 . 1 is set
len x2 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x2 . (len x2) is set
B0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng B0 is Element of K32( the carrier of FT)
B0 . 1 is set
len B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 . (len B0) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | B0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg B0 is V40() V47(B0) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= B0 ) } is set
g | (Seg B0) is Relation-like NAT -defined Seg B0 -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
rng (g | B0) is Element of K32( the carrier of FT)
(g | B0) . 1 is set
len (g | B0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g | B0) . (len (g | B0)) is set
g /. B0 is Element of the carrier of FT
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
rng g is Element of K32( the carrier of FT)
g . 1 is set
g . B0 is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g /^ B0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng (g /^ B0) is Element of K32( the carrier of FT)
(g /^ B0) . 1 is set
1 + B0 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g /. (1 + B0) is Element of the carrier of FT
len (g /^ B0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g /^ B0) . (len (g /^ B0)) is set
(len g) - B0 is V51() V52() ext-real set
rng g is Element of K32( the carrier of FT)
B0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len g) -' B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ B0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
g . (1 + B0) is set
((len g) -' B0) + B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((len g) -' B0) + B0) is set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
rng g is Element of K32( the carrier of FT)
g . (len g) is set
B0 is V35() V39() V51() V52() ext-real non negative set
g | B0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg B0 is V40() V47(B0) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= B0 ) } is set
g | (Seg B0) is Relation-like NAT -defined Seg B0 -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
g /. B0 is Element of the carrier of FT
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg i is V40() V47(i) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
g | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
(g | i) . 1 is set
len (g | i) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(g | i) . (len (g | i)) is set
g /. i is Element of the carrier of FT
rng (g | i) is Element of K32( the carrier of FT)
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
g . i is set
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g /^ i is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(g /^ i) . 1 is set
g . (i + 1) is set
rng (g /^ i) is Element of K32( the carrier of FT)
y0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng y0 is Element of K32( the carrier of FT)
y0 . 1 is set
len y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 . (len y0) is set
y0 ^ (g /^ i) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
x is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g /^ i) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len y0) + (len (g /^ i)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
rng x is Element of K32( the carrier of FT)
(rng y0) \/ (rng (g /^ i)) is Element of K32( the carrier of FT)
dom (g /^ i) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
x . (len x) is set
(g /^ i) . (len (g /^ i)) is set
dom y0 is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
x . 1 is set
y0 /. (len y0) is Element of the carrier of FT
U_FT (y0 /. (len y0)) is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(y0 /. (len y0))) is Element of K32( the carrier of FT)
(g | i) ^ (g /^ i) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(len (g | i)) + (len (g /^ i)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng B0 is Element of K32( the carrier of FT)
B0 . 1 is set
len B0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 . (len B0) is set
rng g is Element of K32( the carrier of FT)
g . 1 is set
g . (len g) is set
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
B0 is set
i is set
g . B0 is set
g . i is set
Seg (len g) is V40() V47( len g) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= len g ) } is set
y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) -' y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | x is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg x is V40() V47(x) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
g | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
g /^ y0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(g | x) ^ (g /^ y0) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g /^ y0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) - y0 is V51() V52() ext-real set
len (g | x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | x) ^ (g /^ y0)) . 1 is set
(g | x) . 1 is set
len ((g | x) ^ (g /^ y0)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | x)) + (len (g /^ y0)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x + ((len g) - y0) is V51() V52() ext-real set
y0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(y0 + 1) - y0 is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s is V35() V39() V51() V52() ext-real non negative set
((g | x) ^ (g /^ y0)) . s is set
s + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | x) ^ (g /^ y0)) . (s + 1) is set
h3 is Element of the carrier of FT
U_FT h3 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h3) is Element of K32( the carrier of FT)
z1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom ((g | x) ^ (g /^ y0)) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
((g | x) ^ (g /^ y0)) . (z1 + 1) is set
((g | x) ^ (g /^ y0)) /. (z1 + 1) is Element of the carrier of FT
i is Element of the carrier of FT
(g | x) . (z1 + 1) is set
g . (z1 + 1) is set
(g | x) . z1 is set
g . z1 is set
(x + ((len g) - y0)) - x is V51() V52() ext-real set
z1 - x is V51() V52() ext-real set
z1 -' x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((len g) - y0) + y0 is V51() V52() ext-real set
(z1 -' x) + y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | x)) + (z1 -' x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x + (z1 - x) is V51() V52() ext-real set
dom (g /^ y0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(g /^ y0) . (z1 -' x) is set
g . ((z1 -' x) + y0) is set
(g | x) . x is set
0 + y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (0 + y0) is set
g . ((z1 -' x) + y0) is set
g . ((z1 -' x) + y0) is set
g . ((z1 -' x) + y0) is set
(z1 -' x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ y0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | x)) + ((z1 -' x) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(z1 - x) + 1 is V51() V52() ext-real set
((z1 - x) + 1) + x is V51() V52() ext-real set
i is Element of the carrier of FT
(g /^ y0) . ((z1 -' x) + 1) is set
((z1 -' x) + 1) + y0 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' x) + 1) + y0) is set
((z1 -' x) + y0) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' x) + y0) + 1) is set
i is Element of the carrier of FT
i is Element of the carrier of FT
rng (g /^ y0) is Element of K32( the carrier of FT)
rng ((g | x) ^ (g /^ y0)) is Element of K32( the carrier of FT)
rng (g | x) is Element of K32( the carrier of FT)
(rng (g | x)) \/ (rng (g /^ y0)) is Element of K32( the carrier of FT)
((len g) -' y0) + y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ y0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | x)) + ((len g) -' y0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | x) ^ (g /^ y0)) . ((len (g | x)) + ((len g) -' y0)) is set
(g /^ y0) . ((len g) -' y0) is set
((g | x) ^ (g /^ y0)) . (len ((g | x) ^ (g /^ y0))) is set
(len g) - x is V51() V52() ext-real set
(x + ((len g) - y0)) - x is V51() V52() ext-real set
s is V35() V39() V51() V52() ext-real non negative set
((g | x) ^ (g /^ y0)) . s is set
s + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | x) ^ (g /^ y0)) . (s + 1) is set
h3 is Element of the carrier of FT
U_FT h3 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h3) is Element of K32( the carrier of FT)
z1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom ((g | x) ^ (g /^ y0)) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
((g | x) ^ (g /^ y0)) . (z1 + 1) is set
((g | x) ^ (g /^ y0)) /. (z1 + 1) is Element of the carrier of FT
i is Element of the carrier of FT
(g | x) . (z1 + 1) is set
g . (z1 + 1) is set
(g | x) . z1 is set
g . z1 is set
(x + ((len g) - y0)) - x is V51() V52() ext-real set
z1 - x is V51() V52() ext-real set
z1 -' x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((len g) - y0) + y0 is V51() V52() ext-real set
(z1 -' x) + y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | x)) + (z1 -' x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x + (z1 - x) is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ y0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(g /^ y0) . (z1 -' x) is set
g . ((z1 -' x) + y0) is set
(g | x) . x is set
0 + y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (0 + y0) is set
g . ((z1 -' x) + y0) is set
g . ((z1 -' x) + y0) is set
g . ((z1 -' x) + y0) is set
(z1 -' x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ y0) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | x)) + ((z1 -' x) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(z1 - x) + 1 is V51() V52() ext-real set
((z1 - x) + 1) + x is V51() V52() ext-real set
i is Element of the carrier of FT
(g /^ y0) . ((z1 -' x) + 1) is set
((z1 -' x) + 1) + y0 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' x) + 1) + y0) is set
((z1 -' x) + y0) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' x) + y0) + 1) is set
rng (g | x) is Element of K32( the carrier of FT)
(g | x) ^ {} is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
((g | x) ^ (g /^ y0)) . (len ((g | x) ^ (g /^ y0))) is set
(len g) - x is V51() V52() ext-real set
(x + ((len g) - y0)) - x is V51() V52() ext-real set
(len g) -' x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | y0 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg y0 is V40() V47(y0) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= y0 ) } is set
g | (Seg y0) is Relation-like NAT -defined Seg y0 -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
g /^ x is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(g | y0) ^ (g /^ x) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g /^ x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) - x is V51() V52() ext-real set
len (g | y0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | y0) ^ (g /^ x)) . 1 is set
(g | y0) . 1 is set
len ((g | y0) ^ (g /^ x)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | y0)) + (len (g /^ x)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 + ((len g) - x) is V51() V52() ext-real set
x + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(x + 1) - x is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s is V35() V39() V51() V52() ext-real non negative set
((g | y0) ^ (g /^ x)) . s is set
s + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | y0) ^ (g /^ x)) . (s + 1) is set
h3 is Element of the carrier of FT
U_FT h3 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h3) is Element of K32( the carrier of FT)
z1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom ((g | y0) ^ (g /^ x)) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
((g | y0) ^ (g /^ x)) . (z1 + 1) is set
((g | y0) ^ (g /^ x)) /. (z1 + 1) is Element of the carrier of FT
i is Element of the carrier of FT
(g | y0) . (z1 + 1) is set
g . (z1 + 1) is set
(g | y0) . z1 is set
g . z1 is set
(y0 + ((len g) - x)) - y0 is V51() V52() ext-real set
z1 - y0 is V51() V52() ext-real set
z1 -' y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((len g) - x) + x is V51() V52() ext-real set
(z1 -' y0) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | y0)) + (z1 -' y0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 + (z1 - y0) is V51() V52() ext-real set
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(g /^ x) . (z1 -' y0) is set
g . ((z1 -' y0) + x) is set
(g | y0) . y0 is set
0 + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (0 + x) is set
g . ((z1 -' y0) + x) is set
g . ((z1 -' y0) + x) is set
g . ((z1 -' y0) + x) is set
(z1 -' y0) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | y0)) + ((z1 -' y0) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(z1 - y0) + 1 is V51() V52() ext-real set
((z1 - y0) + 1) + y0 is V51() V52() ext-real set
i is Element of the carrier of FT
(g /^ x) . ((z1 -' y0) + 1) is set
((z1 -' y0) + 1) + x is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' y0) + 1) + x) is set
((z1 -' y0) + x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' y0) + x) + 1) is set
rng (g /^ x) is Element of K32( the carrier of FT)
rng ((g | y0) ^ (g /^ x)) is Element of K32( the carrier of FT)
rng (g | y0) is Element of K32( the carrier of FT)
(rng (g | y0)) \/ (rng (g /^ x)) is Element of K32( the carrier of FT)
((len g) -' x) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | y0)) + ((len g) -' x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | y0) ^ (g /^ x)) . ((len (g | y0)) + ((len g) -' x)) is set
(g /^ x) . ((len g) -' x) is set
((g | y0) ^ (g /^ x)) . (len ((g | y0) ^ (g /^ x))) is set
(len g) - y0 is V51() V52() ext-real set
(y0 + ((len g) - x)) - y0 is V51() V52() ext-real set
s is V35() V39() V51() V52() ext-real non negative set
((g | y0) ^ (g /^ x)) . s is set
s + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((g | y0) ^ (g /^ x)) . (s + 1) is set
h3 is Element of the carrier of FT
U_FT h3 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h3) is Element of K32( the carrier of FT)
z1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom ((g | y0) ^ (g /^ x)) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
((g | y0) ^ (g /^ x)) . (z1 + 1) is set
((g | y0) ^ (g /^ x)) /. (z1 + 1) is Element of the carrier of FT
i is Element of the carrier of FT
(g | y0) . (z1 + 1) is set
g . (z1 + 1) is set
(g | y0) . z1 is set
g . z1 is set
(y0 + ((len g) - x)) - y0 is V51() V52() ext-real set
z1 - y0 is V51() V52() ext-real set
z1 -' y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((len g) - x) + x is V51() V52() ext-real set
(z1 -' y0) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | y0)) + (z1 -' y0) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 + (z1 - y0) is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(g /^ x) . (z1 -' y0) is set
g . ((z1 -' y0) + x) is set
(g | y0) . y0 is set
0 + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (0 + x) is set
g . ((z1 -' y0) + x) is set
g . ((z1 -' y0) + x) is set
g . ((z1 -' y0) + x) is set
(z1 -' y0) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | y0)) + ((z1 -' y0) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(z1 - y0) + 1 is V51() V52() ext-real set
((z1 - y0) + 1) + y0 is V51() V52() ext-real set
i is Element of the carrier of FT
(g /^ x) . ((z1 -' y0) + 1) is set
((z1 -' y0) + 1) + x is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' y0) + 1) + x) is set
((z1 -' y0) + x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((z1 -' y0) + x) + 1) is set
(g | y0) ^ {} is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
rng (g | y0) is Element of K32( the carrier of FT)
rng ((g | y0) ^ (g /^ x)) is Element of K32( the carrier of FT)
((g | y0) ^ (g /^ x)) . (len ((g | y0) ^ (g /^ x))) is set
(len g) - y0 is V51() V52() ext-real set
(y0 + ((len g) - x)) - y0 is V51() V52() ext-real set
FT is non empty RelStr
the carrier of FT is non empty set
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
g . 1 is set
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (len g) is set
B0 is V35() V39() V51() V52() ext-real non negative set
i is V35() V39() V51() V52() ext-real non negative set
g . B0 is set
g . i is set
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 is Element of the carrier of FT
U_FT y0 is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,y0) is Element of K32( the carrier of FT)
rng g is Element of K32( the carrier of FT)
i -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i - 1 is V51() V52() ext-real set
h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) -' h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | s is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg s is V40() V47(s) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= s ) } is set
g | (Seg s) is Relation-like NAT -defined Seg s -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
g /^ h is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(g | s) ^ (g /^ h) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g | s) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g /^ h) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) - h is V51() V52() ext-real set
z1 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len z1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | s)) + (len (g /^ h)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s + ((len g) - h) is V51() V52() ext-real set
z1 . 1 is set
(g | s) . 1 is set
h + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(h + 1) - h is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i is V35() V39() V51() V52() ext-real non negative set
z1 . i is set
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 . (i + 1) is set
z2 is Element of the carrier of FT
U_FT z2 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,z2) is Element of K32( the carrier of FT)
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom z1 is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
z1 . (i + 1) is set
z1 /. (i + 1) is Element of the carrier of FT
z2 is Element of the carrier of FT
(g | s) . (i + 1) is set
g . (i + 1) is set
(g | s) . i is set
g . i is set
(s + ((len g) - h)) - s is V51() V52() ext-real set
i - s is V51() V52() ext-real set
i -' s is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i -' s) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | s)) + (i -' s) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s + (i - s) is V51() V52() ext-real set
(len (g | s)) + ((i -' s) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i - s) + 1 is V51() V52() ext-real set
((i - s) + 1) + s is V51() V52() ext-real set
dom (g /^ h) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
z2 is Element of the carrier of FT
(g /^ h) . ((i -' s) + 1) is set
((i -' s) + 1) + h is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' s) + 1) + h) is set
(i -' s) + h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((i -' s) + h) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' s) + h) + 1) is set
((len g) - h) + h is V51() V52() ext-real set
(g /^ h) . (i -' s) is set
g . ((i -' s) + h) is set
(g | s) . s is set
z2 is Element of the carrier of FT
(g /^ h) . ((i -' s) + 1) is set
((i -' s) + 1) + h is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' s) + 1) + h) is set
(i -' s) + h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((i -' s) + h) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' s) + h) + 1) is set
0 + (i -' 1) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(0 + (i -' 1)) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((0 + (i -' 1)) + 1) is set
(i - 1) + 1 is V51() V52() ext-real set
g . ((i - 1) + 1) is set
rng (g /^ h) is Element of K32( the carrier of FT)
rng z1 is Element of K32( the carrier of FT)
rng (g | s) is Element of K32( the carrier of FT)
(rng (g | s)) \/ (rng (g /^ h)) is Element of K32( the carrier of FT)
((len g) -' h) + h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ h) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | s)) + ((len g) -' h) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
z1 . ((len (g | s)) + ((len g) -' h)) is set
(g /^ h) . ((len g) -' h) is set
z1 . (len z1) is set
(len g) - s is V51() V52() ext-real set
(s + ((len g) - h)) - s is V51() V52() ext-real set
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 - 1 is V51() V52() ext-real set
x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x3 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) -' x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | x3 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg x3 is V40() V47(x3) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= x3 ) } is set
g | (Seg x3) is Relation-like NAT -defined Seg x3 -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
g /^ x is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
(g | x3) ^ (g /^ x) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g | x3) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g /^ x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) - x is V51() V52() ext-real set
s is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len s is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | x3)) + (len (g /^ x)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x3 + ((len g) - x) is V51() V52() ext-real set
s . 1 is set
(g | x3) . 1 is set
x + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(x + 1) - x is V51() V52() ext-real set
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
h3 is V35() V39() V51() V52() ext-real non negative set
s . h3 is set
h3 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s . (h3 + 1) is set
z1 is Element of the carrier of FT
U_FT z1 is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,z1) is Element of K32( the carrier of FT)
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom s is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
s . (i + 1) is set
s /. (i + 1) is Element of the carrier of FT
z2 is Element of the carrier of FT
(g | x3) . (i + 1) is set
g . (i + 1) is set
(g | x3) . i is set
g . i is set
(x3 + ((len g) - x)) - x3 is V51() V52() ext-real set
i - x3 is V51() V52() ext-real set
i -' x3 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i -' x3) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | x3)) + (i -' x3) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x3 + (i - x3) is V51() V52() ext-real set
(len (g | x3)) + ((i -' x3) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i - x3) + 1 is V51() V52() ext-real set
((i - x3) + 1) + x3 is V51() V52() ext-real set
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
z2 is Element of the carrier of FT
(g /^ x) . ((i -' x3) + 1) is set
((i -' x3) + 1) + x is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' x3) + 1) + x) is set
(i -' x3) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((i -' x3) + x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' x3) + x) + 1) is set
((len g) - x) + x is V51() V52() ext-real set
(g /^ x) . (i -' x3) is set
g . ((i -' x3) + x) is set
(g | x3) . x3 is set
z2 is Element of the carrier of FT
(g /^ x) . ((i -' x3) + 1) is set
((i -' x3) + 1) + x is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' x3) + 1) + x) is set
(i -' x3) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((i -' x3) + x) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i -' x3) + x) + 1) is set
0 + (B0 -' 1) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(0 + (B0 -' 1)) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((0 + (B0 -' 1)) + 1) is set
(B0 - 1) + 1 is V51() V52() ext-real set
g . ((B0 - 1) + 1) is set
rng (g /^ x) is Element of K32( the carrier of FT)
rng s is Element of K32( the carrier of FT)
rng (g | x3) is Element of K32( the carrier of FT)
(rng (g | x3)) \/ (rng (g /^ x)) is Element of K32( the carrier of FT)
((len g) -' x) + x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom (g /^ x) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
(len (g | x3)) + ((len g) -' x) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s . ((len (g | x3)) + ((len g) -' x)) is set
(g /^ x) . ((len g) -' x) is set
s . (len s) is set
(len g) - x3 is V51() V52() ext-real set
(x3 + ((len g) - x)) - x3 is V51() V52() ext-real set
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
rng g is Element of K32( the carrier of FT)
g /. 1 is Element of the carrier of FT
U_FT (g /. 1) is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. 1)) is Element of K32( the carrier of FT)
(rng g) /\ (U_FT (g /. 1)) is Element of K32( the carrier of FT)
g . 1 is set
g . 2 is set
{(g . 1),(g . 2)} is non empty set
g /. (len g) is Element of the carrier of FT
U_FT (g /. (len g)) is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. (len g))) is Element of K32( the carrier of FT)
(rng g) /\ (U_FT (g /. (len g))) is Element of K32( the carrier of FT)
(len g) -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((len g) -' 1) is set
g . (len g) is set
{(g . ((len g) -' 1)),(g . (len g))} is non empty set
A is Element of K32( the carrier of FT)
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
Seg (len g) is V40() V47( len g) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= len g ) } is set
B0 is V35() V39() V51() V52() ext-real non negative set
g /. B0 is Element of the carrier of FT
U_FT (g /. B0) is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. B0)) is Element of K32( the carrier of FT)
(rng g) /\ (U_FT (g /. B0)) is Element of K32( the carrier of FT)
B0 -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (B0 -' 1) is set
g . B0 is set
B0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (B0 + 1) is set
{(g . (B0 -' 1)),(g . B0),(g . (B0 + 1))} is set
1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 - 1 is V51() V52() ext-real set
(B0 -' 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(B0 - 1) + 1 is V51() V52() ext-real set
i is set
y0 is set
g . y0 is set
x is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
x + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i is set
g /. (B0 -' 1) is Element of the carrier of FT
U_FT (g /. (B0 -' 1)) is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. (B0 -' 1))) is Element of K32( the carrier of FT)
1 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(1 + 1) - 1 is V51() V52() ext-real set
(len g) - 1 is V51() V52() ext-real set
B0 is set
i is set
g . i is set
y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 is set
i is Element of the carrier of FT
g . (1 + 1) is set
(len g) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
((len g) + 1) - 1 is V51() V52() ext-real set
g /. ((len g) -' 1) is Element of the carrier of FT
B0 is set
i is set
g . i is set
y0 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
B0 is set
((len g) -' 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((len g) -' 1) + 1) is set
U_FT (g /. ((len g) -' 1)) is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. ((len g) -' 1))) is Element of K32( the carrier of FT)
FT is non empty RelStr
the carrier of FT is non empty set
K32( the carrier of FT) is set
g is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len g is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
A is non empty Element of K32( the carrier of FT)
(FT,A) is non empty strict (FT)
the carrier of (FT,A) is non empty set
K32( the carrier of (FT,A)) is set
x1 is Element of the carrier of FT
x2 is Element of the carrier of FT
{x1} is non empty connected (FT) Element of K32( the carrier of FT)
B0 is Element of K32( the carrier of (FT,A))
rng g is Element of K32( the carrier of FT)
[#] (FT,A) is non empty non proper Element of K32( the carrier of (FT,A))
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,i) is Element of K32( the carrier of (FT,A))
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,(i + 1)) is Element of K32( the carrier of (FT,A))
(i + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
y0 is Element of the carrier of FT
(Finf (B0,i)) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,i) & b₁ in U_FT b₂ ) } is set
x is Element of the carrier of (FT,A)
{y0} is non empty connected (FT) Element of K32( the carrier of FT)
x3 is Element of the carrier of (FT,A)
U_FT x3 is Element of K32( the carrier of (FT,A))
the InternalRel of (FT,A) is Relation-like Element of K32(K33( the carrier of (FT,A), the carrier of (FT,A)))
K33( the carrier of (FT,A), the carrier of (FT,A)) is Relation-like set
K32(K33( the carrier of (FT,A), the carrier of (FT,A))) is set
K123( the carrier of (FT,A), the carrier of (FT,A), the InternalRel of (FT,A),x3) is Element of K32( the carrier of (FT,A))
x3 is Element of the carrier of (FT,A)
U_FT x3 is Element of K32( the carrier of (FT,A))
the InternalRel of (FT,A) is Relation-like Element of K32(K33( the carrier of (FT,A), the carrier of (FT,A)))
K33( the carrier of (FT,A), the carrier of (FT,A)) is Relation-like set
K32(K33( the carrier of (FT,A), the carrier of (FT,A))) is set
K123( the carrier of (FT,A), the carrier of (FT,A), the InternalRel of (FT,A),x3) is Element of K32( the carrier of (FT,A))
h is Element of the carrier of FT
s is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng s is Element of K32( the carrier of FT)
s . 1 is set
len s is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
s . (len s) is set
U_FT h is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,h) is Element of K32( the carrier of FT)
(U_FT h) /\ A is Element of K32( the carrier of FT)
<*y0*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,y0] is set
{1,y0} is non empty set
{{1,y0},{1}} is non empty set
{[1,y0]} is non empty Relation-like Function-like set
s ^ <*y0*> is non empty Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng (s ^ <*y0*>) is non empty Element of K32( the carrier of FT)
rng <*y0*> is non empty Element of K32( the carrier of FT)
(rng s) \/ (rng <*y0*>) is non empty Element of K32( the carrier of FT)
h3 is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng h3 is Element of K32( the carrier of FT)
dom s is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
h3 . 1 is set
len <*y0*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len h3 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len s) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
h3 . (len h3) is set
y0 is Element of the carrier of FT
g . 1 is set
g . (len g) is set
dom g is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
Finf (B0,0) is Element of K32( the carrier of (FT,A))
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i is Element of the carrier of FT
<*x1*> is non empty Relation-like NAT -defined the carrier of FT -valued the carrier of FT -valued Function-like V40() V47(1) FinSequence-like FinSubsequence-like (FT) FinSequence of the carrier of FT
[1,x1] is set
{1,x1} is non empty set
{{1,x1},{1}} is non empty set
{[1,x1]} is non empty Relation-like Function-like set
len <*x1*> is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
rng <*x1*> is non empty Element of K32( the carrier of FT)
<*x1*> . 1 is set
i is Element of the carrier of FT
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (i + 1) is set
Finf (B0,i) is Element of K32( the carrier of (FT,A))
i -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,(i -' 1)) is Element of K32( the carrier of (FT,A))
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((i + 1) + 1) is set
Finf (B0,(i + 1)) is Element of K32( the carrier of (FT,A))
(i + 1) -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,((i + 1) -' 1)) is Element of K32( the carrier of (FT,A))
(i + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(i + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . ((i + 1) + 1) is set
g . (i + 1) is set
g /. (i + 1) is Element of the carrier of FT
i - 1 is V51() V52() ext-real set
(Finf (B0,(i -' 1))) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,(i -' 1)) & b₁ in U_FT b₂ ) } is set
(i -' 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(Finf (B0,(i -' 1))) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,(i -' 1)) & b₁ in U_FT b₂ ) } is set
(Finf (B0,(i -' 1))) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,(i -' 1)) & b₁ in U_FT b₂ ) } is set
(Finf (B0,(i -' 1))) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,(i -' 1)) & b₁ in U_FT b₂ ) } is set
x is Element of the carrier of (FT,A)
x3 is Element of the carrier of FT
h is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
rng h is Element of K32( the carrier of FT)
h . 1 is set
len h is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
h . (len h) is set
g /^ ((i + 1) + 1) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
h ^ (g /^ ((i + 1) + 1)) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
s is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len s is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
len (g /^ ((i + 1) + 1)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len h) + (len (g /^ ((i + 1) + 1))) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g | ((i + 1) + 1) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
Seg ((i + 1) + 1) is non empty V40() V47((i + 1) + 1) V68() V69() V70() V71() V72() V73() Element of K32(NAT)
{ b₁ where b₁ is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT : ( 1 <= b₁ & b₁ <= (i + 1) + 1 ) } is set
g | (Seg ((i + 1) + 1)) is Relation-like NAT -defined Seg ((i + 1) + 1) -defined NAT -defined the carrier of FT -valued Function-like FinSubsequence-like set
(g | ((i + 1) + 1)) ^ (g /^ ((i + 1) + 1)) is Relation-like NAT -defined the carrier of FT -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of FT
len (g | ((i + 1) + 1)) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len (g | ((i + 1) + 1))) + (len (g /^ ((i + 1) + 1))) is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
dom h is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
h /. (len h) is Element of the carrier of FT
1 + ((i + 1) + 1) is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
(len g) - ((i + 1) + 1) is V51() V52() ext-real set
dom (g /^ ((i + 1) + 1)) is V68() V69() V70() V71() V72() V73() Element of K32(NAT)
g /. ((i + 1) + 1) is Element of the carrier of FT
s . (len s) is set
(g /^ ((i + 1) + 1)) . (len (g /^ ((i + 1) + 1))) is set
((i + 1) + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (((i + 1) + 1) + 1) is set
U_FT (g /. ((i + 1) + 1)) is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. ((i + 1) + 1))) is Element of K32( the carrier of FT)
(g /^ ((i + 1) + 1)) . 1 is set
U_FT (h /. (len h)) is Element of K32( the carrier of FT)
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(h /. (len h))) is Element of K32( the carrier of FT)
s . 1 is set
rng (g /^ ((i + 1) + 1)) is Element of K32( the carrier of FT)
rng s is Element of K32( the carrier of FT)
(rng h) \/ (rng (g /^ ((i + 1) + 1))) is Element of K32( the carrier of FT)
<*> the carrier of FT is empty Relation-like non-empty empty-yielding NAT -defined the carrier of FT -valued Function-like one-to-one constant functional V40() FinSequence-like FinSubsequence-like FinSequence-membered V68() V69() V70() V71() V72() V73() V74() FinSequence of the carrier of FT
y0 is Element of the carrier of (FT,A)
U_FT y0 is Element of K32( the carrier of (FT,A))
the InternalRel of (FT,A) is Relation-like Element of K32(K33( the carrier of (FT,A), the carrier of (FT,A)))
K33( the carrier of (FT,A), the carrier of (FT,A)) is Relation-like set
K32(K33( the carrier of (FT,A), the carrier of (FT,A))) is set
K123( the carrier of (FT,A), the carrier of (FT,A), the InternalRel of (FT,A),y0) is Element of K32( the carrier of (FT,A))
U_FT (g /. (i + 1)) is Element of K32( the carrier of FT)
the InternalRel of FT is Relation-like Element of K32(K33( the carrier of FT, the carrier of FT))
K33( the carrier of FT, the carrier of FT) is Relation-like set
K32(K33( the carrier of FT, the carrier of FT)) is set
K123( the carrier of FT, the carrier of FT, the InternalRel of FT,(g /. (i + 1))) is Element of K32( the carrier of FT)
(U_FT (g /. (i + 1))) /\ A is Element of K32( the carrier of FT)
(Finf (B0,i)) ^f is Element of K32( the carrier of (FT,A))
{ b₁ where b₁ is Element of the carrier of (FT,A) : ex b₂ being Element of the carrier of (FT,A) st
( b₂ in Finf (B0,i) & b₁ in U_FT b₂ ) } is set
(i + 1) - 1 is V51() V52() ext-real set
(i + 1) + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
i + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (i + 1) is set
Finf (B0,i) is Element of K32( the carrier of (FT,A))
i -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,(i -' 1)) is Element of K32( the carrier of (FT,A))
Finf ({x1},0) is Element of K32( the carrier of FT)
0 + 1 is non empty V35() V39() V51() V52() ext-real positive non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
g . (0 + 1) is set
0 -' 1 is V35() V39() V51() V52() ext-real non negative V56() V57() V68() V69() V70() V71() V72() V73() Element of NAT
Finf (B0,(0 -' 1)) is Element of K32( the carrier of (FT,A))