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

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

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

g ^b is Element of K32( the carrier of FT)

{ b

A ^b is Element of K32( the carrier of FT)

{ b

(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

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

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

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

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

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

A is Element of K32( the carrier of FT)

A ^b is Element of K32( the carrier of FT)

{ b

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

x1 ^b is Element of K32( the carrier of FT)

{ b

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

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

(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

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

(x2 ^b) /\ B0 is Element of K32( the carrier of g)

B0 ^b is Element of K32( the carrier of g)

{ b

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

([#] 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

(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

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

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

A ^b is Element of K32( the carrier of FT)

{ b

(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

([#] (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

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

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

(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

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

(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

g ^b is Element of K32( the carrier of FT)

{ b

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

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

g /\ (g ^delta) is Element of K32( the carrier of FT)

g ^b is Element of K32( the carrier of FT)

{ b

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

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

(g `) /\ (g ^delta) is Element of K32( the carrier of FT)

(g `) ^b is Element of K32( the carrier of FT)

{ b

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

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

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

(g `) /\ (g ^delta) is Element of K32( the carrier of FT)

g ^b is Element of K32( the carrier of FT)

{ b

(g ^b) \ g is Element of K32( the carrier of FT)

(g `) ^b is Element of K32( the carrier of FT)

{ b

(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

(g `) /\ (g ^delta) is Element of K32( the carrier of FT)

g ^b is Element of K32( the carrier of FT)

{ b

(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

(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

(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

(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

(A `) ^b is Element of K32( the carrier of FT)

{ b

(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

(g `) ^b is Element of K32( the carrier of FT)

{ b

(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

x1 ^b is Element of K32( the carrier of FT)

{ b

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

g /\ (A ^b) is Element of K32( the carrier of FT)

g ^b is Element of K32( the carrier of FT)

{ b

(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

g ^b is Element of K32( the carrier of FT)

{ b

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

g /\ (A ^b) is Element of K32( the carrier of FT)

x2 ^b is Element of K32( the carrier of FT)

{ b

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

(g ^b) /\ A is Element of K32( the carrier of FT)

x1 ^b is Element of K32( the carrier of FT)

{ b

(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

(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

g /\ (A ^b) is Element of K32( the carrier of FT)

x1 ^b is Element of K32( the carrier of FT)

{ b

(A \/ x1) ^b is Element of K32( the carrier of FT)

{ b

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

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

g ^b is Element of K32( the carrier of FT)

{ b

A ^b is Element of K32( the carrier of FT)

{ b

g ^b is Element of K32( the carrier of FT)

{ b

g ^b is Element of K32( the carrier of FT)

{ b

A ^b is Element of K32( the carrier of FT)

{ b

(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

(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

A ^b is Element of K32( the carrier of FT)

{ b

A ^b is Element of K32( the carrier of FT)

{ b

(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

(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

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

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

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

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

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

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

[#] 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

h is Element of K32( the carrier of FT)

h ^b is Element of K32( the carrier of FT)

{ b

(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

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

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

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

( b

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

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