let
x
be
object
;
:: according to
VALUED_0:def 9
:: thesis:
( not
x
in
dom
(
f
^
)
or
(
f
^
)
.
x
is
real
)
set
F
=
f
^
;
assume
x
in
dom
(
f
^
)
;
:: thesis:
(
f
^
)
.
x
is
real
then
(
f
^
)
.
x
=
(
f
.
x
)
"
by
Def2
;
hence
(
f
^
)
.
x
is
real
;
:: thesis:
verum