bool
[:
A
,
B
:]
is
finite
;
hence
Funcs
(
A
,
B
) is
finite
by
Th2
,
FINSET_1:1
;
:: thesis:
verum