:: SCM_INST semantic presentation

REAL is set

NAT is non empty V17() V18() V19() V24() cardinal limit_cardinal Element of bool REAL

bool REAL is set

NAT is non empty V17() V18() V19() V24() cardinal limit_cardinal set

bool NAT is V24() set

bool NAT is V24() set

COMPLEX is set

RAT is set

INT is set

{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set

the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued set

1 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

2 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

3 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

8 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued Element of NAT

4 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

5 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

6 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

7 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

Seg 1 is non empty trivial V24() 1 -element Element of bool NAT

{ b

{1} is non empty trivial 1 -element set

Seg 2 is non empty V24() 2 -element Element of bool NAT

{ b

{1,2} is non empty set

9 is non empty V17() V18() V19() V23() V24() cardinal V39() V42() ext-real positive Element of NAT

Segm 9 is Element of bool NAT

{1} is non empty trivial 1 -element Element of bool NAT

[:{1},NAT:] is Relation-like V24() Element of bool [:NAT,REAL:]

[:NAT,REAL:] is Relation-like set

bool [:NAT,REAL:] is set

() is set

() is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V39() V42() ext-real complex-valued ext-real-valued real-valued natural-valued Element of Segm 9

[(),{},{}] is V1() V2() set

[(),{}] is V1() set

{(),{}} is non empty functional set

{()} is non empty trivial functional 1 -element set

{{(),{}},{()}} is non empty set

[[(),{}],{}] is V1() set

{[(),{}],{}} is non empty set

{[(),{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[(),{}],{}},{[(),{}]}} is non empty set

{[(),{},{}]} is non empty trivial Relation-like 1 -element standard-ins homogeneous J/A-independent with_halt set

{ [b

{[(),{},{}]} \/ { [b

{7,8} is non empty Element of bool NAT

{ [b

({[(),{},{}]} \/ { [b

{1,2,3,4,5} is Element of bool NAT

{ [b

(({[(),{},{}]} \/ { [b

() is non empty set

[0,{},{}] is V1() V2() set

[0,{}] is V1() set

{0,{}} is non empty functional set

{0} is non empty trivial functional 1 -element set

{{0,{}},{0}} is non empty set

[[0,{}],{}] is V1() set

{[0,{}],{}} is non empty set

{[0,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[0,{}],{}},{[0,{}]}} is non empty set

T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*T*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,T] is V1() set

{1,T} is non empty set

{{1,T},{1}} is non empty set

{[1,T]} is non empty trivial Relation-like Function-like constant 1 -element set

[6,<*T*>,{}] is V1() V2() set

[6,<*T*>] is V1() set

{6,<*T*>} is non empty set

{6} is non empty trivial 1 -element set

{{6,<*T*>},{6}} is non empty set

[[6,<*T*>],{}] is V1() set

{[6,<*T*>],{}} is non empty set

{[6,<*T*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[6,<*T*>],{}},{[6,<*T*>]}} is non empty set

f1 is Element of Segm 9

[f1,<*T*>,{}] is V1() V2() set

[f1,<*T*>] is V1() set

{f1,<*T*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*T*>},{f1}} is non empty set

[[f1,<*T*>],{}] is V1() set

{[f1,<*T*>],{}} is non empty set

{[f1,<*T*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*T*>],{}},{[f1,<*T*>]}} is non empty set

T is set

f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

f2 is Element of ()

<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

[T,<*f1*>,<*f2*>] is V1() V2() set

[T,<*f1*>] is V1() set

{T,<*f1*>} is non empty set

{T} is non empty trivial 1 -element set

{{T,<*f1*>},{T}} is non empty set

[[T,<*f1*>],<*f2*>] is V1() set

{[T,<*f1*>],<*f2*>} is non empty set

{[T,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,<*f1*>],<*f2*>},{[T,<*f1*>]}} is non empty set

p is Element of Segm 9

[p,<*f1*>,<*f2*>] is V1() V2() set

[p,<*f1*>] is V1() set

{p,<*f1*>} is non empty set

{p} is non empty trivial 1 -element set

{{p,<*f1*>},{p}} is non empty set

[[p,<*f1*>],<*f2*>] is V1() set

{[p,<*f1*>],<*f2*>} is non empty set

{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set

T is set

f1 is Element of ()

f2 is Element of ()

<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

K183(1,1) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

[T,{},<*f1,f2*>] is V1() V2() set

[T,{}] is V1() set

{T,{}} is non empty set

{T} is non empty trivial 1 -element set

{{T,{}},{T}} is non empty set

[[T,{}],<*f1,f2*>] is V1() set

{[T,{}],<*f1,f2*>} is non empty set

{[T,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,{}],<*f1,f2*>},{[T,{}]}} is non empty set

p is Element of Segm 9

[p,{},<*f1,f2*>] is V1() V2() set

[p,{}] is V1() set

{p,{}} is non empty set

{p} is non empty trivial 1 -element set

{{p,{}},{p}} is non empty set

[[p,{}],<*f1,f2*>] is V1() set

{[p,{}],<*f1,f2*>} is non empty set

{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set

T is Element of ()

p is Element of Segm 9

f1 is Element of ()

f2 is Element of ()

<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

K183(1,1) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

[p,{},<*f1,f2*>] is V1() V2() set

[p,{}] is V1() set

{p,{}} is non empty set

{p} is non empty trivial 1 -element set

{{p,{}},{p}} is non empty set

[[p,{}],<*f1,f2*>] is V1() set

{[p,{}],<*f1,f2*>} is non empty set

{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set

T `3_3 is set

<*f1,f2*> /. 1 is Element of ()

i1 is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

J is Element of ()

i1 /. 1 is Element of ()

a is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

K is Element of ()

a /. 1 is Element of ()

<*f1,f2*> /. 2 is Element of ()

i1 is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

J is Element of ()

i1 /. 2 is Element of ()

a is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

K is Element of ()

a /. 2 is Element of ()

T is Element of ()

(T) is Element of ()

(T) is Element of ()

f1 is Element of ()

f2 is Element of ()

<*f1,f2*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f1*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f1*>,<*f2*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

p is Element of Segm 9

[p,{},<*f1,f2*>] is V1() V2() set

[p,{}] is V1() set

{p,{}} is non empty set

{p} is non empty trivial 1 -element set

{{p,{}},{p}} is non empty set

[[p,{}],<*f1,f2*>] is V1() set

{[p,{}],<*f1,f2*>} is non empty set

{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,{}],<*f1,f2*>},{[p,{}]}} is non empty set

T `3_3 is set

J is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

J /. 1 is Element of ()

K is Relation-like NAT -defined () -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of ()

K /. 2 is Element of ()

T is Element of ()

f2 is Element of Segm 9

f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

[f2,<*f1*>,{}] is V1() V2() set

[f2,<*f1*>] is V1() set

{f2,<*f1*>} is non empty set

{f2} is non empty trivial 1 -element set

{{f2,<*f1*>},{f2}} is non empty set

[[f2,<*f1*>],{}] is V1() set

{[f2,<*f1*>],{}} is non empty set

{[f2,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f2,<*f1*>],{}},{[f2,<*f1*>]}} is non empty set

T `2_3 is set

K13(T) is set

K13(T) `3_3 is set

<*f1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

K is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT

p is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

K /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

i1 is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT

J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

i1 /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

T is Element of ()

(T) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

f2 is Element of Segm 9

[f2,<*f1*>,{}] is V1() V2() set

[f2,<*f1*>] is V1() set

{f2,<*f1*>} is non empty set

{f2} is non empty trivial 1 -element set

{{f2,<*f1*>},{f2}} is non empty set

[[f2,<*f1*>],{}] is V1() set

{[f2,<*f1*>],{}} is non empty set

{[f2,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f2,<*f1*>],{}},{[f2,<*f1*>]}} is non empty set

T `2_3 is set

K13(T) is set

K13(T) `3_3 is set

p is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT

p /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

T is Element of ()

p is Element of Segm 9

f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

f2 is Element of ()

<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

[p,<*f1*>,<*f2*>] is V1() V2() set

[p,<*f1*>] is V1() set

{p,<*f1*>} is non empty set

{p} is non empty trivial 1 -element set

{{p,<*f1*>},{p}} is non empty set

[[p,<*f1*>],<*f2*>] is V1() set

{[p,<*f1*>],<*f2*>} is non empty set

{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set

T `2_3 is set

K13(T) is set

K13(T) `3_3 is set

<*f1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,i1] is V1() set

{1,i1} is non empty set

{{1,i1},{1}} is non empty set

{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set

J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*i1*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

a is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*a*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,a] is V1() set

{1,a} is non empty set

{{1,a},{1}} is non empty set

{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set

K is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*a*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

T `3_3 is set

<*f2*> /. 1 is Element of ()

i1 is Element of ()

<*i1*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,i1] is V1() set

{1,i1} is non empty set

{{1,i1},{1}} is non empty set

{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set

J is Element of ()

<*i1*> /. 1 is Element of ()

a is Element of ()

<*a*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,a] is V1() set

{1,a} is non empty set

{{1,a},{1}} is non empty set

{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set

K is Element of ()

<*a*> /. 1 is Element of ()

T is Element of ()

(T) is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

(T) is Element of ()

f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f1] is V1() set

{1,f1} is non empty set

{{1,f1},{1}} is non empty set

{[1,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

f2 is Element of ()

<*f2*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

p is Element of Segm 9

[p,<*f1*>,<*f2*>] is V1() V2() set

[p,<*f1*>] is V1() set

{p,<*f1*>} is non empty set

{p} is non empty trivial 1 -element set

{{p,<*f1*>},{p}} is non empty set

[[p,<*f1*>],<*f2*>] is V1() set

{[p,<*f1*>],<*f2*>} is non empty set

{[p,<*f1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,<*f1*>],<*f2*>},{[p,<*f1*>]}} is non empty set

T `2_3 is set

K13(T) is set

K13(T) `3_3 is set

J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,J] is V1() set

{1,J} is non empty set

{{1,J},{1}} is non empty set

{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set

<*J*> /. 1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

T `3_3 is set

K is Element of ()

<*K*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,K] is V1() set

{1,K} is non empty set

{{1,K},{1}} is non empty set

{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set

<*K*> /. 1 is Element of ()

NAT * is non empty functional FinSequence-membered set

proj2 () is set

[:NAT,(NAT *),(proj2 ()):] is set

T is set

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,{}] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],{}] is V1() set

{[f1,<*f2*>],{}} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

p is Element of ()

<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,<*p*>] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],<*p*>] is V1() set

{[f1,<*f2*>],<*p*>} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set

f1 is Element of Segm 9

f2 is Element of ()

p is Element of ()

<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[f1,{},<*f2,p*>] is V1() V2() set

[f1,{}] is V1() set

{f1,{}} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,{}},{f1}} is non empty set

[[f1,{}],<*f2,p*>] is V1() set

{[f1,{}],<*f2,p*>} is non empty set

{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set

T is set

f1 is set

[f1,T] is V1() set

{f1,T} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,T},{f1}} is non empty set

p is Element of Segm 9

J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,J] is V1() set

{1,J} is non empty set

{{1,J},{1}} is non empty set

{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set

[p,<*J*>,{}] is V1() V2() set

[p,<*J*>] is V1() set

{p,<*J*>} is non empty set

{p} is non empty trivial 1 -element set

{{p,<*J*>},{p}} is non empty set

[[p,<*J*>],{}] is V1() set

{[p,<*J*>],{}} is non empty set

{[p,<*J*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,<*J*>],{}},{[p,<*J*>]}} is non empty set

p is Element of Segm 9

J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*J*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,J] is V1() set

{1,J} is non empty set

{{1,J},{1}} is non empty set

{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set

K is Element of ()

<*K*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,K] is V1() set

{1,K} is non empty set

{{1,K},{1}} is non empty set

{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set

[p,<*J*>,<*K*>] is V1() V2() set

[p,<*J*>] is V1() set

{p,<*J*>} is non empty set

{p} is non empty trivial 1 -element set

{{p,<*J*>},{p}} is non empty set

[[p,<*J*>],<*K*>] is V1() set

{[p,<*J*>],<*K*>} is non empty set

{[p,<*J*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,<*J*>],<*K*>},{[p,<*J*>]}} is non empty set

p is Element of Segm 9

J is Element of ()

K is Element of ()

<*J,K*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*J*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,J] is V1() set

{1,J} is non empty set

{{1,J},{1}} is non empty set

{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set

<*K*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,K] is V1() set

{1,K} is non empty set

{{1,K},{1}} is non empty set

{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*J*>,<*K*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[p,{},<*J,K*>] is V1() V2() set

[p,{}] is V1() set

{p,{}} is non empty set

{p} is non empty trivial 1 -element set

{{p,{}},{p}} is non empty set

[[p,{}],<*J,K*>] is V1() set

{[p,{}],<*J,K*>} is non empty set

{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,{}],<*J,K*>},{[p,{}]}} is non empty set

T is Element of ()

T `1_3 is set

K13(T) is set

K13(K13(T)) is set

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,{}] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],{}] is V1() set

{[f1,<*f2*>],{}} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

p is Element of ()

<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,<*p*>] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],<*p*>] is V1() set

{[f1,<*f2*>],<*p*>} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set

f1 is Element of Segm 9

f2 is Element of ()

p is Element of ()

<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[f1,{},<*f2,p*>] is V1() V2() set

[f1,{}] is V1() set

{f1,{}} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,{}},{f1}} is non empty set

[[f1,{}],<*f2,p*>] is V1() set

{[f1,{}],<*f2,p*>} is non empty set

{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set

T is non empty set

T * is non empty functional FinSequence-membered set

[:NAT,(NAT *),(T *):] is set

T is Element of ()

InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K13(T) is set

K13(K13(T)) is set

T is Element of ()

InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K13(T) is set

K13(K13(T)) is set

T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(T) `3_3 is set

f1 is Element of Segm 9

f2 is Element of ()

p is Element of ()

<*f2,p*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*f2*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*f2*>,<*p*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[f1,{},<*f2,p*>] is V1() V2() set

[f1,{}] is V1() set

{f1,{}} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,{}},{f1}} is non empty set

[[f1,{}],<*f2,p*>] is V1() set

{[f1,{}],<*f2,p*>} is non empty set

{[f1,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,{}],<*f2,p*>},{[f1,{}]}} is non empty set

T is Element of ()

InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K13(T) is set

K13(K13(T)) is set

T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(T) `3_3 is set

dom (T `2_3) is Element of bool NAT

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

p is Element of ()

<*p*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,p] is V1() set

{1,p} is non empty set

{{1,p},{1}} is non empty set

{[1,p]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,<*p*>] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],<*p*>] is V1() set

{[f1,<*f2*>],<*p*>} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],<*p*>},{[f1,<*f2*>]}} is non empty set

T is Element of ()

InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K13(T) is set

K13(K13(T)) is set

T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(T) `3_3 is set

dom (T `2_3) is Element of bool NAT

f1 is Element of Segm 9

f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*f2*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,f2] is V1() set

{1,f2} is non empty set

{{1,f2},{1}} is non empty set

{[1,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

[f1,<*f2*>,{}] is V1() V2() set

[f1,<*f2*>] is V1() set

{f1,<*f2*>} is non empty set

{f1} is non empty trivial 1 -element set

{{f1,<*f2*>},{f1}} is non empty set

[[f1,<*f2*>],{}] is V1() set

{[f1,<*f2*>],{}} is non empty set

{[f1,<*f2*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[f1,<*f2*>],{}},{[f1,<*f2*>]}} is non empty set

T is Element of ()

InsCode T is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K13(T) is set

K13(K13(T)) is set

f1 is Element of ()

InsCode f1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(f1) is set

K13(K13(f1)) is set

T `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(T) `3_3 is set

dom (T `2_3) is Element of bool NAT

f1 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(f1) `3_3 is set

dom (f1 `2_3) is Element of bool NAT

InsCodes () is non empty set

K23(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

T is Element of InsCodes ()

f1 is set

[T,f1] is V1() set

{T,f1} is non empty set

{T} is non empty trivial 1 -element set

{{T,f1},{T}} is non empty set

f2 is set

[[T,f1],f2] is V1() set

{[T,f1],f2} is non empty set

{[T,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,f1],f2},{[T,f1]}} is non empty set

[T,f1,f2] is V1() V2() set

p is Element of ()

InsCode p is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(p) is set

K13(K13(p)) is set

{0} is non empty trivial functional 1 -element Element of bool NAT

T is Element of InsCodes ()

JumpParts T is non empty functional set

{ (b

f1 is set

f2 is Element of ()

f2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(f2) is set

K13(f2) `3_3 is set

InsCode f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(K13(f2)) is set

f1 is set

[(),{},{}] `2_3 is set

K13([(),{},{}]) is set

K13([(),{},{}]) `3_3 is set

[(),{},{}] `1_3 is set

K13(K13([(),{},{}])) is set

{{}} is non empty trivial functional 1 -element set

T is Element of InsCodes ()

JumpParts T is non empty functional set

{ (b

f1 is set

f2 is Element of ()

f2 `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(f2) is set

K13(f2) `3_3 is set

InsCode f2 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(K13(f2)) is set

p is Element of Segm 9

J is Element of ()

K is Element of ()

<*J,K*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<*J*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,J] is V1() set

{1,J} is non empty set

{{1,J},{1}} is non empty set

{[1,J]} is non empty trivial Relation-like Function-like constant 1 -element set

<*K*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1,K] is V1() set

{1,K} is non empty set

{{1,K},{1}} is non empty set

{[1,K]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<*J*>,<*K*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[p,{},<*J,K*>] is V1() V2() set

[p,{}] is V1() set

{p,{}} is non empty set

{p} is non empty trivial 1 -element set

{{p,{}},{p}} is non empty set

[[p,{}],<*J,K*>] is V1() set

{[p,{}],<*J,K*>} is non empty set

{[p,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[p,{}],<*J,K*>},{[p,{}]}} is non empty set

the Element of () is Element of ()

f2 is set

<* the Element of (), the Element of ()*> is non empty Relation-like NAT -defined () -valued Function-like V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of ()

<* the Element of ()*> is non empty trivial Relation-like NAT -defined Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like set

[1, the Element of ()] is V1() set

{1, the Element of ()} is non empty set

{{1, the Element of ()},{1}} is non empty set

{[1, the Element of ()]} is non empty trivial Relation-like Function-like constant 1 -element set

K116(<* the Element of ()*>,<* the Element of ()*>) is non empty Relation-like NAT -defined Function-like V24() K183(1,1) -element FinSequence-like FinSubsequence-like set

[T,{},<* the Element of (), the Element of ()*>] is V1() V2() set

[T,{}] is V1() set

{T,{}} is non empty set

{T} is non empty trivial 1 -element set

{{T,{}},{T}} is non empty set

[[T,{}],<* the Element of (), the Element of ()*>] is V1() set

{[T,{}],<* the Element of (), the Element of ()*>} is non empty set

{[T,{}]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,{}],<* the Element of (), the Element of ()*>},{[T,{}]}} is non empty set

[T,{},<* the Element of (), the Element of ()*>] `2_3 is set

K13([T,{},<* the Element of (), the Element of ()*>]) is set

K13([T,{},<* the Element of (), the Element of ()*>]) `3_3 is set

[T,{},<* the Element of (), the Element of ()*>] `1_3 is set

K13(K13([T,{},<* the Element of (), the Element of ()*>])) is set

T is Element of InsCodes ()

JumpParts T is non empty functional set

{ (b

f1 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 f1 is set

f2 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 f2 is set

p is set

[T,f1,p] is V1() V2() set

[T,f1] is V1() set

{T,f1} is non empty set

{T} is non empty trivial 1 -element set

{{T,f1},{T}} is non empty set

[[T,f1],p] is V1() set

{[T,f1],p} is non empty set

{[T,f1]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,f1],p},{[T,f1]}} is non empty set

[T,f2,p] is V1() V2() set

[T,f2] is V1() set

{T,f2} is non empty set

{{T,f2},{T}} is non empty set

[[T,f2],p] is V1() set

{[T,f2],p} is non empty set

{[T,f2]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[T,f2],p},{[T,f2]}} is non empty set

J is Element of ()

InsCode J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(J) is set

K13(K13(J)) is set

K is Element of Segm 9

i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,i1] is V1() set

{1,i1} is non empty set

{{1,i1},{1}} is non empty set

{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set

[K,<*i1*>,{}] is V1() V2() set

[K,<*i1*>] is V1() set

{K,<*i1*>} is non empty set

{K} is non empty trivial 1 -element set

{{K,<*i1*>},{K}} is non empty set

[[K,<*i1*>],{}] is V1() set

{[K,<*i1*>],{}} is non empty set

{[K,<*i1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[K,<*i1*>],{}},{[K,<*i1*>]}} is non empty set

f2 . 1 is V17() V18() V19() V23() V24() cardinal V39() V41() V42() ext-real set

[T,f2,{}] is V1() V2() set

[[T,f2],{}] is V1() set

{[T,f2],{}} is non empty set

{{[T,f2],{}},{[T,f2]}} is non empty set

a is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*a*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,a] is V1() set

{1,a} is non empty set

{{1,a},{1}} is non empty set

{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set

[6,<*a*>,{}] is V1() V2() set

[6,<*a*>] is V1() set

{6,<*a*>} is non empty set

{6} is non empty trivial 1 -element set

{{6,<*a*>},{6}} is non empty set

[[6,<*a*>],{}] is V1() set

{[6,<*a*>],{}} is non empty set

{[6,<*a*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[6,<*a*>],{}},{[6,<*a*>]}} is non empty set

I is Element of ()

I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued set

K13(I) is set

K13(I) `3_3 is set

J is Element of ()

InsCode J is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of InsCodes ()

K13(J) is set

K13(K13(J)) is set

K is Element of Segm 9

i1 is V17() V18() V19() V23() V24() cardinal V39() V42() ext-real Element of NAT

<*i1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V50() decreasing non-decreasing non-increasing FinSequence of NAT

[1,i1] is V1() set

{1,i1} is non empty set

{{1,i1},{1}} is non empty set

{[1,i1]} is non empty trivial Relation-like Function-like constant 1 -element set

a is Element of ()

<*a*> is non empty trivial Relation-like NAT -defined () -valued Function-like constant V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of ()

[1,a] is V1() set

{1,a} is non empty set

{{1,a},{1}} is non empty set

{[1,a]} is non empty trivial Relation-like Function-like constant 1 -element set

[K,<*i1*>,<*a*>] is V1() V2() set

[K,<*i1*>] is V1() set

{K,<*i1*>} is non empty set

{K} is non empty trivial 1 -element set

{{K,<*i1*>},{K}} is non empty set

[[K,<*i1*>],<*a*>] is V1() set

{[K,<*i1*>],<*a*>} is non empty set

{[K,<*i1*>]} is non empty trivial Relation-like Function-like constant 1 -element set

{{[K,<*i1*>],<*a*>},{[K,<*i1*>]}} is non empty set

f2 . 1 is V17() V18() V19() V23() V24() cardinal V39() V41() V42() ext-real set

l is V17() V18() V19()