let
f
be
Function
;
:: thesis:
(
rng
f
=
{
{}
}
implies
product
f
=
{}
)
assume
rng
f
=
{
{}
}
;
:: thesis:
product
f
=
{}
then
{}
in
rng
f
by
TARSKI:def 1
;
hence
product
f
=
{}
by
CARD_3:26
;
:: thesis:
verum