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