per
cases
(
k
in
dom
s
or not
k
in
dom
s
)
;
suppose
A1
:
k
in
dom
s
;
:: thesis:
s
.
k
is
Element
of
COMPLEX
A2
:
rng
s
c=
COMPLEX
by
VALUED_0:def 1
;
s
.
k
in
rng
s
by
A1
,
FUNCT_1:def 3
;
hence
s
.
k
is
Element
of
COMPLEX
by
A2
;
:: thesis:
verum
end;
suppose
not
k
in
dom
s
;
:: thesis:
s
.
k
is
Element
of
COMPLEX
then
s
.
k
=
0c
by
FUNCT_1:def 2
;
hence
s
.
k
is
Element
of
COMPLEX
;
:: thesis:
verum
end;
end;