let A, B be set ; :: thesis: ( A is finite & B is finite implies Funcs (A,B) is finite )
assume that
A1: A is finite and
A2: B is finite ; :: thesis: Funcs (A,B) is finite
bool [:A,B:] is finite by A1, A2;
hence Funcs (A,B) is finite by Th5, FINSET_1:13; :: thesis: verum