let
x
be
set
;
:: thesis:
for
F
being
Function
holds
F
[:]
(
{}
,
x
)
=
{}
let
F
be
Function
;
:: thesis:
F
[:]
(
{}
,
x
)
=
{}
F
[:]
(
{}
,
x
)
=
F
.:
(
{}
,
(
(
dom
{}
)
-->
x
)
) ;
hence
F
[:]
(
{}
,
x
)
=
{}
by
Th3
;
:: thesis:
verum