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