reconsider
f
=
id
X
as
Function
of
X
,
X
;
rng
f
=
X
;
hence
id
X
is
onto
by
FUNCT_2:def 3
;
:: thesis:
verum