A1
:
f
is
Function
of
X
,
X
by
FUNCT_2:66
;
per
cases
(
X
=
{}
or
X
<>
{}
)
;
suppose
A2
:
X
=
{}
;
:: thesis:
f
.
g
is
Element
of
X
then
{}
=
dom
f
by
A1
;
then
f
.
g
=
{}
by
FUNCT_1:def 2
;
hence
f
.
g
is
Element
of
X
by
A2
,
SUBSET_1:def 1
;
:: thesis:
verum
end;
suppose
X
<>
{}
;
:: thesis:
f
.
g
is
Element
of
X
hence
f
.
g
is
Element
of
X
by
A1
,
FUNCT_2:5
;
:: thesis:
verum
end;
end;