:: TRIANG_1 semantic presentation

REAL is V97() V98() V99() V103() set

NAT is non empty V2() non empty-membered V28() non finite cardinal limit_cardinal V97() V98() V99() V100() V101() V102() V103() Element of K10(REAL)

K10(REAL) is cup-closed diff-closed preBoolean set

NAT is non empty V2() non empty-membered V28() non finite cardinal limit_cardinal V97() V98() V99() V100() V101() V102() V103() set

K10(NAT) is non empty V2() non empty-membered non finite cup-closed diff-closed preBoolean set

K10(NAT) is non empty V2() non empty-membered non finite cup-closed diff-closed preBoolean set

COMPLEX is V97() V103() set

RAT is V97() V98() V99() V100() V103() set

INT is V97() V98() V99() V100() V101() V103() set

{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding V28() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V97() V98() V99() V100() V101() V102() V103() FinSequence-yielding finite-support set

the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding V28() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V97() V98() V99() V100() V101() V102() V103() FinSequence-yielding finite-support set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding V28() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V97() V98() V99() V100() V101() V102() V103() FinSequence-yielding finite-support set

2 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

3 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

C is non empty set

K11(C,C) is Relation-like set

K10(K11(C,C)) is cup-closed diff-closed preBoolean set

T1 is Relation-like C -defined C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11(C,C))

RelStr(# C,T1 #) is non empty strict total reflexive transitive antisymmetric RelStr

C is set

{} |_2 C is Relation-like set

K11(C,C) is Relation-like set

{} /\ K11(C,C) is Relation-like NAT -defined RAT -valued finite V75() V76() V77() V78() V97() V98() V99() V100() V101() V102() set

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

K10( the carrier of C) is cup-closed diff-closed preBoolean set

T1 is Element of K10( the carrier of C)

T2 is Element of the carrier of C

i is Element of K10( the carrier of C)

n is Element of the carrier of C

{T2} is non empty V2() finite 1 -element Element of K10( the carrier of C)

i \/ {T2} is non empty Element of K10( the carrier of C)

F1n is Element of the carrier of C

F2n is Element of the carrier of C

n is Element of the carrier of C

{T2} is non empty V2() finite 1 -element Element of K10( the carrier of C)

i \/ {T2} is non empty Element of K10( the carrier of C)

F1n is Element of the carrier of C

F1n is Element of the carrier of C

F2n is Element of the carrier of C

F2n is Element of the carrier of C

x is Element of the carrier of C

x1 is Element of the carrier of C

n is Element of the carrier of C

F1n is Element of the carrier of C

{T2} is non empty V2() finite 1 -element Element of K10( the carrier of C)

i \/ {T2} is non empty Element of K10( the carrier of C)

{T2} is non empty V2() finite 1 -element Element of K10( the carrier of C)

i \/ {T2} is non empty Element of K10( the carrier of C)

F1n is Element of the carrier of C

{} the carrier of C is Element of K10( the carrier of C)

T2 is Element of the carrier of C

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

K10( the carrier of C) is cup-closed diff-closed preBoolean set

T1 is non empty finite Element of K10( the carrier of C)

T2 is Element of the carrier of C

InitSegm (T1,T2) is Element of K10( the carrier of C)

{T2} is non empty V2() finite 1 -element Element of K10( the carrier of C)

LowerCone {T2} is Element of K10( the carrier of C)

{ b

( not b

(LowerCone {T2}) /\ T1 is finite Element of K10( the carrier of C)

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

T2 is set

i is finite Element of Fin the carrier of C

C is non empty total reflexive transitive antisymmetric RelStr

(C) is Element of K10((Fin the carrier of C))

the carrier of C is non empty set

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

the Element of the carrier of C is Element of the carrier of C

{ the Element of the carrier of C} is non empty V2() finite 1 -element Element of K10( the carrier of C)

K10( the carrier of C) is cup-closed diff-closed preBoolean set

T2 is finite Element of Fin the carrier of C

i is set

n is set

[i,n] is set

{i,n} is non empty finite set

{i} is non empty V2() finite 1 -element set

{{i,n},{i}} is non empty with_non-empty_elements non empty-membered finite V37() set

[n,i] is set

{n,i} is non empty finite set

{n} is non empty V2() finite 1 -element set

{{n,i},{n}} is non empty with_non-empty_elements non empty-membered finite V37() set

field the InternalRel of C is set

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

(C) is non empty non empty-membered Element of K10((Fin the carrier of C))

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

T1 is Element of the carrier of C

{T1} is non empty V2() finite 1 -element Element of K10( the carrier of C)

K10( the carrier of C) is cup-closed diff-closed preBoolean set

T2 is finite Element of Fin the carrier of C

i is set

n is set

[i,n] is set

{i,n} is non empty finite set

{i} is non empty V2() finite 1 -element set

{{i,n},{i}} is non empty with_non-empty_elements non empty-membered finite V37() set

[n,i] is set

{n,i} is non empty finite set

{n} is non empty V2() finite 1 -element set

{{n,i},{n}} is non empty with_non-empty_elements non empty-membered finite V37() set

field the InternalRel of C is set

C is non empty total reflexive transitive antisymmetric RelStr

(C) is non empty non empty-membered Element of K10((Fin the carrier of C))

the carrier of C is non empty set

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

K10( the carrier of C) is cup-closed diff-closed preBoolean set

field the InternalRel of C is set

T1 is finite Element of Fin the carrier of C

T2 is set

i is set

[T2,i] is set

{T2,i} is non empty finite set

{T2} is non empty V2() finite 1 -element set

{{T2,i},{T2}} is non empty with_non-empty_elements non empty-membered finite V37() set

[i,T2] is set

{i,T2} is non empty finite set

{i} is non empty V2() finite 1 -element set

{{i,T2},{i}} is non empty with_non-empty_elements non empty-membered finite V37() set

C is non empty total reflexive transitive antisymmetric RelStr

(C) is non empty non empty-membered Element of K10((Fin the carrier of C))

the carrier of C is non empty set

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

T1 is set

T2 is set

i is finite Element of Fin the carrier of C

n is finite Element of Fin the carrier of C

C is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg C is finite C -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

T1 is non empty total reflexive transitive antisymmetric RelStr

the carrier of T1 is non empty set

(T1) is non empty non empty-membered Element of K10((Fin the carrier of T1))

Fin the carrier of T1 is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of T1)) is cup-closed diff-closed preBoolean set

the InternalRel of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of T1, the carrier of T1))

K11( the carrier of T1, the carrier of T1) is Relation-like set

K10(K11( the carrier of T1, the carrier of T1)) is cup-closed diff-closed preBoolean set

{ b

T2 is non empty finite Element of (T1)

card T2 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

SgmX ( the InternalRel of T1,T2) is Relation-like NAT -defined the carrier of T1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of T1

dom (SgmX ( the InternalRel of T1,T2)) is finite V97() V98() V99() V100() V101() V102() Element of K10(NAT)

len (SgmX ( the InternalRel of T1,T2)) is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

n is finite Element of Fin the carrier of T1

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

(C) is non empty non empty-membered Element of K10((Fin the carrier of C))

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

the Element of the carrier of C is Element of the carrier of C

{ the Element of the carrier of C} is non empty V2() finite 1 -element Element of K10( the carrier of C)

K10( the carrier of C) is cup-closed diff-closed preBoolean set

NAT --> 1 is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total V30() V75() V76() V77() V78() Element of K10(K11(NAT,NAT))

K11(NAT,NAT) is non empty V2() non empty-membered Relation-like RAT -valued INT -valued non finite V75() V76() V77() V78() set

K10(K11(NAT,NAT)) is non empty V2() non empty-membered non finite cup-closed diff-closed preBoolean set

T1 is Relation-like NAT -defined Function-like total set

T2 is V28() V32() finite cardinal ext-real non negative set

T1 . T2 is set

i is V28() V32() finite cardinal ext-real non negative set

T1 . i is set

C is Relation-like NAT -defined Function-like total set

T1 is Relation-like NAT -defined Function-like total set

T2 is Relation-like NAT -defined Function-like total set

i is V28() V32() finite cardinal ext-real non negative set

T2 . i is set

i + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

C . (i + 1) is set

C . i is set

Funcs ((C . (i + 1)),(C . i)) is functional set

T1 is Relation-like NAT -defined Function-like total set

T2 is Relation-like NAT -defined Function-like total set

i is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

T1 . i is set

T2 . i is set

i + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

C . (i + 1) is set

C . i is set

Funcs ((C . (i + 1)),(C . i)) is functional set

C is Relation-like NAT -defined Function-like total () set

(C) is Relation-like NAT -defined Function-like total set

T1 is V28() V32() finite cardinal ext-real non negative set

(C) . T1 is set

T1 + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

C . (T1 + 1) is set

C . T1 is set

Funcs ((C . (T1 + 1)),(C . T1)) is functional set

C is V28() V32() finite cardinal ext-real non negative set

Seg C is finite C -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

C + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg (C + 1) is non empty finite C + 1 -element C + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

Funcs ((Seg C),(Seg (C + 1))) is non empty functional FUNCTION_DOMAIN of Seg C, Seg (C + 1)

T1 is Relation-like Seg C -defined Seg (C + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg C),(Seg (C + 1)))

T2 is Relation-like Function-like set

dom T2 is set

rng T2 is set

i is Relation-like NAT -defined Seg (C + 1) -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() V78() finite-support FinSequence of Seg (C + 1)

{ b

C is Relation-like NAT -defined Function-like total set

T1 is Relation-like NAT -defined Function-like total set

T2 is V28() V32() finite cardinal ext-real non negative set

T1 . T2 is set

Seg T2 is finite T2 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

T2 + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg (T2 + 1) is non empty finite T2 + 1 -element T2 + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

Funcs ((Seg T2),(Seg (T2 + 1))) is non empty functional FUNCTION_DOMAIN of Seg T2, Seg (T2 + 1)

{ b

C is Relation-like NAT -defined Function-like total set

T1 is Relation-like NAT -defined Function-like total set

T2 is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

C . T2 is set

T1 . T2 is set

Seg T2 is finite T2 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

T2 + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg (T2 + 1) is non empty finite T2 + 1 -element T2 + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

T2 + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Funcs ((Seg T2),(Seg (T2 + 1))) is non empty functional FUNCTION_DOMAIN of Seg T2, Seg (T2 + 1)

{ b

() is Relation-like NAT -defined Function-like total set

C is V28() V32() finite cardinal ext-real non negative set

() . C is set

C + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg C is finite C -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

Seg (C + 1) is non empty finite C + 1 -element C + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

id (Seg C) is Relation-like Seg C -defined Seg C -valued RAT -valued INT -valued Function-like one-to-one total quasi_total finite V75() V76() V77() V78() increasing V81() finite-support Element of K10(K11((Seg C),(Seg C)))

K11((Seg C),(Seg C)) is Relation-like RAT -valued INT -valued finite V75() V76() V77() V78() set

K10(K11((Seg C),(Seg C))) is finite V37() cup-closed diff-closed preBoolean set

rng (id (Seg C)) is finite V97() V98() V99() V100() V101() V102() set

dom (id (Seg C)) is finite set

Funcs ((Seg C),(Seg (C + 1))) is non empty functional FUNCTION_DOMAIN of Seg C, Seg (C + 1)

idseq C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

T1 is Relation-like Seg C -defined Seg (C + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg C),(Seg (C + 1)))

(C,T1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

{ b

C is V28() V32() finite cardinal ext-real non negative set

() . C is non empty set

T2 is Element of () . C

T1 is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

() . T1 is non empty set

Seg C is finite C -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

C + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg (C + 1) is non empty finite C + 1 -element C + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

Funcs ((Seg C),(Seg (C + 1))) is non empty functional FUNCTION_DOMAIN of Seg C, Seg (C + 1)

{ b

i is Relation-like Seg C -defined Seg (C + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg C),(Seg (C + 1)))

(C,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

NAT --> {} is non empty Relation-like NAT -defined {{}} -valued Function-like total quasi_total V30() V75() V76() V77() V78() Element of K10(K11(NAT,{{}}))

{{}} is non empty V2() functional finite V37() 1 -element V97() V98() V99() V100() V101() V102() set

K11(NAT,{{}}) is non empty V2() non empty-membered Relation-like RAT -valued INT -valued non finite V75() V76() V77() V78() set

K10(K11(NAT,{{}})) is non empty V2() non empty-membered non finite cup-closed diff-closed preBoolean set

T1 is Relation-like NAT -defined Function-like total set

(T1) is Relation-like NAT -defined Function-like total set

the Relation-like NAT -defined Function-like total ManySortedFunction of (),(T1) is Relation-like NAT -defined Function-like total ManySortedFunction of (),(T1)

(T1, the Relation-like NAT -defined Function-like total ManySortedFunction of (),(T1)) is () ()

i is V28() V32() finite cardinal ext-real non negative set

T1 . i is set

n is V28() V32() finite cardinal ext-real non negative set

T1 . n is set

C is () ()

the of C is Relation-like NAT -defined Function-like total set

C is Relation-like NAT -defined Function-like total () set

(C) is Relation-like NAT -defined Function-like total set

T1 is Relation-like NAT -defined Function-like total ManySortedFunction of (),(C)

(C,T1) is () ()

C is () ()

the of C is Relation-like NAT -defined Function-like total () set

T1 is V28() V32() finite cardinal ext-real non negative set

T1 + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of C . (T1 + 1) is set

() . T1 is non empty set

the of C . T1 is set

the of C is Relation-like NAT -defined Function-like total ManySortedFunction of (),( the of C)

( the of C) is Relation-like NAT -defined Function-like total set

the of C . T1 is set

i is Relation-like Function-like Element of () . T1

T2 is Element of the of C . (T1 + 1)

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

() . n is non empty set

( the of C) . n is non empty set

K11((() . n),(( the of C) . n)) is Relation-like set

K10(K11((() . n),(( the of C) . n))) is cup-closed diff-closed preBoolean set

the of C . n is set

F1n is non empty Relation-like () . n -defined ( the of C) . n -valued Function-like total quasi_total Element of K10(K11((() . n),(( the of C) . n)))

F1n . i is set

Funcs (( the of C . (T1 + 1)),( the of C . T1)) is functional set

F2n is Relation-like Function-like set

dom F2n is set

rng F2n is set

F2n . T2 is set

x is Element of the of C . T1

x1 is Relation-like Function-like set

F1nx is Relation-like Function-like set

x1 . i is set

F1nx . T2 is set

F1n is Element of the of C . T1

F2n is Element of the of C . T1

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

() . n is non empty set

( the of C) . n is non empty set

K11((() . n),(( the of C) . n)) is Relation-like set

K10(K11((() . n),(( the of C) . n))) is cup-closed diff-closed preBoolean set

the of C . n is set

x is non empty Relation-like () . n -defined ( the of C) . n -valued Function-like total quasi_total Element of K10(K11((() . n),(( the of C) . n)))

x . i is set

Funcs (( the of C . (T1 + 1)),( the of C . T1)) is functional set

x1 is Relation-like Function-like set

dom x1 is set

rng x1 is set

x1 . T2 is set

0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding V28() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V74() V75() V76() V77() V78() V94() V95() V96() V97() V98() V99() V100() V101() V102() V103() FinSequence-yielding finite-support Element of NAT

{{}} is non empty V2() functional finite V37() 1 -element V97() V98() V99() V100() V101() V102() set

C is non empty total reflexive transitive antisymmetric RelStr

the carrier of C is non empty set

(C) is non empty non empty-membered Element of K10((Fin the carrier of C))

Fin the carrier of C is non empty cup-closed diff-closed preBoolean set

K10((Fin the carrier of C)) is cup-closed diff-closed preBoolean set

the InternalRel of C is Relation-like the carrier of C -defined the carrier of C -valued total quasi_total reflexive antisymmetric transitive Element of K10(K11( the carrier of C, the carrier of C))

K11( the carrier of C, the carrier of C) is Relation-like set

K10(K11( the carrier of C, the carrier of C)) is cup-closed diff-closed preBoolean set

{ b

{ (SgmX ( the InternalRel of C,b

T1 is Relation-like NAT -defined Function-like total set

T2 is V28() V32() finite cardinal ext-real non negative set

T1 . T2 is set

{ (SgmX ( the InternalRel of C,b

IFEQ (T2,0,{{}}, { (SgmX ( the InternalRel of C,b

T1 . 0 is set

{ (SgmX ( the InternalRel of C,b

IFEQ (0,0,{{}}, { (SgmX ( the InternalRel of C,b

T2 is V28() V32() finite cardinal ext-real non negative set

T1 . T2 is set

i is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

i + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

T1 . (i + 1) is set

T1 . i is set

n is set

{ (SgmX ( the InternalRel of C,b

F1n is non empty finite Element of (C)

SgmX ( the InternalRel of C,F1n) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

card F1n is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the Element of F1n is Element of F1n

{ the Element of F1n} is non empty V2() finite 1 -element Element of K10(F1n)

K10(F1n) is finite V37() cup-closed diff-closed preBoolean set

F1n \ { the Element of F1n} is finite Element of K10( the carrier of C)

K10( the carrier of C) is cup-closed diff-closed preBoolean set

x is finite set

x \/ { the Element of F1n} is non empty finite set

F1n \/ { the Element of F1n} is non empty finite set

card x is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

(card x) + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

x1 is non empty finite Element of (C)

SgmX ( the InternalRel of C,x1) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

{ (SgmX ( the InternalRel of C,b

i is V28() V32() finite cardinal ext-real non negative set

T1 . i is set

T2 is Relation-like NAT -defined Function-like total () set

(T2) is Relation-like NAT -defined Function-like total set

i is set

() . i is set

(T2) . i is set

F1n is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

() . n is non empty set

F2n is Relation-like Function-like Element of () . n

Seg n is finite n -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

n + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Seg (n + 1) is non empty finite n + 1 -element n + 1 -element V97() V98() V99() V100() V101() V102() Element of K10(NAT)

n + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

Funcs ((Seg n),(Seg (n + 1))) is non empty functional FUNCTION_DOMAIN of Seg n, Seg (n + 1)

{ b

x is Relation-like Function-like set

x1 is Relation-like Seg n -defined Seg (n + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg n),(Seg (n + 1)))

(n,x1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

x1 is Relation-like Function-like set

dom x1 is set

rng x1 is set

F1nx is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len F1nx is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

T2 . (n + 1) is set

F2nx is set

{ (SgmX ( the InternalRel of C,b

y is non empty finite Element of (C)

SgmX ( the InternalRel of C,y) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

card y is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

F2n * (SgmX ( the InternalRel of C,y)) is Relation-like the carrier of C -valued Function-like set

y2 is Relation-like Function-like set

y1 is set

x * y2 is Relation-like Function-like set

F2nx is Relation-like Function-like set

dom F2nx is set

y1 is set

y is Relation-like NAT -defined Seg (n + 1) -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() V78() finite-support FinSequence of Seg (n + 1)

y2 is set

dom y is finite set

A is set

y . y2 is V28() V32() finite cardinal ext-real non negative V74() V94() set

y . A is V28() V32() finite cardinal ext-real non negative V74() V94() set

dom y is finite V97() V98() V99() V100() V101() V102() Element of K10(NAT)

A is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

g1 is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

s1 is Relation-like Seg n -defined Seg (n + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg n),(Seg (n + 1)))

(n,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

s1 is Relation-like Seg n -defined Seg (n + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg n),(Seg (n + 1)))

(n,s1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

rng F2nx is set

T2 . n is set

A is set

A is set

F2nx . A is set

g1 is Relation-like Function-like set

y * g1 is Relation-like NAT -defined Function-like finite finite-support set

x * g1 is Relation-like Function-like set

dom (x * g1) is set

{ (SgmX ( the InternalRel of C,b

s1 is non empty finite Element of (C)

SgmX ( the InternalRel of C,s1) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

card s1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

rng g1 is set

f is finite Element of Fin the carrier of C

the InternalRel of C |_2 s1 is Relation-like s1 -defined s1 -valued total quasi_total finite reflexive antisymmetric transitive Element of K10(K11(s1,s1))

K11(s1,s1) is Relation-like finite set

K10(K11(s1,s1)) is finite V37() cup-closed diff-closed preBoolean set

the InternalRel of C /\ K11(s1,s1) is Relation-like the carrier of C -defined the carrier of C -valued finite set

RelStr(# s1,( the InternalRel of C |_2 s1) #) is non empty strict total reflexive transitive antisymmetric RelStr

the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #) is non empty set

f is Relation-like NAT -defined s1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of s1

f is Relation-like NAT -defined the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #)

z1 is finite Element of Fin the carrier of C

dom f is finite V97() V98() V99() V100() V101() V102() Element of K10(NAT)

K11((dom f),s1) is Relation-like finite set

K10(K11((dom f),s1)) is finite V37() cup-closed diff-closed preBoolean set

K11((Seg (n + 1)), the carrier of C) is Relation-like set

K10(K11((Seg (n + 1)), the carrier of C)) is cup-closed diff-closed preBoolean set

RelStr(# the carrier of C, the InternalRel of C #) is non empty strict total reflexive transitive antisymmetric RelStr

the carrier of RelStr(# the carrier of C, the InternalRel of C #) is non empty set

f is non empty Relation-like Seg (n + 1) -defined the carrier of C -valued Function-like total quasi_total finite finite-support Element of K10(K11((Seg (n + 1)), the carrier of C))

f * y is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

dom (f * y) is finite V97() V98() V99() V100() V101() V102() Element of K10(NAT)

rng (f * y) is finite set

y2 is non empty non empty-membered Element of K10((Fin the carrier of C))

r is finite Element of Fin the carrier of C

z1 is Relation-like NAT -defined the carrier of RelStr(# the carrier of C, the InternalRel of C #) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of RelStr(# the carrier of C, the InternalRel of C #)

dom z1 is finite V97() V98() V99() V100() V101() V102() Element of K10(NAT)

n1 is V28() V32() finite cardinal ext-real non negative set

m1 is V28() V32() finite cardinal ext-real non negative set

z1 /. n1 is Element of the carrier of RelStr(# the carrier of C, the InternalRel of C #)

z1 /. m1 is Element of the carrier of RelStr(# the carrier of C, the InternalRel of C #)

[(z1 /. n1),(z1 /. m1)] is Element of K11( the carrier of RelStr(# the carrier of C, the InternalRel of C #), the carrier of RelStr(# the carrier of C, the InternalRel of C #))

K11( the carrier of RelStr(# the carrier of C, the InternalRel of C #), the carrier of RelStr(# the carrier of C, the InternalRel of C #)) is Relation-like set

{(z1 /. n1),(z1 /. m1)} is non empty finite set

{(z1 /. n1)} is non empty V2() finite 1 -element set

{{(z1 /. n1),(z1 /. m1)},{(z1 /. n1)}} is non empty with_non-empty_elements non empty-membered finite V37() set

y . m1 is V28() V32() finite cardinal ext-real non negative V74() V94() set

y . n1 is V28() V32() finite cardinal ext-real non negative V74() V94() set

ym is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

yn is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

fm is Relation-like Seg n -defined Seg (n + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg n),(Seg (n + 1)))

(n,fm) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V75() V76() V77() finite-support FinSequence of REAL

rng y is finite V97() V98() V99() V100() V101() V102() set

f . ym is set

fm is Element of the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #)

f /. ym is Element of the carrier of C

z1 . m1 is set

zm is Element of the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #)

f . (y . m1) is set

z1 . n1 is set

f . (y . n1) is set

f . yn is set

fn is Element of the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #)

zn is Element of the carrier of RelStr(# s1,( the InternalRel of C |_2 s1) #)

f /. yn is Element of the carrier of C

c

s9 is non empty finite Element of y2

SgmX ( the InternalRel of C,s9) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

len (f * y) is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

card s9 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

{ (SgmX ( the InternalRel of C,b

Funcs ((T2 . (n + 1)),(T2 . n)) is functional set

T2 . (n + 1) is set

y2 is Relation-like Function-like Element of () . n

A is Element of T2 . (n + 1)

F2nx . A is set

A is non empty finite Element of (C)

SgmX ( the InternalRel of C,A) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

y2 * (SgmX ( the InternalRel of C,A)) is Relation-like the carrier of C -valued Function-like set

g1 is Relation-like Function-like set

g1 . A is set

s1 is Relation-like Function-like set

x * s1 is Relation-like Function-like set

i is Relation-like NAT -defined Function-like total ManySortedFunction of (),(T2)

(T2,i) is () () ()

the of (T2,i) is Relation-like NAT -defined Function-like total () set

the of (T2,i) . 0 is set

n is V28() V32() finite cardinal ext-real non negative set

the of (T2,i) . n is set

{ (SgmX ( the InternalRel of C,b

n is V28() V32() finite cardinal ext-real non negative set

() . n is non empty set

n + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of (T2,i) . (n + 1) is set

(T2) . n is non empty set

K11((() . n),((T2) . n)) is Relation-like set

K10(K11((() . n),((T2) . n))) is cup-closed diff-closed preBoolean set

i . n is set

F1n is non empty Relation-like () . n -defined (T2) . n -valued Function-like total quasi_total Element of K10(K11((() . n),((T2) . n)))

F2n is Relation-like Function-like Element of () . n

x is Element of the of (T2,i) . (n + 1)

((T2,i),n,x,F2n) is Element of the of (T2,i) . n

the of (T2,i) . n is set

x1 is non empty finite Element of (C)

SgmX ( the InternalRel of C,x1) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

F2n * (SgmX ( the InternalRel of C,x1)) is Relation-like the carrier of C -valued Function-like set

F1n . F2n is Element of (T2) . n

T2 . (n + 1) is set

T2 . n is set

Funcs ((T2 . (n + 1)),(T2 . n)) is functional set

F1nx is Relation-like Function-like set

dom F1nx is set

rng F1nx is set

F1nx . x is set

F2nx is V28() V32() finite cardinal ext-real non negative set

() . F2nx is non empty set

y is Relation-like Function-like Element of () . F2nx

F2nx + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

T2 . (F2nx + 1) is set

T1 is () () ()

the of T1 is Relation-like NAT -defined Function-like total () set

the of T1 . 0 is set

T2 is () () ()

the of T2 is Relation-like NAT -defined Function-like total () set

the of T2 . 0 is set

i is set

the of T1 . i is set

the of T2 . i is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of T1 . n is set

the of T2 . n is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of T1 . n is set

{ (SgmX ( the InternalRel of C,b

the of T2 . n is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of T1 . n is set

the of T2 . n is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of T1 . n is set

the of T2 . n is set

i is set

n is V28() V32() finite cardinal ext-real non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

() . n is non empty set

( the of T1) is Relation-like NAT -defined Function-like total set

( the of T1) . n is non empty set

K11((() . n),(( the of T1) . n)) is Relation-like set

K10(K11((() . n),(( the of T1) . n))) is cup-closed diff-closed preBoolean set

the of T1 is Relation-like NAT -defined Function-like total ManySortedFunction of (),( the of T1)

the of T1 . n is set

the of T2 is Relation-like NAT -defined Function-like total ManySortedFunction of (),( the of T2)

( the of T2) is Relation-like NAT -defined Function-like total set

the of T2 . n is set

F2n is non empty Relation-like () . n -defined ( the of T1) . n -valued Function-like total quasi_total Element of K10(K11((() . n),(( the of T1) . n)))

dom F2n is non empty set

x is set

F1n is non empty Relation-like () . n -defined ( the of T1) . n -valued Function-like total quasi_total Element of K10(K11((() . n),(( the of T1) . n)))

x1 is Relation-like Function-like Element of () . n

F1n . x1 is Element of ( the of T1) . n

n + 1 is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

the of T1 . (n + 1) is set

the of T1 . n is set

Funcs (( the of T1 . (n + 1)),( the of T1 . n)) is functional set

F1nx is Relation-like Function-like set

dom F1nx is set

rng F1nx is set

F2n . x1 is Element of ( the of T1) . n

F2nx is Relation-like Function-like set

dom F2nx is set

rng F2nx is set

y is set

y1 is Element of the of T1 . (n + 1)

F1nx . y1 is set

(T1,n,y1,x1) is Element of the of T1 . n

the of T2 . (n + 1) is set

y2 is Element of the of T2 . (n + 1)

F2nx . y2 is set

(T2,n,y2,x1) is Element of the of T2 . n

the of T2 . n is set

{ (SgmX ( the InternalRel of C,b

A is non empty finite Element of (C)

SgmX ( the InternalRel of C,A) is Relation-like NAT -defined the carrier of C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of C

card A is non empty V28() V32() finite cardinal ext-real positive non negative V74() V94() V95() V96() V97() V98() V99() V100() V101() V102() Element of NAT

x1 * (SgmX ( the InternalRel of C,A)) is Relation-like the carrier of C -valued Function-like set

F1nx . y is set

F2nx . y is set

F1n . x is set

F2n . x is set

dom F1n is non empty set

the of T1 . i is set

the of T2 . i is set