Processing math: 100%
Sequence end
Function
context
X
… set
definiendum
l
a
s
t
:
F
i
n
i
t
e
S
e
q
u
e
n
c
e
(
X
)
→
X
definiendum
l
a
s
t
(
S
)
:=
π
l
e
n
g
t
h
(
S
)
(
S
)
Discussion
Parents
Subset of
Surjective function
Context
Sequence length