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

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

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

RelStr(# C,T1 #) is non empty strict total reflexive transitive antisymmetric RelStr
C is 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

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

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)
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier of C holds
( not b2 in {T2} or b1 < b2 )
}
is set

() /\ T1 is finite Element of K10( 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
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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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 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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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

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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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 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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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 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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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)

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
{ b1 where b1 is finite Element of Fin the carrier of T1 : the InternalRel of T1 linearly_orders b1 } is set
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

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

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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
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

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

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

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

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

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

dom T2 is set
rng T2 is set

{ b1 where b1 is Relation-like Seg a1 -defined Seg (a1 + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg a1),(Seg (a1 + 1))) : (a1,b1) is increasing } is 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)
{ b1 where b1 is Relation-like Seg T2 -defined Seg (T2 + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg T2),(Seg (T2 + 1))) : (T2,b1) is increasing } is 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)
{ b1 where b1 is Relation-like Seg T2 -defined Seg (T2 + 1) -valued Function-like total quasi_total finite-support Element of Funcs ((Seg T2),(Seg (T2 + 1))) : (T2,b1) is increasing } is 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)

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)

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

{ b1 where b1 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,b1) is increasing } is set
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)
{ b1 where b1 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,b1) is increasing } is set
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)))

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, 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 () ()

(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

dom F2n is set
rng F2n is set
F2n . T2 is set
x is Element of the of C . T1

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

dom x1 is set
rng x1 is set
x1 . T2 is set

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

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
{ b1 where b1 is finite Element of Fin the carrier of C : the InternalRel of C linearly_orders b1 } is set
{ (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = a1 } is set

T2 is V28() V32() finite cardinal ext-real non negative set
T1 . T2 is set
{ (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = T2 } is set
IFEQ (T2,0,, { (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = T2 } ) is set
T1 . 0 is set
{ (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = 0 } is set
IFEQ (0,0,, { (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = 0 } ) is 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 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,b1)) where b1 is non empty finite Element of (C) : card b1 = i + 1 } is set
F1n is non empty finite Element 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)

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,b1)) where b1 is non empty finite Element of (C) : card b1 = i } is set
i is V28() V32() finite cardinal ext-real non negative set
T1 . i is 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)
{ b1 where b1 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,b1) is increasing } is 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)))

dom x1 is set
rng x1 is 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,b1)) where b1 is non empty finite Element of (C) : card b1 = n + 1 } is set
y is non empty finite Element 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

y1 is set

dom F2nx is set
y1 is set

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

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

rng F2nx is set
T2 . n is set
A is set
A is set
F2nx . A is set

dom (x * g1) is set
{ (SgmX ( the InternalRel of C,b1)) where b1 is non empty finite Element of (C) : card b1 = n + 1 } is set
s1 is non empty finite Element 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

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

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

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
c33 is finite Element of Fin the carrier of C
s9 is non empty finite Element of y2

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,b1)) where b1 is non empty finite Element of (C) : card b1 = n } is set
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)

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

g1 . A is set

(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,b1)) where b1 is non empty finite Element of (C) : card b1 = n } is set
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)

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

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,b1)) where b1 is non empty finite Element of (C) : card b1 = 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
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

dom F1nx is set
rng F1nx is set
F2n . x1 is Element of ( the of T1) . n

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,b1)) where b1 is non empty finite Element of (C) : card b1 = n + 1 } is set
A is non empty finite Element 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