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