let
f
be
FinSequence
of
REAL
;
:: thesis:
(
len
f
=
len
(
abs
f
)
&
dom
f
=
dom
(
abs
f
)
)
(
rng
f
c=
REAL
&
dom
absreal
=
REAL
)
by
FUNCT_2:def 1
;
hence
len
f
=
len
(
abs
f
)
by
FINSEQ_2:29
;
:: thesis:
dom
f
=
dom
(
abs
f
)
hence
dom
f
=
dom
(
abs
f
)
by
FINSEQ_3:29
;
:: thesis:
verum