let
f
be
Function
;
:: thesis:
for
Y
being
set
holds
Y
`
f
=
f

(
dom
(
Y
`
f
)
)
let
Y
be
set
;
:: thesis:
Y
`
f
=
f

(
dom
(
Y
`
f
)
)
thus
Y
`
f
=
f

(
f
"
Y
)
by
FUNCT_1:113
.=
f

(
dom
(
Y
`
f
)
)
by
MFOLD_2:1
;
:: thesis:
verum