:: ALGSEQ_1 semantic presentation

REAL is set

NAT is non empty V27() V28() V29() Element of K19(REAL)

K19(REAL) is set

NAT is non empty V27() V28() V29() set

K19(NAT) is set

K19(NAT) is set

{} is set

the empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() set is empty ext-real V26() V27() V28() V29() V31() V32() V33() V34() set

1 is non empty ext-real positive V26() V27() V28() V29() V33() V34() Element of NAT

0 is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

{{}} is set

2 is non empty ext-real positive V26() V27() V28() V29() V33() V34() Element of NAT

{{},1} is set

R is ext-real V26() V27() V28() V29() V33() V34() set

p is ext-real V26() V27() V28() V29() V33() V34() set

Segm p is Element of K19(NAT)

i is ext-real V26() V27() V28() V29() V33() V34() set

k is ext-real V26() V27() V28() V29() V33() V34() set

Segm i is Element of K19(NAT)

Segm 0 is Element of K19(NAT)

Segm 1 is Element of K19(NAT)

{0} is set

Segm 2 is Element of K19(NAT)

{0,1} is set

R is ext-real V26() V27() V28() V29() V33() V34() set

R + 1 is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm (R + 1) is Element of K19(NAT)

R is ext-real V26() V27() V28() V29() V33() V34() set

p is ext-real V26() V27() V28() V29() V33() V34() set

Segm R is Element of K19(NAT)

Segm p is Element of K19(NAT)

k is ext-real V26() V27() V28() V29() V33() V34() set

Segm k is Element of K19(NAT)

i is ext-real V26() V27() V28() V29() V33() V34() set

Segm i is Element of K19(NAT)

R is ext-real V26() V27() V28() V29() V33() V34() set

Segm R is Element of K19(NAT)

p is ext-real V26() V27() V28() V29() V33() V34() set

Segm p is Element of K19(NAT)

R is ext-real V26() V27() V28() V29() V33() V34() set

p is ext-real V26() V27() V28() V29() V33() V34() set

Segm R is Element of K19(NAT)

Segm p is Element of K19(NAT)

(Segm R) /\ (Segm p) is Element of K19(NAT)

(Segm p) /\ (Segm R) is Element of K19(NAT)

R is ext-real V26() V27() V28() V29() V33() V34() set

Segm R is Element of K19(NAT)

p is ext-real V26() V27() V28() V29() V33() V34() set

Segm p is Element of K19(NAT)

(Segm R) /\ (Segm p) is Element of K19(NAT)

(Segm p) /\ (Segm R) is Element of K19(NAT)

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

0. R is V54(R) Element of the carrier of R

NAT --> (0. R) is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) Element of K19(K20(NAT, the carrier of R))

k is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) Element of K19(K20(NAT, the carrier of R))

i is ext-real V26() V27() V28() V29() V33() V34() set

k . i is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

0. R is V54(R) Element of the carrier of R

k is ext-real V26() V27() V28() V29() V33() V34() set

R is ext-real V26() V27() V28() V29() V33() V34() set

p is ext-real V26() V27() V28() V29() V33() V34() set

k is non empty ZeroStr

the carrier of k is non empty set

K20(NAT, the carrier of k) is set

K19(K20(NAT, the carrier of k)) is set

i is Relation-like NAT -defined the carrier of k -valued Function-like V18( NAT , the carrier of k) (k) Element of K19(K20(NAT, the carrier of k))

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

k is ext-real V26() V27() V28() V29() V33() V34() set

k is ext-real V26() V27() V28() V29() V33() V34() set

i is ext-real V26() V27() V28() V29() V33() V34() set

k is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

i is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

R is ext-real V26() V27() V28() V29() V33() V34() set

p is non empty ZeroStr

the carrier of p is non empty set

K20(NAT, the carrier of p) is set

K19(K20(NAT, the carrier of p)) is set

0. p is V54(p) Element of the carrier of p

k is Relation-like NAT -defined the carrier of p -valued Function-like V18( NAT , the carrier of p) (p) Element of K19(K20(NAT, the carrier of p))

(p,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k . R is set

R is ext-real V26() V27() V28() V29() V33() V34() set

p is non empty ZeroStr

the carrier of p is non empty set

K20(NAT, the carrier of p) is set

K19(K20(NAT, the carrier of p)) is set

0. p is V54(p) Element of the carrier of p

k is Relation-like NAT -defined the carrier of p -valued Function-like V18( NAT , the carrier of p) (p) Element of K19(K20(NAT, the carrier of p))

(p,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

i is ext-real V26() V27() V28() V29() V33() V34() set

k . i is set

R is ext-real V26() V27() V28() V29() V33() V34() set

R + 1 is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

p is non empty ZeroStr

the carrier of p is non empty set

K20(NAT, the carrier of p) is set

K19(K20(NAT, the carrier of p)) is set

0. p is V54(p) Element of the carrier of p

k is Relation-like NAT -defined the carrier of p -valued Function-like V18( NAT , the carrier of p) (p) Element of K19(K20(NAT, the carrier of p))

(p,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k . R is set

i is ext-real V26() V27() V28() V29() V33() V34() set

k . i is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm (R,p) is Element of K19(NAT)

p is non empty ZeroStr

the carrier of p is non empty set

K20(NAT, the carrier of p) is set

K19(K20(NAT, the carrier of p)) is set

i is non empty ZeroStr

the carrier of i is non empty set

K20(NAT, the carrier of i) is set

K19(K20(NAT, the carrier of i)) is set

R is ext-real V26() V27() V28() V29() V33() V34() set

k is Relation-like NAT -defined the carrier of p -valued Function-like V18( NAT , the carrier of p) (p) Element of K19(K20(NAT, the carrier of p))

(p,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm R is Element of K19(NAT)

(p,k) is Element of K19(NAT)

Segm (p,k) is Element of K19(NAT)

i is ext-real V26() V27() V28() V29() V33() V34() set

Segm i is Element of K19(NAT)

p is Relation-like NAT -defined the carrier of i -valued Function-like V18( NAT , the carrier of i) (i) Element of K19(K20(NAT, the carrier of i))

(i,p) is Element of K19(NAT)

(i,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm (i,p) is Element of K19(NAT)

F

the carrier of F

K20(NAT, the carrier of F

K19(K20(NAT, the carrier of F

F

0. F

R is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

F

R is Relation-like NAT -defined the carrier of F

R is Relation-like NAT -defined the carrier of F

p is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k is ext-real V26() V27() V28() V29() V33() V34() set

R . k is set

k is ext-real V26() V27() V28() V29() V33() V34() set

p is Relation-like NAT -defined the carrier of F

(F

k is ext-real V26() V27() V28() V29() V33() V34() set

p . k is set

k is ext-real V26() V27() V28() V29() V33() V34() set

p . k is set

F

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

i is set

p . i is set

k . i is set

i is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

p . i is Element of the carrier of R

k . i is Element of the carrier of R

0. R is V54(R) Element of the carrier of R

dom p is set

dom k is set

R is non empty ZeroStr

the carrier of R is non empty set

0. R is V54(R) Element of the carrier of R

{(0. R)} is set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

k is set

i is ext-real V26() V27() V28() V29() V33() V34() set

i is Element of the carrier of R

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

c

p . c

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

p is Element of the carrier of R

k is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k . 0 is Element of the carrier of R

k is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,k) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k . 0 is Element of the carrier of R

i is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,i) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

i . 0 is Element of the carrier of R

0 + 1 is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

0. R is V54(R) Element of the carrier of R

i is ext-real V26() V27() V28() V29() V33() V34() set

k . i is set

i . i is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

0. R is V54(R) Element of the carrier of R

(R,(0. R)) is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

p . 0 is Element of the carrier of R

0 + 1 is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

0. R is V54(R) Element of the carrier of R

(R,(0. R)) is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

(R,(R,(0. R))) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

k is ext-real V26() V27() V28() V29() V33() V34() set

p . k is set

(R,(0. R)) . k is set

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

k is non empty ZeroStr

the carrier of k is non empty set

K20(NAT, the carrier of k) is set

K19(K20(NAT, the carrier of k)) is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

0. R is V54(R) Element of the carrier of R

(R,(0. R)) is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

(R,p) is Element of K19(NAT)

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm (R,p) is Element of K19(NAT)

i is Relation-like NAT -defined the carrier of k -valued Function-like V18( NAT , the carrier of k) (k) Element of K19(K20(NAT, the carrier of k))

(k,i) is Element of K19(NAT)

(k,i) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

Segm (k,i) is Element of K19(NAT)

0. k is V54(k) Element of the carrier of k

(k,(0. k)) is Relation-like NAT -defined the carrier of k -valued Function-like V18( NAT , the carrier of k) (k) Element of K19(K20(NAT, the carrier of k))

R is ext-real V26() V27() V28() V29() V33() V34() set

p is non empty ZeroStr

0. p is V54(p) Element of the carrier of p

the carrier of p is non empty set

(p,(0. p)) is Relation-like NAT -defined the carrier of p -valued Function-like V18( NAT , the carrier of p) (p) Element of K19(K20(NAT, the carrier of p))

K20(NAT, the carrier of p) is set

K19(K20(NAT, the carrier of p)) is set

(p,(0. p)) . R is set

(p,(p,(0. p))) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

R is non empty ZeroStr

the carrier of R is non empty set

K20(NAT, the carrier of R) is set

K19(K20(NAT, the carrier of R)) is set

0. R is V54(R) Element of the carrier of R

(R,(0. R)) is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

{(0. R)} is set

p is Relation-like NAT -defined the carrier of R -valued Function-like V18( NAT , the carrier of R) (R) Element of K19(K20(NAT, the carrier of R))

rng p is set

k is set

dom p is set

i is set

p . i is set

i is ext-real V26() V27() V28() V29() V33() V34() Element of NAT

p . i is Element of the carrier of R

k is set

p . 0 is Element of the carrier of R

dom p is set

k is ext-real V26() V27() V28() V29() V33() V34() set

p . k is set

dom p is set

k is ext-real V26() V27() V28() V29() V33() V34() set

(R,p) is ext-real V26() V27() V28() V29() V33() V34() Element of NAT