let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or ((Funcs) (A,B)) . i is finite )
assume i in I ; :: thesis: ((Funcs) (A,B)) . i is finite
then ( ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) & A . i is finite ) by PBOOLE:def 17;
hence ((Funcs) (A,B)) . i is finite by FRAENKEL:6; :: thesis: verum