:: SCMPDS_I semantic presentation

REAL is non empty V24() set

NAT is V6() V7() V8() non empty Element of bool REAL

bool REAL is set

NAT is V6() V7() V8() non empty set

bool NAT is set

bool NAT is set

9 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

Segm 9 is non empty Element of bool NAT

SCM-Data-Loc is non empty set

K158() is set

bool K158() is set

2 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

[:K158(),2:] is Relation-like set

bool [:K158(),2:] is set

K160() is Relation-like Function-like V36(K158(),2) Element of bool [:K158(),2:]

K161() is Relation-like 2 -defined Function-like total set

K160() * K161() is Relation-like Function-like set

K133((K160() * K161())) is set

SCM-Instr is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set

K120(K133((K160() * K161())),K133((K160() * K161()))) is set

[:SCM-Instr,K120(K133((K160() * K161())),K133((K160() * K161()))):] is Relation-like set

bool [:SCM-Instr,K120(K133((K160() * K161())),K133((K160() * K161()))):] is set

RAT is non empty V24() set

INT is non empty V24() set

1 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

3 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

4 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

5 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

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

{ b

{1} is non empty set

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

{ b

{1,2} is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered V44() integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty V24() FinSequence-like FinSubsequence-like FinSequence-membered V44() integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of NAT

K180(NAT,0) is functional non empty Element of bool NAT

14 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

6 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

7 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

8 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

10 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

11 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

12 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

13 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

15 is V6() V7() V8() V12() non empty V44() integer ext-real positive non negative Element of NAT

Segm 15 is non empty Element of bool NAT

SCM-Data-Loc \/ INT is non empty set

T is V44() integer set

[0,{},{}] is V21() V22() set

[0,{}] is V21() set

{0,{}} is functional non empty set

{0} is functional non empty set

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

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

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

{[0,{}]} is Relation-like Function-like non empty set

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

{[0,{},{}]} is Relation-like non empty standard-ins homogeneous J/A-independent with_halt set

{ [14,{},<*b

{[0,{},{}]} \/ { [14,{},<*b

{ [1,{},<*b

({[0,{},{}]} \/ { [14,{},<*b

{2,3} is non empty set

{ [b

(({[0,{},{}]} \/ { [14,{},<*b

{4,5,6,7,8} is set

{ [b

((({[0,{},{}]} \/ { [14,{},<*b

{9,10,11,12,13} is set

{ [b

(((({[0,{},{}]} \/ { [14,{},<*b

() is set

<*0*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT

[1,0] is V21() set

{1,0} is non empty set

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

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

[14,{},<*0*>] is V21() V22() set

[14,{}] is V21() set

{14,{}} is non empty set

{14} is non empty set

{{14,{}},{14}} is non empty set

[[14,{}],<*0*>] is V21() set

{[14,{}],<*0*>} is non empty set

{[14,{}]} is Relation-like Function-like non empty set

{{[14,{}],<*0*>},{[14,{}]}} is non empty set

T is Element of SCM-Data-Loc

f1 is V44() integer set

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

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

[1,T] is V21() set

{1,T} is non empty set

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

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

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

[1,f1] is V21() set

{1,f1} is non empty set

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

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

K75(<*T*>,<*f1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

K210(1,1) is V6() V7() V8() V12() V44() integer ext-real Element of NAT

f2 is set

proj2 <*T,f1*> is non empty set

dom <*T,f1*> is non empty Element of bool NAT

p is set

<*T,f1*> . p is set

T is Element of ()

f2 is Element of Segm 15

f1 is Element of SCM-Data-Loc

<*f1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc

[1,f1] is V21() set

{1,f1} is non empty set

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

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

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

[f2,{}] is V21() set

{f2,{}} is non empty set

{f2} is non empty set

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

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

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

{[f2,{}]} is Relation-like Function-like non empty set

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

T `3_3 is set

<*f1*> /. 1 is Element of SCM-Data-Loc

c1 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc

p is Element of SCM-Data-Loc

c1 /. 1 is Element of SCM-Data-Loc

c2 is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc

i is Element of SCM-Data-Loc

c2 /. 1 is Element of SCM-Data-Loc

T is Element of Segm 15

f1 is Element of ()

(f1) is Element of SCM-Data-Loc

f2 is Element of SCM-Data-Loc

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

[T,{},<*f2*>] is V21() V22() set

[T,{}] is V21() set

{T,{}} is non empty set

{T} is non empty set

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

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

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

{[T,{}]} is Relation-like Function-like non empty set

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

f1 `3_3 is set

p is Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc

p /. 1 is Element of SCM-Data-Loc

T is Element of ()

f2 is Element of Segm 15

f1 is V44() integer set

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

[1,f1] is V21() set

{1,f1} is non empty set

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

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

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

[f2,{}] is V21() set

{f2,{}} is non empty set

{f2} is non empty set

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

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

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

{[f2,{}]} is Relation-like Function-like non empty set

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

T `3_3 is set

p is V44() integer Element of INT

<*p*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT

[1,p] is V21() set

{1,p} is non empty set

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

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

<*p*> /. 1 is V44() integer Element of INT

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

p is V44() integer set

c1 /. 1 is V44() integer Element of INT

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

i is V44() integer set

c2 /. 1 is V44() integer Element of INT

T is Element of Segm 15

f1 is Element of ()

(f1) is V44() integer set

f2 is V44() integer set

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

[T,{},<*f2*>] is V21() V22() set

[T,{}] is V21() set

{T,{}} is non empty set

{T} is non empty set

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

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

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

{[T,{}]} is Relation-like Function-like non empty set

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

f1 `3_3 is set

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

p /. 1 is V44() integer Element of INT

T is Element of ()

p is Element of Segm 15

f1 is Element of SCM-Data-Loc

f2 is V44() integer set

(f1,f2) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,f1] is V21() set

{1,f1} is non empty set

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

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

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

[p,{},(f1,f2)] is V21() V22() set

[p,{}] is V21() set

{p,{}} is non empty set

{p} is non empty set

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

[[p,{}],(f1,f2)] is V21() set

{[p,{}],(f1,f2)} is non empty set

{[p,{}]} is Relation-like Function-like non empty set

{{[p,{}],(f1,f2)},{[p,{}]}} is non empty set

T `3_3 is set

(f1,f2) /. 1 is Element of SCM-Data-Loc \/ INT

c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

i is Element of SCM-Data-Loc

c2 /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 is Element of SCM-Data-Loc

f /. 1 is Element of SCM-Data-Loc \/ INT

(f1,f2) /. 2 is Element of SCM-Data-Loc \/ INT

c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

i is V44() integer set

c2 /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 is V44() integer set

f /. 2 is Element of SCM-Data-Loc \/ INT

T is Element of Segm 15

f1 is Element of ()

(f1) is Element of SCM-Data-Loc

(f1) is V44() integer set

f2 is Element of SCM-Data-Loc

p is V44() integer set

(f2,p) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

[T,{},(f2,p)] is V21() V22() set

[T,{}] is V21() set

{T,{}} is non empty set

{T} is non empty set

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

[[T,{}],(f2,p)] is V21() set

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

{[T,{}]} is Relation-like Function-like non empty set

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

f1 `3_3 is set

i is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

i /. 1 is Element of SCM-Data-Loc \/ INT

c1 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 /. 2 is Element of SCM-Data-Loc \/ INT

T is Element of ()

i is Element of Segm 15

f1 is Element of SCM-Data-Loc

f2 is V44() integer set

p is V44() integer set

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

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

[1,f1] is V21() set

{1,f1} is non empty set

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

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

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

K210(K210(1,1),1) is V6() V7() V8() V12() V44() integer ext-real Element of NAT

[i,{},<*f1,f2,p*>] is V21() V22() set

[i,{}] is V21() set

{i,{}} is non empty set

{i} is non empty set

{{i,{}},{i}} is non empty set

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

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

{[i,{}]} is Relation-like Function-like non empty set

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

T `3_3 is set

c1 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

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

[1,c2] is V21() set

{1,c2} is non empty set

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

{[1,c2]} is Relation-like Function-like non empty set

K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

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

[1,f] is V21() set

{1,f} is non empty set

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

{[1,f]} is Relation-like Function-like non empty set

K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 is Element of SCM-Data-Loc

f /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc

f /. 1 is Element of SCM-Data-Loc \/ INT

c1 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

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

[1,c2] is V21() set

{1,c2} is non empty set

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

{[1,c2]} is Relation-like Function-like non empty set

K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

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

[1,f] is V21() set

{1,f} is non empty set

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

{[1,f]} is Relation-like Function-like non empty set

K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 is V44() integer set

f /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is V44() integer set

f /. 2 is Element of SCM-Data-Loc \/ INT

c1 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c1,c2,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

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

[1,c2] is V21() set

{1,c2} is non empty set

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

{[1,c2]} is Relation-like Function-like non empty set

K75(<*c1*>,<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

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

[1,f] is V21() set

{1,f} is non empty set

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

{[1,f]} is Relation-like Function-like non empty set

K75(K75(<*c1*>,<*c2*>),<*f*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 3 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 is V44() integer set

f /. 3 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is V44() integer set

f /. 3 is Element of SCM-Data-Loc \/ INT

T is Element of Segm 15

f1 is Element of ()

(f1) is Element of SCM-Data-Loc

(f1) is V44() integer set

(f1) is V44() integer set

f2 is Element of SCM-Data-Loc

p is V44() integer set

i is V44() integer set

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

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

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

[T,{},<*f2,p,i*>] is V21() V22() set

[T,{}] is V21() set

{T,{}} is non empty set

{T} is non empty set

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

[[T,{}],<*f2,p,i*>] is V21() set

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

{[T,{}]} is Relation-like Function-like non empty set

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

f1 `3_3 is set

c1 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c1 /. 1 is Element of SCM-Data-Loc \/ INT

c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 3 is Element of SCM-Data-Loc \/ INT

T is Element of ()

c1 is Element of Segm 15

f1 is Element of SCM-Data-Loc

f2 is Element of SCM-Data-Loc

p is V44() integer set

i is V44() integer set

<*f1,f2,p,i*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set

[c1,{},<*f1,f2,p,i*>] is V21() V22() set

[c1,{}] is V21() set

{c1,{}} is non empty set

{c1} is non empty set

{{c1,{}},{c1}} is non empty set

[[c1,{}],<*f1,f2,p,i*>] is V21() set

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

{[c1,{}]} is Relation-like Function-like non empty set

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

T `3_3 is set

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc

f /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc

f /. 1 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc

f /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc

f /. 2 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 3 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is V44() integer set

f /. 3 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is V44() integer set

f /. 3 is Element of SCM-Data-Loc \/ INT

c2 is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

f is Element of SCM-Data-Loc \/ INT

<*c2,f,f,f*> is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 4 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 is V44() integer set

f /. 4 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f is V44() integer set

f /. 4 is Element of SCM-Data-Loc \/ INT

T is Element of Segm 15

f1 is Element of ()

(f1) is Element of SCM-Data-Loc

(f1) is Element of SCM-Data-Loc

(f1) is V44() integer set

(f1) is V44() integer set

f2 is Element of SCM-Data-Loc

p is Element of SCM-Data-Loc

i is V44() integer set

c1 is V44() integer set

<*f2,p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set

[T,{},<*f2,p,i,c1*>] is V21() V22() set

[T,{}] is V21() set

{T,{}} is non empty set

{T} is non empty set

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

[[T,{}],<*f2,p,i,c1*>] is V21() set

{[T,{}],<*f2,p,i,c1*>} is non empty set

{[T,{}]} is Relation-like Function-like non empty set

{{[T,{}],<*f2,p,i,c1*>},{[T,{}]}} is non empty set

f1 `3_3 is set

c2 is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

c2 /. 1 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 2 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 3 is Element of SCM-Data-Loc \/ INT

f is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

f /. 4 is Element of SCM-Data-Loc \/ INT

() is V6() V7() V8() V12() V44() integer ext-real Element of NAT

() is V6() V7() V8() V12() V44() integer ext-real Element of NAT

{ [b

T is Element of ()

T `1_3 is set

K41(T) is set

K41(K41(T)) is set

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

f1 is V44() integer Element of INT

<*f1*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT

[1,f1] is V21() set

{1,f1} is non empty set

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

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

[14,{},<*f1*>] is V21() V22() set

[[14,{}],<*f1*>] is V21() set

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

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

f1 is Element of SCM-Data-Loc

<*f1*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc

[1,f1] is V21() set

{1,f1} is non empty set

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

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

[1,{},<*f1*>] is V21() V22() set

[1,{}] is V21() set

{1,{}} is non empty set

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

[[1,{}],<*f1*>] is V21() set

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

{[1,{}]} is Relation-like Function-like non empty set

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

f1 is Element of Segm 15

f2 is Element of SCM-Data-Loc

p is V44() integer Element of INT

(f2,p) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

[f1,{},(f2,p)] is V21() V22() set

[f1,{}] is V21() set

{f1,{}} is non empty set

{f1} is non empty set

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

[[f1,{}],(f2,p)] is V21() set

{[f1,{}],(f2,p)} is non empty set

{[f1,{}]} is Relation-like Function-like non empty set

{{[f1,{}],(f2,p)},{[f1,{}]}} is non empty set

f1 is Element of Segm 15

f2 is Element of SCM-Data-Loc

p is V44() integer Element of INT

i is V44() integer Element of INT

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

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

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

[f1,{},<*f2,p,i*>] is V21() V22() set

[f1,{}] is V21() set

{f1,{}} is non empty set

{f1} is non empty set

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

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

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

{[f1,{}]} is Relation-like Function-like non empty set

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

f1 is Element of Segm 15

f2 is Element of SCM-Data-Loc

p is Element of SCM-Data-Loc

i is V44() integer Element of INT

c1 is V44() integer Element of INT

<*f2,p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set

[f1,{},<*f2,p,i,c1*>] is V21() V22() set

[f1,{}] is V21() set

{f1,{}} is non empty set

{f1} is non empty set

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

[[f1,{}],<*f2,p,i,c1*>] is V21() set

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

{[f1,{}]} is Relation-like Function-like non empty set

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

proj2 () is set

T is set

f1 is set

[f1,T] is V21() set

{f1,T} is non empty set

{f1} is non empty set

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

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

{ [14,{},<*b

{[0,{},{}]} \/ ( { [14,{},<*b

({[0,{},{}]} \/ ( { [14,{},<*b

p is V44() integer Element of INT

<*p*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT

[1,p] is V21() set

{1,p} is non empty set

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

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

[14,{},<*p*>] is V21() V22() set

[[14,{}],<*p*>] is V21() set

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

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

p is Element of SCM-Data-Loc

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

[1,p] is V21() set

{1,p} is non empty set

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

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

[1,{},<*p*>] is V21() V22() set

[1,{}] is V21() set

{1,{}} is non empty set

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

[[1,{}],<*p*>] is V21() set

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

{[1,{}]} is Relation-like Function-like non empty set

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

p is Element of Segm 15

i is Element of SCM-Data-Loc

c1 is V44() integer Element of INT

(i,c1) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

K75(<*i*>,<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

[p,{},(i,c1)] is V21() V22() set

[p,{}] is V21() set

{p,{}} is non empty set

{p} is non empty set

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

[[p,{}],(i,c1)] is V21() set

{[p,{}],(i,c1)} is non empty set

{[p,{}]} is Relation-like Function-like non empty set

{{[p,{}],(i,c1)},{[p,{}]}} is non empty set

p is Element of Segm 15

i is Element of SCM-Data-Loc

c1 is V44() integer Element of INT

c2 is V44() integer Element of INT

<*i,c1,c2*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

K75(<*i*>,<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

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

[1,c2] is V21() set

{1,c2} is non empty set

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

{[1,c2]} is Relation-like Function-like non empty set

K75(K75(<*i*>,<*c1*>),<*c2*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set

[p,{},<*i,c1,c2*>] is V21() V22() set

[p,{}] is V21() set

{p,{}} is non empty set

{p} is non empty set

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

[[p,{}],<*i,c1,c2*>] is V21() set

{[p,{}],<*i,c1,c2*>} is non empty set

{[p,{}]} is Relation-like Function-like non empty set

{{[p,{}],<*i,c1,c2*>},{[p,{}]}} is non empty set

p is Element of Segm 15

i is Element of SCM-Data-Loc

c1 is Element of SCM-Data-Loc

c2 is V44() integer Element of INT

f is V44() integer Element of INT

<*i,c1,c2,f*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set

[p,{},<*i,c1,c2,f*>] is V21() V22() set

[p,{}] is V21() set

{p,{}} is non empty set

{p} is non empty set

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

[[p,{}],<*i,c1,c2,f*>] is V21() set

{[p,{}],<*i,c1,c2,f*>} is non empty set

{[p,{}]} is Relation-like Function-like non empty set

{{[p,{}],<*i,c1,c2,f*>},{[p,{}]}} is non empty set

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

T is non empty set

T * is functional non empty FinSequence-membered set

NAT * is functional non empty FinSequence-membered set

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

f1 is set

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

f2 is V44() integer Element of INT

<*f2*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT

[1,f2] is V21() set

{1,f2} is non empty set

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

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

[14,{},<*f2*>] is V21() V22() set

[[14,{}],<*f2*>] is V21() set

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

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

f2 is Element of SCM-Data-Loc

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

[1,f2] is V21() set

{1,f2} is non empty set

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

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

[1,{},<*f2*>] is V21() V22() set

[1,{}] is V21() set

{1,{}} is non empty set

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

[[1,{}],<*f2*>] is V21() set

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

{[1,{}]} is Relation-like Function-like non empty set

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

f2 is Element of Segm 15

p is Element of SCM-Data-Loc

i is V44() integer Element of INT

(p,i) is Relation-like NAT -defined SCM-Data-Loc \/ INT -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like FinSequence of SCM-Data-Loc \/ INT

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

K75(<*p*>,<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

[f2,{},(p,i)] is V21() V22() set

[f2,{}] is V21() set

{f2,{}} is non empty set

{f2} is non empty set

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

[[f2,{}],(p,i)] is V21() set

{[f2,{}],(p,i)} is non empty set

{[f2,{}]} is Relation-like Function-like non empty set

{{[f2,{}],(p,i)},{[f2,{}]}} is non empty set

f2 is Element of Segm 15

p is Element of SCM-Data-Loc

i is V44() integer Element of INT

c1 is V44() integer Element of INT

<*p,i,c1*> is Relation-like NAT -defined Function-like non empty V24() 3 -element FinSequence-like FinSubsequence-like set

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

[1,p] is V21() set

{1,p} is non empty set

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

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

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

[1,i] is V21() set

{1,i} is non empty set

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

{[1,i]} is Relation-like Function-like non empty set

K75(<*p*>,<*i*>) is Relation-like NAT -defined Function-like non empty V24() K210(1,1) -element FinSequence-like FinSubsequence-like set

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

[1,c1] is V21() set

{1,c1} is non empty set

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

{[1,c1]} is Relation-like Function-like non empty set

K75(K75(<*p*>,<*i*>),<*c1*>) is Relation-like NAT -defined Function-like non empty V24() K210(K210(1,1),1) -element FinSequence-like FinSubsequence-like set

[f2,{},<*p,i,c1*>] is V21() V22() set

[f2,{}] is V21() set

{f2,{}} is non empty set

{f2} is non empty set

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

[[f2,{}],<*p,i,c1*>] is V21() set

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

{[f2,{}]} is Relation-like Function-like non empty set

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

f2 is Element of Segm 15

p is Element of SCM-Data-Loc

i is Element of SCM-Data-Loc

c1 is V44() integer Element of INT

c2 is V44() integer Element of INT

<*p,i,c1,c2*> is Relation-like NAT -defined Function-like non empty V24() 4 -element FinSequence-like FinSubsequence-like set

[f2,{},<*p,i,c1,c2*>] is V21() V22() set

[f2,{}] is V21() set

{f2,{}} is non empty set

{f2} is non empty set

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

[[f2,{}],<*p,i,c1,c2*>] is V21() set

{[f2,{}],<*p,i,c1,c2*>} is non empty set

{[f2,{}]} is Relation-like Function-like non empty set

{{[f2,{}],<*p,i,c1,c2*>},{[f2,{}]}} is non empty set

(({[0,{},{}]} \/ { [14,{},<*b

((({[0,{},{}]} \/ { [14,{},<*b

T is Element of ()

InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()

InsCodes () is non empty set

K51(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K41(T) is set

K41(K41(T)) is set

T is Element of ()

InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()

InsCodes () is non empty set

K51(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K41(T) is set

K41(K41(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

K41(T) `3_3 is set

T is Element of ()

InsCode T is V6() V7() V8() V12() V44() integer ext-real Element of InsCodes ()

InsCodes () is non empty set

K51(()) is set

proj1 () is non empty set

proj1 (proj1 ()) is set

K41(T) is set

K41(K41(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

K41(T) `3_3 is set

f1 is V44() integer Element of INT

<*f1*> is Relation-like NAT -defined INT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT

[1,f1] is V21() set

{1,f1} is non empty set

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

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

[14,{},<*f1*>] is V21() V22() set

[[14,{}],<*f1*>] is V21() set

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

{{[14,{}],<*f1*>