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