(Funcs)
(
A
,
B
) is
V2
()
by
A1
,
Th18
;
then
not
{}
in
rng
(
(Funcs)
(
A
,
B
)
)
by
PBOOLE:137
;
hence
product
(
(Funcs)
(
A
,
B
)
)
is non
empty
set
by
CARD_3:26
;
:: thesis:
verum