let
f
be
Function
;
:: thesis:
for
x
,
y
being
set
st
x
in
f
"
{
y
}
holds
f
.
x
=
y
let
x
,
y
be
set
;
:: thesis:
(
x
in
f
"
{
y
}
implies
f
.
x
=
y
)
assume
A1
:
x
in
f
"
{
y
}
;
:: thesis:
f
.
x
=
y
f
.
x
in
{
y
}
by
A1
,
FUNCT_1:def 7
;
hence
f
.
x
=
y
by
TARSKI:def 1
;
:: thesis:
verum