let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or (A (\) B) . i is finite )
assume A1: i in I ; :: thesis: (A (\) B) . i is finite
(A . i) \ (B . i) is finite ;
hence (A (\) B) . i is finite by A1, PBOOLE:def 6; :: thesis: verum