:: 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₁() is non empty ZeroStr
the carrier of F₁() is non empty set
K20(NAT, the carrier of F₁()) is set
K19(K20(NAT, the carrier of F₁())) is set
F₂() is ext-real V26() V27() V28() V29() V33() V34() set
0. F₁() is V54(F₁()) Element of the carrier of F₁()
R is ext-real V26() V27() V28() V29() V33() V34() Element of NAT
F₃(R) is Element of the carrier of F₁()
R is Relation-like NAT -defined the carrier of F₁() -valued Function-like V18( NAT , the carrier of F₁()) Element of K19(K20(NAT, the carrier of F₁()))
R is Relation-like NAT -defined the carrier of F₁() -valued Function-like V18( NAT , the carrier of F₁()) Element of K19(K20(NAT, 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₁() -valued Function-like V18( NAT , the carrier of F₁()) (F₁()) Element of K19(K20(NAT, the carrier of F₁()))
(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
p . k is set
k is ext-real V26() V27() V28() V29() V33() V34() set
p . k is set
F₃(k) is Element of the carrier of 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₇ is ext-real V26() V27() V28() V29() V33() V34() set
p . c₇ 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 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