set
f
=
id
X
;
let
a
be
set
;
:: according to
PARTIT_2:def 2
:: thesis:
(
a
in
dom
(
id
X
)
implies
(
id
X
)
.
(
(
id
X
)
.
a
)
=
a
)
assume
a
in
dom
(
id
X
)
;
:: thesis:
(
id
X
)
.
(
(
id
X
)
.
a
)
=
a
then
a
in
X
;
then
(
id
X
)
.
a
=
a
by
FUNCT_1:17
;
hence
(
id
X
)
.
(
(
id
X
)
.
a
)
=
a
;
:: thesis:
verum