let
A
be
set
;
:: thesis:
{}
is
Function
of
A
,
{}
per
cases
(
A
=
{}
or
A
<>
{}
)
;
suppose
A1
:
A
=
{}
;
:: thesis:
{}
is
Function
of
A
,
{}
reconsider
f
=
{}
as
PartFunc
of
A
,
{}
by
RELSET_1:12
;
f
is
total
by
A1
;
hence
{}
is
Function
of
A
,
{}
;
:: thesis:
verum
end;
suppose
A
<>
{}
;
:: thesis:
{}
is
Function
of
A
,
{}
thus
{}
is
Function
of
A
,
{}
by
FUNCT_2:def 1
,
RELSET_1:12
;
:: thesis:
verum
end;
end;