reconsider
f
=
f
,
g
=
g
as
Function
of
X
,
X
by
FUNCT_2:66
;
g
*
f
in
Funcs
(
X
,
X
)
by
FUNCT_2:9
;
hence
f
*
g
is
Element
of
Funcs
(
X
,
X
) ;
:: thesis:
verum