let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or (F .:.: A) . i is finite )
assume A1: i in I ; :: thesis: (F .:.: A) . i is finite
reconsider f = F . i as Function ;
A . i is finite by A1, Lm1;
then f .: (A . i) is finite ;
hence (F .:.: A) . i is finite by A1, PBOOLE:def 25; :: thesis: verum