per
cases
(
x
in
dom
f
or not
x
in
dom
f
)
;
suppose
x
in
dom
f
;
:: thesis:
f
.
x
is
Element
of
Segm
k
then
f
.
x
in
rng
f
by
FUNCT_1:3
;
hence
f
.
x
is
Element
of
Segm
k
;
:: thesis:
verum
end;
suppose
A1
: not
x
in
dom
f
;
:: thesis:
f
.
x
is
Element
of
Segm
k
A2
: (
k
=
0
or
k
>
0
) ;
f
.
x
=
0
by
A1
,
FUNCT_1:def 2
;
hence
f
.
x
is
Element
of
Segm
k
by
A2
,
NAT_1:44
,
SUBSET_1:def 1
;
:: thesis:
verum
end;
end;